diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/program.ml | 14 | ||||
| -rw-r--r-- | lib/vm.ml | 143 | ||||
| -rw-r--r-- | lib/vm.mli | 25 |
3 files changed, 138 insertions, 44 deletions
diff --git a/lib/program.ml b/lib/program.ml index ac62781..b0e363b 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -21,7 +21,19 @@ let load statements = pending in match Vm.Standalone.solve world pending_body with - | Ok (_ :: _) -> admit rest + (* Membership must be proven outright: an answer that is + itself conditioned on residual constraints does not + admit a fact. *) + | Ok solutions + when List.exists (fun s -> s.Vm.residue = []) solutions -> + admit rest + | Ok (_ :: _) -> + Error + (Undecidable_criterion + { + relation = pending_relation; + label = Label.to_string pending_label; + }) | Ok [] -> Error (Integrity @@ -5,7 +5,20 @@ let pp_error fmt (Non_total_plan goals) = "non-total plan rejected: no decidable goal among %s (bind more arguments or bound the search)" (String.concat ", " goals) -type solution = (string * Pattern.t) list +type residual = string * Pattern.t Label.Map.t + +let pp_residual fmt (name, bindings) = + Format.fprintf fmt "@[<hv 1>[%s" name; + Label.Map.iter + (fun label pattern -> + Format.fprintf fmt "@ %a %a" Label.pp label Pattern.pp pattern) + bindings; + Format.fprintf fmt "]@]" + +type solution = { + bindings : (string * Pattern.t) list; + residue : residual list; +} module Make (W : World.WORLD) = struct exception Stuck of string list @@ -15,6 +28,14 @@ module Make (W : World.WORLD) = struct positively and the denial negatively. *) type goal = Positive of World.expr | Negated of World.expr + (* What attempting a goal can say: run it into branches, or wait. + A waiting goal is residuatable when it is pure membership that + decides as soon as its arguments are ground; searches are + never residuatable. *) + type attempt = + | Run of (Pattern.Subst.t * goal list) list + | Wait of { residuatable : bool } + let rec flatten = function | World.And (a, b) -> flatten a @ flatten b | World.Not (universe, denial) -> flatten universe @ [ Negated denial ] @@ -74,40 +95,57 @@ module Make (W : World.WORLD) = struct | None -> None)) goal_bindings (Some subst) - (* Executing one goal yields branches: an extended substitution - and the extra goals it owes (rule bodies, disjuncts). [None] - means not decidable yet; the planner retries it later, and - rejects the plan if nothing ever runs. *) + let proven solutions = List.exists (fun (_, residue) -> residue = []) solutions + let rec try_goal world subst goal = match goal with | Negated denial -> if unresolved_vars subst denial = [] then match search world subst (flatten denial) with - | [] -> Some [ (subst, []) ] - | _ -> Some [] - else None - | Positive (World.Or (a, b)) -> Some [ (subst, flatten a); (subst, flatten b) ] - | Positive (World.And _ | World.Not _) -> - Some [ (subst, flatten (match goal with Positive e -> e | _ -> assert false)) ] + | [] -> Run [ (subst, []) ] + | solutions -> + (* Ground denials cannot residuate in practice, but if + one somehow does, refusing to conclude is the only + sound answer. *) + if proven solutions then Run [] else Wait { residuatable = false } + else Wait { residuatable = false } + | Positive (World.Or (a, b)) -> + Run [ (subst, flatten a); (subst, flatten b) ] + | Positive ((World.And _ | World.Not _) as expr) -> Run [ (subst, flatten expr) ] | Positive (World.Forall (quantifier, body)) -> ( - (* Universal over the quantifier's solutions. Decidable only - when the quantifier itself is; a stuck quantifier defers - the universal, and an infinite one therefore never runs. *) + (* Universal over the quantifier's solutions. Runs only when + the quantifier is decidable and closed; an undetermined + quantifier or body defers the universal, and an infinite + one therefore never runs. *) match search world subst (flatten quantifier) with - | exception Stuck _ -> None + | exception Stuck _ -> Wait { residuatable = false } | quantified -> - let holds s = search world s (flatten body) <> [] in - if List.for_all holds quantified then Some [ (subst, []) ] else Some [] - ) + if List.exists (fun (_, residue) -> residue <> []) quantified then + Wait { residuatable = false } + else + let body_status (s, _) = + match search world s (flatten body) with + | exception Stuck _ -> `Unknown + | [] -> `Fails + | solutions -> if proven solutions then `Holds else `Unknown + in + let statuses = List.map body_status quantified in + if List.mem `Fails statuses then Run [] + else if List.mem `Unknown statuses then + Wait { residuatable = false } + else Run [ (subst, []) ]) | Positive (World.Apply (name, bindings)) -> ( match Builtin.run subst name bindings with | Some (Builtin.Solved substs) -> - Some (List.map (fun s -> (s, [])) substs) - | Some Builtin.Stuck -> None + Run (List.map (fun s -> (s, [])) substs) + | Some Builtin.Stuck -> + (* Pure membership waiting on bindings: the residuatable + case. Constraining is not searching. *) + Wait { residuatable = true } | None -> ( match W.find world name with | Some (World.Table { facts; _ }) -> - Some + Run (List.filter_map (fun tuple -> let target = Label.Map.map Pattern.of_term tuple in @@ -126,7 +164,7 @@ module Make (W : World.WORLD) = struct | None -> false) in if List.for_all witness_ground rules then - Some + Run (List.filter_map (fun rule -> let head, body = freshen rule in @@ -134,31 +172,44 @@ module Make (W : World.WORLD) = struct (fun s -> (s, flatten body)) (unify_bindings subst bindings head)) rules) - else None + else Wait { residuatable = false } | None -> (* Unreachable on admitted programs: the loader checks references. An embedded host that lies about its catalog surfaces here as a stuck goal rather than a crash. *) - None)) + Wait { residuatable = false })) + (* Search yields substitutions with the goals they left + residuated. A state where every remaining goal is residuatable + membership is an answer; one with a stalled search is a + non-total plan. *) and search world subst goals = match goals with - | [] -> [ subst ] + | [] -> [ (subst, []) ] | _ -> ( let rec select scanned = function | [] -> None | goal :: rest -> ( match try_goal world subst goal with - | Some branches -> Some (branches, List.rev_append scanned rest) - | None -> select (goal :: scanned) rest) + | Run branches -> Some (branches, List.rev_append scanned rest) + | Wait _ -> select (goal :: scanned) rest) in match select [] goals with | Some (branches, remaining) -> List.concat_map (fun (subst, extra) -> search world subst (extra @ remaining)) branches - | None -> raise (Stuck (List.map goal_name goals))) + | None -> + if + List.for_all + (fun goal -> + match try_goal world subst goal with + | Wait { residuatable } -> residuatable + | Run _ -> false) + goals + then [ (subst, goals) ] + else raise (Stuck (List.map goal_name goals))) (* Solution variables: the free variables of the query. Whatever occurs only under a universal is bound per quantifier solution @@ -179,22 +230,40 @@ module Make (W : World.WORLD) = struct in match search world Pattern.Subst.empty (flatten expr) with | exception Stuck goals -> Error (Non_total_plan goals) - | substs -> - let read subst = - List.map - (fun v -> (v, Pattern.Subst.resolve subst (Pattern.Var v))) - variables + | outcomes -> + let read (subst, residue_goals) = + let bindings = + List.map + (fun v -> (v, Pattern.Subst.resolve subst (Pattern.Var v))) + variables + in + let residue = + List.filter_map + (function + | Positive (World.Apply (name, goal_bindings)) -> + Some + (name, Label.Map.map (Pattern.Subst.resolve subst) goal_bindings) + | _ -> None) + residue_goals + in + { bindings; residue } + in + let equal_residual (n, b) (m, c) = + String.equal n m && Label.Map.equal Pattern.equal b c in let equal_solution a b = - List.for_all2 (fun (_, p) (_, q) -> Pattern.equal p q) a b + List.for_all2 (fun (_, p) (_, q) -> Pattern.equal p q) a.bindings + b.bindings + && List.length a.residue = List.length b.residue + && List.for_all2 equal_residual a.residue b.residue in let solutions = List.fold_left - (fun acc subst -> - let solution = read subst in + (fun acc outcome -> + let solution = read outcome in if List.exists (equal_solution solution) acc then acc else acc @ [ solution ]) - [] substs + [] outcomes in Ok solutions end @@ -15,15 +15,28 @@ type error = | Non_total_plan of string list - (** No remaining goal is decidable; the relation names of the - stuck goals, for the message. *) + (** No remaining goal is decidable or residuatable; the + relation names of the stuck goals, for the message. *) val pp_error : Format.formatter -> error -> unit -(** One answer: each free variable of the query, resolved. Ground in - the common case; open exactly when the query admits any value - there. *) -type solution = (string * Pattern.t) list +(** A residual constraint: a membership goal that stayed + underdetermined. It is decidable the moment its variables are + ground; returning it is the honest answer to a satisfiable but + open query. Only builtin membership residuates; searches never + do. *) +type residual = string * Pattern.t Label.Map.t + +val pp_residual : Format.formatter -> residual -> unit +(** Prints the constraint as the proposition it is, [[Rel l: t ...]]. *) + +(** One answer: each free variable of the query resolved, plus the + residual constraints the answer is conditioned on. Ground and + residue-free in the common case. *) +type solution = { + bindings : (string * Pattern.t) list; + residue : residual list; +} module Make (W : World.WORLD) : sig val solve : W.t -> World.expr -> (solution list, error) result |