package acgtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(*  let c = Printf.sprintf "%c" (char_of_int (97+i)) in
    c *)
    
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 -> (* Const.to_string 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 string_of_predicate_list lst = string_of_list "," (fun p -> Predicate.to_string p pred_id_table cst_id_table) lst in *)
      let vdash,e_i_sep =
	match r.e_rhs,r.i_rhs with
	| [],[] -> "",""
	| [],_ -> ":- "," "
	| _,[] -> ":- "," "
	| _,_ -> ":- "," , " in
      (*
      Printf.sprintf "%s%s%s%s%s." head vdash ((string_of_predicate_list >> fst >> List.split)  r.e_rhs) e_i_sep ((string_of_predicate_list >> fst >> List.split) r.i_rhs) *)
      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 =
	(* all the rules that were pointed to by an extensional
	   predicate that has be turned into an intensional predicate
	   because of the program extension have to be updated *)
	(* We check if some the new intensional predicates also are
	   keys of the e_pred_to_rules map of the previous program *)
	Predicate.PredIds.fold
	  (fun p_id ((e_p_to_r,rules_acc) as acc) -> 
	    try
	      (* First we check wether this predicate was considered
		 as an extensional one *)
	      let to_be_modified_rules =
		Predicate.PredIdMap.find p_id prog.e_pred_to_rules in
	      (* If yes, we nee to remove it from the map *)
	      Predicate.PredIdMap.remove p_id e_p_to_r,
	      (* And to modify the rules it pointed to *)
	      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
	    (* If no, don't do anything *)
	    | 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

OCaml

Innovation. Community. Security.