grew_grs.ml 7.59 KB
Newer Older
pj2m's avatar
pj2m committed
1 2 3
open Printf
open Log

4
open Grew_fs
bguillaum's avatar
bguillaum committed
5 6
open Grew_utils
open Grew_ast
7
open Grew_edge
bguillaum's avatar
bguillaum committed
8 9 10
open Grew_command
open Grew_graph
open Grew_rule
pj2m's avatar
pj2m committed
11 12 13 14 15


module Rewrite_history = struct

  type t = {
16 17 18 19 20
    instance: Instance.t;
    module_name: string;
    good_nf: t list;
    bad_nf: Instance.t list;
  }
pj2m's avatar
pj2m committed
21

22
  let rec is_empty t =
bguillaum's avatar
bguillaum committed
23
    (t.instance.Instance.rules = []) && List.for_all is_empty t.good_nf
bguillaum's avatar
bguillaum committed
24 25

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

30

31
  let save_nfs ?main_feat ~dot base_name t =
32
    let rec loop file_name rules t =
33
      match (t.good_nf, t.bad_nf) with
34
        | [],[] when dot -> Instance.save_dot_png ?main_feat file_name t.instance; [rules, file_name]
35 36 37
        | [],[] -> Instance.save_dep_png ?main_feat file_name t.instance; [rules, file_name]
        | [],_ -> []
        | l, _ ->
38
          List_.foldi_left
39
            (fun i acc son ->
40
              (* Instance.save_dep_png ?main_feat (sprintf "%s_%d" file_name i) son.instance; *)
41 42 43 44
              let nfs = loop
                (sprintf "%s_%d" file_name i)
                (rules @ [t.module_name, son.instance.Instance.rules])
                son in
45 46 47 48 49
              nfs @ acc
            )
            [] l
    in loop base_name [] t

50

51 52 53 54 55 56 57
  let save_gr base t =
    let rec loop file_name t =
      match (t.good_nf, t.bad_nf) with
        | [],[] -> File.write (Instance.to_gr t.instance) (file_name^".gr")
        | l, _ -> List_.iteri (fun i son -> loop (sprintf "%s_%d" file_name i) son) l
    in loop base t

pj2m's avatar
pj2m committed
58 59 60 61 62 63 64
end




module Modul = struct
  type t = {
65 66 67 68 69 70 71
    name: string;
    local_labels: (string * string option) array;
    rules: Rule.t list;
    filters: Rule.t list;
    confluent: bool;
    loc: Loc.t;
  }
pj2m's avatar
pj2m committed
72

73 74 75 76
  let check t =
    (* check for duplicate rules *)
    let rec loop already_defined = function
      | [] -> ()
77 78
      | 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)
79 80
      | r::tail -> loop ((Rule.get_name r) :: already_defined) tail in
    loop [] t.rules
pj2m's avatar
pj2m committed
81

82
  let build ast_module =
83 84
    let locals = Array.of_list ast_module.Ast.local_labels in
    Array.sort compare locals;
85
    let rules_or_filters = List.map (Rule.build ~locals ast_module.Ast.mod_dir) ast_module.Ast.rules in
86 87
    let (filters, rules) = List.partition Rule.is_filter rules_or_filters in
    let modul =
88
      {
89 90 91 92 93 94 95
        name = ast_module.Ast.module_id;
        local_labels = locals;
        rules = rules;
        filters = filters;
        confluent = ast_module.Ast.confluent;
        loc = ast_module.Ast.mod_loc;
      } in
96 97 98 99 100
    check modul; modul
end

module Sequence = struct
  type t = {
101 102 103 104
    name: string;
    def: string list;
    loc: Loc.t;
  }
105 106 107

  let check module_list t =
    List.iter
108
      (fun module_name ->
109 110
        if not (List.exists (fun modul -> modul.Modul.name = module_name) module_list)
        then Error.build ~loc:t.loc "sequence \"%s\", refers to the unknown module \"%s\"."
111
          t.name module_name
112 113
      ) t.def

114 115
  let build module_list ast_sequence =
    let sequence =
116
      {
117 118 119 120
        name = ast_sequence.Ast.seq_name;
        def = ast_sequence.Ast.seq_mod;
        loc = ast_sequence.Ast.seq_loc;
      } in
121
    check module_list sequence; sequence
pj2m's avatar
pj2m committed
122 123 124
end

module Grs = struct
125

pj2m's avatar
pj2m committed
126
  type t = {
127 128 129 130 131
    labels: Label.t list;    (* the list of global edge labels *)
    modules: Modul.t list;          (* the ordered list of modules used from rewriting *)
    sequences: Sequence.t list;
  }

bguillaum's avatar
bguillaum committed
132 133
  let get_modules t = t.modules

134 135
  let sequence_names t = List.map (fun s -> s.Sequence.name) t.sequences

pj2m's avatar
pj2m committed
136 137
  let empty = {labels=[]; modules=[]; sequences=[];}

138 139 140 141
  let check t =
    (* check for duplicate modules *)
    let rec loop already_defined = function
      | [] -> ()
142 143
      | m::_ when List.mem m.Modul.name already_defined ->
        Error.build ~loc:m.Modul.loc "Module '%s' is defined twice" m.Modul.name
144 145 146 147 148 149
      | m::tail -> loop (m.Modul.name :: already_defined) tail in
    loop [] t.modules;

    (* check for duplicate sequences *)
    let rec loop already_defined = function
      | [] -> ()
150 151
      | s::_ when List.mem s.Sequence.name already_defined ->
        Error.build ~loc:s.Sequence.loc "Sequence '%s' is defined twice" s.Sequence.name
152 153 154
      | s::tail -> loop (s.Sequence.name :: already_defined) tail in
    loop [] t.sequences

pj2m's avatar
pj2m committed
155
  let build ast_grs =
156
    Label.init ast_grs.Ast.labels;
157 158
    Domain.init ast_grs.Ast.domain;
    let modules = List.map Modul.build ast_grs.Ast.modules in
159 160 161 162 163 164
    let grs = {
      labels = List.map (fun (l,_) -> Label.from_string l) ast_grs.Ast.labels;
      modules = modules;
      sequences = List.map (Sequence.build modules) ast_grs.Ast.sequences;
    } in
    check grs; grs
pj2m's avatar
pj2m committed
165

bguillaum's avatar
bguillaum committed
166
  let modules_of_sequence grs sequence =
167
    let module_names =
168
      try
169 170
        let seq = List.find (fun s -> s.Sequence.name = sequence) grs.sequences in
        seq.Sequence.def
bguillaum's avatar
bguillaum committed
171 172
      with Not_found -> [sequence] in (* a module name can be used as a singleton sequence *)

173 174 175
    List.map
      (fun name ->
        try List.find (fun m -> m.Modul.name=name) grs.modules
bguillaum's avatar
bguillaum committed
176 177 178 179
        with Not_found -> Log.fcritical "No sequence or module named '%s'" name
      )
      module_names

180
  let rewrite grs sequence instance =
bguillaum's avatar
bguillaum committed
181
    let modules_to_apply = modules_of_sequence grs sequence in
182

pj2m's avatar
pj2m committed
183
    let rec loop instance = function
184 185 186 187 188 189 190 191 192
      | [] -> (* no more modules to apply *)
        {Rewrite_history.instance = instance; module_name = ""; good_nf = []; bad_nf = []; }
      | next::tail ->
        let (good_set, bad_set) =
          Rule.normalize
            next.Modul.name
            ~confluent: next.Modul.confluent
            next.Modul.rules
            next.Modul.filters
193
            (Instance.flatten instance) in
194 195 196 197 198 199 200 201
        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;
          good_nf = List.map (fun i -> loop i tail) good_list;
          bad_nf = bad_list;
        } in
bguillaum's avatar
bguillaum committed
202
    loop instance modules_to_apply
203

bguillaum's avatar
bguillaum committed
204 205
  let build_rew_display grs sequence instance =
    let modules_to_apply = modules_of_sequence grs sequence in
pj2m's avatar
pj2m committed
206 207 208

    let rec loop instance = function
      | [] -> Grew_types.Leaf instance.Instance.graph
209
      | next :: tail ->
210 211 212 213 214 215
        let (good_set, bad_set) =
          Rule.normalize
            next.Modul.name
            ~confluent: next.Modul.confluent
            next.Modul.rules
            next.Modul.filters
216
            (Instance.flatten instance) in
217
        let inst_list = Instance_set.elements good_set
218
              (* and bad_list = Instance_set.elements bad_set *) in
pj2m's avatar
pj2m committed
219

220
        match inst_list with
221
          | [{Instance.big_step = None}] ->
222
            Grew_types.Local_normal_form (instance.Instance.graph, next.Modul.name, loop instance tail)
223
          | _ -> Grew_types.Node
224 225 226 227 228 229 230 231 232 233
            (
              instance.Instance.graph,
              next.Modul.name,
              List.map
                (fun inst ->
                  match inst.Instance.big_step with
                    | None -> Error.bug "Cannot have no big_steps and more than one reducts at the same time"
                    | Some bs -> (bs, loop inst tail)
                ) inst_list
            )
pj2m's avatar
pj2m committed
234
    in loop instance modules_to_apply
bguillaum's avatar
bguillaum committed
235

bguillaum's avatar
bguillaum committed
236 237 238
  let rule_iter fct grs =
    List.iter
      (fun modul ->
bguillaum's avatar
bguillaum committed
239 240 241 242 243 244 245
        List.iter (fun rule -> fct modul.Modul.name rule) modul.Modul.rules
      ) grs.modules

  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
246
      ) grs.modules
247
end