diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/vm.ml | 6 | ||||
| -rw-r--r-- | lib/world.ml | 216 | ||||
| -rw-r--r-- | lib/world.mli | 12 |
3 files changed, 159 insertions, 75 deletions
@@ -155,13 +155,13 @@ module Make (W : World.WORLD) = struct facts) | Some (World.Rules rules) -> let witness_ground rule = - match rule.World.witness with - | None -> true - | Some label -> ( + List.for_all + (fun label -> match Label.Map.find_opt label bindings with | Some pattern -> Pattern.is_ground (Pattern.Subst.resolve subst pattern) | None -> false) + rule.World.witness in if List.for_all witness_ground rules then Run diff --git a/lib/world.ml b/lib/world.ml index 6e1e883..8ade9da 100644 --- a/lib/world.ml +++ b/lib/world.ml @@ -9,7 +9,7 @@ type rule = { rule_name : string; head : Pattern.t Label.Map.t; body : expr; - witness : Label.t option; + witness : Label.t list; } type primitive = D_integer | D_natural | D_rational | D_string @@ -42,8 +42,7 @@ type error = | Fact_not_ground of string | Schema_mismatch of { relation : string; detail : string } | Domain_violation of { relation : string; label : string } - | Non_total_rule of string - | Mutual_recursion of string list + | Non_total_component of string list | Criterion_arity of { relation : string; label : string } type pending = { @@ -69,13 +68,10 @@ let pp_error fmt = function Format.fprintf fmt "schema mismatch on %s: %s" relation detail | Domain_violation { relation; label } -> Format.fprintf fmt "domain violation on %s at %s:" relation label - | Non_total_rule name -> + | Non_total_component relations -> Format.fprintf fmt - "rule %S rejected: no structurally decreasing argument in its recursive call" - name - | Mutual_recursion cycle -> - Format.fprintf fmt "mutual recursion rejected: %s" - (String.concat " -> " cycle) + "recursion among %s rejected: no lexicographic structural decrease covers every call" + (String.concat ", " relations) | Criterion_arity { relation; label } -> Format.fprintf fmt "criterion on %s at %s: must have exactly one free variable, the subject" @@ -268,37 +264,55 @@ module Standalone = struct |> Result.map List.rev | _ -> Error (Malformed_directive "schema: takes #( ... ) of entries") - (* The structural decrease check of decision 10, rung one. Every - self-recursive application must have an argument strictly - contained in the head's argument at the same label; that label - is kept as the runtime witness. *) - let admit_rule ~relation rule_name head body = - let recursive = - applications body |> List.filter (fun (name, _) -> String.equal name relation) - in - match recursive with - | [] -> Ok { rule_name; head; body; witness = None } + (* The structural decrease check of decision 10, rung one, + generalized to call-graph components. For every strongly + connected component of the call graph among rule-defined + relations, a lexicographic measure of shared labels must + decrease on every intra-component call: at some position the + call argument sits strictly inside the head's, and at every + earlier position they are syntactically equal. The measure is + stored on each recursive rule and its positions must be ground + at unfolding, which turns the proof into a runtime termination + measure. *) + + type call = { head : Pattern.t Label.Map.t; args : Pattern.t Label.Map.t } + + let decreases c label = + match (Label.Map.find_opt label c.head, Label.Map.find_opt label c.args) with + | Some head_arg, Some call_arg -> + Pattern.strictly_contains head_arg ~sub:call_arg + | _ -> false + + let stays_equal c label = + match (Label.Map.find_opt label c.head, Label.Map.find_opt label c.args) with + | Some head_arg, Some call_arg -> Pattern.equal head_arg call_arg + | _ -> false + + (* Greedy lexicographic search with backtracking: pick a label + that decreases or stays equal on every remaining call and + decreases on at least one; the calls it covers drop out, the + rest must be covered by later positions. *) + let rec lex_measure calls candidates = + match calls with + | [] -> Some [] | _ -> - let witness_for (_, call_bindings) = - Label.Map.fold - (fun label head_arg found -> - match found with - | Some _ -> found - | None -> ( - match Label.Map.find_opt label call_bindings with - | Some call_arg - when Pattern.strictly_contains head_arg ~sub:call_arg -> - Some label - | _ -> None)) - head None - in - let witnesses = List.map witness_for recursive in - if List.for_all Option.is_some witnesses then - (* All recursive calls decrease; any common witness works - at runtime, and per-call witnesses agree by label here - because they are all drawn from the same head. *) - Ok { rule_name; head; body; witness = List.nth witnesses 0 } - else Error (Non_total_rule rule_name) + List.find_map + (fun label -> + if + List.for_all + (fun c -> decreases c label || stays_equal c label) + calls + && List.exists (fun c -> decreases c label) calls + then + let remaining = + List.filter (fun c -> not (decreases c label)) calls + in + Option.map + (fun rest -> label :: rest) + (lex_measure remaining + (List.filter (fun l -> not (Label.equal l label)) candidates)) + else None) + candidates let load statements = (* First pass: declare tables, collect raw material. *) @@ -350,7 +364,7 @@ module Standalone = struct | _ -> Error (Malformed_directive "a rule head is a single [...] block") in let* body = expr_of_node body_node in - let* rule = admit_rule ~relation rule_name head body in + let rule = { rule_name; head; body; witness = [] } in let existing = Option.value ~default:[] (String_map.find_opt relation grouped) in @@ -484,40 +498,108 @@ module Standalone = struct (Ok ()) rules) world (Ok ()) in - let dependencies relation = + (* Component analysis: group rule-defined relations into + strongly connected components of the call graph, find a + lexicographic measure for each recursive component, and stamp + it on the recursive rules as their runtime witness. *) + let rule_defined name = + match String_map.find_opt name world with + | Some (Rules _) -> true + | _ -> false + in + let edges relation = match String_map.find_opt relation world with | Some (Rules rules) -> List.concat_map - (fun rule -> - applications rule.body - |> List.filter_map (fun (name, _) -> - if - (not (String.equal name relation)) - && (match String_map.find_opt name world with - | Some (Rules _) -> true - | _ -> false) - then Some name - else None)) + (fun rule -> List.map fst (applications rule.body)) rules + |> List.filter rule_defined + |> List.sort_uniq String.compare | _ -> [] in - let* () = - let rec visit path relation = - if List.mem relation path then - Error (Mutual_recursion (List.rev (relation :: path))) - else - List.fold_left - (fun acc dep -> - let* () = acc in - visit (relation :: path) dep) - (Ok ()) - (dependencies relation) + let reachable start = + let rec go seen frontier = + match frontier with + | [] -> seen + | name :: rest -> + if List.mem name seen then go seen rest + else go (name :: seen) (edges name @ rest) in - String_map.fold - (fun relation def acc -> - let* () = acc in - match def with Rules _ -> visit [] relation | Table _ -> Ok ()) - world (Ok ()) + go [] (edges start) + in + let* world = + let relations = + String_map.fold + (fun name def acc -> + match def with Rules _ -> name :: acc | Table _ -> acc) + world [] + in + let component relation = + let reach = reachable relation in + relation + :: List.filter + (fun other -> + (not (String.equal other relation)) + && List.mem other reach + && List.mem relation (reachable other)) + relations + in + List.fold_left + (fun acc relation -> + let* world = acc in + let members = component relation in + (* Process each component once, from its least member. *) + if not (String.equal relation (List.fold_left min relation members)) + then Ok world + else + let member name = List.mem name members in + let calls_of (rule : rule) = + applications rule.body + |> List.filter_map (fun (target, args) -> + if member target then Some { head = rule.head; args } + else None) + in + let rules_of name = + match String_map.find_opt name world with + | Some (Rules rules) -> rules + | _ -> [] + in + let calls = List.concat_map calls_of (List.concat_map rules_of members) in + if calls = [] then Ok world + else + let candidates = + match calls with + | [] -> [] + | first :: rest -> + Label.Map.fold + (fun label _ acc -> + if + List.for_all + (fun c -> + Label.Map.mem label c.head + && Label.Map.mem label c.args) + rest + && Label.Map.mem label first.args + then label :: acc + else acc) + first.head [] + in + match lex_measure calls candidates with + | None -> Error (Non_total_component members) + | Some measure -> + Ok + (List.fold_left + (fun world name -> + let stamped = + List.map + (fun rule -> + if calls_of rule = [] then rule + else { rule with witness = measure }) + (rules_of name) + in + String_map.add name (Rules stamped) world) + world members)) + (Ok world) relations in (* Queries compile last, against the full catalog. *) let* queries = 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. *) |