diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/vm.ml | 106 |
1 files changed, 76 insertions, 30 deletions
@@ -10,19 +10,34 @@ type solution = (string * Pattern.t) 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 + let rec flatten = function | World.And (a, b) -> flatten a @ flatten b - | goal -> [ goal ] + | 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) -> expr_vars a @ expr_vars b + | 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 - | World.Apply (name, _) -> name - | World.And _ -> ":and" - | World.Or _ -> ":or" + | 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 @@ -42,6 +57,8 @@ module Make (W : World.WORLD) = struct 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) @@ -59,12 +76,30 @@ module Make (W : World.WORLD) = struct (* 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 = + means not decidable yet; the planner retries it later, and + rejects the plan if nothing ever runs. *) + let rec 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) -> ( + | 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)) ] + | 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. *) + match search world subst (flatten quantifier) with + | exception Stuck _ -> None + | quantified -> + let holds s = search world s (flatten body) <> [] in + if List.for_all holds quantified then Some [ (subst, []) ] else Some [] + ) + | Positive (World.Apply (name, bindings)) -> ( match Builtin.run subst name bindings with | Some (Builtin.Solved substs) -> Some (List.map (fun s -> (s, [])) substs) @@ -107,31 +142,42 @@ module Make (W : World.WORLD) = struct rather than a crash. *) None)) + and search world 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 world subst (extra @ remaining)) + branches + | None -> 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 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) + [] (outer_vars expr) + |> List.filter (fun v -> not (String.contains v '@')) in - match search Pattern.Subst.empty (flatten expr) with + match search world Pattern.Subst.empty (flatten expr) with | exception Stuck goals -> Error (Non_total_plan goals) | substs -> let read subst = |