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 residual = string * Pattern.t Label.Map.t let pp_residual fmt (name, bindings) = Format.fprintf fmt "@[[%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 (* A goal is a proposition to establish or a denial to refute. Conjunction flattens; [u :not d] contributes the universe 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 ] | expr -> [ Positive expr ] 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) | World.Not (a, b) | World.Forall (a, b) -> expr_vars a @ expr_vars b let goal_name = function | Positive (World.Apply (name, _)) -> name | Positive (World.Or _) -> ":or" | Positive (World.And _) -> ":and" | Positive (World.Not _) | Negated _ -> ":not" | Positive (World.Forall _) -> "ForAll" let unresolved_vars subst expr = expr_vars expr |> List.filter (fun v -> not (Pattern.is_ground (Pattern.Subst.resolve subst (Pattern.Var v)))) (* 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) | World.Not (a, b) -> World.Not (rename_expr a, rename_expr b) | World.Forall (a, b) -> World.Forall (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) let proven solutions = List.exists (fun (_, residue) -> residue = []) solutions (* Interval propagation over waiting membership constraints. What residuation returns inert, this looks at together: bounds with an empty intersection fail the branch outright, and an integer variable squeezed into a finite range converts to bounded generation, the same admissible enumeration Between performs explicitly. Sakura's cardinality analysis, inside the engine. *) module Propagate = struct let forced_label name = match Label.of_string name with Ok l -> l | Error _ -> assert false let value_l = forced_label "value" let left_l = forced_label "left" let right_l = forced_label "right" type bound = { value : Q.t; strict : bool } type info = { integer : bool; stringy : bool; lower : bound option; upper : bound option; } let no_info = { integer = false; stringy = false; lower = None; upper = None } module M = Map.Make (String) let note var f store = M.update var (fun info -> Some (f (Option.value ~default:no_info info))) store let stronger_lower a b = if Q.gt a.value b.value then a else if Q.lt a.value b.value then b else { a with strict = a.strict || b.strict } let stronger_upper a b = if Q.lt a.value b.value then a else if Q.gt a.value b.value then b else { a with strict = a.strict || b.strict } let add_lower bound info = { info with lower = Some (match info.lower with | None -> bound | Some existing -> stronger_lower bound existing); } let add_upper bound info = { info with upper = Some (match info.upper with | None -> bound | Some existing -> stronger_upper bound existing); } let numeric_value = function | Pattern.Integer z -> Some (Q.of_bigint z) | Pattern.Rational q -> Some q | _ -> None (* Read one waiting builtin goal into the store. Bindings arrive already resolved, so a variable here is genuinely unbound. *) let gather store (name, bindings) = let value = Label.Map.find_opt value_l bindings and left = Label.Map.find_opt left_l bindings and right = Label.Map.find_opt right_l bindings in match (name, value, left, right) with | ("Integer" | "Natural"), Some (Pattern.Var x), _, _ -> let store = note x (fun i -> { i with integer = true }) store in if String.equal name "Natural" then note x (add_lower { value = Q.zero; strict = false }) store else store | "String", Some (Pattern.Var x), _, _ -> note x (fun i -> { i with stringy = true }) store | ( ("LessThan" | "LessThanEqual" | "GreaterThan" | "GreaterEqual"), _, Some left, Some right ) -> ( let strict = String.equal name "LessThan" || String.equal name "GreaterThan" in let less = String.equal name "LessThan" || String.equal name "LessThanEqual" in match (left, right) with | Pattern.Var x, ground when Option.is_some (numeric_value ground) -> let bound = { value = Option.get (numeric_value ground); strict } in note x (if less then add_upper bound else add_lower bound) store | ground, Pattern.Var x when Option.is_some (numeric_value ground) -> let bound = { value = Option.get (numeric_value ground); strict } in note x (if less then add_lower bound else add_upper bound) store | _ -> store) | _ -> store (* Integer endpoints of a rational interval. *) let lower_int { value; strict } = let n = Q.num value and d = Q.den value in if strict then Z.add (Z.fdiv n d) Z.one else Z.cdiv n d let upper_int { value; strict } = let n = Q.num value and d = Q.den value in if strict then Z.sub (Z.cdiv n d) Z.one else Z.fdiv n d type verdict = Fail | Enumerate of string * Z.t * Z.t | Unknown let analyze constraints = let store = List.fold_left gather M.empty constraints in let contradictory _ info = (info.stringy && (info.integer || info.lower <> None || info.upper <> None)) || match (info.lower, info.upper) with | Some lo, Some hi -> Q.gt lo.value hi.value || (Q.equal lo.value hi.value && (lo.strict || hi.strict)) || (info.integer && Z.gt (lower_int lo) (upper_int hi)) | _ -> false in if M.exists contradictory store then Fail else match M.choose_opt (M.filter (fun _ info -> info.integer && info.lower <> None && info.upper <> None) store) with | Some (var, info) -> Enumerate ( var, lower_int (Option.get info.lower), upper_int (Option.get info.upper) ) | None -> Unknown end 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 | [] -> 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. 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 _ -> Wait { residuatable = false } | quantified -> 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) -> 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; _ }) -> Run (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 = 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 (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 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. *) 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, []) ] | _ -> ( let rec select scanned = function | [] -> None | goal :: rest -> ( match try_goal world subst goal with | 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 -> ( (* Everything waits. Propagate over the waiting membership constraints before residuating or rejecting: they may be jointly unsatisfiable, or may pin a variable into a finite range that unblocks the rest. *) let attempts = List.map (fun g -> (g, try_goal world subst g)) goals in let membership = List.filter_map (fun (goal, attempt) -> match (goal, attempt) with | ( Positive (World.Apply (name, bindings)), Wait { residuatable = true } ) -> Some ( name, Label.Map.map (Pattern.Subst.resolve subst) bindings ) | _ -> None) attempts in match Propagate.analyze membership with | Propagate.Fail -> [] | Propagate.Enumerate (var, lo, hi) -> let rec enumerate v acc = if Z.gt v hi then acc else let branch = match Pattern.Subst.unify subst (Pattern.Var var) (Pattern.Integer v) with | Some subst -> search world subst goals | None -> [] in enumerate (Z.succ v) (acc @ branch) in enumerate lo [] | Propagate.Unknown -> if List.for_all (fun (_, attempt) -> match attempt with | Wait { residuatable } -> residuatable | Run _ -> false) attempts 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 and is nobody's answer. *) let rec outer_vars = function | World.Apply (_, bindings) -> Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings [] | World.And (a, b) | World.Or (a, b) | World.Not (a, b) -> outer_vars a @ outer_vars b | World.Forall _ -> [] let solve world expr = let variables = List.fold_left (fun acc v -> if List.mem v acc then acc else acc @ [ v ]) [] (outer_vars expr) |> List.filter (fun v -> not (String.contains v '@')) in match search world Pattern.Subst.empty (flatten expr) with | exception Stuck goals -> Error (Non_total_plan goals) | 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.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 outcome -> let solution = read outcome in if List.exists (equal_solution solution) acc then acc else acc @ [ solution ]) [] outcomes in Ok solutions end module Standalone = Make (World.Standalone)