package acgtk

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

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; (* Probably useless *)
  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
  (* Free on the left, and Bound on the right *)

  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;
  (* map from the id of the adorned predicate (the predicate of the
     unique binding program) to the id of the original predicate it
     replaces *)
  rule_to_rule_map : (int * int) Datalog_AbstractSyntax.RuleIdMap.t;
  (* map from the id of the new rule to the pair
     consisting of the id of the rule it replaces and the
     i_rhs_num *)
  adornments : Adornment.status list AdPredMap.t;
  (* a map to keep track of the adornments of the
     predicates in a given rule with a given adornment
     (avoids parsing the predicate symbol) *)
  pred_map : ASPred.pred_id AdornmentTrie.t ASPred.PredIdMap.t;
      (* map from original predicate ids to adornments to id of the
         corresponding unique binding predicate *)
}

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) ->
      (* The current node is a [Goal] node, hence it will generate a
         predicate at position [r_n.position+1] in the rule *)
      (* Find an id (possibly create one) for this goal *)
      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
      (* We need to recover the argument characteristics from the rule
         being processed *)
      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
      (* Record the mapping from [new_body_pred] to [body_pred] *)
      let new_unadorned_map =
        ASPred.(PredIdMap.add new_goal_id goal_pred.p_id data_acc.unadorned_map)
      in
      (* First update the program with the new predicate table *)
      let new_prog =
        { data_acc.adorned_prog with ASProg.pred_table = new_table }
      in
      if is_intensional then
        (* This new adorned predicate has to be added to the
           intensional predicates of the new program *)
        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 ->
      (* This rule node is going to be processed recursively on each of its successor nodes *)
      (* TODO: tail recursion is possible because a rule node has 0 or 2 successors *)
      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 _ ->
          (* If it's a rule node, there is nothing to do. We only
             consider goals *)
          l_data
      | Rgg.Goal (head_pred_sym, _)
        when not ASPred.(PredIds.mem head_pred_sym.p_id prog.ASProg.i_preds) ->
          (* If the goal node is extensional, there is nothing to do
             either. It will be dealt with when constructing the rules
             for intensional predicates *)
          l_data
      | Rgg.Goal (head_pred, head_adornment) ->
          (* We are dealing with an intensional predicate.*)

          (* We can generate a new id and a new symbol table for the
             adorned head *)
          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

          (* We then check all successors of this node in order to find
             those corresponding to rules it is a head of *)
          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 ->
                  (* If the successor is a rule node with a position
                     different from 0, then the goal g is not the head
                     of the rule r_n, so it is bypassed *)
                  l_acc
              | Rgg.Rule r_n ->
                  (* The head predicate is assigned the parameters of the r_n to be processed *)
                  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

                  (* The rule node describes a rule the goal g is a head
                     of. We fetch the rhs following this node *)
                  let e_rhs, i_rhs, l_acc' =
                    get_rule_rhs ~from:r_n graph prog ([], [], l_acc)
                  in

                  (* Generate a new id for the rule *)
                  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
                  (* We sort the (pred,position) lists *)
                  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
                  (* TODO: Est-ce vraiment nécessaire *)
                  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

                  (* We add the rule to the program *)
                  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;
    }
OCaml

Innovation. Community. Security.