Source file datalog_AbstractSyntax.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
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
open UtilsLib.IdGenerator
open UtilsLib.Utils
module Var=
struct
type t=Var of int
let compare (Var i) (Var j)=i-j
let succ (Var i)=Var (i+1)
let start=Var 0
let to_string (Var i) =
let dec = decompose ~input:i ~base:26 in
List.fold_left
(fun acc i ->
Printf.sprintf "%s%c" acc (char_of_int (97+i)))
""
dec
end
module VarGen = IdGen(Var)
module Const=
struct
type t=Const of int
let compare (Const i) (Const j)=i-j
let start=Const 0
let succ (Const i)=Const (i+1)
let to_string (Const i) = string_of_int i
end
module ConstGen=IdGen(Const)
module AbstractSyntax =
struct
module Log = (val Logs.src_log (Logs.Src.create "ACGtkLib.datalog_AbstractSyntax" ~doc:"logs ACGtkLib datalog_AbstractSyntax events") : Logs.LOG)
(** These modules are the abstract syntactic representations of the
predicates, of the rules, and of the programs *)
module Predicate =
struct
type term =
| Var of VarGen.id
| Const of ConstGen.id
module VarMap = Map.Make (Var)
let map_content_compare (k1,map1) (k2,map2) =
try
let val1 = VarMap.find k1 map1 in
(try
val1-(VarMap.find k2 map2)
with
| Not_found -> 1)
with
| Not_found ->
(try
let _ = VarMap.find k2 map2 in
-1
with
| Not_found -> 0)
let term_compare l1 l2 =
let rec term_compare_aux l1 l2 (l1_vars,l2_vars) pos =
match l1,l2 with
| [],[] -> 0
| [],_ -> -1
| _,[] -> 1
| (Const _)::_,(Var _)::_ -> 1
| (Var _)::_,(Const _)::_ -> -1
| (Const a1)::tl1,(Const a2)::tl2 ->
let res = ConstGen.compare a1 a2 in
if ConstGen.compare a1 a2 <> 0 then
res
else
term_compare_aux tl1 tl2 (l1_vars,l2_vars) (pos+1)
| (Var a1)::tl1,(Var a2)::tl2 ->
let res = map_content_compare (a1,l1_vars) (a2,l2_vars) in
if VarGen.compare a1 a2 <> 0 then
res
else
term_compare_aux tl1 tl2 (VarMap.add a1 pos l1_vars,VarMap.add a2 pos l2_vars) (pos+1) in
term_compare_aux l1 l2 (VarMap.empty,VarMap.empty) 0
let term_to_string t cst_id_table =
match t with
| Var v -> Var.to_string v
| Const c ->
ConstGen.Table.find_sym_from_id c cst_id_table
type pred_id=int
module PredIdMap = IntIdGen.IdMap
module PredIdTable = IntIdGen.Table
type predicate={p_id:pred_id;
arity:int;
arguments: term list
(** It is assumed that the size of the list is the
arity *)
}
let to_string predicate ?position pred_id_table cst_id_table=
let position_info =
match position with
| None -> ""
| Some i -> Printf.sprintf " (* position: %d*)" i in
Printf.sprintf "%s(%s)%s"
(PredIdTable.find_sym_from_id predicate.p_id pred_id_table)
(string_of_list "," (fun p -> term_to_string p cst_id_table) predicate.arguments)
position_info
let compare ({p_id=id1;arity=a1;arguments=l1}:predicate) ({p_id=id2;arity=a2;arguments=l2}:predicate) =
let res = compare id1 id2 in
if res<>0 then
res
else
let res = a1-a2 in
if res<>0 then
res
else
term_compare l1 l2
let fake_pred_id = -1
module PredIds=IntSet
end
module Proto_Rule =
struct
type t = {proto_id:int;
proto_lhs:Predicate.predicate;
proto_rhs:Predicate.predicate list;
(** represents the predicates of the rule *)
}
let to_string r pred_id_table cst_id_table=
let head=Predicate.to_string r.proto_lhs pred_id_table cst_id_table in
let tail=
match r.proto_rhs with
| [] -> "."
| _ ->
Printf.sprintf
":- %s."
(string_of_list "," (fun p -> Predicate.to_string p pred_id_table cst_id_table) r.proto_rhs) in
Printf.sprintf "%s%s\n" head tail
let to_buffer rules pred_id_table cst_id_table =
let buff=Buffer.create 4 in
let () =
List.iter
(fun r -> Buffer.add_string
buff
(Printf.sprintf "%s\n" (to_string r pred_id_table cst_id_table)))
rules in
buff
[@@warning "-32"]
let to_log rules pred_id_table cst_id_table src level =
List.iter
(fun r -> Logs.msg ~src level (fun m -> m "@;<4>%s" (to_string r pred_id_table cst_id_table)))
rules
[@@warning "-32"]
end
module Rule =
struct
type rule={id:int;
lhs:Predicate.predicate;
e_rhs:(Predicate.predicate*int) list;
i_rhs:(Predicate.predicate*int) list;
i_rhs_num:int;
}
let to_string r ?(with_position=false) pred_id_table cst_id_table =
let head=Predicate.to_string r.lhs pred_id_table cst_id_table in
let vdash,e_i_sep =
match r.e_rhs,r.i_rhs with
| [],[] -> "",""
| [],_ -> ":- "," "
| _,[] -> ":- "," "
| _,_ -> ":- "," , " in
let string_of_pred (pred,pos) =
match with_position with
| false -> Predicate.to_string pred pred_id_table cst_id_table
| true -> Predicate.to_string pred ~position:pos pred_id_table cst_id_table in
Printf.sprintf "%s%s%s%s%s." head vdash (string_of_list "," string_of_pred r.e_rhs) e_i_sep (string_of_list "," string_of_pred r.i_rhs)
module Rules=Set.Make(struct
type t=rule
let compare {id=i;_} {id=j;_} = i-j
end)
module RuleMap=Map.Make(struct
type t=rule
let compare {id=i;_} {id=j;_} = i-j
end)
let ids_to_rules ids id_to_rule_map =
IntSet.fold
(fun e acc -> Rules.add (IntMap.find e id_to_rule_map) acc)
ids
Rules.empty
let to_buffer rules pred_id_table cst_id_table =
let buff=Buffer.create 4 in
let () =
Rules.iter
(fun r ->
let () =
Buffer.add_string
buff
(to_string r pred_id_table cst_id_table) in
Buffer.add_string buff "\n")
rules in
buff
let to_log rules pred_id_table cst_id_table src level =
Rules.iter
(fun r -> Logs.msg ~src level (fun m -> m "@;<4>%s" (to_string r pred_id_table cst_id_table)))
rules
let init_split_rhs proto_preds intensional_pred =
let i_num,i_p,e_p,_=
List.fold_left
(fun (i_num,i_preds,e_preds,i) ({Predicate.p_id=p_id;_} as pred) ->
if Predicate.PredIds.mem p_id intensional_pred
then
(i_num+1,(pred,i)::i_preds,e_preds,i+1)
else
(i_num,i_preds,(pred,i)::e_preds,i+1))
(0,[],[],1)
proto_preds in
i_num,i_p,e_p
let update_split_rhs init proto_preds intensional_pred =
List.fold_left
(fun (i_preds,e_preds) (({Predicate.p_id=p_id;_},_) as pred) ->
if Predicate.PredIds.mem p_id intensional_pred
then
(pred::i_preds,e_preds)
else
(i_preds,pred::e_preds))
init
proto_preds
let extend_map_to_set k v map_to_set =
let current_set =
try
Predicate.PredIdMap.find k map_to_set
with
| Not_found -> IntSet.empty in
Predicate.PredIdMap.add k (IntSet.add v current_set) map_to_set
let proto_rule_to_rule proto_rule intensional_pred =
let i_num,i_preds,e_preds =
init_split_rhs proto_rule.Proto_Rule.proto_rhs intensional_pred in
{id=proto_rule.Proto_Rule.proto_id;
lhs=proto_rule.Proto_Rule.proto_lhs;
e_rhs=List.rev e_preds;
i_rhs=List.rev i_preds;
i_rhs_num=i_num}
let update rule intensional_pred =
let i_preds,e_preds =
update_split_rhs (rule.i_rhs,[]) rule.e_rhs intensional_pred in
{rule with e_rhs=e_preds;i_rhs=i_preds}
end
module Proto_Program =
struct
type t = {rules:Proto_Rule.t list;
pred_table: Predicate.PredIdTable.table;
const_table: ConstGen.Table.table;
i_preds:Predicate.PredIds.t;
rule_id_gen:IntIdGen.t;
pred_to_rules:IntSet.t Predicate.PredIdMap.t}
type tables = Predicate.PredIdTable.table*(VarGen.Table.table*ConstGen.Table.table)
let empty = {rules=[];
pred_table=Predicate.PredIdTable.empty;
const_table=ConstGen.Table.empty;
i_preds=Predicate.PredIds.empty;
rule_id_gen=IntIdGen.init ();
pred_to_rules=Predicate.PredIdMap.empty}
let extension pred_table const_table rule_id_gen=
{rules=[];
pred_table;
const_table;
i_preds=Predicate.PredIds.empty;
rule_id_gen;
pred_to_rules=Predicate.PredIdMap.empty}
let add_proto_rule (f_lhs,f_rhs) prog =
let rule_id,new_rule_id_gen=IntIdGen.get_fresh_id prog.rule_id_gen in
let lhs,(new_pred_id_table,new_tables)=f_lhs (prog.pred_table,(VarGen.Table.empty,prog.const_table)) in
let rhs,(new_pred_id_table',(_,new_const_table))=f_rhs (new_pred_id_table,new_tables) in
let new_i_preds=
match rhs with
| [] -> prog.i_preds
| _ -> Predicate.PredIds.add lhs.Predicate.p_id prog.i_preds in
let new_rule = {Proto_Rule.proto_id=rule_id;
Proto_Rule.proto_lhs=lhs;
Proto_Rule.proto_rhs=rhs} in
{rules=new_rule::prog.rules;
pred_table=new_pred_id_table';
const_table=new_const_table;
i_preds=new_i_preds;
rule_id_gen=new_rule_id_gen;
pred_to_rules=
List.fold_left
(fun acc p -> Rule.extend_map_to_set p.Predicate.p_id rule_id acc)
prog.pred_to_rules
rhs
}
end
module Program =
struct
type program = {rules:Rule.Rules.t;
pred_table: Predicate.PredIdTable.table;
const_table: ConstGen.Table.table;
i_preds:Predicate.PredIds.t;
rule_id_gen:IntIdGen.t;
e_pred_to_rules: Rule.Rules.t Predicate.PredIdMap.t}
type modifier = {modified_rules:Rule.Rules.t;
new_pred_table: Predicate.PredIdTable.table;
new_const_table: ConstGen.Table.table;
new_i_preds:Predicate.PredIds.t;
new_e_preds:Predicate.PredIds.t;
new_rule_id_gen:IntIdGen.t;}
let make_program {Proto_Program.rules;Proto_Program.pred_table;Proto_Program.const_table;Proto_Program.i_preds;Proto_Program.rule_id_gen;Proto_Program.pred_to_rules}=
let actual_rules,ids_to_rule_map =
List.fold_left
(fun (acc,ids_to_rule_map) p_rule ->
let rule = Rule.proto_rule_to_rule p_rule i_preds in
Rule.Rules.add rule acc,
IntMap.add p_rule.Proto_Rule.proto_id rule ids_to_rule_map)
(Rule.Rules.empty,IntMap.empty)
rules in
{rules=actual_rules;
pred_table=pred_table;
const_table=const_table;
i_preds=i_preds;
rule_id_gen=rule_id_gen;
e_pred_to_rules=
Predicate.PredIdMap.fold
(fun p rule_ids acc ->
if Predicate.PredIds.mem p i_preds then
Predicate.PredIdMap.remove p acc
else
Predicate.PredIdMap.add p (Rule.ids_to_rules rule_ids ids_to_rule_map) acc)
pred_to_rules
Predicate.PredIdMap.empty}
let extend prog {Proto_Program.rules;Proto_Program.pred_table;Proto_Program.const_table;Proto_Program.i_preds;Proto_Program.rule_id_gen;Proto_Program.pred_to_rules}=
let new_i_preds = Predicate.PredIds.union prog.i_preds i_preds in
let updated_e_pred_map_to_r,updated_rules =
Predicate.PredIds.fold
(fun p_id ((e_p_to_r,rules_acc) as acc) ->
try
let to_be_modified_rules =
Predicate.PredIdMap.find p_id prog.e_pred_to_rules in
Predicate.PredIdMap.remove p_id e_p_to_r,
Rule.Rules.fold
(fun r acc ->
Rule.Rules.add (Rule.update r new_i_preds) (Rule.Rules.remove r acc))
to_be_modified_rules
rules_acc
with
| Not_found -> acc)
i_preds
(prog.e_pred_to_rules,prog.rules) in
let new_rules,id_to_rule_map =
List.fold_left
(fun (acc,id_to_rule_map) p_rule ->
let rule=Rule.proto_rule_to_rule p_rule new_i_preds in
Rule.Rules.add rule acc,
IntMap.add p_rule.Proto_Rule.proto_id rule id_to_rule_map)
(updated_rules,IntMap.empty)
rules in
{rules=new_rules;
pred_table=pred_table;
const_table=const_table;
i_preds=new_i_preds;
rule_id_gen=rule_id_gen;
e_pred_to_rules=
Predicate.PredIdMap.merge
(fun _ opt_rule_ids opt_rules ->
match opt_rule_ids, opt_rules with
| None,None -> None
| None,_ -> opt_rules
| Some ids,None -> Some (Rule.ids_to_rules ids id_to_rule_map)
| Some ids,Some rules ->
Some (Rule.Rules.union rules (Rule.ids_to_rules ids id_to_rule_map)))
pred_to_rules
updated_e_pred_map_to_r
}
let to_buffer prog =
let buff = Rule.to_buffer prog.rules prog.pred_table prog.const_table in
let () = Buffer.add_string buff "Intensional predicates are:\n" in
let () =
Predicate.PredIds.iter
(fun elt -> Buffer.add_string buff (Printf.sprintf "\t%s\n%!" (Predicate.PredIdTable.find_sym_from_id elt prog.pred_table)))
prog.i_preds in
buff
let log_content ?(src=Logs.default) level prog =
let () = Rule.to_log prog.rules prog.pred_table prog.const_table src level in
let () = Logs.msg ~src level (fun m -> m "Intensional predicates are:") in
let () = Predicate.PredIds.iter
(fun elt ->
Logs.msg
~src
level
(fun m -> m "@;<4>%s" (Predicate.PredIdTable.find_sym_from_id elt prog.pred_table)))
prog.i_preds in
Logs.msg
~src
level
(fun m -> m "Done.")
end
end