1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
|
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
(* 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
| 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)
(* 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 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)) ]
| 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)
| 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))
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 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)
| 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)
|
