mutual recursion admitted under lexicographic measures

1 files changed, 7 insertions, 5 deletions

diff --git a/lib/world.mli b/lib/world.mli
index 51ee078..14f82d3 100644
--- a/lib/world.mli
+++ b/lib/world.mli
@@ -29,11 +29,13 @@ type rule = {
   rule_name : string;
   head : Pattern.t Label.Map.t;
   body : expr;
-  witness : Label.t option;
-      (** For a recursive rule, the label whose argument strictly
-          decreases. The VM requires it ground before unfolding,
-          which is what turns the admission proof into runtime
-          termination. [None] on non-recursive rules. *)
+  witness : Label.t list;
+      (** For a recursive rule, the lexicographic measure of its
+          call-graph component: at some position the recursive
+          argument strictly decreases, all earlier positions staying
+          equal. The VM requires every position ground before
+          unfolding, which is what turns the admission proof into
+          runtime termination. Empty on non-recursive rules. *)
 }
 
 (** The primitive host-checked domains. *)