diff options
Diffstat (limited to 'lib/world.ml')
| -rw-r--r-- | lib/world.ml | 21 |
1 files changed, 21 insertions, 0 deletions
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 |