diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/dune | 9 | ||||
| -rw-r--r-- | lib/extract.v | 9 | ||||
| -rw-r--r-- | lib/pattern.ml | 40 |
3 files changed, 52 insertions, 6 deletions
@@ -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 |