diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/vm.ml | 156 | ||||
| -rw-r--r-- | lib/vm.mli | 37 |
2 files changed, 193 insertions, 0 deletions
diff --git a/lib/vm.ml b/lib/vm.ml new file mode 100644 index 0000000..bde087a --- /dev/null +++ b/lib/vm.ml @@ -0,0 +1,156 @@ +type error = Non_total_plan of string list + +let pp_error fmt (Non_total_plan goals) = + Format.fprintf fmt + "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 + +module Make (W : World.WORLD) = struct + exception Stuck of string list + + let rec flatten = function + | World.And (a, b) -> flatten a @ flatten b + | goal -> [ goal ] + + let rec expr_vars = function + | World.Apply (_, bindings) -> + Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings [] + | World.And (a, b) | World.Or (a, b) -> expr_vars a @ expr_vars b + + let goal_name = function + | World.Apply (name, _) -> name + | World.And _ -> ":and" + | World.Or _ -> ":or" + + (* Rule variables are renamed apart at every unfolding. The suffix + character cannot be lexed, so renamed variables are unforgeable + from source text. *) + let freshen = + let counter = ref 0 in + fun rule -> + incr counter; + let stamp = "@" ^ string_of_int !counter in + let rec rename = function + | Pattern.Var v -> Pattern.Var (v ^ stamp) + | Pattern.Record map -> Pattern.Record (Label.Map.map rename map) + | ground -> ground + in + let rec rename_expr = function + | World.Apply (name, bindings) -> + World.Apply (name, Label.Map.map rename bindings) + | World.And (a, b) -> World.And (rename_expr a, rename_expr b) + | World.Or (a, b) -> World.Or (rename_expr a, rename_expr b) + in + (Label.Map.map rename rule.World.head, rename_expr rule.World.body) + + (* Unify a goal's bindings against a rule head or a stored tuple. + Goal labels absent from the head fail the branch; head labels + absent from the goal are existential. *) + let unify_bindings subst goal_bindings target_bindings = + Label.Map.fold + (fun label pattern acc -> + Option.bind acc (fun subst -> + match Label.Map.find_opt label target_bindings with + | Some target -> Pattern.Subst.unify subst pattern target + | 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. *) + let try_goal world subst goal = + match goal with + | World.Or (a, b) -> Some [ (subst, flatten a); (subst, flatten b) ] + | World.And _ -> Some [ (subst, flatten goal) ] + | 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 + | None -> ( + match W.find world name with + | Some (World.Table { facts; _ }) -> + Some + (List.filter_map + (fun tuple -> + let target = Label.Map.map Pattern.of_term tuple in + Option.map + (fun s -> (s, [])) + (unify_bindings subst bindings target)) + facts) + | Some (World.Rules rules) -> + let witness_ground rule = + match rule.World.witness with + | None -> true + | Some label -> ( + match Label.Map.find_opt label bindings with + | Some pattern -> + Pattern.is_ground (Pattern.Subst.resolve subst pattern) + | None -> false) + in + if List.for_all witness_ground rules then + Some + (List.filter_map + (fun rule -> + let head, body = freshen rule in + Option.map + (fun s -> (s, flatten body)) + (unify_bindings subst bindings head)) + rules) + else None + | 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)) + + let solve world expr = + let rec search subst goals = + match goals with + | [] -> [ 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) + in + match select [] goals with + | Some (branches, remaining) -> + List.concat_map + (fun (subst, extra) -> search subst (extra @ remaining)) + branches + | None -> raise (Stuck (List.map goal_name goals))) + in + let variables = + List.fold_left + (fun acc v -> if List.mem v acc then acc else acc @ [ v ]) + [] (expr_vars expr) + in + match search 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 + in + let equal_solution a b = + List.for_all2 (fun (_, p) (_, q) -> Pattern.equal p q) a b + in + let solutions = + List.fold_left + (fun acc subst -> + let solution = read subst in + if List.exists (equal_solution solution) acc then acc + else acc @ [ solution ]) + [] substs + in + Ok solutions +end + +module Standalone = Make (World.Standalone) diff --git a/lib/vm.mli b/lib/vm.mli new file mode 100644 index 0000000..6ce3f93 --- /dev/null +++ b/lib/vm.mli @@ -0,0 +1,37 @@ +(** The solver: proof search over an admitted world. + + Functorized over {!World.WORLD} (decision 4): the standalone + binary instantiates it with {!World.Standalone}; RNT instantiates + it with its own catalog and links the same engine in-process. + + Execution is dynamic goal selection: at each step the engine + runs any goal that is decidable at the current bindings, so + conjunction stays honestly commutative and order on the page + means nothing. A conjunction where no goal can ever run (an + unbounded membership, an unbounded recursion) is rejected as a + non-total plan, never attempted. Together with admission-time + rule checking, this is what makes every accepted query + terminate. *) + +type error = + | Non_total_plan of string list + (** No remaining goal is decidable; 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 + +module Make (W : World.WORLD) : sig + val solve : W.t -> World.expr -> (solution list, error) result + (** All answers to the query, duplicates collapsed. Total: the + world was admitted, so search terminates; the only failure is + a plan the engine refuses to run. *) +end + +module Standalone : sig + val solve : World.Standalone.t -> World.expr -> (solution list, error) result +end |