admission runs the containment checker extracted from rocq

3 files changed, 52 insertions, 6 deletions

diff --git a/lib/dune b/lib/dune
index 2d9154e..3f8be6f 100644
--- a/lib/dune
+++ b/lib/dune
@@ -3,6 +3,15 @@
  (public_name sol)
  (libraries zarith))
 
+; The proven containment checker, extracted from Rocq. The .v files
+; are the source of truth; the generated module is a build artifact.
+(rule
+ (targets decrease_extracted.ml decrease_extracted.mli)
+ (deps extract.v ../theories/DecreaseChecker.vo)
+ (action
+  (setenv OCAMLPATH ""
+   (run coqc -q -Q ../theories "" extract.v))))
+
 (ocamllex lexer)
 
 (menhir
diff --git a/lib/extract.v b/lib/extract.v
new file mode 100644
index 0000000..5c8ff7c
--- /dev/null
+++ b/lib/extract.v
@@ -0,0 +1,9 @@
+(* Extraction driver: turns the proven checker of
+   theories/DecreaseChecker.v into lib/decrease_extracted.ml, which
+   Pattern.strictly_contains runs. Kept beside the library so the
+   generated module lands where dune collects it. *)
+
+From Stdlib Require Import Extraction ExtrOcamlBasic.
+Require Import DecreaseChecker.
+
+Extraction "decrease_extracted.ml" contains term_eqb.
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