Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/corelang.ml
14 14
open Machine_code_types
15 15
(*open Dimension*)
16 16

  
17

  
18
module VDeclModule =
19
struct (* Node module *)
17
module VDeclModule = struct
18
  (* Node module *)
20 19
  type t = var_decl
20

  
21 21
  let compare v1 v2 = compare v1.var_id v2.var_id
22 22
end
23 23

  
24
module VMap = Map.Make(VDeclModule)
24
module VMap = Map.Make (VDeclModule)
25 25

  
26
module VSet: sig
26
module VSet : sig
27 27
  include Set.S
28
  val pp: Format.formatter -> t -> unit
29
  val get: ident -> t -> elt
30
end with type elt = var_decl =
31
  struct
32
    include Set.Make(VDeclModule)
33
    let pp fmt s =
34
      Format.fprintf fmt "{@[%a}@]" (Utils.fprintf_list ~sep:",@ " Printers.pp_var) (elements s)
35
    (* Strangley the find_first function of Set.Make is incorrect (at
36
       the current time of writting this comment. Had to switch to
37
       lists *)
38
    let get id s = List.find (fun v -> v.var_id = id) (elements s)
39
  end
40
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
41 28

  
42
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
29
  val pp : Format.formatter -> t -> unit
30

  
31
  val get : ident -> t -> elt
32
end
33
with type elt = var_decl = struct
34
  include Set.Make (VDeclModule)
35

  
36
  let pp fmt s =
37
    Format.fprintf fmt "{@[%a}@]"
38
      (Utils.fprintf_list ~sep:",@ " Printers.pp_var)
39
      (elements s)
43 40

  
41
  (* Strangley the find_first function of Set.Make is incorrect (at the current
42
     time of writting this comment. Had to switch to lists *)
43
  let get id s = List.find (fun v -> v.var_id = id) (elements s)
44
end
44 45

  
46
let dummy_type_dec =
47
  { ty_dec_desc = Tydec_any; ty_dec_loc = Location.dummy_loc }
48

  
49
let dummy_clock_dec =
50
  { ck_dec_desc = Ckdec_any; ck_dec_loc = Location.dummy_loc }
45 51

  
46 52
(************************************************************)
47 53
(* *)
48 54

  
49
let mktyp loc d =
50
  { ty_dec_desc = d; ty_dec_loc = loc }
55
let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc }
51 56

  
52
let mkclock loc d =
53
  { ck_dec_desc = d; ck_dec_loc = loc }
57
let mkclock loc d = { ck_dec_desc = d; ck_dec_loc = loc }
54 58

  
55
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) =
59
let mkvar_decl loc ?(orig = false)
60
    (id, ty_dec, ck_dec, is_const, value, parentid) =
56 61
  assert (value = None || is_const);
57
  { var_id = id;
62
  {
63
    var_id = id;
58 64
    var_orig = orig;
59 65
    var_dec_type = ty_dec;
60 66
    var_dec_clock = ck_dec;
......
63 69
    var_parent_nodeid = parentid;
64 70
    var_type = Types.new_var ();
65 71
    var_clock = Clocks.new_var true;
66
    var_loc = loc }
72
    var_loc = loc;
73
  }
67 74

  
68 75
let dummy_var_decl name typ =
69 76
  {
......
74 81
    var_dec_const = false;
75 82
    var_dec_value = None;
76 83
    var_parent_nodeid = None;
77
    var_type =  typ;
84
    var_type = typ;
78 85
    var_clock = Clocks.new_ck Clocks.Cvar true;
79
    var_loc = Location.dummy_loc
86
    var_loc = Location.dummy_loc;
80 87
  }
81 88

  
82 89
let mkexpr loc d =
83
  { expr_tag = Utils.new_tag ();
90
  {
91
    expr_tag = Utils.new_tag ();
84 92
    expr_desc = d;
85 93
    expr_type = Types.new_var ();
86 94
    expr_clock = Clocks.new_var true;
87 95
    expr_delay = Delay.new_var ();
88 96
    expr_annot = None;
89
    expr_loc = loc }
97
    expr_loc = loc;
98
  }
90 99

  
91
let var_decl_of_const ?(parentid=None) c =
92
  { var_id = c.const_id;
100
let var_decl_of_const ?(parentid = None) c =
101
  {
102
    var_id = c.const_id;
93 103
    var_orig = true;
94 104
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
95 105
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
......
98 108
    var_parent_nodeid = parentid;
99 109
    var_type = c.const_type;
100 110
    var_clock = Clocks.new_var false;
101
    var_loc = c.const_loc }
111
    var_loc = c.const_loc;
112
  }
102 113

  
103 114
let mk_new_name used id =
104 115
  let rec new_name name cpt =
105
    if used name
106
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
107
    else name
108
  in new_name id 1
109

  
110
let mkeq loc (lhs, rhs) =
111
  { eq_lhs = lhs;
112
    eq_rhs = rhs;
113
    eq_loc = loc }
114

  
115
let mkassert loc expr =
116
  { assert_loc = loc;
117
    assert_expr = expr
118
  }
116
    if used name then new_name (sprintf "_%s_%i" id cpt) (cpt + 1) else name
117
  in
118
  new_name id 1
119

  
120
let mkeq loc (lhs, rhs) = { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc }
121

  
122
let mkassert loc expr = { assert_loc = loc; assert_expr = expr }
119 123

  
120 124
let mktop_decl loc own itf d =
121
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
125
  {
126
    top_decl_desc = d;
127
    top_decl_loc = loc;
128
    top_decl_owner = own;
129
    top_decl_itf = itf;
130
  }
122 131

  
123 132
let mkpredef_call loc funname args =
124 133
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
125 134

  
126
let is_clock_dec_type cty =
127
  match cty with
128
  | Tydec_clock _ -> true
129
  | _             -> false
135
let is_clock_dec_type cty = match cty with Tydec_clock _ -> true | _ -> false
130 136

  
131 137
let const_of_top top_decl =
132
  match top_decl.top_decl_desc with
133
  | Const c -> c
134
  | _ -> assert false
138
  match top_decl.top_decl_desc with Const c -> c | _ -> assert false
135 139

  
136 140
let node_of_top top_decl =
137
  match top_decl.top_decl_desc with
138
  | Node nd -> nd
139
  | _ -> raise Not_found
141
  match top_decl.top_decl_desc with Node nd -> nd | _ -> raise Not_found
140 142

  
141 143
let imported_node_of_top top_decl =
142 144
  match top_decl.top_decl_desc with
143
  | ImportedNode ind -> ind
144
  | _ -> assert false
145
  | ImportedNode ind ->
146
    ind
147
  | _ ->
148
    assert false
145 149

  
146 150
let typedef_of_top top_decl =
147
  match top_decl.top_decl_desc with
148
  | TypeDef tdef -> tdef
149
  | _ -> assert false
151
  match top_decl.top_decl_desc with TypeDef tdef -> tdef | _ -> assert false
150 152

  
151 153
let dependency_of_top top_decl =
152 154
  match top_decl.top_decl_desc with
153
  | Open (local, dep) -> (local, dep)
154
  | _ -> assert false
155
  | Open (local, dep) ->
156
    local, dep
157
  | _ ->
158
    assert false
155 159

  
156 160
let consts_of_enum_type top_decl =
157 161
  match top_decl.top_decl_desc with
158
  | TypeDef tdef ->
159
    (match tdef.tydef_desc with
162
  | TypeDef tdef -> (
163
    match tdef.tydef_desc with
160 164
    | Tydec_enum tags ->
161
       List.map
162
	 (fun tag ->
163
	   let cdecl = {
164
	     const_id = tag;
165
	     const_loc = top_decl.top_decl_loc;
166
	     const_value = Const_tag tag;
167
	     const_type = Type_predef.type_const tdef.tydef_id
168
	   } in
169
	   { top_decl with top_decl_desc = Const cdecl })
170
	 tags
171
     | _               -> [])
172
  | _ -> assert false
165
      List.map
166
        (fun tag ->
167
          let cdecl =
168
            {
169
              const_id = tag;
170
              const_loc = top_decl.top_decl_loc;
171
              const_value = Const_tag tag;
172
              const_type = Type_predef.type_const tdef.tydef_id;
173
            }
174
          in
175
          { top_decl with top_decl_desc = Const cdecl })
176
        tags
177
    | _ ->
178
      [])
179
  | _ ->
180
    assert false
173 181

  
174 182
(************************************************************)
175 183
(*   Eexpr functions *)
176 184
(************************************************************)
177 185

  
178

  
179 186
let empty_contract =
180 187
  {
181
    consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
188
    consts = [];
189
    locals = [];
190
    stmts = [];
191
    assume = [];
192
    guarantees = [];
193
    modes = [];
194
    imports = [];
195
    spec_loc = Location.dummy_loc;
182 196
  }
183 197

  
184
(* For const declaration we do as for regular lustre node.
185
But for local flows we registered the variable and the lustre flow definition *)
198
(* For const declaration we do as for regular lustre node. But for local flows
199
   we registered the variable and the lustre flow definition *)
186 200
let mk_contract_var id is_const type_opt expr loc =
187 201
  let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
188 202
  if is_const then
189
  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
190
  { empty_contract with consts = [v]; spec_loc = loc; }
203
    let v =
204
      mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None)
205
    in
206
    { empty_contract with consts = [ v ]; spec_loc = loc }
191 207
  else
192
    let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
193
    let eq = mkeq loc ([id], expr) in 
194
    { empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
208
    let v =
209
      mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None)
210
    in
211
    let eq = mkeq loc ([ id ], expr) in
212
    { empty_contract with locals = [ v ]; stmts = [ Eq eq ]; spec_loc = loc }
195 213

  
196
let eexpr_add_name eexpr eexpr_name =
197
  { eexpr with eexpr_name }
214
let eexpr_add_name eexpr eexpr_name = { eexpr with eexpr_name }
198 215

  
199 216
let mk_contract_guarantees name eexpr =
200
  { empty_contract with guarantees = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
217
  {
218
    empty_contract with
219
    guarantees = [ eexpr_add_name eexpr name ];
220
    spec_loc = eexpr.eexpr_loc;
221
  }
201 222

  
202 223
let mk_contract_assume name eexpr =
203
  { empty_contract with assume = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
224
  {
225
    empty_contract with
226
    assume = [ eexpr_add_name eexpr name ];
227
    spec_loc = eexpr.eexpr_loc;
228
  }
204 229

  
205 230
let mk_contract_mode id rl el loc =
206
  { empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc }
231
  {
232
    empty_contract with
233
    modes = [ { mode_id = id; require = rl; ensure = el; mode_loc = loc } ];
234
    spec_loc = loc;
235
  }
207 236

  
208 237
let mk_contract_import id ins outs loc =
209
  { empty_contract with imports = [{import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc; }]; spec_loc = loc }
238
  {
239
    empty_contract with
240
    imports =
241
      [ { import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc } ];
242
    spec_loc = loc;
243
  }
210 244

  
211
    
212
let merge_contracts ann1 ann2 = (* keeping the first item loc *)
213
  { consts = ann1.consts @ ann2.consts;
245
let merge_contracts ann1 ann2 =
246
  (* keeping the first item loc *)
247
  {
248
    consts = ann1.consts @ ann2.consts;
214 249
    locals = ann1.locals @ ann2.locals;
215 250
    stmts = ann1.stmts @ ann2.stmts;
216 251
    assume = ann1.assume @ ann2.assume;
217 252
    guarantees = ann1.guarantees @ ann2.guarantees;
218 253
    modes = ann1.modes @ ann2.modes;
219 254
    imports = ann1.imports @ ann2.imports;
220
    spec_loc = ann1.spec_loc
255
    spec_loc = ann1.spec_loc;
221 256
  }
222 257

  
223 258
let mkeexpr loc expr =
224
  { eexpr_tag = Utils.new_tag ();
259
  {
260
    eexpr_tag = Utils.new_tag ();
225 261
    eexpr_qfexpr = expr;
226 262
    eexpr_quantifiers = [];
227 263
    eexpr_name = None;
228 264
    eexpr_type = Types.new_var ();
229 265
    eexpr_clock = Clocks.new_var true;
230
    eexpr_loc = loc }
266
    eexpr_loc = loc;
267
  }
231 268

  
232
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
269
let extend_eexpr q e = { e with eexpr_quantifiers = q @ e.eexpr_quantifiers }
233 270

  
234
(*
235
let mkepredef_call loc funname args =
236
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
271
(* let mkepredef_call loc funname args = mkeexpr loc (EExpr_appl (funname,
272
   mkeexpr loc (EExpr_tuple args), None))
237 273

  
238
let mkepredef_unary_call loc funname arg =
239
  mkeexpr loc (EExpr_appl (funname, arg, None))
240
*)
274
   let mkepredef_unary_call loc funname arg = mkeexpr loc (EExpr_appl (funname,
275
   arg, None)) *)
241 276

  
242 277
let merge_expr_annot ann1 ann2 =
243 278
  match ann1, ann2 with
244
    | None, None -> assert false
245
    | Some _, None -> ann1
246
    | None, Some _ -> ann2
247
    | Some ann1, Some ann2 -> Some {
248
      annots = ann1.annots @ ann2.annots;
249
      annot_loc = ann1.annot_loc
250
    }
279
  | None, None ->
280
    assert false
281
  | Some _, None ->
282
    ann1
283
  | None, Some _ ->
284
    ann2
285
  | Some ann1, Some ann2 ->
286
    Some { annots = ann1.annots @ ann2.annots; annot_loc = ann1.annot_loc }
251 287

  
252 288
let update_expr_annot node_id e annot =
253
  List.iter (fun (key, _) -> 
254
    Annotations.add_expr_ann node_id e.expr_tag key
255
  ) annot.annots;
289
  List.iter
290
    (fun (key, _) -> Annotations.add_expr_ann node_id e.expr_tag key)
291
    annot.annots;
256 292
  e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
257 293
  e
258 294

  
259

  
260
let mkinstr ?lustre_eq ?(instr_spec=[]) instr_desc = {
261
  instr_desc;
262
  (* lustre_expr = lustre_expr; *)
263
  instr_spec;
264
  lustre_eq;
265
}
295
let mkinstr ?lustre_eq ?(instr_spec = []) instr_desc =
296
  { instr_desc; (* lustre_expr = lustre_expr; *)
297
                instr_spec; lustre_eq }
266 298

  
267 299
let get_instr_desc i = i.instr_desc
300

  
268 301
let update_instr_desc i id = { i with instr_desc = id }
269 302

  
270 303
(***********************************************************)
271 304
(* Fast access to nodes, by name *)
272 305
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
306

  
273 307
let consts_table = Hashtbl.create 30
274 308

  
275 309
let print_node_table fmt () =
276
  begin
277
    Format.fprintf fmt "{ /* node table */@.";
278
    Hashtbl.iter (fun id nd ->
279
      Format.fprintf fmt "%s |-> %a"
280
	id
281
	Printers.pp_short_decl nd
282
    ) node_table;
283
    Format.fprintf fmt "}@."
284
  end
310
  Format.fprintf fmt "{ /* node table */@.";
311
  Hashtbl.iter
312
    (fun id nd -> Format.fprintf fmt "%s |-> %a" id Printers.pp_short_decl nd)
313
    node_table;
314
  Format.fprintf fmt "}@."
285 315

  
286 316
let print_consts_table fmt () =
287
  begin
288
    Format.fprintf fmt "{ /* consts table */@.";
289
    Hashtbl.iter (fun id const ->
290
      Format.fprintf fmt "%s |-> %a"
291
	id
292
	Printers.pp_const_decl (const_of_top const)
293
    ) consts_table;
294
    Format.fprintf fmt "}@."
295
  end
317
  Format.fprintf fmt "{ /* consts table */@.";
318
  Hashtbl.iter
319
    (fun id const ->
320
      Format.fprintf fmt "%s |-> %a" id Printers.pp_const_decl
321
        (const_of_top const))
322
    consts_table;
323
  Format.fprintf fmt "}@."
296 324

  
297 325
let node_name td =
298
    match td.top_decl_desc with 
299
    | Node nd         -> nd.node_id
300
    | ImportedNode nd -> nd.nodei_id
301
    | _ -> assert false
326
  match td.top_decl_desc with
327
  | Node nd ->
328
    nd.node_id
329
  | ImportedNode nd ->
330
    nd.nodei_id
331
  | _ ->
332
    assert false
302 333

  
303 334
let is_generic_node td =
304
  match td.top_decl_desc with 
305
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
306
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
307
  | _ -> assert false
335
  match td.top_decl_desc with
336
  | Node nd ->
337
    List.exists (fun v -> v.var_dec_const) nd.node_inputs
338
  | ImportedNode nd ->
339
    List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
340
  | _ ->
341
    assert false
308 342

  
309 343
let node_inputs td =
310
  match td.top_decl_desc with 
311
  | Node nd         -> nd.node_inputs
312
  | ImportedNode nd -> nd.nodei_inputs
313
  | _ -> assert false
344
  match td.top_decl_desc with
345
  | Node nd ->
346
    nd.node_inputs
347
  | ImportedNode nd ->
348
    nd.nodei_inputs
349
  | _ ->
350
    assert false
351

  
352
let node_from_name id = Hashtbl.find node_table id
314 353

  
315
let node_from_name id =
316
      Hashtbl.find node_table id
317
      
318
let update_node id top =
319
  Hashtbl.replace node_table id top
354
let update_node id top = Hashtbl.replace node_table id top
320 355

  
321 356
let is_imported_node td =
322
  match td.top_decl_desc with 
323
  | Node _         -> false
324
  | ImportedNode _ -> true
325
  | _ -> assert false
357
  match td.top_decl_desc with
358
  | Node _ ->
359
    false
360
  | ImportedNode _ ->
361
    true
362
  | _ ->
363
    assert false
326 364

  
327 365
let is_node_contract nd =
328
  match nd.node_spec with
329
  | Some (Contract _) -> true
330
  | _ -> false
331
  
366
  match nd.node_spec with Some (Contract _) -> true | _ -> false
367

  
332 368
let get_node_contract nd =
333
  match nd.node_spec with
334
  | Some (Contract c) -> c
335
  | _ -> assert false
336
  
369
  match nd.node_spec with Some (Contract c) -> c | _ -> assert false
370

  
337 371
let is_contract td =
338
  match td.top_decl_desc with 
339
  | Node nd -> is_node_contract nd
340
  | _ -> false
372
  match td.top_decl_desc with Node nd -> is_node_contract nd | _ -> false
341 373

  
342 374
(* alias and type definition table *)
343 375

  
344 376
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
345 377

  
346
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
347
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
348
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
349
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
378
let top_int_type = mktop (TypeDef { tydef_id = "int"; tydef_desc = Tydec_int })
379

  
380
let top_bool_type =
381
  mktop (TypeDef { tydef_id = "bool"; tydef_desc = Tydec_bool })
382

  
383
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc =
384
   Tydec_float}) *)
385
let top_real_type =
386
  mktop (TypeDef { tydef_id = "real"; tydef_desc = Tydec_real })
350 387

  
351 388
let type_table =
352
  Utils.create_hashtable 20 [
353
    Tydec_int  , top_int_type;
354
    Tydec_bool , top_bool_type;
355
    (* Tydec_float, top_float_type; *)
356
    Tydec_real , top_real_type
357
  ]
389
  Utils.create_hashtable 20
390
    [
391
      Tydec_int, top_int_type;
392
      Tydec_bool, top_bool_type;
393
      (* Tydec_float, top_float_type; *)
394
      Tydec_real, top_real_type;
395
    ]
358 396

  
359 397
let print_type_table fmt () =
360
  begin
361
    Format.fprintf fmt "{ /* type table */@.";
362
    Hashtbl.iter (fun tydec tdef ->
363
      Format.fprintf fmt "%a |-> %a"
364
	Printers.pp_var_type_dec_desc tydec
365
	Printers.pp_typedef (typedef_of_top tdef)
366
    ) type_table;
367
    Format.fprintf fmt "}@."
368
  end
398
  Format.fprintf fmt "{ /* type table */@.";
399
  Hashtbl.iter
400
    (fun tydec tdef ->
401
      Format.fprintf fmt "%a |-> %a" Printers.pp_var_type_dec_desc tydec
402
        Printers.pp_typedef (typedef_of_top tdef))
403
    type_table;
404
  Format.fprintf fmt "}@."
369 405

  
370 406
let rec is_user_type typ =
371 407
  match typ with
372
  | Tydec_int | Tydec_bool | Tydec_real 
373
  (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
374
  | Tydec_clock typ' -> is_user_type typ'
375
  | _ -> true
408
  | Tydec_int
409
  | Tydec_bool
410
  | Tydec_real (* | Tydec_float *)
411
  | Tydec_any
412
  | Tydec_const _ ->
413
    false
414
  | Tydec_clock typ' ->
415
    is_user_type typ'
416
  | _ ->
417
    true
376 418

  
377 419
let get_repr_type typ =
378 420
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
......
380 422

  
381 423
let rec coretype_equal ty1 ty2 =
382 424
  let res =
383
  match ty1, ty2 with
384
  | Tydec_any           , _
385
  | _                   , Tydec_any             -> assert false
386
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
387
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
388
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
389
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
390
  | Tydec_int           , Tydec_int
391
  | Tydec_real          , Tydec_real
392
  (* | Tydec_float         , Tydec_float *)
393
  | Tydec_bool          , Tydec_bool            -> true
394
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
395
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
396
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
397
  | Tydec_struct fl1    , Tydec_struct fl2      ->
398
       List.length fl1 = List.length fl2
399
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
400
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
401
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
402
  | _                                  -> false
403
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
425
    match ty1, ty2 with
426
    | Tydec_any, _ | _, Tydec_any ->
427
      assert false
428
    | Tydec_const _, Tydec_const _ ->
429
      get_repr_type ty1 = get_repr_type ty2
430
    | Tydec_const _, _ ->
431
      let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc in
432
      (not (is_user_type ty1')) && coretype_equal ty1' ty2
433
    | _, Tydec_const _ ->
434
      coretype_equal ty2 ty1
435
    | Tydec_int, Tydec_int
436
    | Tydec_real, Tydec_real
437
    (* | Tydec_float , Tydec_float *)
438
    | Tydec_bool, Tydec_bool ->
439
      true
440
    | Tydec_clock ty1, Tydec_clock ty2 ->
441
      coretype_equal ty1 ty2
442
    | Tydec_array (d1, ty1), Tydec_array (d2, ty2) ->
443
      Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
444
    | Tydec_enum tl1, Tydec_enum tl2 ->
445
      List.sort compare tl1 = List.sort compare tl2
446
    | Tydec_struct fl1, Tydec_struct fl2 ->
447
      List.length fl1 = List.length fl2
448
      && List.for_all2
449
           (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
450
           (List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl1)
451
           (List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl2)
452
    | _ ->
453
      false
454
  in
455
  (*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc
456
    ty1 Printers.pp_var_type_dec_desc ty2 res;*)
457
  res
404 458

  
405 459
let tag_default = "default"
406 460

  
407 461
let const_is_bool c =
408
 match c with
409
 | Const_tag t -> t = tag_true || t = tag_false
410
 | _           -> false
462
  match c with Const_tag t -> t = tag_true || t = tag_false | _ -> false
411 463

  
412 464
(* Computes the negation of a boolean constant *)
413 465
let const_negation c =
414 466
  assert (const_is_bool c);
415 467
  match c with
416
  | Const_tag t when t = tag_true  -> Const_tag tag_false
417
  | _                              -> Const_tag tag_true
468
  | Const_tag t when t = tag_true ->
469
    Const_tag tag_false
470
  | _ ->
471
    Const_tag tag_true
418 472

  
419 473
let const_or c1 c2 =
420 474
  assert (const_is_bool c1 && const_is_bool c2);
421 475
  match c1, c2 with
422
  | Const_tag t1, _            when t1 = tag_true -> c1
423
  | _           , Const_tag t2 when t2 = tag_true -> c2
424
  | _                                             -> Const_tag tag_false
476
  | Const_tag t1, _ when t1 = tag_true ->
477
    c1
478
  | _, Const_tag t2 when t2 = tag_true ->
479
    c2
480
  | _ ->
481
    Const_tag tag_false
425 482

  
426 483
let const_and c1 c2 =
427 484
  assert (const_is_bool c1 && const_is_bool c2);
428 485
  match c1, c2 with
429
  | Const_tag t1, _            when t1 = tag_false -> c1
430
  | _           , Const_tag t2 when t2 = tag_false -> c2
431
  | _                                              -> Const_tag tag_true
486
  | Const_tag t1, _ when t1 = tag_false ->
487
    c1
488
  | _, Const_tag t2 when t2 = tag_false ->
489
    c2
490
  | _ ->
491
    Const_tag tag_true
432 492

  
433 493
let const_xor c1 c2 =
434 494
  assert (const_is_bool c1 && const_is_bool c2);
435
   match c1, c2 with
436
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
437
  | _                                         -> Const_tag tag_false
495
  match c1, c2 with
496
  | Const_tag t1, Const_tag t2 when t1 <> t2 ->
497
    Const_tag tag_true
498
  | _ ->
499
    Const_tag tag_false
438 500

  
439 501
let const_impl c1 c2 =
440 502
  assert (const_is_bool c1 && const_is_bool c2);
441 503
  match c1, c2 with
442
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
443
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
444
  | _                                             -> Const_tag tag_false
504
  | Const_tag t1, _ when t1 = tag_false ->
505
    Const_tag tag_true
506
  | _, Const_tag t2 when t2 = tag_true ->
507
    Const_tag tag_true
508
  | _ ->
509
    Const_tag tag_false
445 510

  
446 511
(* To guarantee uniqueness of tags in enum types *)
447 512
let tag_table =
448
  Utils.create_hashtable 20 [
449
   tag_true, top_bool_type;
450
   tag_false, top_bool_type
451
  ]
513
  Utils.create_hashtable 20
514
    [ tag_true, top_bool_type; tag_false, top_bool_type ]
452 515

  
453 516
(* To guarantee uniqueness of fields in struct types *)
454
let field_table =
455
  Utils.create_hashtable 20 [
456
  ]
517
let field_table = Utils.create_hashtable 20 []
457 518

  
458 519
let get_enum_type_tags cty =
459
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
460
 match cty with
461
 | Tydec_bool    -> [tag_true; tag_false]
462
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
463
                     | Tydec_enum tl -> tl
464
                     | _             -> assert false)
465
 | _            -> assert false
520
  (*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
521
  match cty with
522
  | Tydec_bool ->
523
    [ tag_true; tag_false ]
524
  | Tydec_const _ -> (
525
    match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
526
    | Tydec_enum tl ->
527
      tl
528
    | _ ->
529
      assert false)
530
  | _ ->
531
    assert false
466 532

  
467 533
let get_struct_type_fields cty =
468
 match cty with
469
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
470
                     | Tydec_struct fl -> fl
471
                     | _               -> assert false)
472
 | _            -> assert false
534
  match cty with
535
  | Tydec_const _ -> (
536
    match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
537
    | Tydec_struct fl ->
538
      fl
539
    | _ ->
540
      assert false)
541
  | _ ->
542
    assert false
473 543

  
474
let const_of_bool b =
475
 Const_tag (if b then tag_true else tag_false)
544
let const_of_bool b = Const_tag (if b then tag_true else tag_false)
476 545

  
477 546
(* let get_const c = snd (Hashtbl.find consts_table c) *)
478 547

  
479 548
let ident_of_expr expr =
480
 match expr.expr_desc with
481
 | Expr_ident id -> id
482
 | _             -> assert false
549
  match expr.expr_desc with Expr_ident id -> id | _ -> assert false
483 550

  
484 551
(* Generate a new ident expression from a declared variable *)
485 552
let expr_of_vdecl v =
486
  { expr_tag = Utils.new_tag ();
553
  {
554
    expr_tag = Utils.new_tag ();
487 555
    expr_desc = Expr_ident v.var_id;
488 556
    expr_type = v.var_type;
489 557
    expr_clock = v.var_clock;
490 558
    expr_delay = Delay.new_var ();
491 559
    expr_annot = None;
492
    expr_loc = v.var_loc }
560
    expr_loc = v.var_loc;
561
  }
493 562

  
494 563
(* Caution, returns an untyped and unclocked expression *)
495 564
let expr_of_ident id loc =
496
  {expr_tag = Utils.new_tag ();
497
   expr_desc = Expr_ident id;
498
   expr_type = Types.new_var ();
499
   expr_clock = Clocks.new_var true;
500
   expr_delay = Delay.new_var ();
501
   expr_loc = loc;
502
   expr_annot = None}
565
  {
566
    expr_tag = Utils.new_tag ();
567
    expr_desc = Expr_ident id;
568
    expr_type = Types.new_var ();
569
    expr_clock = Clocks.new_var true;
570
    expr_delay = Delay.new_var ();
571
    expr_loc = loc;
572
    expr_annot = None;
573
  }
503 574

  
504 575
let is_tuple_expr expr =
505
 match expr.expr_desc with
506
  | Expr_tuple _ -> true
507
  | _            -> false
576
  match expr.expr_desc with Expr_tuple _ -> true | _ -> false
508 577

  
509 578
let expr_list_of_expr expr =
510
  match expr.expr_desc with
511
  | Expr_tuple elist -> elist
512
  | _                -> [expr]
579
  match expr.expr_desc with Expr_tuple elist -> elist | _ -> [ expr ]
513 580

  
514 581
let expr_of_expr_list loc elist =
515
 match elist with
516
 | [t]  -> { t with expr_loc = loc }
517
 | t::_ ->
582
  match elist with
583
  | [ t ] ->
584
    { t with expr_loc = loc }
585
  | t :: _ ->
518 586
    let tlist = List.map (fun e -> e.expr_type) elist in
519 587
    let clist = List.map (fun e -> e.expr_clock) elist in
520
    { t with expr_desc = Expr_tuple elist;
521
	     expr_type = Type_predef.type_tuple tlist;
522
	     expr_clock = Clock_predef.ck_tuple clist;
523
	     expr_tag = Utils.new_tag ();
524
	     expr_loc = loc }
525
 | _    -> assert false
588
    {
589
      t with
590
      expr_desc = Expr_tuple elist;
591
      expr_type = Type_predef.type_tuple tlist;
592
      expr_clock = Clock_predef.ck_tuple clist;
593
      expr_tag = Utils.new_tag ();
594
      expr_loc = loc;
595
    }
596
  | _ ->
597
    assert false
526 598

  
527 599
let call_of_expr expr =
528
 match expr.expr_desc with
529
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
530
 | _                      -> assert false
600
  match expr.expr_desc with
601
  | Expr_appl (f, args, r) ->
602
    f, expr_list_of_expr args, r
603
  | _ ->
604
    assert false
531 605

  
532
    
533
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
606
(* Conversion from dimension expr to standard expr, for the purpose of printing,
607
   typing, etc... *)
534 608
let rec expr_of_dimension dim =
535 609
  let open Dimension in
536 610
  let expr =
537
  match dim.dim_desc with
538
 | Dbool b        ->
539
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
540
 | Dint i         ->
541
     mkexpr dim.dim_loc (Expr_const (Const_int i))
542
 | Dident id      ->
543
     mkexpr dim.dim_loc (Expr_ident id)
544
 | Dite (c, t, e) ->
545
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
546
 | Dappl (id, args) ->
547
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
548
 | Dlink dim'       -> expr_of_dimension dim'
549
 | Dvar
550
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
551
			assert false)
611
    match dim.dim_desc with
612
    | Dbool b ->
613
      mkexpr dim.dim_loc (Expr_const (const_of_bool b))
614
    | Dint i ->
615
      mkexpr dim.dim_loc (Expr_const (Const_int i))
616
    | Dident id ->
617
      mkexpr dim.dim_loc (Expr_ident id)
618
    | Dite (c, t, e) ->
619
      mkexpr dim.dim_loc
620
        (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
621
    | Dappl (id, args) ->
622
      mkexpr dim.dim_loc
623
        (Expr_appl
624
           ( id,
625
             expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args),
626
             None ))
627
    | Dlink dim' ->
628
      expr_of_dimension dim'
629
    | Dvar | Dunivar ->
630
      Format.eprintf "internal error: Corelang.expr_of_dimension %a@."
631
        Dimension.pp_dimension dim;
632
      assert false
552 633
  in
553
  { expr
554
  with
555
    expr_type = Types.new_ty Types.type_int;
556
  }
557
  
634
  { expr with expr_type = Types.new_ty Types.type_int }
635

  
558 636
let dimension_of_const loc const =
559 637
  let open Dimension in
560
 match const with
561
 | Const_int i                                    -> mkdim_int loc i
562
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
563
 | _                                              -> raise InvalidDimension
564

  
565
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
566
   into dimension expressions *)
638
  match const with
639
  | Const_int i ->
640
    mkdim_int loc i
641
  | Const_tag t when t = tag_true || t = tag_false ->
642
    mkdim_bool loc (t = tag_true)
643
  | _ ->
644
    raise InvalidDimension
645

  
646
(* Conversion from standard expr to dimension expr, for the purpose of injecting
647
   static call arguments into dimension expressions *)
567 648
let rec dimension_of_expr expr =
568 649
  let open Dimension in
569 650
  match expr.expr_desc with
570
  | Expr_const c  -> dimension_of_const expr.expr_loc c
571
  | Expr_ident id -> mkdim_ident expr.expr_loc id
651
  | Expr_const c ->
652
    dimension_of_const expr.expr_loc c
653
  | Expr_ident id ->
654
    mkdim_ident expr.expr_loc id
572 655
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
573
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
574
      if k = None then raise InvalidDimension;
575
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
576
  | Expr_ite (i, t, e)        ->
577
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
578
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
579

  
580

  
581
let sort_handlers hl =
582
 List.sort (fun (t, _) (t', _) -> compare t t') hl
656
    let k =
657
      Types.get_static_value (Env.lookup_value Basic_library.type_env f)
658
    in
659
    if k = None then raise InvalidDimension;
660
    mkdim_appl expr.expr_loc f
661
      (List.map dimension_of_expr (expr_list_of_expr args))
662
  | Expr_ite (i, t, e) ->
663
    mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t)
664
      (dimension_of_expr e)
665
  | _ ->
666
    raise InvalidDimension
667
(* not a simple dimension expression *)
668

  
669
let sort_handlers hl = List.sort (fun (t, _) (t', _) -> compare t t') hl
583 670

  
584
  
585 671
let rec is_eq_const c1 c2 =
586 672
  match c1, c2 with
587
  | Const_real r1, Const_real _
588
    -> Real.eq r1 r1 
589
  | Const_struct lcl1, Const_struct lcl2
590
    -> List.length lcl1 = List.length lcl2
591
    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
592
  | _  -> c1 = c2
593

  
594
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
595
  | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2
596
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
597
  | Expr_array el1, Expr_array el2 
598
  | Expr_tuple el1, Expr_tuple el2 -> 
599
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
600
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
601
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
602
  | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2
603
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
673
  | Const_real r1, Const_real _ ->
674
    Real.eq r1 r1
675
  | Const_struct lcl1, Const_struct lcl2 ->
676
    List.length lcl1 = List.length lcl2
677
    && List.for_all2
678
         (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2)
679
         lcl1 lcl2
680
  | _ ->
681
    c1 = c2
682

  
683
let rec is_eq_expr e1 e2 =
684
  match e1.expr_desc, e2.expr_desc with
685
  | Expr_const c1, Expr_const c2 ->
686
    is_eq_const c1 c2
687
  | Expr_ident i1, Expr_ident i2 ->
688
    i1 = i2
689
  | Expr_array el1, Expr_array el2 | Expr_tuple el1, Expr_tuple el2 ->
690
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2
691
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') ->
692
    is_eq_expr e1 e1' && is_eq_expr e2 e2'
693
  | Expr_fby (e1, e2), Expr_fby (e1', e2') ->
694
    is_eq_expr e1 e1' && is_eq_expr e2 e2'
695
  | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) ->
696
    is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2
697
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' &&
698
     is_eq_expr e2 e2' *)
604 699
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
605
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
606
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
607
  | Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl')
608
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
700
  | Expr_pre e, Expr_pre e' ->
701
    is_eq_expr e e'
702
  | Expr_when (e, i, l), Expr_when (e', i', l') ->
703
    l = l' && i = i' && is_eq_expr e e'
704
  | Expr_merge (i, hl), Expr_merge (i', hl') ->
705
    i = i'
706
    && List.for_all2
707
         (fun (t, h) (t', h') -> t = t' && is_eq_expr h h')
708
         (sort_handlers hl) (sort_handlers hl')
709
  | Expr_appl (i, e, r), Expr_appl (i', e', r') ->
710
    i = i' && r = r' && is_eq_expr e e'
609 711
  | Expr_power (e1, i1), Expr_power (e2, i2)
610
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
611
  | _ -> false
712
  | Expr_access (e1, i1), Expr_access (e2, i2) ->
713
    is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
714
  | _ ->
715
    false
612 716

  
613
let get_node_vars nd =
614
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
717
let get_node_vars nd = nd.node_inputs @ nd.node_locals @ nd.node_outputs
615 718

  
616 719
let mk_new_node_name nd id =
617 720
  let used_vars = get_node_vars nd in
618 721
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
619 722
  mk_new_name used id
620 723

  
621
let get_var id var_list =
622
  List.find (fun v -> v.var_id = id) var_list
724
let get_var id var_list = List.find (fun v -> v.var_id = id) var_list
623 725

  
624 726
let get_node_var id node =
625
  try
626
    get_var id (get_node_vars node)
627
  with Not_found -> begin
628
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
727
  try get_var id (get_node_vars node)
728
  with Not_found ->
729
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id
730
       node.node_id; *)
629 731
    raise Not_found
630
  end
631

  
632 732

  
633 733
let get_node_eqs =
634 734
  let get_eqs stmts =
635 735
    List.fold_right
636 736
      (fun stmt (res_eq, res_aut) ->
637
	match stmt with
638
	| Eq eq -> eq :: res_eq, res_aut
639
	| Aut aut -> res_eq, aut::res_aut)
640
      stmts
641
      ([], []) in
737
        match stmt with
738
        | Eq eq ->
739
          eq :: res_eq, res_aut
740
        | Aut aut ->
741
          res_eq, aut :: res_aut)
742
      stmts ([], [])
743
  in
642 744
  let table_eqs = Hashtbl.create 23 in
643
  (fun nd ->
745
  fun nd ->
644 746
    try
645
      let (old, res) = Hashtbl.find table_eqs nd.node_id
646
      in if old == nd.node_stmts then res else raise Not_found
647
    with Not_found -> 
747
      let old, res = Hashtbl.find table_eqs nd.node_id in
748
      if old == nd.node_stmts then res else raise Not_found
749
    with Not_found ->
648 750
      let res = get_eqs nd.node_stmts in
649
      begin
650
	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
651
	res
652
      end)
751
      Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
752
      res
653 753

  
654 754
let get_node_eq id node =
655 755
  let eqs, _ = get_node_eqs node in
656
  try
657
    List.find (fun eq -> List.mem id eq.eq_lhs) eqs
658
  with
659
    Not_found -> (* Shall be defined in automata auts *) raise Not_found
660
      
661
let get_nodes prog = 
662
  List.fold_left (
663
    fun nodes decl ->
756
  try List.find (fun eq -> List.mem id eq.eq_lhs) eqs
757
  with Not_found -> (* Shall be defined in automata auts *)
758
                    raise Not_found
759

  
760
let get_nodes prog =
761
  List.fold_left
762
    (fun nodes decl ->
664 763
      match decl.top_decl_desc with
665
      | Node _ -> decl::nodes
666
      | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes
667
  ) [] prog
764
      | Node _ ->
765
        decl :: nodes
766
      | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ ->
767
        nodes)
768
    [] prog
668 769
  |> List.rev
669 770

  
670
let get_imported_nodes prog = 
671
  List.fold_left (
672
    fun nodes decl ->
771
let get_imported_nodes prog =
772
  List.fold_left
773
    (fun nodes decl ->
673 774
      match decl.top_decl_desc with
674
	| ImportedNode _ -> decl::nodes
675
	| Const _ | Node _ | Include _ | Open _ | TypeDef _-> nodes  
676
  ) [] prog
677

  
678
let get_consts prog = 
679
  List.fold_right (
680
    fun decl consts ->
775
      | ImportedNode _ ->
776
        decl :: nodes
777
      | Const _ | Node _ | Include _ | Open _ | TypeDef _ ->
778
        nodes)
779
    [] prog
780

  
781
let get_consts prog =
782
  List.fold_right
783
    (fun decl consts ->
681 784
      match decl.top_decl_desc with
682
	| Const _ -> decl::consts
683
	| Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> consts  
684
  ) prog []
685

  
686
let get_typedefs prog = 
687
  List.fold_right (
688
    fun decl types ->
785
      | Const _ ->
786
        decl :: consts
787
      | Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ ->
788
        consts)
789
    prog []
790

  
791
let get_typedefs prog =
792
  List.fold_right
793
    (fun decl types ->
689 794
      match decl.top_decl_desc with
690
	| TypeDef _ -> decl::types
691
	| Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> types  
692
  ) prog []
795
      | TypeDef _ ->
796
        decl :: types
797
      | Node _ | ImportedNode _ | Include _ | Open _ | Const _ ->
798
        types)
799
    prog []
693 800

  
694 801
let get_dependencies prog =
695
  List.fold_right (
696
    fun decl deps ->
802
  List.fold_right
803
    (fun decl deps ->
697 804
      match decl.top_decl_desc with
698
	| Open _ -> decl::deps
699
	| Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> deps  
700
  ) prog []
805
      | Open _ ->
806
        decl :: deps
807
      | Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ ->
808
        deps)
809
    prog []
701 810

  
702 811
let get_node_interface nd =
703
 {nodei_id = nd.node_id;
704
  nodei_type = nd.node_type;
705
  nodei_clock = nd.node_clock;
706
  nodei_inputs = nd.node_inputs;
707
  nodei_outputs = nd.node_outputs;
708
  nodei_stateless = nd.node_dec_stateless;
709
  nodei_spec = nd.node_spec;
710
  (* nodei_annot = nd.node_annot; *)
711
  nodei_prototype = None;
712
  nodei_in_lib = [];
713
 }
812
  {
813
    nodei_id = nd.node_id;
814
    nodei_type = nd.node_type;
815
    nodei_clock = nd.node_clock;
816
    nodei_inputs = nd.node_inputs;
817
    nodei_outputs = nd.node_outputs;
818
    nodei_stateless = nd.node_dec_stateless;
819
    nodei_spec = nd.node_spec;
820
    (* nodei_annot = nd.node_annot; *)
821
    nodei_prototype = None;
822
    nodei_in_lib = [];
823
  }
714 824

  
715 825
(************************************************************************)
716
(*        Renaming / Copying                                                      *)
826
(* Renaming / Copying *)
717 827

  
718 828
let copy_var_decl vdecl =
719
  mkvar_decl
720
    vdecl.var_loc
721
    ~orig:vdecl.var_orig
722
    (
723
      vdecl.var_id,
829
  mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig
830
    ( vdecl.var_id,
724 831
      vdecl.var_dec_type,
725 832
      vdecl.var_dec_clock,
726 833
      vdecl.var_dec_const,
727 834
      vdecl.var_dec_value,
728
      vdecl.var_parent_nodeid
729
    )
835
      vdecl.var_parent_nodeid )
730 836

  
731
let copy_const cdecl =
732
  { cdecl with const_type = Types.new_var () }
837
let copy_const cdecl = { cdecl with const_type = Types.new_var () }
733 838

  
734 839
let copy_node nd =
735
  { nd with
736
    node_type     = Types.new_var ();
737
    node_clock    = Clocks.new_var true;
738
    node_inputs   = List.map copy_var_decl nd.node_inputs;
739
    node_outputs  = List.map copy_var_decl nd.node_outputs;
740
    node_locals   = List.map copy_var_decl nd.node_locals;
840
  {
841
    nd with
842
    node_type = Types.new_var ();
843
    node_clock = Clocks.new_var true;
844
    node_inputs = List.map copy_var_decl nd.node_inputs;
845
    node_outputs = List.map copy_var_decl nd.node_outputs;
846
    node_locals = List.map copy_var_decl nd.node_locals;
741 847
    node_gencalls = [];
742
    node_checks   = [];
848
    node_checks = [];
743 849
    node_stateless = None;
744 850
  }
745 851

  
746 852
let copy_top top =
747 853
  match top.top_decl_desc with
748
  | Node nd -> { top with top_decl_desc = Node (copy_node nd)  }
749
  | Const c -> { top with top_decl_desc = Const (copy_const c) }
750
  | _       -> top
854
  | Node nd ->
855
    { top with top_decl_desc = Node (copy_node nd) }
856
  | Const c ->
857
    { top with top_decl_desc = Const (copy_const c) }
858
  | _ ->
859
    top
751 860

  
752
let copy_prog top_list =
753
  List.map copy_top top_list
861
let copy_prog top_list = List.map copy_top top_list
754 862

  
755
  
756 863
let rec rename_static rename cty =
757
 match cty with
758
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
759
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
760
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
761
 | _                      -> cty
864
  match cty with
865
  | Tydec_array (d, cty') ->
866
    Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
867
  | Tydec_clock cty ->
868
    Tydec_clock (rename_static rename cty)
869
  | Tydec_struct fl ->
870
    Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
871
  | _ ->
872
    cty
762 873

  
763 874
let rename_carrier rename cck =
764
 match cck with
765
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
766
 | _             -> cck
875
  match cck with
876
  | Ckdec_bool cl ->
877
    Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
878
  | _ ->
879
    cck
767 880

  
768
 (*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
881
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
769 882

  
770 883
(* applies the renaming function [fvar] to all variables of expression [expr] *)
771
 (* let rec expr_replace_var fvar expr = *)
772
 (*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
773

  
774
 (* and expr_desc_replace_var fvar expr_desc = *)
775
 (*   match expr_desc with *)
776
 (*   | Expr_const _ -> expr_desc *)
777
 (*   | Expr_ident i -> Expr_ident (fvar i) *)
778
 (*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
779
 (*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
780
 (*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
781
 (*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
782
 (*   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *)
783
 (*   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)  *)
784
 (*   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
785
 (*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
786
 (*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
787
 (*   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *)
788
 (*   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *)
789

  
790

  
791

  
792
 let rec rename_expr  f_node f_var expr =
793
   { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
794
 and rename_expr_desc f_node f_var expr_desc =
795
   let re = rename_expr  f_node f_var in
796
   match expr_desc with
797
   | Expr_const _ -> expr_desc
798
   | Expr_ident i -> Expr_ident (f_var i)
799
   | Expr_array el -> Expr_array (List.map re el)
800
   | Expr_access (e1, d) -> Expr_access (re e1, d)
801
   | Expr_power (e1, d) -> Expr_power (re e1, d)
802
   | Expr_tuple el -> Expr_tuple (List.map re el)
803
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
804
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
805
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
806
   | Expr_pre e' -> Expr_pre (re e')
807
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
808
   | Expr_merge (i, hl) -> 
809
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
810
   | Expr_appl (i, e', i') -> 
811
     Expr_appl (f_node i, re e', Utils.option_map re i')
812
   
813
 let rename_var f_var v = {
814
     (copy_var_decl v) with
815
     var_id = f_var v.var_id;
816
     var_type = v.var_type;
817
     var_clock = v.var_clock;
818
 } 
819

  
820
 let rename_vars f_var = List.map (rename_var f_var)
821

  
822
 let rec rename_eq f_node f_var eq = { eq with
823
   eq_lhs = List.map f_var eq.eq_lhs; 
824
   eq_rhs = rename_expr f_node f_var eq.eq_rhs
825
 } 
826
 and rename_handler f_node f_var  h = {h with
827
   hand_state = f_var h.hand_state;
828
   hand_unless = List.map (
829
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
830
   ) h.hand_unless;
831
   hand_until = List.map (
832
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
833
   ) h.hand_until;
834
   hand_locals = rename_vars f_var h.hand_locals;
835
   hand_stmts = rename_stmts f_node f_var h.hand_stmts;
836
   hand_annots = rename_annots f_node f_var h.hand_annots;
837
   
838
 } 
839
 and rename_aut f_node f_var  aut = { aut with
840
   aut_id = f_var aut.aut_id;
841
   aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
842
 }
843
 and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with
844
   | Eq eq -> Eq (rename_eq f_node f_var eq)
845
   | Aut at -> Aut (rename_aut f_node f_var at))
846
   stmts
847
 and rename_annotl f_node f_var  annots = 
848
   List.map 
849
     (fun (key, value) -> key, rename_eexpr f_node f_var value) 
850
     annots
851
 and rename_annot f_node f_var annot =
852
   { annot with annots = rename_annotl f_node f_var annot.annots }
853
 and rename_annots f_node f_var annots =
854
   List.map (rename_annot f_node f_var) annots
884
(* let rec expr_replace_var fvar expr = *)
885
(*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
886

  
887
(* and expr_desc_replace_var fvar expr_desc = *)
888
(*   match expr_desc with *)
889
(*   | Expr_const _ -> expr_desc *)
890
(*   | Expr_ident i -> Expr_ident (fvar i) *)
891
(*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
892
(*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
893
(*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
894
(*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
895
(* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var
896
   fvar t, expr_replace_var fvar e) *)
897
(* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1,
898
   expr_replace_var fvar e2) *)
899
(* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var
900
   fvar e2) *)
901
(*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
902
(*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
903
(* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t,
904
   expr_replace_var fvar h)) hl) *)
905
(* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e',
906
   Utils.option_map (expr_replace_var fvar) i') *)
907

  
908
let rec rename_expr f_node f_var expr =
909
  { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
910

  
911
and rename_expr_desc f_node f_var expr_desc =
912
  let re = rename_expr f_node f_var in
913
  match expr_desc with
914
  | Expr_const _ ->
915
    expr_desc
916
  | Expr_ident i ->
917
    Expr_ident (f_var i)
918
  | Expr_array el ->
919
    Expr_array (List.map re el)
920
  | Expr_access (e1, d) ->
921
    Expr_access (re e1, d)
922
  | Expr_power (e1, d) ->
923
    Expr_power (re e1, d)
924
  | Expr_tuple el ->
925
    Expr_tuple (List.map re el)
926
  | Expr_ite (c, t, e) ->
927
    Expr_ite (re c, re t, re e)
928
  | Expr_arrow (e1, e2) ->
929
    Expr_arrow (re e1, re e2)
930
  | Expr_fby (e1, e2) ->
931
    Expr_fby (re e1, re e2)
932
  | Expr_pre e' ->
933
    Expr_pre (re e')
934
  | Expr_when (e', i, l) ->
935
    Expr_when (re e', f_var i, l)
936
  | Expr_merge (i, hl) ->
937
    Expr_merge (f_var i, List.map (fun (t, h) -> t, re h) hl)
938
  | Expr_appl (i, e', i') ->
939
    Expr_appl (f_node i, re e', Utils.option_map re i')
940

  
941
let rename_var f_var v =
942
  {
943
    (copy_var_decl v) with
944
    var_id = f_var v.var_id;
945
    var_type = v.var_type;
946
    var_clock = v.var_clock;
947
  }
948

  
949
let rename_vars f_var = List.map (rename_var f_var)
950

  
951
let rec rename_eq f_node f_var eq =
952
  {
953
    eq with
954
    eq_lhs = List.map f_var eq.eq_lhs;
955
    eq_rhs = rename_expr f_node f_var eq.eq_rhs;
956
  }
957

  
958
and rename_handler f_node f_var h =
959
  {
960
    h with
961
    hand_state = f_var h.hand_state;
962
    hand_unless =
963
      List.map
964
        (fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id)
965
        h.hand_unless;
966
    hand_until =
967
      List.map
968
        (fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id)
969
        h.hand_until;
970
    hand_locals = rename_vars f_var h.hand_locals;
971
    hand_stmts = rename_stmts f_node f_var h.hand_stmts;
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff