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
|
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)
|
