Source file unique_binding.ml
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
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
open DatalogLib
module ASProg = Datalog_AbstractSyntax.AbstractSyntax.Program
module ASPred = Datalog_AbstractSyntax.AbstractSyntax.Predicate
module ASRule = Datalog_AbstractSyntax.AbstractSyntax.Rule
module PredTable =
DatalogLib.Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable
module PredIds =
DatalogLib.Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIds
module Log = UtilsLib.Xlog.Make (struct
let name = "Unique_binding"
end)
module RgNodeMap = Map.Make (Rgg.Rg_graph.V)
let new_id_for_adorned_pred ~intensional:is_intensional (pred, adornment)
old_table table =
let pred_sym =
ASPred.PredIdTable.find_sym_from_id pred.ASPred.p_id old_table
in
let () = Log.debug (fun m -> m "Dealing with pred '%s'" pred_sym) in
let ad_pred =
if is_intensional then
Printf.sprintf "%s_%s" pred_sym
(Adornment.to_string adornment)
else pred_sym
in
ASPred.PredIdTable.add_sym ad_pred table
type ad_pred_key = {
key_rule : int;
key_head_ad : Adornment.status list;
key_pred : ASPred.pred_id;
key_pos : int;
}
module AdPredMap = Map.Make (struct
type t = ad_pred_key
let compare k1 k2 =
match k1.key_rule - k2.key_rule with
| 0 -> (
match Adornment.compare k1.key_head_ad k2.key_head_ad with
| 0 -> k1.key_pos - k2.key_pos
| r -> r)
| r -> r
end)
module AdornmentTrie = struct
exception Not_found
exception Conflict
type 'a t = Node of ('a option * 'a alternative)
and 'a alternative = 'a t option * 'a t option
type key = Adornment.status list
let empty = Node (None, (None, None))
let rec add ?(overwrite = false) k v t =
match (k, t) with
| [], Node (None, alt) -> Node (Some v, alt)
| [], Node (Some _, alt) when overwrite -> Node (Some v, alt)
| [], Node (Some _, _) -> raise Conflict
| Adornment.Free :: tl, Node (n, (None, right)) ->
Node (n, (Some (add ~overwrite tl v empty), right))
| Adornment.Free :: tl, Node (n, (Some child, right)) ->
Node (n, (Some (add ~overwrite tl v child), right))
| Adornment.Bound :: tl, Node (n, (left, None)) ->
Node (n, (left, Some (add ~overwrite tl v empty)))
| Adornment.Bound :: tl, Node (n, (left, Some child)) ->
Node (n, (left, Some (add ~overwrite tl v child)))
let rec find key t =
match (key, t) with
| [], Node (None, _) -> raise Not_found
| [], Node (Some v, _) -> v
| Adornment.Free :: _, Node (_, (None, _)) -> raise Not_found
| Adornment.Free :: tl, Node (_, (Some t', _)) -> find tl t'
| Adornment.Bound :: _, Node (_, (_, None)) -> raise Not_found
| Adornment.Bound :: tl, Node (_, (_, Some t')) -> find tl t'
let rec fold_aux f key acc t =
match t with
| Node (None, (None, None)) -> acc
| Node (Some v, (None, None)) -> f (List.rev key) v acc
| Node (None, (Some left, None)) ->
fold_aux f (Adornment.Free :: key) acc left
| Node (None, (None, Some right)) ->
fold_aux f (Adornment.Bound :: key) acc right
| Node (None, (Some left, Some right)) ->
fold_aux f
(Adornment.Bound :: key)
(fold_aux f (Adornment.Free :: key) acc left)
right
| Node (Some v, (Some left, None)) ->
fold_aux f (Adornment.Free :: key) (f (List.rev key) v acc) left
| Node (Some v, (None, Some right)) ->
fold_aux f (Adornment.Bound :: key) (f (List.rev key) v acc) right
| Node (Some v, (Some left, Some right)) ->
fold_aux f
(Adornment.Bound :: key)
(fold_aux f (Adornment.Free :: key) (f (List.rev key) v acc) left)
right
let fold f acc t = fold_aux f [] acc t
let iter f t = fold (fun k v () -> f k v) () t
let pp ?sep:_ _pp_a _fmt _t = failwith "Not implemented"
end
type data = {
adorned_prog : ASProg.program;
unadorned_map : ASPred.pred_id ASPred.PredIdMap.t;
rule_to_rule_map : (int * int) Datalog_AbstractSyntax.RuleIdMap.t;
adornments : Adornment.status list AdPredMap.t;
pred_map : ASPred.pred_id AdornmentTrie.t ASPred.PredIdMap.t;
}
let find_goal Rgg.{ rule; position; _ } =
match
List.find_opt (fun (_, pos) -> pos = position + 1) rule.ASRule.e_rhs
with
| Some res -> res
| None -> List.find (fun (_, pos) -> pos = position + 1) rule.ASRule.i_rhs
let extend_map_to_trie p_id (ad, new_p_id) m =
match ASPred.PredIdMap.find_opt p_id m with
| None -> ASPred.PredIdMap.add p_id AdornmentTrie.(add ad new_p_id empty) m
| Some t ->
ASPred.PredIdMap.add p_id
AdornmentTrie.(add ~overwrite:true ad new_p_id t)
m
let rec get_rule_rhs_aux ~from:r_n node graph prog
((e_body, i_body, data_acc) as acc) =
match node with
| Rgg.Goal (goal_pred, goal_ad) ->
let is_intensional =
ASPred.(PredIds.mem goal_pred.p_id prog.ASProg.i_preds)
in
let new_goal_id, new_table =
new_id_for_adorned_pred ~intensional:is_intensional (goal_pred, goal_ad)
prog.ASProg.pred_table data_acc.adorned_prog.ASProg.pred_table
in
let () = Log.debug (fun m -> m "Intensional? %b" is_intensional) in
let new_pred_map =
extend_map_to_trie goal_pred.ASPred.p_id (goal_ad, new_goal_id)
data_acc.pred_map
in
let goal_in_rule, goal_position = find_goal r_n in
let () = Log.debug (fun m -> m "At position '%d'" goal_position) in
let () = assert (ASPred.(goal_pred.p_id = goal_in_rule.p_id)) in
let new_goal_pred = ASPred.{ goal_in_rule with p_id = new_goal_id } in
let new_unadorned_map =
ASPred.(PredIdMap.add new_goal_id goal_pred.p_id data_acc.unadorned_map)
in
let new_prog =
{ data_acc.adorned_prog with ASProg.pred_table = new_table }
in
if is_intensional then
let new_prog' =
{
new_prog with
ASProg.i_preds =
ASPred.PredIds.add new_goal_id new_prog.ASProg.i_preds;
}
in
( e_body,
(new_goal_pred, goal_position) :: i_body,
{
data_acc with
adorned_prog = new_prog';
unadorned_map = new_unadorned_map;
pred_map = new_pred_map;
} )
else
( (new_goal_pred, goal_position) :: e_body,
i_body,
{
data_acc with
adorned_prog = new_prog;
unadorned_map = new_unadorned_map;
pred_map = new_pred_map;
} )
| Rgg.Rule new_r_n when new_r_n.Rgg.position = r_n.Rgg.position + 1 ->
Rgg.Rg_graph.fold_succ
(fun n l_acc -> get_rule_rhs_aux ~from:new_r_n n graph prog l_acc)
graph node acc
| Rgg.Rule _ -> failwith "Bug: wrong from_position for rule"
let get_rule_rhs ~from:r_n graph prog acc =
Rgg.Rg_graph.fold_succ
(fun n l_acc -> get_rule_rhs_aux ~from:r_n n graph prog l_acc)
graph (Rgg.Rule r_n) acc
let derive_program graph prog =
let () =
Log.debug (fun m -> m "Going to derive program for:@,@[<v> @[%a@]@]"
(ASProg.pp ~with_position:false ~with_id:true) prog)
in
let new_prog =
ASProg.
{
rules = ASRule.Rules.empty;
pred_table = ASPred.PredIdTable.empty;
const_table = prog.const_table;
i_preds = ASPred.PredIds.empty;
rule_id_gen = UtilsLib.IdGenerator.IntIdGen.init ();
head_to_rules = ASPred.PredIdMap.empty;
e_pred_to_rules = ASPred.PredIdMap.empty;
}
in
Rgg.Rg_graph.fold_vertex
(fun node l_data ->
match node with
| Rgg.Rule _ ->
l_data
| Rgg.Goal (head_pred_sym, _)
when not ASPred.(PredIds.mem head_pred_sym.p_id prog.ASProg.i_preds) ->
l_data
| Rgg.Goal (head_pred, head_adornment) ->
let head_id, new_table =
new_id_for_adorned_pred ~intensional:true
(head_pred, head_adornment)
prog.ASProg.pred_table l_data.adorned_prog.ASProg.pred_table
in
let new_pred_map =
extend_map_to_trie head_pred.ASPred.p_id (head_adornment, head_id)
l_data.pred_map
in
let new_unadorned_map =
ASPred.PredIdMap.add head_id head_pred.ASPred.p_id
l_data.unadorned_map
in
Rgg.Rg_graph.fold_succ
(fun vertex l_acc ->
match vertex with
| Rgg.Goal _ ->
failwith
"A goal node should not be the successor of a goal node"
| Rgg.Rule r_n when r_n.Rgg.position <> 0 ->
l_acc
| Rgg.Rule r_n ->
let () = assert (head_adornment = r_n.Rgg.adorned_head) in
let () =
Log.debug (fun m ->
m "Extracting rule:@,@[ @[%a@]@]"
(ASRule.pp ~with_position:true
~with_id:true prog.ASProg.pred_table
prog.ASProg.const_table) r_n.Rgg.rule)
in
let head_pred =
ASPred.{ r_n.Rgg.rule.ASRule.lhs with p_id = head_id }
in
let e_rhs, i_rhs, l_acc' =
get_rule_rhs ~from:r_n graph prog ([], [], l_acc)
in
let new_rule_id, new_rule_id_gen =
UtilsLib.IdGenerator.IntIdGen.get_fresh_id
l_acc'.adorned_prog.ASProg.rule_id_gen
in
let new_prog =
{
l_acc'.adorned_prog with
ASProg.rule_id_gen = new_rule_id_gen;
}
in
let sorted_e_rhs =
List.sort (fun (_, pos1) (_, pos2) -> pos1 - pos2) e_rhs
in
let sorted_i_rhs =
List.sort (fun (_, pos1) (_, pos2) -> pos1 - pos2) i_rhs
in
let i_length = List.length sorted_i_rhs in
let () =
Log.debug (fun m ->
m "i_length = %d, i_rhs_num = %d" i_length
r_n.Rgg.rule.ASRule.i_rhs_num)
in
let () = assert (i_length = r_n.Rgg.rule.ASRule.i_rhs_num) in
let new_rule =
ASRule.
{
id = new_rule_id;
lhs = head_pred;
e_rhs = sorted_e_rhs;
i_rhs = sorted_i_rhs;
i_rhs_num = i_length;
rhs_num = r_n.Rgg.rule.rhs_num;
}
in
let new_prog' =
ASProg.
{
new_prog with
rules = ASRule.Rules.add new_rule new_prog.rules;
head_to_rules =
ASRule.extend_head_id_map_to_rules head_id new_rule
new_prog.head_to_rules;
}
in
{
l_acc' with
adorned_prog = new_prog';
rule_to_rule_map =
Datalog_AbstractSyntax.RuleIdMap.add new_rule_id
(r_n.Rgg.rule.ASRule.id, i_length)
l_acc'.rule_to_rule_map;
})
graph node
{
l_data with
adorned_prog =
{
l_data.adorned_prog with
ASProg.pred_table = new_table;
ASProg.i_preds =
ASPred.PredIds.add head_id
l_data.adorned_prog.ASProg.i_preds;
};
pred_map = new_pred_map;
unadorned_map = new_unadorned_map;
})
graph
{
adorned_prog = new_prog;
unadorned_map = ASPred.PredIdMap.empty;
rule_to_rule_map = Datalog_AbstractSyntax.RuleIdMap.empty;
adornments = AdPredMap.empty;
pred_map = ASPred.PredIdMap.empty;
}