grew_rule.ml 32.7 KB
Newer Older
pj2m's avatar
pj2m committed
1
open Log
bguillaum's avatar
bguillaum committed
2
open Printf
pj2m's avatar
pj2m committed
3

bguillaum's avatar
bguillaum committed
4 5
open Grew_utils
open Grew_ast
pj2m's avatar
pj2m committed
6
open Grew_edge
bguillaum's avatar
bguillaum committed
7
open Grew_fs
pj2m's avatar
pj2m committed
8
open Grew_node
bguillaum's avatar
bguillaum committed
9 10
open Grew_command
open Grew_graph
pj2m's avatar
pj2m committed
11

12
(* ================================================================================ *)
pj2m's avatar
pj2m committed
13 14
module Instance = struct
  type t = {
15
      graph: G_graph.t;
pj2m's avatar
pj2m committed
16 17
      commands: Command.h list;
      rules: string list;
bguillaum's avatar
bguillaum committed
18
      big_step: Grew_types.big_step option;
pj2m's avatar
pj2m committed
19 20
    }

21
  let empty = {graph = G_graph.empty; rules=[]; commands=[]; big_step=None;}
pj2m's avatar
pj2m committed
22

bguillaum's avatar
bguillaum committed
23
  let from_graph g = {empty with graph = g}
pj2m's avatar
pj2m committed
24

bguillaum's avatar
bguillaum committed
25
  let build gr_ast =
26
    let graph = G_graph.build gr_ast.Ast.nodes gr_ast.Ast.edges in
27
    { empty with graph = graph }
pj2m's avatar
pj2m committed
28

bguillaum's avatar
bguillaum committed
29
  let of_conll ?loc lines =
bguillaum's avatar
bguillaum committed
30
    { empty with graph = G_graph.of_conll ?loc lines }
bguillaum's avatar
bguillaum committed
31

bguillaum's avatar
bguillaum committed
32
  let rev_steps t =
pj2m's avatar
pj2m committed
33 34 35 36 37 38 39 40
    { t with big_step = match t.big_step with
    | None -> None
    | Some bs -> Some {bs with Grew_types.small_step = List.rev bs.Grew_types.small_step }
    }

  let clear t = {empty with graph = t.graph } (* FIXME: normalization of node ids ??? *)
  let get_graph t = t.graph

41
  (* comparison is done on the list of commands *)
pj2m's avatar
pj2m committed
42 43 44
  (* only graph rewrited from the same init graph can be "compared" *)
  let compare t1 t2 = Pervasives.compare t1.commands t2.commands

45 46
  let to_gr t = G_graph.to_gr t.graph

bguillaum's avatar
bguillaum committed
47
  let save_dot_png ?main_feat base t =
48 49
    ignore (Grew_utils.png_file_from_dot (G_graph.to_dot ?main_feat t.graph) (base^".png"))

pj2m's avatar
pj2m committed
50
IFDEF DEP2PICT THEN
51 52 53 54
  let save_dep_png ?main_feat base t =
    ignore (Dep2pict.Dep2pict.fromDepStringToPng (G_graph.to_dep ?main_feat t.graph) (base^".png"))
ELSE
  let save_dep_png ?main_feat base t = ()
pj2m's avatar
pj2m committed
55
ENDIF
56
end (* module Instance *)
pj2m's avatar
pj2m committed
57 58

module Instance_set = Set.Make (Instance)
59
(* ================================================================================ *)
pj2m's avatar
pj2m committed
60

bguillaum's avatar
bguillaum committed
61
module Rule = struct
bguillaum's avatar
bguillaum committed
62
  (* the [pid] type is used for pattern identifier *)
63
  type pid = Pid.t
bguillaum's avatar
bguillaum committed
64

bguillaum's avatar
bguillaum committed
65
  (* the [gid] type is used for graph identifier *)
66
  type gid = Gid.t
67

bguillaum's avatar
bguillaum committed
68
  (* the rewriting depth is bounded to stop rewriting when the system is not terminating *)
69
  let max_depth = ref 500
pj2m's avatar
pj2m committed
70

71
  type const =
bguillaum's avatar
bguillaum committed
72
    | Cst_out of pid * P_edge.t
73
    | Cst_in of pid * P_edge.t
74
    | Feature_eq of pid * string * pid * string
75
    | Filter of pid * P_fs.t (* used when a without impose a fs on a node defined by the match pattern *)
pj2m's avatar
pj2m committed
76

bguillaum's avatar
bguillaum committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90
  let build_pos_constraint ?locals pos_table const =
    let pid_of_name loc node_name = Pid.Pos (Id.build ~loc node_name pos_table) in
    match const with
      | (Ast.Start (node_name, labels), loc) ->
        Cst_out (pid_of_name loc node_name, P_edge.make ?locals labels)
      | (Ast.Cst_out node_name, loc) ->
        Cst_out (pid_of_name loc node_name, P_edge.all)
      | (Ast.End (node_name, labels),loc) ->
        Cst_in (pid_of_name loc node_name, P_edge.make ?locals labels)
      | (Ast.Cst_in node_name, loc) ->
        Cst_in (pid_of_name loc node_name, P_edge.all)
      | (Ast.Feature_eq ((node_name1, feat_name1), (node_name2, feat_name2)), loc) ->
        Feature_eq (pid_of_name loc node_name1, feat_name1, pid_of_name loc node_name2, feat_name2)

bguillaum's avatar
bguillaum committed
91 92 93 94
  type pattern = {
      graph: P_graph.t;
      constraints: const list;
    }
pj2m's avatar
pj2m committed
95

96
  let build_pos_pattern ?pat_vars ?(locals=[||]) pattern_ast =
97
    let (graph, pos_table) =
bguillaum's avatar
bguillaum committed
98
      P_graph.build ?pat_vars ~locals pattern_ast.Ast.pat_nodes pattern_ast.Ast.pat_edges in
pj2m's avatar
pj2m committed
99
    (
bguillaum's avatar
bguillaum committed
100 101
      {
        graph = graph;
102
        constraints = List.map (build_pos_constraint ~locals pos_table) pattern_ast.Ast.pat_const
bguillaum's avatar
bguillaum committed
103 104
      },
      pos_table
pj2m's avatar
pj2m committed
105 106
    )

bguillaum's avatar
bguillaum committed
107
  (* the neg part *)
pj2m's avatar
pj2m committed
108
  let build_neg_constraint ?locals pos_table neg_table const =
bguillaum's avatar
bguillaum committed
109 110 111 112
    let pid_of_name loc node_name =
      match Id.build_opt node_name pos_table with
        | Some i -> Pid.Pos i
        | None -> Pid.Neg (Id.build ~loc node_name neg_table) in
pj2m's avatar
pj2m committed
113
    match const with
bguillaum's avatar
bguillaum committed
114 115 116 117 118 119 120 121 122 123
      | (Ast.Start (node_name, labels),loc) ->
        Cst_out (pid_of_name loc node_name, P_edge.make ?locals labels)
      | (Ast.Cst_out node_name, loc) ->
        Cst_out (pid_of_name loc node_name, P_edge.all)
      | (Ast.End (node_name, labels),loc) ->
        Cst_in (pid_of_name loc node_name, P_edge.make ?locals labels)
      | (Ast.Cst_in node_name, loc) ->
        Cst_in (pid_of_name loc node_name, P_edge.all)
      | (Ast.Feature_eq ((node_name1, feat_name1), (node_name2, feat_name2)), loc) ->
        Feature_eq (pid_of_name loc node_name1, feat_name1, pid_of_name loc node_name2, feat_name2)
pj2m's avatar
pj2m committed
124

125
  let build_neg_pattern ?(locals=[||]) pos_table pattern_ast =
pj2m's avatar
pj2m committed
126
    let (extension, neg_table) =
127
      P_graph.build_extension ~locals pos_table pattern_ast.Ast.pat_nodes pattern_ast.Ast.pat_edges in
128
    let filters = Pid_map.fold (fun id node acc -> Filter (id, P_node.get_fs node) :: acc) extension.P_graph.old_map [] in
pj2m's avatar
pj2m committed
129
    {
bguillaum's avatar
bguillaum committed
130 131 132
      graph = extension.P_graph.ext_map;
      constraints = filters @ List.map (build_neg_constraint ~locals pos_table neg_table) pattern_ast.Ast.pat_const ;
    }
pj2m's avatar
pj2m committed
133

134
  let get_edge_ids pattern =
135
    Pid_map.fold
bguillaum's avatar
bguillaum committed
136 137
      (fun _ node acc ->
        Massoc_pid.fold
138 139 140
          (fun acc2 _ edge -> match P_edge.get_id edge with None -> acc2 | Some id -> id::acc2)
          acc (P_node.get_next node)
      ) pattern.graph []
bguillaum's avatar
bguillaum committed
141

pj2m's avatar
pj2m committed
142 143 144 145 146
  type t = {
      name: string;
      pos: pattern;
      neg: pattern list;
      commands: Command.t list;
147
      param: Lex_par.t option;
148
      param_names: (string list * string list);
bguillaum's avatar
bguillaum committed
149
      loc: Loc.t;
pj2m's avatar
pj2m committed
150 151
    }

bguillaum's avatar
bguillaum committed
152 153
  let get_name t = t.name

154
  let get_loc t = t.loc
pj2m's avatar
pj2m committed
155

156 157 158 159
  let to_dep t =
    let buff = Buffer.create 32 in
    bprintf buff "[GRAPH] { scale = 200; }\n";

bguillaum's avatar
bguillaum committed
160 161
    let nodes =
      Pid_map.fold
162
        (fun id node acc ->
bguillaum's avatar
bguillaum committed
163 164
          (node, sprintf "  N_%s { word=\"%s\"; subword=\"%s\"}"
            (Pid.to_id id) (P_node.get_name node) (P_fs.to_dep t.param_names (P_node.get_fs node))
165
          )
166 167 168
          :: acc
        ) t.pos.graph [] in

169
    (* nodes are sorted to appear in the same order in dep picture and in input file *)
170
    let sorted_nodes = List.sort (fun (n1,_) (n2,_) -> P_node.compare_pos n1 n2) nodes in
bguillaum's avatar
bguillaum committed
171

172 173 174 175 176 177 178 179
    bprintf buff "[WORDS] {\n";
    List.iter
      (fun (_, dep_line) -> bprintf buff "%s\n" dep_line
      ) sorted_nodes;

    List_.iteri
      (fun i cst ->
        match cst with
bguillaum's avatar
bguillaum committed
180
          | Cst_out _ | Cst_in _ -> bprintf buff "  C_%d { word=\"*\"}\n" i
181 182 183
          | _ -> ()
      ) t.pos.constraints;
    bprintf buff "}\n";
bguillaum's avatar
bguillaum committed
184

185
    bprintf buff "[EDGES] {\n";
bguillaum's avatar
bguillaum committed
186

187 188
    Pid_map.iter
      (fun id_src node ->
bguillaum's avatar
bguillaum committed
189
        Massoc_pid.iter
190
          (fun id_tar edge ->
bguillaum's avatar
bguillaum committed
191 192 193
            bprintf buff "  N_%s -> N_%s { label=\"%s\"}\n"
              (Pid.to_id id_src)
              (Pid.to_id id_tar)
194 195 196 197 198 199 200 201 202
              (P_edge.to_string edge)
          )
          (P_node.get_next node)
      ) t.pos.graph;

    List_.iteri
      (fun i cst ->
        match cst with
          | Cst_out (pid, edge) ->
bguillaum's avatar
bguillaum committed
203 204 205 206 207
            bprintf buff "  N_%s -> C_%d {label = \"%s\"; style=dot; bottom; color=green;}\n"
              (Pid.to_id pid) i (P_edge.to_string edge)
          | Cst_in (pid, edge) ->
            bprintf buff "  C_%d -> N_%s {label = \"%s\"; style=dot; bottom; color=green;}\n"
              i (Pid.to_id pid) (P_edge.to_string edge)
208 209 210 211
          | _ -> ()
      ) t.pos.constraints;
    bprintf buff "}\n";
    Buffer.contents buff
bguillaum's avatar
bguillaum committed
212

213 214
  let is_filter t = t.commands = []

bguillaum's avatar
bguillaum committed
215
  let build_commands ?param ?(locals=[||]) pos pos_table ast_commands =
216 217 218 219 220
    let known_node_ids = Array.to_list pos_table in
    let known_edge_ids = get_edge_ids pos in
    let rec loop (kni,kei) = function
      | [] -> []
      | ast_command :: tail ->
bguillaum's avatar
bguillaum committed
221
          let (command, (new_kni, new_kei)) =
bguillaum's avatar
bguillaum committed
222
            Command.build ?param (kni,kei) pos_table locals ast_command in
223 224 225
          command :: (loop (new_kni,new_kei) tail) in
    loop (known_node_ids, known_edge_ids) ast_commands

bguillaum's avatar
bguillaum committed
226 227 228 229 230 231 232 233 234 235 236 237
  let parse_vars loc vars =
    let rec parse_cmd_vars = function
      | [] -> []
      | x::t when x.[0] = '@' -> x :: parse_cmd_vars t
      | x::t -> Error.bug ~loc "Illegal feature definition '%s' in the lexical rule" x in
    let rec parse_pat_vars = function
      | [] -> ([],[])
      | x::t when x.[0] = '@' -> ([],parse_cmd_vars (x::t))
      | x::t when x.[0] = '$' -> let (pv,cv) = parse_pat_vars t in (x::pv, cv)
      | x::t -> Error.bug ~loc "Illegal feature definition '%s' in the lexical rule" x in
    parse_pat_vars vars

bguillaum's avatar
bguillaum committed
238 239 240
  let build ?(locals=[||]) dir rule_ast =

    let (param, pat_vars, cmd_vars) =
bguillaum's avatar
bguillaum committed
241 242
      match rule_ast.Ast.param with
      | None -> (None,[],[])
243
      | Some (files,vars) ->
bguillaum's avatar
bguillaum committed
244 245 246
          let (pat_vars, cmd_vars) = parse_vars rule_ast.Ast.rule_loc vars in
          let nb_pv = List.length pat_vars in
          let nb_cv = List.length cmd_vars in
247 248 249 250 251 252
          let param = List.fold_left
            (fun acc file ->
              Lex_par.append
                (Lex_par.load ~loc:rule_ast.Ast.rule_loc dir nb_pv nb_cv file)
                acc
            )
bguillaum's avatar
bguillaum committed
253 254
            (match rule_ast.Ast.lp with
              | None -> Lex_par.empty
255 256 257
              | Some lines -> Lex_par.from_lines ~loc:rule_ast.Ast.rule_loc nb_pv nb_cv lines
            )
            files in
258
          (Some param, pat_vars, cmd_vars) in
259

bguillaum's avatar
bguillaum committed
260
    let (pos, pos_table) = build_pos_pattern ~pat_vars ~locals rule_ast.Ast.pos_pattern in
pj2m's avatar
pj2m committed
261
    {
bguillaum's avatar
bguillaum committed
262 263 264 265 266 267 268 269 270
      name = rule_ast.Ast.rule_id;
      pos = pos;
      neg = List.map (fun pattern_ast -> build_neg_pattern ~locals pos_table pattern_ast) rule_ast.Ast.neg_patterns;
      commands = build_commands ~param:(pat_vars,cmd_vars) ~locals pos pos_table rule_ast.Ast.commands;
      loc = rule_ast.Ast.rule_loc;
      param = param;
      param_names = (pat_vars,cmd_vars)
    }

pj2m's avatar
pj2m committed
271
  type matching = {
bguillaum's avatar
bguillaum committed
272
      n_match: gid Pid_map.t;                   (* partial fct: pattern nodes |--> graph nodes *)
pj2m's avatar
pj2m committed
273 274
      e_match: (string*(gid*Label.t*gid)) list; (* edge matching: edge ident  |--> (src,label,tar) *)
      a_match: (gid*Label.t*gid) list;          (* anonymous edge mached *)
275
      m_param: Lex_par.t option;
pj2m's avatar
pj2m committed
276
    }
277

bguillaum's avatar
bguillaum committed
278
  let empty_matching param = { n_match = Pid_map.empty; e_match = []; a_match = []; m_param = param;}
279

pj2m's avatar
pj2m committed
280 281
  let e_comp (e1,_) (e2,_) = compare e1 e2

bguillaum's avatar
bguillaum committed
282
  let e_match_add ?pos edge_id matching =
pj2m's avatar
pj2m committed
283 284
    match List_.usort_insert ~compare:e_comp edge_id matching.e_match with
    | Some new_e_match -> { matching with e_match = new_e_match }
bguillaum's avatar
bguillaum committed
285
    | None -> Error.bug "The edge identifier '%s' is binded twice in the same pattern" (fst edge_id)
bguillaum's avatar
bguillaum committed
286

pj2m's avatar
pj2m committed
287 288
  let a_match_add edge matching = {matching with a_match = edge::matching.a_match }

bguillaum's avatar
bguillaum committed
289
  let up_deco matching =
290 291
    { G_deco.nodes = Pid_map.fold (fun _ gid acc -> gid::acc) matching.n_match [];
      G_deco.edges = List.fold_left (fun acc (_,edge) -> edge::acc) matching.a_match matching.e_match;
pj2m's avatar
pj2m committed
292 293
    }

bguillaum's avatar
bguillaum committed
294
  let find cnode ?loc (matching, created_nodes) =
pj2m's avatar
pj2m committed
295
    match cnode with
bguillaum's avatar
bguillaum committed
296
    | Command.Pid pid ->
297
        (try Pid_map.find pid matching.n_match
bguillaum's avatar
bguillaum committed
298 299 300
        with Not_found -> Error.bug ?loc "Inconsistent matching pid '%s' not found" (Pid.to_string pid))
    | Command.New name ->
        try List.assoc name created_nodes
301
        with Not_found -> Error.run ?loc "Identifier '%s' not found" name
bguillaum's avatar
bguillaum committed
302

pj2m's avatar
pj2m committed
303 304 305

  let down_deco (matching,created_nodes) commands =
    {
306
     G_deco.nodes = List.fold_left
pj2m's avatar
pj2m committed
307
       (fun acc -> function
308
         | (Command.UPDATE_FEAT (tar_cn,_,_),loc)
bguillaum's avatar
bguillaum committed
309
         | (Command.SHIFT_EDGE (_,tar_cn),loc) ->
310 311
             (find tar_cn (matching, created_nodes)) :: acc
         | _ -> acc
pj2m's avatar
pj2m committed
312
       ) [] commands;
313
     G_deco.edges = List.fold_left
bguillaum's avatar
bguillaum committed
314 315
       (fun acc -> function
         | (Command.ADD_EDGE (src_cn,tar_cn,edge),loc) ->
316
             (find src_cn (matching, created_nodes), edge, find tar_cn (matching, created_nodes)) :: acc
317
         | _ -> acc
pj2m's avatar
pj2m committed
318 319 320 321 322 323
       ) [] commands
   }

  exception Fail
(* ================================================================================ *)
  type partial = {
bguillaum's avatar
bguillaum committed
324
      sub: matching;
pj2m's avatar
pj2m committed
325
      unmatched_nodes: pid list;
326
      unmatched_edges: (pid * P_edge.t * pid) list;
pj2m's avatar
pj2m committed
327 328
      already_matched_gids: gid list; (* to ensure injectivity *)
      check: const list (* constraints to verify at the end of the matching *)
bguillaum's avatar
bguillaum committed
329 330 331 332
    }

        (* PREREQUISITES:
           - all partial matching have the same domain
333 334
           - the domain of the pattern P is the disjoint union of domain([sub]) and [unmatched_nodes]
         *)
pj2m's avatar
pj2m committed
335

bguillaum's avatar
bguillaum committed
336
  let init param pattern =
337
    let roots = P_graph.roots pattern.graph in
pj2m's avatar
pj2m committed
338

339
    let node_list = Pid_map.fold (fun pid _ acc -> pid::acc) pattern.graph [] in
pj2m's avatar
pj2m committed
340 341

    (* put all roots in the front of the list to speed up the algo *)
bguillaum's avatar
bguillaum committed
342
    let sorted_node_list =
pj2m's avatar
pj2m committed
343
      List.sort
344 345 346 347
        (fun n1 n2 -> match (List.mem n1 roots, List.mem n2 roots) with
        | true, false -> -1
        | false, true -> 1
        | _ -> 0) node_list in
bguillaum's avatar
bguillaum committed
348

bguillaum's avatar
bguillaum committed
349
    { sub = empty_matching param;
pj2m's avatar
pj2m committed
350 351 352 353 354 355
      unmatched_nodes = sorted_node_list;
      unmatched_edges = [];
      already_matched_gids = [];
      check = pattern.constraints;
    }

356 357 358
(* Ocaml < 3.12 doesn't have exists function for maps! *)
  exception True
  let gid_map_exists fct map =
bguillaum's avatar
bguillaum committed
359
    try
360 361 362 363 364 365
      Gid_map.iter (fun k v -> if fct k v then raise True) map;
      false
    with True -> true
(* Ocaml < 3.12 doesn't have exists function for maps! *)


bguillaum's avatar
bguillaum committed
366 367
  let fullfill graph matching = function
    | Cst_out (pid,edge) ->
368 369
        let gid = Pid_map.find pid matching.n_match in
        G_graph.edge_out graph gid edge
bguillaum's avatar
bguillaum committed
370
    | Cst_in (pid,edge) ->
371
        let gid = Pid_map.find pid matching.n_match in
372
        gid_map_exists (* should be Gid_map.exists with ocaml 3.12 *)
373
          (fun _ node ->
374
            List.exists (fun e -> P_edge.compatible edge e) (Massoc_gid.assoc gid (G_node.get_next node))
375
          ) graph.G_graph.map
376
    | Feature_eq (pid1, feat_name1, pid2, feat_name2) ->
377 378
        let gnode1 = Gid_map.find (Pid_map.find pid1 matching.n_match) graph.G_graph.map in
        let gnode2 = Gid_map.find (Pid_map.find pid2 matching.n_match) graph.G_graph.map in
379 380
        (match (G_fs.get_atom feat_name1 (G_node.get_fs gnode1),
                G_fs.get_atom feat_name2 (G_node.get_fs gnode2)
381
               ) with
bguillaum's avatar
bguillaum committed
382 383
        | Some fv1, Some fv2 when fv1 = fv2 -> true
        | _ -> false)
pj2m's avatar
pj2m committed
384
    | Filter (pid, fs) ->
385 386
        let gid = Pid_map.find pid matching.n_match in
        let gnode = Gid_map.find gid graph.G_graph.map in
387
        P_fs.filter fs (G_node.get_fs gnode)
pj2m's avatar
pj2m committed
388

bguillaum's avatar
bguillaum committed
389
  (* returns all extension of the partial input matching *)
390
  let rec extend_matching (positive,neg) (graph:G_graph.t) (partial:partial) =
pj2m's avatar
pj2m committed
391
    match (partial.unmatched_edges, partial.unmatched_nodes) with
bguillaum's avatar
bguillaum committed
392 393
    | [], [] ->
        if List.for_all (fun const -> fullfill graph partial.sub const) partial.check
394 395
        then [partial.sub, partial.already_matched_gids]
        else []
pj2m's avatar
pj2m committed
396
    | (src_pid, p_edge, tar_pid)::tail_ue, _ ->
397 398
        begin
          try (* is the tar already found in the matching ? *)
bguillaum's avatar
bguillaum committed
399
            let new_partials =
400 401 402
              let src_gid = Pid_map.find src_pid partial.sub.n_match in
              let tar_gid = Pid_map.find tar_pid partial.sub.n_match in
              let src_gnode = G_graph.find src_gid graph in
403
              let g_edges = Massoc_gid.assoc tar_gid (G_node.get_next src_gnode) in
bguillaum's avatar
bguillaum committed
404

405 406
              match P_edge.match_list p_edge g_edges with
              | P_edge.Fail -> (* no good edge in graph for this pattern edge -> stop here *)
407
                  []
408
              | P_edge.Ok label -> (* at least an edge in the graph fits the p_edge "constraint" -> go on *)
bguillaum's avatar
bguillaum committed
409
                  [ {partial with unmatched_edges = tail_ue; sub = a_match_add (src_gid,label,tar_gid) partial.sub} ]
410
              | P_edge.Binds (id,labels) -> (* n edges in the graph match the identified p_edge -> make copies of the [k] matchings (and returns n*k matchings) *)
bguillaum's avatar
bguillaum committed
411
                  List.map
412 413
                    (fun label ->
                      {partial with sub = e_match_add (id,(src_gid,label,tar_gid)) partial.sub; unmatched_edges = tail_ue }
bguillaum's avatar
bguillaum committed
414
                    ) labels
415 416 417
            in List_.flat_map (extend_matching (positive,neg) graph) new_partials
          with Not_found -> (* p_edge goes to an unmatched node *)
            let candidates = (* candidates (of type (gid, matching)) for m(tar_pid) = gid) with new partial matching m *)
bguillaum's avatar
bguillaum committed
418
              let (src_gid : Gid.t) = Pid_map.find src_pid partial.sub.n_match in
419
              let src_gnode = G_graph.find src_gid graph in
420
              Massoc_gid.fold
421
                (fun acc gid_next g_edge ->
422 423
                  match P_edge.match_ p_edge g_edge with
                  | P_edge.Fail -> (* g_edge does not fit, no new candidate *)
424
                      acc
425
                  | P_edge.Ok label -> (* g_edge fits with the same matching *)
bguillaum's avatar
bguillaum committed
426
                      (gid_next, a_match_add (src_gid, label, gid_next) partial.sub) :: acc
427
                  | P_edge.Binds (id,[label]) -> (* g_edge fits with an extended matching *)
428
                      (gid_next, e_match_add (id, (src_gid, label, gid_next)) partial.sub) :: acc
429 430
                  | _ -> Error.bug "P_edge.match_ must return exactly one label"
                ) [] (G_node.get_next src_gnode) in
431
            List_.flat_map
bguillaum's avatar
bguillaum committed
432
              (fun (gid_next, matching) ->
433 434 435 436
                extend_matching_from (positive,neg) graph tar_pid gid_next
                  {partial with sub=matching; unmatched_edges = tail_ue}
              ) candidates
        end
bguillaum's avatar
bguillaum committed
437 438
    | [], pid :: _ ->
        Gid_map.fold
439 440
          (fun gid _ acc ->
            (extend_matching_from (positive,neg) graph pid gid partial) @ acc
441
          ) graph.G_graph.map []
bguillaum's avatar
bguillaum committed
442 443

  and extend_matching_from (positive,neg) (graph:G_graph.t) pid (gid : Gid.t) partial =
pj2m's avatar
pj2m committed
444 445 446
    if List.mem gid partial.already_matched_gids
    then [] (* the required association pid -> gid is not injective *)
    else
bguillaum's avatar
bguillaum committed
447 448 449 450 451 452 453 454 455 456
      let p_node =
        try P_graph.find pid positive
        with Not_found ->
          try P_graph.find pid neg
          with Not_found -> Error.bug "[Grew_rule.extend_matching_from] cannot find node" in

      (* let p_node =  *)
      (*   if pid >= 0  *)
      (*   then try P_graph.find pid positive with Not_found -> failwith "POS" *)
      (*   else try P_graph.find pid neg with Not_found -> failwith "NEG" in *)
457
      let g_node = try G_graph.find gid graph with Not_found -> failwith "INS" in
bguillaum's avatar
bguillaum committed
458

bguillaum's avatar
bguillaum committed
459
      try
460 461 462

        let new_param = P_node.match_ ?param: partial.sub.m_param p_node g_node in

463
        (* add all out-edges from pid in pattern *)
bguillaum's avatar
bguillaum committed
464 465
        let new_unmatched_edges =
          Massoc_pid.fold
466
            (fun acc pid_next p_edge -> (pid, p_edge, pid_next) :: acc
467
            ) partial.unmatched_edges (P_node.get_next p_node) in
bguillaum's avatar
bguillaum committed
468 469

        let new_partial =
bguillaum's avatar
bguillaum committed
470
          { partial with
bguillaum's avatar
bguillaum committed
471
            unmatched_nodes = (try List_.rm pid partial.unmatched_nodes with Not_found -> failwith "List_.rm");
bguillaum's avatar
bguillaum committed
472 473 474 475
            unmatched_edges = new_unmatched_edges;
            already_matched_gids = gid :: partial.already_matched_gids;
            sub = {partial.sub with n_match = Pid_map.add pid gid partial.sub.n_match; m_param = new_param};
          } in
476
        extend_matching (positive,neg) graph new_partial
477
      with P_fs.Fail -> []
pj2m's avatar
pj2m committed
478 479

(* the exception below is added to handle unification failure in merge!! *)
480
  exception Command_execution_fail
pj2m's avatar
pj2m committed
481 482

(** [apply_command instance matching created_nodes command] returns [(new_instance, new_created_nodes)] *)
483 484 485 486
  let apply_command (command,loc) instance matching created_nodes =
    let node_find cnode = find ~loc cnode (matching, created_nodes) in

    match command with
bguillaum's avatar
bguillaum committed
487
    | Command.ADD_EDGE (src_cn,tar_cn,edge) ->
488 489 490
        let src_gid = node_find src_cn in
        let tar_gid = node_find tar_cn in
        begin
491
          match G_graph.add_edge instance.Instance.graph src_gid edge tar_gid with
bguillaum's avatar
bguillaum committed
492
          | Some new_graph ->
493
              (
bguillaum's avatar
bguillaum committed
494 495
               {instance with
                Instance.graph = new_graph;
496 497 498 499
                commands = List_.sort_insert (Command.H_ADD_EDGE (src_gid,tar_gid,edge)) instance.Instance.commands
              },
               created_nodes
              )
bguillaum's avatar
bguillaum committed
500
          | None ->
501
              Error.run "ADD_EDGE: the edge '%s' already exists %s" (G_edge.to_string edge) (Loc.to_string loc)
502 503
        end

bguillaum's avatar
bguillaum committed
504
    | Command.DEL_EDGE_EXPL (src_cn,tar_cn,edge) ->
505 506 507
        let src_gid = node_find src_cn in
        let tar_gid = node_find tar_cn in
        (
bguillaum's avatar
bguillaum committed
508 509
         {instance with
          Instance.graph = G_graph.del_edge loc instance.Instance.graph src_gid edge tar_gid;
510 511 512 513 514 515
          commands = List_.sort_insert (Command.H_DEL_EDGE_EXPL (src_gid,tar_gid,edge)) instance.Instance.commands
        },
         created_nodes
        )

    | Command.DEL_EDGE_NAME edge_ident ->
bguillaum's avatar
bguillaum committed
516 517
        let (src_gid,edge,tar_gid) =
          try List.assoc edge_ident matching.e_match
518 519
          with Not_found -> Error.bug "The edge identifier '%s' is undefined %s" edge_ident (Loc.to_string loc) in
        (
bguillaum's avatar
bguillaum committed
520 521
         {instance with
          Instance.graph = G_graph.del_edge ~edge_ident loc instance.Instance.graph src_gid edge tar_gid;
522 523 524
          commands = List_.sort_insert (Command.H_DEL_EDGE_EXPL (src_gid,tar_gid,edge)) instance.Instance.commands
        },
         created_nodes
bguillaum's avatar
bguillaum committed
525
        )
526

bguillaum's avatar
bguillaum committed
527
    | Command.DEL_NODE node_cn ->
528 529
        let node_gid = node_find node_cn in
        (
bguillaum's avatar
bguillaum committed
530
         {instance with
531
          Instance.graph = G_graph.del_node instance.Instance.graph node_gid;
532 533 534 535 536 537 538 539
          commands = List_.sort_insert (Command.H_DEL_NODE node_gid) instance.Instance.commands
        },
         created_nodes
        )

    | Command.MERGE_NODE (src_cn, tar_cn) ->
        let src_gid = node_find src_cn in
        let tar_gid = node_find tar_cn in
540
        (match G_graph.merge_node loc instance.Instance.graph src_gid tar_gid with
bguillaum's avatar
bguillaum committed
541
        | Some new_graph ->
542
            (
bguillaum's avatar
bguillaum committed
543
             {instance with
544 545 546 547 548 549 550
              Instance.graph = new_graph;
              commands = List_.sort_insert (Command.H_MERGE_NODE (src_gid,tar_gid)) instance.Instance.commands
            },
             created_nodes
            )
        | None -> raise Command_execution_fail
        )
bguillaum's avatar
bguillaum committed
551

552
    | Command.UPDATE_FEAT (tar_cn,tar_feat_name, item_list) ->
bguillaum's avatar
bguillaum committed
553
        let tar_gid = node_find tar_cn in
554 555
        let rule_items = List.map
            (function
bguillaum's avatar
bguillaum committed
556 557
              | Command.Feat (cnode, feat_name) -> Concat_item.Feat (node_find cnode, feat_name)
              | Command.String s -> Concat_item.String s
bguillaum's avatar
bguillaum committed
558
              | Command.Param_out index ->
bguillaum's avatar
bguillaum committed
559 560
                  (match matching.m_param with
                  | None -> Error.bug "Cannot apply a UPDATE_FEAT command without parameter"
bguillaum's avatar
bguillaum committed
561
                  | Some param -> Concat_item.String (Lex_par.get_command_value index param))
bguillaum's avatar
bguillaum committed
562
              | Command.Param_in index ->
bguillaum's avatar
bguillaum committed
563
                  (match matching.m_param with
564
                  | None -> Error.bug "Cannot apply a UPDATE_FEAT command without parameter"
bguillaum's avatar
bguillaum committed
565
                  | Some param -> Concat_item.String (Lex_par.get_param_value index param))
566
            ) item_list in
567

bguillaum's avatar
bguillaum committed
568
        let (new_graph, new_feature_value) =
569
          G_graph.update_feat ~loc instance.Instance.graph tar_gid tar_feat_name rule_items in
bguillaum's avatar
bguillaum committed
570
        (
571 572 573 574
         {instance with
          Instance.graph = new_graph;
          commands = List_.sort_insert
            (Command.H_UPDATE_FEAT (tar_gid,tar_feat_name,new_feature_value))
bguillaum's avatar
bguillaum committed
575 576 577
            instance.Instance.commands
        },
         created_nodes
578
        )
579 580 581 582

    | Command.DEL_FEAT (tar_cn,feat_name) ->
        let tar_gid = node_find tar_cn in
        (
bguillaum's avatar
bguillaum committed
583
         {instance with
584
          Instance.graph = G_graph.del_feat instance.Instance.graph tar_gid feat_name;
585 586 587
          commands = List_.sort_insert (Command.H_DEL_FEAT (tar_gid,feat_name)) instance.Instance.commands
        },
         created_nodes
bguillaum's avatar
bguillaum committed
588
        )
589 590

    | Command.NEW_NEIGHBOUR (created_name,edge,base_pid) ->
591 592
        let base_gid = Pid_map.find base_pid matching.n_match in
        let (new_gid,new_graph) = G_graph.add_neighbour loc instance.Instance.graph base_gid edge in
593
        (
bguillaum's avatar
bguillaum committed
594
         {instance with
595 596 597 598 599 600
          Instance.graph = new_graph;
          commands = List_.sort_insert (Command.H_NEW_NEIGHBOUR (created_name,edge,new_gid)) instance.Instance.commands
        },
         (created_name,new_gid) :: created_nodes
        )

601 602 603 604
    | Command.SHIFT_IN (src_cn,tar_cn) ->
        let src_gid = node_find src_cn in
        let tar_gid = node_find tar_cn in
        (
bguillaum's avatar
bguillaum committed
605 606
         {instance with
          Instance.graph = G_graph.shift_in loc instance.Instance.graph src_gid tar_gid;
607 608 609 610 611 612 613 614 615
          commands = List_.sort_insert (Command.H_SHIFT_IN (src_gid,tar_gid)) instance.Instance.commands
        },
         created_nodes
        )

    | Command.SHIFT_OUT (src_cn,tar_cn) ->
        let src_gid = node_find src_cn in
        let tar_gid = node_find tar_cn in
        (
bguillaum's avatar
bguillaum committed
616 617
         {instance with
          Instance.graph = G_graph.shift_out loc instance.Instance.graph src_gid tar_gid;
618 619 620 621 622
          commands = List_.sort_insert (Command.H_SHIFT_OUT (src_gid,tar_gid)) instance.Instance.commands
        },
         created_nodes
        )

bguillaum's avatar
bguillaum committed
623
    | Command.SHIFT_EDGE (src_cn,tar_cn) ->
624 625 626
        let src_gid = node_find src_cn in
        let tar_gid = node_find tar_cn in
        (
bguillaum's avatar
bguillaum committed
627 628
         {instance with
          Instance.graph = G_graph.shift_edges loc instance.Instance.graph src_gid tar_gid;
629 630 631 632
          commands = List_.sort_insert (Command.H_SHIFT_EDGE (src_gid,tar_gid)) instance.Instance.commands
        },
         created_nodes
        )
pj2m's avatar
pj2m committed
633

bguillaum's avatar
bguillaum committed
634
(** [apply_rule instance matching rule] returns a new instance after the application of the rule
pj2m's avatar
pj2m committed
635 636
    [Command_execution_fail] is raised if some merge unification fails
 *)
bguillaum's avatar
bguillaum committed
637
  let apply_rule instance matching rule =
pj2m's avatar
pj2m committed
638

bguillaum's avatar
bguillaum committed
639 640 641
    (* Timeout check *)
    (try Timeout.check () with Timeout.Stop -> Error.run "Time out");

642 643
    (* limit the rewriting depth to avoid looping rewriting *)
    begin
bguillaum's avatar
bguillaum committed
644
      if List.length instance.Instance.rules >= !max_depth
645 646
      then Error.run "Bound reached (when applying rule %s)" rule.name
    end;
bguillaum's avatar
bguillaum committed
647

648
    let (new_instance, created_nodes) =
bguillaum's avatar
bguillaum committed
649
      List.fold_left
650 651
        (fun (instance, created_nodes) command ->
          apply_command command instance matching created_nodes
bguillaum's avatar
bguillaum committed
652 653
        )
        (instance, [])
654 655 656
        rule.commands in

    let rule_app = {Grew_types.rule_name = rule.name; up = up_deco matching; down = down_deco (matching,created_nodes) rule.commands } in
pj2m's avatar
pj2m committed
657

bguillaum's avatar
bguillaum committed
658
    {new_instance with
659 660 661 662
     Instance.rules = rule.name :: new_instance.Instance.rules;
     big_step = match new_instance.Instance.big_step with
     | None -> Some { Grew_types.first = rule_app; small_step = [] }
     | Some bs -> Some { bs with Grew_types.small_step = (instance.Instance.graph, rule_app) :: bs.Grew_types.small_step }
bguillaum's avatar
bguillaum committed
663
   }
pj2m's avatar
pj2m committed
664 665 666

(*-----------------------------*)

bguillaum's avatar
bguillaum committed
667
  let update_partial pos_graph without (sub, already_matched_gids) =
668
    let neg_graph = without.graph in
bguillaum's avatar
bguillaum committed
669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688
    let unmatched_nodes =
      Pid_map.fold
        (fun pid _ acc -> match pid with Pid.Neg _ -> pid::acc | _ -> acc)
        neg_graph [] in
    let unmatched_edges =
      Pid_map.fold
        (fun pid node acc ->
          match pid with
            | Pid.Neg _ -> acc
            | Pid.Pos i ->
          (* if pid < 0  *)
          (* then acc *)
          (* else  *)
              Massoc_pid.fold
                (fun acc2 pid_next p_edge -> (pid, p_edge, pid_next) :: acc2)
                acc (P_node.get_next node)

            (* Massoc.fold_left  *)
            (*   (fun acc2 pid_next p_edge -> (pid, p_edge, pid_next) :: acc2) *)
            (*   acc (P_node.get_next node) *)
689
        ) neg_graph [] in
690 691 692 693 694 695 696
    {
     sub = sub;
     unmatched_nodes = unmatched_nodes;
     unmatched_edges = unmatched_edges;
     already_matched_gids = already_matched_gids;
     check = without.constraints;
   }
bguillaum's avatar
bguillaum committed
697

pj2m's avatar
pj2m committed
698

699 700 701
  let fulfill (pos_graph,neg_graph) graph new_partial_matching  =
    match extend_matching (pos_graph, neg_graph) graph new_partial_matching with
    | [] -> true (* the without pattern in not found -> OK *)
bguillaum's avatar
bguillaum committed
702
    | x -> false
pj2m's avatar
pj2m committed
703 704 705


(** [one_step instance rules] computes the list of one-step reduct with rules *)
706
  let one_step instance rules =
bguillaum's avatar
bguillaum committed
707 708
    List.fold_left
      (fun acc rule ->
709 710 711
        let pos_graph = rule.pos.graph in

        (* get the list of partial matching for positive part of the pattern *)
bguillaum's avatar
bguillaum committed
712 713 714 715
        let matching_list =
          extend_matching
            (pos_graph,P_graph.empty)
            instance.Instance.graph
bguillaum's avatar
bguillaum committed
716
            (init rule.param rule.pos) in
717 718 719 720

        let filtered_matching_list =
          List.filter
            (fun (sub, already_matched_gids) ->
bguillaum's avatar
bguillaum committed
721 722
              List.for_all
                (fun without ->
723 724 725 726 727
                  let neg_graph = without.graph in
                  let new_partial_matching = update_partial pos_graph without (sub, already_matched_gids) in
                  fulfill (pos_graph,neg_graph) instance.Instance.graph new_partial_matching
                ) rule.neg
            ) matching_list in
bguillaum's avatar
bguillaum committed
728 729 730 731

        List.fold_left
          (fun acc1 (matching,_) ->
            try (apply_rule instance matching rule) :: acc1
732 733
            with Command_execution_fail -> Printf.printf "******\n%!"; acc1
          ) acc filtered_matching_list
bguillaum's avatar
bguillaum committed
734
      ) [] rules
pj2m's avatar
pj2m committed
735 736

(** [conf_one_step instance rules] computes one Some (one-step reduct) with rules, None if no rule apply *)
737 738 739 740 741 742
  let rec conf_one_step (instance : Instance.t) = function
    | [] -> None
    | rule::rule_tail ->
        let pos_graph = rule.pos.graph in

        (* get the list of partial matching for positive part of the pattern *)
bguillaum's avatar
bguillaum committed
743 744 745 746
        let matching_list =
          extend_matching
            (pos_graph,P_graph.empty)
            instance.Instance.graph
bguillaum's avatar
bguillaum committed
747
            (init rule.param rule.pos) in
bguillaum's avatar
bguillaum committed
748 749

        try
750 751 752
          let (first_matching_where_all_witout_are_fulfilled,_) =
            List.find
              (fun (sub, already_matched_gids) ->
bguillaum's avatar
bguillaum committed
753 754
                List.for_all
                  (fun without ->
755 756 757 758 759 760 761
                    let neg_graph = without.graph in
                    let new_partial_matching = update_partial pos_graph without (sub, already_matched_gids) in
                    fulfill (pos_graph,neg_graph) instance.Instance.graph new_partial_matching
                  ) rule.neg
              ) matching_list in
          Some (apply_rule instance first_matching_where_all_witout_are_fulfilled rule)
        with Not_found -> (* try another rule *) conf_one_step instance rule_tail
pj2m's avatar
pj2m committed
762 763 764


(** filter nfs being equal *)
765
  let rec filter_equal_nfs nfs =
bguillaum's avatar
bguillaum committed
766
    Instance_set.fold
767 768 769 770 771
      (fun nf acc ->
        if Instance_set.exists (fun e -> G_graph.equals e.Instance.graph nf.Instance.graph) acc
        then acc
        else Instance_set.add nf acc
      ) nfs Instance_set.empty
bguillaum's avatar
bguillaum committed
772

pj2m's avatar
pj2m committed
773 774
(** normalize [t] according to the [rules]
 * [t] is a raw graph
775
 * Info about the commands applied on [t] are kept
pj2m's avatar
pj2m committed
776 777
 *)

778
  (* type: Instance.t -> t list -> Instance_set.t *)
779
  let normalize_instance modul_name instance rules =
bguillaum's avatar
bguillaum committed
780
    let rec loop to_do nf =
pj2m's avatar
pj2m committed
781
      if to_do = Instance_set.empty
782 783
      then nf
      else
bguillaum's avatar
bguillaum committed
784 785
        let (new_to_do,new_nf) =
          Instance_set.fold
786 787 788 789 790 791 792 793
            (fun v (to_do1,nf1) ->
              let step_of_v = one_step v rules in
              if step_of_v = [] (* nothing came out of v*)
              then (to_do1,Instance_set.add (Instance.rev_steps v) nf1)
              else (List.fold_left (fun acc v1 -> Instance_set.add v1 acc) to_do1 step_of_v,nf1)
            )
            to_do (Instance_set.empty,nf) in
        loop new_to_do new_nf in
bguillaum's avatar
bguillaum committed
794
    let nfs = loop (Instance_set.singleton instance) Instance_set.empty in
795
    let reduced_nfs = filter_equal_nfs nfs in
bguillaum's avatar
bguillaum committed
796

797 798
    let reduced_nfs_card = Instance_set.cardinal reduced_nfs in
    let nfs_card = Instance_set.cardinal nfs in
bguillaum's avatar
bguillaum committed
799
    if reduced_nfs_card < nfs_card
800 801 802
    then Log.fwarning "In module \"%s\", %d nf are produced, only %d different ones" modul_name nfs_card reduced_nfs_card;

    reduced_nfs
bguillaum's avatar
bguillaum committed
803

804 805 806 807 808 809 810
  (* [filter_instance instance filters] return a boolean:
     - true iff the instance does NOT match any pattern in [filters] *)
  let filter_instance filters instance =
    let rec loop = function
      | [] -> true (* no more filter to check *)
      | filter::filter_tail ->
          let pos_graph = filter.pos.graph in
bguillaum's avatar
bguillaum committed
811

812
          (* get the list of partial matching for positive part of the pattern *)
bguillaum's avatar
bguillaum committed
813 814 815 816
          let matching_list =
            extend_matching
              (pos_graph,P_graph.empty)
              instance.Instance.graph
817
              (init filter.param filter.pos) in
bguillaum's avatar
bguillaum committed
818

819 820
          if List.exists
              (fun (sub, already_matched_gids) ->
bguillaum's avatar
bguillaum committed
821 822
                List.for_all
                  (fun without ->
823 824 825 826 827 828 829 830 831 832
                    let neg_graph = without.graph in
                    let new_partial_matching = update_partial pos_graph without (sub, already_matched_gids) in
                    fulfill (pos_graph,neg_graph) instance.Instance.graph new_partial_matching
                  ) filter.neg
              ) matching_list
          then (* one of the matching can be extended *) false
          else loop filter_tail in
    loop filters


pj2m's avatar
pj2m committed
833

834 835 836 837 838
  let rec conf_normalize instance rules =
    match conf_one_step instance rules with
    | Some new_instance -> conf_normalize new_instance rules
    | None -> Instance.rev_steps instance

839
  let normalize modul_name ?(confluent=false) rules filters instance =
bguillaum's avatar
bguillaum committed
840
    Timeout.start ();
841 842 843
    if confluent
    then
      let output = conf_normalize instance rules in
bguillaum's avatar
bguillaum committed
844
      if filter_instance filters output
845 846 847
      then (Instance_set.singleton output, Instance_set.empty)
      else (Instance_set.empty, Instance_set.singleton output)
    else
bguillaum's avatar
bguillaum committed
848
      let output_set = normalize_instance modul_name instance rules in
849
      let (good_set, bad_set) = Instance_set.partition (filter_instance filters) output_set in
850
      (good_set, bad_set)
851

bguillaum's avatar
bguillaum committed
852
end (* module Rule *)