fix nested pattern

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
dannypsnl · Feb 6, 2025 · dd908fd · dd908fd
1 parent 2783aac
commit dd908fd
Showing 1 changed file with 60 additions and 9 deletions.
diff --git a/pattern-coverage/lib/Algo.ml b/pattern-coverage/lib/Algo.ml
@@ -11,11 +11,14 @@ type pattern =
   | Spine of pattern spine
   [@printer
     fun fmt sp ->
-      fprintf
-        fmt
-        "%s %s"
-        sp.constructor
-        (String.concat " " (List.map show_pattern sp.spine))]
+      if List.is_empty sp.spine
+      then fprintf fmt "%s" sp.constructor
+      else
+        fprintf
+          fmt
+          "%s %s"
+          sp.constructor
+          (String.concat " " (List.map show_pattern sp.spine))]
 [@@deriving show]
 
 exception Split of pattern list
@@ -40,11 +43,32 @@ and cover (case : pattern) (pattern : pattern) : unit =
     Printf.printf "split %s\n" x;
     let cases = Hashtbl.find type_meta ty in
     raise @@ Split cases
-  | Spine { constructor = c1; spine = s1 }, Spine { constructor = c2; spine = s2 } ->
-    if String.equal c1 c2 then List.iter2 cover s1 s2 else raise FailMatch
+  | Spine { constructor = c1; spine = cs }, Spine { constructor = c2; spine = pats } ->
+    if String.equal c1 c2
+    then
+      (* This is super ugly, the idea is if sub-split in a Spine happened,
+         we should wrap the sub-split with proper Spine, to ensure nested pattern work as well.
+
+         Since OCaml List API is like this, the way is using iteri to compute which nth sub-case raise Split,
+         then replace nth Var with splits
+      *)
+      List.iteri
+        (fun n case ->
+           let pat = List.nth pats n in
+           try cover case pat with
+           | Split cases ->
+             let wrapper =
+               fun c ->
+               let cs = List.mapi (fun k case -> if n == k then c else case) cs in
+               Spine { constructor = c1; spine = cs }
+             in
+             let cases = List.map wrapper cases in
+             raise @@ Split cases)
+        cs
+    else raise FailMatch
 ;;
 
-let%expect_test "" =
+let%expect_test "basic split" =
   Hashtbl.add
     type_meta
     Nat
@@ -55,9 +79,36 @@ let%expect_test "" =
      check_coverage
        (Var ("m", Nat))
        [ Spine { constructor = "zero"; spine = [] }
-       ; Spine { constructor = "suc"; spine = [ Var ("m1", Nat) ] }
+       ; Spine { constructor = "suc"; spine = [ Var ("m", Nat) ] }
        ]
    with
    | NotCovered case -> Printf.printf "`%s` is not covered\n" ([%show: pattern] case));
   [%expect {| split m |}]
 ;;
+
+let%expect_test "nested pattern" =
+  Hashtbl.add
+    type_meta
+    Nat
+    [ Spine { constructor = "zero"; spine = [] }
+    ; Spine { constructor = "suc"; spine = [ Var ("n", Nat) ] }
+    ];
+  (try
+     check_coverage
+       (Var ("m", Nat))
+       [ Spine { constructor = "zero"; spine = [] }
+       ; Spine
+           { constructor = "suc"; spine = [ Spine { constructor = "zero"; spine = [] } ] }
+       ; Spine
+           { constructor = "suc"
+           ; spine = [ Spine { constructor = "suc"; spine = [ Var ("m1", Nat) ] } ]
+           }
+       ]
+   with
+   | NotCovered case -> Printf.printf "`%s` is not covered\n" ([%show: pattern] case));
+  [%expect
+    {|
+    split m
+    split n
+    |}]
+;;