admission runs the containment checker extracted from rocq

1 files changed, 34 insertions, 6 deletions

diff --git a/lib/pattern.ml b/lib/pattern.ml
index 823162c..5186e04 100644
--- a/lib/pattern.ml
+++ b/lib/pattern.ml
@@ -64,13 +64,41 @@ let rec equal a b =
   | Record x, Record y -> Label.Map.equal equal x y
   | _ -> false
 
+(* Containment runs the checker extracted from
+   theories/DecreaseChecker.v, whose soundness and decrease are
+   proven. The trusted seam is this conversion (injective by leaf
+   kind) and the two equality functions. *)
+type checker_leaf =
+  | L_var of string
+  | L_int of Z.t
+  | L_rat of Q.t
+  | L_str of string
+  | L_nil
+
+let checker_leaf_equal a b =
+  match (a, b) with
+  | L_var x, L_var y | L_str x, L_str y -> String.equal x y
+  | L_int x, L_int y -> Z.equal x y
+  | L_rat x, L_rat y -> Q.equal x y
+  | L_nil, L_nil -> true
+  | _ -> false
+
+let rec to_checker = function
+  | Var v -> Decrease_extracted.Leaf (L_var v)
+  | Integer z -> Decrease_extracted.Leaf (L_int z)
+  | Rational q -> Decrease_extracted.Leaf (L_rat q)
+  | String s -> Decrease_extracted.Leaf (L_str s)
+  | Nil -> Decrease_extracted.Leaf L_nil
+  | Record map ->
+      Decrease_extracted.Node
+        (List.fold_right
+           (fun (label, value) rest ->
+             Decrease_extracted.FCons (label, to_checker value, rest))
+           (Label.Map.bindings map) Decrease_extracted.FNil)
+
 let strictly_contains pattern ~sub =
-  let rec inside p = equal p sub || strictly p
-  and strictly = function
-    | Record map -> Label.Map.exists (fun _ p -> inside p) map
-    | _ -> false
-  in
-  strictly pattern
+  Decrease_extracted.contains Label.equal checker_leaf_equal (to_checker sub)
+    (to_checker pattern)
 
 let rec pp fmt = function
   | Var v -> Format.pp_print_string fmt v