diff options
Diffstat (limited to 'lib/pattern.ml')
| -rw-r--r-- | lib/pattern.ml | 40 |
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 |