diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/dune | 2 | ||||
| -rw-r--r-- | lib/extract.v | 5 | ||||
| -rw-r--r-- | lib/pattern.mli | 11 | ||||
| -rw-r--r-- | lib/world.ml | 21 |
4 files changed, 36 insertions, 3 deletions
@@ -7,7 +7,7 @@ ; 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) + (deps extract.v ../theories/DecreaseChecker.vo ../theories/Lex.vo) (action (setenv OCAMLPATH "" (run coqc -q -Q ../theories "" extract.v)))) diff --git a/lib/extract.v b/lib/extract.v index 5c8ff7c..3fee1f7 100644 --- a/lib/extract.v +++ b/lib/extract.v @@ -3,7 +3,8 @@ Pattern.strictly_contains runs. Kept beside the library so the generated module lands where dune collects it. *) -From Stdlib Require Import Extraction ExtrOcamlBasic. +From Stdlib Require Import Extraction ExtrOcamlBasic ExtrOcamlNatInt. Require Import DecreaseChecker. +Require Import Lex. -Extraction "decrease_extracted.ml" contains term_eqb. +Extraction "decrease_extracted.ml" contains term_eqb lex_ltb. diff --git a/lib/pattern.mli b/lib/pattern.mli index 5fc16c6..f79dce0 100644 --- a/lib/pattern.mli +++ b/lib/pattern.mli @@ -45,6 +45,17 @@ val strictly_contains : t -> sub:t -> bool val pp : Format.formatter -> t -> unit +(** The verified checker's view of patterns. Admission projects + patterns through {!to_checker} and runs the containment and + lexicographic checkers extracted from Rocq; the conversion is + injective by leaf kind, and these two equalities are the + trusted seam. *) +type checker_leaf + +val checker_leaf_equal : checker_leaf -> checker_leaf -> bool + +val to_checker : t -> (Label.t, checker_leaf) Decrease_extracted.term + (** Substitutions bind variables to patterns. They only grow; unification never revokes a binding. *) module Subst : sig diff --git a/lib/world.ml b/lib/world.ml index 8ade9da..a053c2c 100644 --- a/lib/world.ml +++ b/lib/world.ml @@ -586,6 +586,27 @@ module Standalone = struct in match lex_measure calls candidates with | None -> Error (Non_total_component members) + | Some measure + when + (* The search is an untrusted heuristic; the + measure it found is validated call by call with + the lexicographic checker extracted from Rocq, + whose soundness and well-foundedness are + proven. *) + not + (List.for_all + (fun c -> + let project bindings = + List.map + (fun label -> + Pattern.to_checker (Label.Map.find label bindings)) + measure + in + Decrease_extracted.lex_ltb Label.equal + Pattern.checker_leaf_equal (project c.args) + (project c.head)) + calls) -> + Error (Non_total_component members) | Some measure -> Ok (List.fold_left |