grew_grs.ml 24.4 KB
Newer Older
bguillaum's avatar
bguillaum committed
1
2
3
4
5
6
7
8
9
10
(**********************************************************************************)
(*    Libcaml-grew - a Graph Rewriting library dedicated to NLP applications      *)
(*                                                                                *)
(*    Copyright 2011-2013 Inria, Université de Lorraine                           *)
(*                                                                                *)
(*    Webpage: http://grew.loria.fr                                               *)
(*    License: CeCILL (see LICENSE folder or "http://www.cecill.info")            *)
(*    Authors: see AUTHORS file                                                   *)
(**********************************************************************************)

pj2m's avatar
pj2m committed
11
12
13
open Printf
open Log

14
open Grew_fs
bguillaum's avatar
bguillaum committed
15
open Grew_base
16
open Grew_types
bguillaum's avatar
bguillaum committed
17
open Grew_ast
18
open Grew_domain
19
open Grew_edge
bguillaum's avatar
bguillaum committed
20
21
22
open Grew_command
open Grew_graph
open Grew_rule
bguillaum's avatar
bguillaum committed
23
open Grew_loader
pj2m's avatar
pj2m committed
24

bguillaum's avatar
bguillaum committed
25
(* ================================================================================ *)
pj2m's avatar
pj2m committed
26
27
module Rewrite_history = struct
  type t = {
28
29
30
31
32
    instance: Instance.t;
    module_name: string;
    good_nf: t list;
    bad_nf: Instance.t list;
  }
pj2m's avatar
pj2m committed
33

34
35
36
37
38
  let rec get_graphs = function
    | { good_nf = []; bad_nf = []; instance } -> [instance.Instance.graph]
    | { good_nf = [] } -> []
    | { good_nf = l} -> List_.flat_map get_graphs l

39
  let rec is_empty t =
bguillaum's avatar
bguillaum committed
40
    (t.instance.Instance.rules = []) && List.for_all is_empty t.good_nf
bguillaum's avatar
bguillaum committed
41
42

  let rec num_sol = function
43
44
    | { good_nf = []; bad_nf = [] } -> 1
    | { good_nf = [] } -> 0 (* dead branch *)
bguillaum's avatar
bguillaum committed
45
    | { good_nf = l} -> List.fold_left (fun acc t -> acc + (num_sol t)) 0 l
46

bguillaum's avatar
bguillaum committed
47
  let save_nfs ?domain ?filter ?main_feat ~dot base_name t =
48
    let rec loop file_name rules t =
49
      match (t.good_nf, t.bad_nf) with
bguillaum's avatar
bguillaum committed
50
51
        | [],[] when dot -> Instance.save_dot_png ?domain ?filter ?main_feat file_name t.instance; [rules, file_name]
        | [],[] -> ignore (Instance.save_dep_png ?domain ?filter ?main_feat file_name t.instance); [rules, file_name]
52
53
        | [],_ -> []
        | l, _ ->
54
          List_.foldi_left
55
            (fun i acc son ->
56
              (* Instance.save_dep_png ?main_feat (sprintf "%s_%d" file_name i) son.instance; *)
57
58
59
60
              let nfs = loop
                (sprintf "%s_%d" file_name i)
                (rules @ [t.module_name, son.instance.Instance.rules])
                son in
61
62
              nfs @ acc
            )
bguillaum's avatar
bguillaum committed
63
64
            [] l in
    loop base_name [] t
65

bguillaum's avatar
bguillaum committed
66
  let save_gr ?domain base t =
67
68
    let rec loop file_name t =
      match (t.good_nf, t.bad_nf) with
bguillaum's avatar
bguillaum committed
69
        | [],[] -> File.write (Instance.to_gr ?domain t.instance) (file_name^".gr")
70
        | l, _ -> List.iteri (fun i son -> loop (sprintf "%s_%d" file_name i) son) l
71
72
    in loop base t

bguillaum's avatar
bguillaum committed
73
  let save_conll ?domain base t =
bguillaum's avatar
bguillaum committed
74
75
    let rec loop file_name t =
      match (t.good_nf, t.bad_nf) with
bguillaum's avatar
bguillaum committed
76
        | [],[] -> File.write (Instance.to_conll_string ?domain t.instance) (file_name^".conll")
77
        | l, _ -> List.iteri (fun i son -> loop (sprintf "%s_%d" file_name i) son) l
bguillaum's avatar
bguillaum committed
78
79
    in loop base t

bguillaum's avatar
bguillaum committed
80
  let save_full_conll ?domain base t =
81
82
83
    let cpt = ref 0 in
    let rec loop t =
      match (t.good_nf, t.bad_nf) with
Bruno Guillaume's avatar
Bruno Guillaume committed
84
        | [],[] ->
bguillaum's avatar
bguillaum committed
85
          File.write (Instance.to_conll_string ?domain t.instance) (sprintf "%s__%d.conll" base !cpt);
86
87
          incr cpt
        | l, _ -> List.iter loop l
88
    in loop t; !cpt
89

90
  (* suppose that all modules are confluent and produced exacly one normal form *)
bguillaum's avatar
bguillaum committed
91
  let save_det_gr ?domain base t =
92
93
    let rec loop t =
      match (t.good_nf, t.bad_nf) with
bguillaum's avatar
bguillaum committed
94
        | [],[] -> File.write (Instance.to_gr ?domain t.instance) (base^".gr")
95
        | [one], [] -> loop one
96
        | _ -> Error.run "[save_det_gr] Not a single rewriting"
97
    in loop t
bguillaum's avatar
bguillaum committed
98

bguillaum's avatar
bguillaum committed
99
  let save_annot ?domain out_dir base_name t =
100
    List.mapi
bguillaum's avatar
bguillaum committed
101
102
103
104
105
      (fun i alts ->
        match alts.good_nf with
      | [alt_1; alt_2] ->
        let a = sprintf "%s_%d_A" base_name i in
        let b = sprintf "%s_%d_B" base_name i in
bguillaum's avatar
bguillaum committed
106
107
        let hpa = Instance.save_dep_svg ?domain (Filename.concat out_dir a) alt_1.instance in
        let hpb = Instance.save_dep_svg ?domain (Filename.concat out_dir b) alt_2.instance in
bguillaum's avatar
bguillaum committed
108
109
110
        let (afn,apos) = G_graph.get_annot_info alt_1.instance.Instance.graph
        and (bfn,bpos) = G_graph.get_annot_info alt_2.instance.Instance.graph in
        (base_name,i,(afn,apos),(bfn,bpos),(hpa,hpb))
bguillaum's avatar
bguillaum committed
111
112
113
      | _ -> Error.run "Not two alternatives in an annotation rewriting in %s" base_name
      ) t.good_nf

bguillaum's avatar
bguillaum committed
114
  let save_det_conll ?domain ?header base t =
bguillaum's avatar
bguillaum committed
115
116
    let rec loop t =
      match (t.good_nf, t.bad_nf) with
117
118
119
        | ([],[]) ->
          let output =
            match header with
bguillaum's avatar
bguillaum committed
120
121
              | Some h -> sprintf "%% %s\n%s" h (Instance.to_conll_string ?domain t.instance)
              | None -> Instance.to_conll_string ?domain t.instance in
122
123
          File.write output (base^".conll")
        | ([one], []) -> loop one
124
        | _ -> Error.run "[save_det_conll] Not a single rewriting"
bguillaum's avatar
bguillaum committed
125
126
    in loop t

bguillaum's avatar
bguillaum committed
127
  let det_dep_string ?domain t =
bguillaum's avatar
bguillaum committed
128
129
130
131
    let rec loop t =
      match (t.good_nf, t.bad_nf) with
        | [],[] ->
          let graph = t.instance.Instance.graph in
bguillaum's avatar
bguillaum committed
132
          Some (G_graph.to_dep ?domain graph)
bguillaum's avatar
bguillaum committed
133
        | [one], [] -> loop one
bguillaum's avatar
bguillaum committed
134
        | _ -> None
bguillaum's avatar
bguillaum committed
135
    in loop t
bguillaum's avatar
bguillaum committed
136

bguillaum's avatar
bguillaum committed
137
  let conll_dep_string ?domain ?(keep_empty_rh=false) t =
bguillaum's avatar
bguillaum committed
138
139
140
141
142
143
144
    if (not keep_empty_rh) && is_empty t
    then None
    else
      let rec loop t =
        match (t.good_nf, t.bad_nf) with
          | [],[] ->
            let graph = t.instance.Instance.graph in
bguillaum's avatar
bguillaum committed
145
            Some (G_graph.to_conll_string ?domain graph)
bguillaum's avatar
bguillaum committed
146
147
148
          | [one], [] -> loop one
          | _ -> None
      in loop t
149
end (* module Rewrite_history *)
pj2m's avatar
pj2m committed
150

bguillaum's avatar
bguillaum committed
151
(* ================================================================================ *)
pj2m's avatar
pj2m committed
152
153
module Modul = struct
  type t = {
154
    name: string;
155
    local_labels: (string * string list) array;
156
157
158
159
160
    rules: Rule.t list;
    filters: Rule.t list;
    confluent: bool;
    loc: Loc.t;
  }
pj2m's avatar
pj2m committed
161

Bruno Guillaume's avatar
Bruno Guillaume committed
162
163
164
165
166
167
168
  let to_json ?domain t =
    `Assoc [
      ("module_name", `String t.name);
      ("confluent", `Bool t.confluent);
      ("rules", `List (List.map (Rule.to_json ?domain) t.rules));
    ]

169
170
171
172
  let check t =
    (* check for duplicate rules *)
    let rec loop already_defined = function
      | [] -> ()
173
174
      | r::_ when List.mem (Rule.get_name r) already_defined ->
        Error.build ~loc:(Rule.get_loc r) "Rule '%s' is defined twice in the same module" (Rule.get_name r)
175
176
      | r::tail -> loop ((Rule.get_name r) :: already_defined) tail in
    loop [] t.rules
pj2m's avatar
pj2m committed
177

bguillaum's avatar
bguillaum committed
178
  let build ?domain ast_module =
179
180
    let locals = Array.of_list ast_module.Ast.local_labels in
    Array.sort compare locals;
bguillaum's avatar
bguillaum committed
181
    let rules_or_filters = List.map (Rule.build ?domain ~locals ast_module.Ast.mod_dir) ast_module.Ast.rules in
182
183
    let (filters, rules) = List.partition Rule.is_filter rules_or_filters in
    let modul =
184
      {
185
186
        name = ast_module.Ast.module_id;
        local_labels = locals;
187
188
        rules;
        filters;
189
190
191
        confluent = ast_module.Ast.confluent;
        loc = ast_module.Ast.mod_loc;
      } in
192
    check modul; modul
193
end (* module Modul *)
194

bguillaum's avatar
bguillaum committed
195
(* ================================================================================ *)
pj2m's avatar
pj2m committed
196
module Grs = struct
197

pj2m's avatar
pj2m committed
198
  type t = {
bguillaum's avatar
bguillaum committed
199
    domain: Domain.t option;
200
    modules: Modul.t list;       (* the ordered list of modules used from rewriting *)
201
    strategies: Ast.strategy list;
bguillaum's avatar
bguillaum committed
202
203
    filename: string;
    ast: Ast.grs;
204
205
  }

206
  let to_json t = `List (List.map (Modul.to_json ?domain:t.domain) t.modules)
Bruno Guillaume's avatar
Bruno Guillaume committed
207

bguillaum's avatar
bguillaum committed
208
  let get_modules t = t.modules
bguillaum's avatar
bguillaum committed
209
210
  let get_ast t = t.ast
  let get_filename t = t.filename
bguillaum's avatar
bguillaum committed
211

212
  let get_domain t = t.domain
213

214
  let sequence_names t = List.map (fun s -> s.Ast.strat_name) t.strategies
bguillaum's avatar
bguillaum committed
215
216

  let empty = {domain=None; modules=[]; strategies=[]; ast=Ast.empty_grs; filename=""; }
pj2m's avatar
pj2m committed
217

Bruno Guillaume's avatar
Bruno Guillaume committed
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
  let check_strategy strat t =
    let rec loop = function
    | Ast.Ref name ->
      (if not (List.exists (fun m -> name = m.Modul.name) t.modules)
      then Error.build ~loc:strat.Ast.strat_loc "In sequence '%s' definition, module '%s' undefined" strat.Ast.strat_name name)
    | Ast.Seq sd_list -> List.iter loop sd_list
    | Ast.Plus sd_list -> List.iter loop sd_list
    | Ast.Star sd -> loop sd
    | Ast.Bang sd -> loop sd
    | Ast.Pick sd -> loop sd
    | Ast.Try sd -> loop sd
    | Ast.Sequence name_list ->
      List.iter (fun name ->
        if not (List.exists (fun m -> name = m.Modul.name) t.modules)
        then Error.build ~loc:strat.Ast.strat_loc "In sequence '%s' definition, module '%s' undefined" strat.Ast.strat_name name
      ) name_list
    in loop strat.Ast.strat_def

236
237
238
239
  let check t =
    (* check for duplicate modules *)
    let rec loop already_defined = function
      | [] -> ()
240
241
      | m::_ when List.mem m.Modul.name already_defined ->
        Error.build ~loc:m.Modul.loc "Module '%s' is defined twice" m.Modul.name
242
243
244
      | m::tail -> loop (m.Modul.name :: already_defined) tail in
    loop [] t.modules;

bguillaum's avatar
bguillaum committed
245
    (* check for duplicate strategies *)
246
247
    let rec loop already_defined = function
      | [] -> ()
248
249
250
      | s::_ when List.mem s.Ast.strat_name already_defined ->
        Error.build ~loc:s.Ast.strat_loc "Sequence '%s' is defined twice" s.Ast.strat_name
      | s::tail -> loop (s.Ast.strat_name :: already_defined) tail in
Bruno Guillaume's avatar
Bruno Guillaume committed
251
252
253
254
255
256
257
258
    loop [] t.strategies;

    (* check for undefined module or strategy *)
    List.iter (fun strat ->
      check_strategy strat t
    ) t.strategies


259

bguillaum's avatar
bguillaum committed
260
261
  let domain_build ast_domain =
    Domain.build
262
263
264
      (Label_domain.build ast_domain.Ast.label_domain)
      (Feature_domain.build ast_domain.Ast.feature_domain)

bguillaum's avatar
bguillaum committed
265
  let build filename =
bguillaum's avatar
bguillaum committed
266
    let ast = Loader.grs filename in
bguillaum's avatar
bguillaum committed
267
    let domain = match ast.Ast.domain with None -> None | Some ast_dom -> Some (domain_build ast_dom) in
bguillaum's avatar
bguillaum committed
268
    let modules = List.map (Modul.build ?domain) ast.Ast.modules in
bguillaum's avatar
bguillaum committed
269
    let grs = {domain; strategies = ast.Ast.strategies; modules; ast; filename} in
270
271
    check grs;
    grs
pj2m's avatar
pj2m committed
272

273
274
  (* ---------------------------------------------------------------------------------------------------- *)
  let rewrite grs strategy_name graph =
275
276
277
278
279
280
    let strategy =
      try List.find (fun s -> s.Ast.strat_name = strategy_name) grs.strategies
      with Not_found ->
        Error.run "[rewrite] Undefined stategy \"%s\"\nAvailable stategies: %s"
        strategy_name
        (String.concat "; " (List.map (fun s -> s.Ast.strat_name) grs.strategies)) in
bguillaum's avatar
bguillaum committed
281

282
    let rec old_loop instance module_list =
283
      match module_list with
284
285
286
287
288
      | [] -> {Rewrite_history.instance = instance; module_name = ""; good_nf = []; bad_nf = []; }
      | module_name :: tail ->
         let next =
           try List.find (fun m -> m.Modul.name=module_name) grs.modules
           with Not_found -> Log.fcritical "No module named '%s'" module_name in
289
290
        let (good_set, bad_set) =
          Rule.normalize
bguillaum's avatar
bguillaum committed
291
            ?domain: grs.domain
292
293
294
295
            next.Modul.name
            ~confluent: next.Modul.confluent
            next.Modul.rules
            next.Modul.filters
296
            (Instance.refresh instance) in
297
298
299
300
301
        let good_list = Instance_set.elements good_set
        and bad_list = Instance_set.elements bad_set in
        {
          Rewrite_history.instance = instance;
          module_name = next.Modul.name;
302
          good_nf = List.map (fun i -> old_loop i tail) good_list;
303
304
305
          bad_nf = bad_list;
        } in

306
307
308
    let loop instance def =
      match def with

309
      | Ast.Sequence module_list -> old_loop instance module_list
310
311
      | _ -> failwith "Not yet implemented" in

312
    loop (Instance.from_graph graph) (strategy.Ast.strat_def)
313

314
  (* [new_style grs module_list] return an equivalent strategy expressed with Seq, Pick and Star *)
315
  let new_style grs module_list =
316
    Ast.Seq
317
318
319
320
      (List.map
        (fun module_name ->
           let modul =
           try List.find (fun m -> m.Modul.name=module_name) grs.modules
321
           with Not_found -> Error.build "No module named '%s'" module_name in
322
           if modul.Modul.confluent
323
           then Ast.Pick (Ast.Star (Ast.Ref module_name))
324
           else Ast.Star (Ast.Ref module_name)
325
326
327
328
329
330
331
        ) module_list
      )

  (* [one_rewrite grs strat inst] tries to rewrite deterministically [inst] with [strat] defined in [grs] *)
  let one_rewrite grs strat inst =
    let rec loop inst = function
    (* name can refer to another strategy def or to a module *)
332
    | Ast.Ref name ->
333
334
      begin
        try
335
336
          let sub_strat = List.find (fun s -> s.Ast.strat_name = name) grs.strategies in
          loop inst sub_strat.Ast.strat_def
337
338
339
        with Not_found ->
          let modul =
            try List.find (fun m -> m.Modul.name=name) grs.modules
340
            with Not_found -> Error.build "No module or strategy named '%s'" name in
341
342
343
          Rule.conf_one_step ?domain: grs.domain name inst modul.Modul.rules
      end
    (* Union of strategies *)
344
345
    | Ast.Plus [] -> None (* the list can be empty in a recursive call! *)
    | Ast.Plus (head::tail) ->
346
347
348
      begin
        match loop inst head with
        | Some new_inst -> Some new_inst
349
        | None -> loop inst (Ast.Plus tail)
350
351
      end
    (* Sequence of strategies *)
352
353
354
    | Ast.Seq [] -> Log.fcritical "Empty sequence in strategy definition"
    | Ast.Seq [one] -> loop inst one
    | Ast.Seq (head::tail) ->
355
356
      begin
        match loop inst head with
357
        | Some new_inst -> loop new_inst (Ast.Seq tail)
358
359
360
        | None -> None
      end
    (* Interation of a strategy *)
361
    | Ast.Star sub_strat ->
362
363
364
      begin
        match loop inst sub_strat with
        | None -> Some inst
365
        | Some new_inst -> loop new_inst (Ast.Star sub_strat)
366
      end
367
368
369
370
371
372
373
374
375
376
377
    (* Pick *)
    | Ast.Pick sub_strat -> loop inst sub_strat
    (* Bang *)
    | Ast.Bang sub_strat -> loop inst (Ast.Star sub_strat)
    (* Try *)
    | Ast.Try sub_strat ->
      begin
        match loop inst sub_strat with
        | None -> Some inst
        | Some new_inst -> Some new_inst
      end
378
    (* Old style seq definition *)
379
    | Ast.Sequence module_list -> loop inst (new_style grs module_list) in
380
381
382
383
384
385
    loop inst strat


  let simple_rewrite grs strat_desc graph =
    let rec loop inst = function
    (* name can refer to another strategy def or to a module *)
386
    | Ast.Ref name ->
387
388
      begin
        try
389
390
          let sub_strat = List.find (fun s -> s.Ast.strat_name = name) grs.strategies in
          loop inst sub_strat.Ast.strat_def
391
392
393
        with Not_found ->
          let modul =
            try List.find (fun m -> m.Modul.name=name) grs.modules
394
            with Not_found -> Error.build "No module or strategy named '%s'" name in
395
396
397
          Rule.one_step ?domain: grs.domain name inst modul.Modul.rules
      end
    (* Union of strategies *)
398
399
    | Ast.Plus strat_list ->
      List.fold_left (fun acc strat -> Instance_set.union acc (loop inst strat)) Instance_set.empty strat_list
400
    (* Sequence of strategies *)
401
402
403
    | Ast.Seq [] -> Log.fcritical "Empty sequence in strategy definition"
    | Ast.Seq [one] -> loop inst one
    | Ast.Seq (head::tail) ->
404
      let after_first_mod = loop inst head in
405
      Instance_set.fold (fun new_inst acc -> Instance_set.union acc (loop new_inst (Ast.Seq tail))) after_first_mod Instance_set.empty
406
    (* Interation of a strategy *)
407
    | Ast.Star sub_strat ->
408
409
410
411
      let one_iter = loop inst sub_strat in
      if Instance_set.is_empty one_iter
      then Instance_set.singleton inst
      else Instance_set.fold (fun new_inst acc -> Instance_set.union acc (loop new_inst (Ast.Star sub_strat))) one_iter Instance_set.empty
412
413
    (* Pick *)
    | Ast.Pick sub_strat ->
414
415
      begin
        match one_rewrite grs sub_strat inst with
416
417
        | Some new_inst -> Instance_set.singleton new_inst
        | None -> Instance_set.empty
418
      end
419
420
421
422
423
424
425
426
427
    (* Try *)
    | Ast.Try sub_strat ->
      begin
        match one_rewrite grs sub_strat inst with
        | Some new_inst -> Instance_set.singleton new_inst
        | None -> Instance_set.singleton inst
      end
    (* Bang *)
    | Ast.Bang sub_strat -> loop inst (Ast.Pick (Ast.Star sub_strat))
428
    (* Old style seq definition *)
429
    | Ast.Sequence module_list -> loop inst (new_style grs module_list) in
430
431
    List.map
      (fun inst -> inst.Instance.graph)
432
      (Instance_set.elements (loop (Instance.from_graph graph) (Parser.strat_def strat_desc)))
433

434
  (* ---------------------------------------------------------------------------------------------------- *)
bguillaum's avatar
bguillaum committed
435
  (* construction of the rew_display *)
436
437
438
439
440
441
  let rec pick = function
    | Libgrew_types.Node (_, _, []) -> Log.bug "Empty node"; exit 12
    | Libgrew_types.Node (graph, name, (bs,rd)::_) -> Libgrew_types.Node (graph, "pick(" ^ name^")", [(bs, pick rd)])
    | x -> x

  let rec try_ = function
bguillaum's avatar
bguillaum committed
442
    | Libgrew_types.Node (_, _, []) -> Log.bug "Empty node"; exit 12
443
    | Libgrew_types.Node (graph, name, (bs,rd)::_) -> Libgrew_types.Node (graph, "try(" ^ name^")", [(bs, pick rd)])
bguillaum's avatar
bguillaum committed
444
445
    | x -> x

446
  (* ---------------------------------------------------------------------------------------------------- *)
bguillaum's avatar
bguillaum committed
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
  let rec clean = function
    | Libgrew_types.Empty -> Libgrew_types.Empty
    | Libgrew_types.Leaf graph -> Libgrew_types.Leaf graph
    | Libgrew_types.Local_normal_form (graph, name, Libgrew_types.Empty) -> Libgrew_types.Empty
    | Libgrew_types.Local_normal_form (graph, name, rd) -> Libgrew_types.Local_normal_form (graph, name, clean rd)
    | Libgrew_types.Node (graph, name, bs_rd_list) ->
        match
          List.fold_left (fun acc (bs,rd) ->
            match clean rd with
              | Libgrew_types.Empty -> acc
              | crd -> (bs, crd) :: acc
          ) [] bs_rd_list
        with
        | [] -> Libgrew_types.Empty
        | new_bs_rd_list -> Libgrew_types.Node (graph, name, new_bs_rd_list)

pj2m's avatar
pj2m committed
463

464
465
  (* ---------------------------------------------------------------------------------------------------- *)
  let build_rew_display grs strategy_name graph =
466
    let strategy = List.find (fun s -> s.Ast.strat_name = strategy_name) grs.strategies in
467
468
469

    let instance = Instance.from_graph graph in
    let rec old_loop instance module_list =
470
      match module_list with
bguillaum's avatar
bguillaum committed
471
      | [] -> Libgrew_types.Leaf instance.Instance.graph
472
473
474
475
      | next_name :: tail ->
         let next =
           try List.find (fun m -> m.Modul.name=next_name) grs.modules
           with Not_found -> Log.fcritical "No module named '%s'" next_name in
476
477
        let (good_set, bad_set) =
          Rule.normalize
bguillaum's avatar
bguillaum committed
478
            ?domain: grs.domain
479
480
481
482
            next.Modul.name
            ~confluent: next.Modul.confluent
            next.Modul.rules
            next.Modul.filters
483
            (Instance.refresh instance) in
484
        let inst_list = Instance_set.elements good_set
485
              (* and bad_list = Instance_set.elements bad_set *) in
pj2m's avatar
pj2m committed
486

487
        match inst_list with
488
          | [{Instance.big_step = None}] ->
489
            Libgrew_types.Local_normal_form (instance.Instance.graph, next.Modul.name, old_loop instance tail)
bguillaum's avatar
bguillaum committed
490
          | _ -> Libgrew_types.Node
491
492
493
494
495
496
            (
              instance.Instance.graph,
              next.Modul.name,
              List.map
                (fun inst ->
                  match inst.Instance.big_step with
497
498
499
                    | None -> Error.bug "Cannot have no big_steps and more than one reducts at the same time"
                    | Some bs -> (bs, old_loop inst tail)
                ) inst_list
Bruno Guillaume's avatar
Bruno Guillaume committed
500
            ) in
bguillaum's avatar
bguillaum committed
501

502
    let indent = ref 10 in
bguillaum's avatar
bguillaum committed
503

504
    let rec apply_leaf strat_def = function
bguillaum's avatar
bguillaum committed
505
      | Libgrew_types.Empty -> Libgrew_types.Empty
506
507
508
      | Libgrew_types.Leaf graph -> loop (Instance.from_graph graph) strat_def
      | Libgrew_types.Local_normal_form (graph, name, rd) -> Libgrew_types.Local_normal_form (graph, name, apply_leaf strat_def rd)
      | Libgrew_types.Node (graph, name, bs_rd_list) -> Libgrew_types.Node (graph, name, List.map (fun (bs,rd) -> (bs, apply_leaf strat_def rd)) bs_rd_list)
bguillaum's avatar
bguillaum committed
509

510
511
    and loop instance strat_def =
      printf "%s===> loop  strat_def=%s\n%!"
bguillaum's avatar
bguillaum committed
512
        (String.make (2 * (max 0 !indent)) ' ')
513
        (Ast.strat_def_to_string strat_def);
bguillaum's avatar
bguillaum committed
514
515
      incr indent;

516
517
      match strat_def with

518
      | Ast.Sequence module_list -> old_loop instance module_list
bguillaum's avatar
bguillaum committed
519
520

      (* ========> reference to a module or to another strategy <========= *)
521
      | Ast.Ref name ->
bguillaum's avatar
bguillaum committed
522
523
        begin
          try
524
525
            let strategy = List.find (fun s -> s.Ast.strat_name = name) grs.strategies in
            loop instance strategy.Ast.strat_def
bguillaum's avatar
bguillaum committed
526
527
528
529
530
          with Not_found ->
            let modul =
              try List.find (fun m -> m.Modul.name=name) grs.modules
              with Not_found -> Log.fcritical "No [strategy or] module named '%s'" name in
            begin
bguillaum's avatar
bguillaum committed
531
              printf "%s one_step (module=%s)...%!" (String.make (2 * (max 0 !indent)) ' ') modul.Modul.name;
bguillaum's avatar
bguillaum committed
532
              let domain = get_domain grs in
533
              match Instance_set.elements (Rule.one_step ?domain modul.Modul.name instance modul.Modul.rules) with
bguillaum's avatar
bguillaum committed
534
535
536
537
538
539
540
              | [] -> printf "0\n%!"; let res = Libgrew_types.Empty in decr indent; res
              | instance_list -> printf "%d\n%!" (List.length instance_list);
                Libgrew_types.Node
                (instance.Instance.graph,
                  name,
                  List.map
                    (fun inst -> match inst.Instance.big_step with
541
                    | None -> Error.bug "Cannot have no big_steps and more than one reducts at the same time"
bguillaum's avatar
bguillaum committed
542
543
544
545
546
547
548
                    | Some bs -> let res = (bs, Libgrew_types.Leaf inst.Instance.graph) in decr indent; res
                    ) instance_list
                )
            end
        end

      (* ========> Strat defined as a sequence of sub-strategies <========= *)
549
550
551
      | Ast.Seq [] -> Log.bug "[Grs.build_rew_display] Empty sequence!"; exit 2
      | Ast.Seq [one] -> let res = loop instance one in decr indent; res
      | Ast.Seq (head_strat :: tail_strat) ->
bguillaum's avatar
bguillaum committed
552
        let one_step = loop instance head_strat in decr indent;
553
        apply_leaf (Ast.Seq tail_strat) one_step
bguillaum's avatar
bguillaum committed
554

555
556
557
      | Ast.Pick strat -> pick (loop instance strat)
      | Ast.Try strat -> try_ (loop instance strat)
      | Ast.Bang strat -> loop instance (Ast.Pick (Ast.Star strat))
bguillaum's avatar
bguillaum committed
558
559

      (* ========> Strat defined as a sequence of sub-strategies <========= *)
560
561
      | Ast.Plus [] -> Log.bug "[Grs.build_rew_display] Empty union!"; exit 2
      | Ast.Plus strat_list ->
bguillaum's avatar
bguillaum committed
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
        let rd_list = List.map (fun strat -> loop instance strat) strat_list in
        let (opt_lnf, opt_node_info) =
          List.fold_left (fun (acc_lnf, acc_node) rd ->
            match (rd, acc_lnf, acc_node) with
            | (Libgrew_types.Empty, acc_lnf, acc_node) -> (acc_lnf, acc_node)

            | (Libgrew_types.Leaf graph, None ,_) -> (Some (graph,"0"), acc_node)
            | (Libgrew_types.Leaf _,Some (graph,names) ,_) -> (Some (graph,"0+"^names), acc_node)

            | (Libgrew_types.Local_normal_form (graph,name,_), None, _) -> (Some (graph,name), acc_node)
            | (Libgrew_types.Local_normal_form (_,name,_), Some (graph,names), _) -> (Some (graph,name^"+"^names), acc_node)

            | (Libgrew_types.Node (graph,name,bs_rd_list), _, None) -> (acc_lnf, Some (graph,name,bs_rd_list))
            | (Libgrew_types.Node (_,name,bs_rd_list), _, Some (graph,acc_names,acc_bs_rd_list)) ->
                (acc_lnf, Some (graph, name^"+"^acc_names,bs_rd_list @ acc_bs_rd_list))
          ) (None,None) rd_list in
        begin
          match (opt_lnf, opt_node_info) with
            | (None, None) -> Libgrew_types.Empty
            | (Some (graph,lnf_name), None) -> Libgrew_types.Local_normal_form (graph, lnf_name, Libgrew_types.Leaf graph)
            | (None, Some (a,b,c)) -> Libgrew_types.Node (a,b,c)
            | (Some (_,lnf_name), Some (graph,acc_name,acc_bs_rd_list)) ->
                let bs = {Libgrew_types.first={Libgrew_types.rule_name="dummy";up=G_deco.empty;down=G_deco.empty}; small_step=[]} in
                Libgrew_types.Node (graph,acc_name,(bs, Libgrew_types.Leaf graph) :: acc_bs_rd_list)
        end

588
      | Ast.Star strat ->
bguillaum's avatar
bguillaum committed
589
590
591
592
        begin
          match clean (loop instance strat) with
          | Libgrew_types.Empty -> Libgrew_types.Leaf instance.Instance.graph
          | Libgrew_types.Local_normal_form _ -> Log.bug "dont know if 'Local_normal_form' in star should happen or not ???"; exit 1
593
          | rd -> apply_leaf (Ast.Star strat) rd
bguillaum's avatar
bguillaum committed
594
595
596
        end
      in

597
    loop instance (strategy.Ast.strat_def)
bguillaum's avatar
bguillaum committed
598

599
  (* ---------------------------------------------------------------------------------------------------- *)
bguillaum's avatar
bguillaum committed
600
601
602
  let rule_iter fct grs =
    List.iter
      (fun modul ->
bguillaum's avatar
bguillaum committed
603
604
605
        List.iter (fun rule -> fct modul.Modul.name rule) modul.Modul.rules
      ) grs.modules

606
  (* ---------------------------------------------------------------------------------------------------- *)
bguillaum's avatar
bguillaum committed
607
608
609
610
  let filter_iter fct grs =
    List.iter
      (fun modul ->
        List.iter (fun filter -> fct modul.Modul.name filter) modul.Modul.filters
bguillaum's avatar
bguillaum committed
611
      ) grs.modules
612
end (* module Grs *)