From dbec0a97bbf121da417065ade0ec991a1ccb18e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=AEm=20Ts=C3=BA-thu=C3=A0n?= Date: Thu, 6 Feb 2025 15:18:15 +0800 Subject: [PATCH] misc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Lîm Tsú-thuàn --- pattern-coverage/lib/Algo.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/pattern-coverage/lib/Algo.ml b/pattern-coverage/lib/Algo.ml index abb6b38..e3ca371 100644 --- a/pattern-coverage/lib/Algo.ml +++ b/pattern-coverage/lib/Algo.ml @@ -1,7 +1,3 @@ -exception CannotSplit -exception CanSplit -exception FailMatch - type typ = Nat [@printer fun fmt _ -> fprintf fmt "Nat"] [@@deriving show] type 'a spine = @@ -22,7 +18,10 @@ type pattern = (String.concat " " (List.map show_pattern sp.spine))] [@@deriving show] -exception NotCover of pattern +exception CannotSplit +exception CanSplit +exception FailMatch +exception NotCovered of pattern let type_meta : (typ, pattern list) Hashtbl.t = Hashtbl.create 100 @@ -43,7 +42,7 @@ let rec check_coverage (case : pattern) (patterns : pattern list) : unit = | CanSplit -> let cases = split case in List.iter (fun c -> check_coverage c patterns) cases) - | [] -> raise @@ NotCover case + | [] -> raise @@ NotCovered case and cover (case : pattern) (pattern : pattern) : unit = match case, pattern with @@ -67,6 +66,6 @@ let%expect_test "" = ; Spine { constructor = "suc"; spine = [ Var ("m1", Nat) ] } ] with - | NotCover case -> Printf.printf "`%s` is not covered\n" ([%show: pattern] case)); + | NotCovered case -> Printf.printf "`%s` is not covered\n" ([%show: pattern] case)); [%expect {| split m |}] ;;