Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 9a9058f4

History | View | Annotate | Download (40 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Format
13
open Lustre_types
14
open Machine_code_types
15
(*open Dimension*)
16

    
17

    
18
exception Error of Location.t * Error.error_kind
19

    
20
module VDeclModule =
21
struct (* Node module *)
22
  type t = var_decl
23
  let compare v1 v2 = compare v1.var_id v2.var_id
24
end
25

    
26
module VMap = Map.Make(VDeclModule)
27

    
28
module VSet : Set.S with type elt = var_decl = Set.Make(VDeclModule)
29

    
30
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
31

    
32
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
33

    
34

    
35

    
36
(************************************************************)
37
(* *)
38

    
39
let mktyp loc d =
40
  { ty_dec_desc = d; ty_dec_loc = loc }
41

    
42
let mkclock loc d =
43
  { ck_dec_desc = d; ck_dec_loc = loc }
44

    
45
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) =
46
  assert (value = None || is_const);
47
  { var_id = id;
48
    var_orig = orig;
49
    var_dec_type = ty_dec;
50
    var_dec_clock = ck_dec;
51
    var_dec_const = is_const;
52
    var_dec_value = value;
53
    var_parent_nodeid = parentid;
54
    var_type = Types.new_var ();
55
    var_clock = Clocks.new_var true;
56
    var_loc = loc }
57

    
58
let dummy_var_decl name typ =
59
  {
60
    var_id = name;
61
    var_orig = false;
62
    var_dec_type = dummy_type_dec;
63
    var_dec_clock = dummy_clock_dec;
64
    var_dec_const = false;
65
    var_dec_value = None;
66
    var_parent_nodeid = None;
67
    var_type =  typ;
68
    var_clock = Clocks.new_ck Clocks.Cvar true;
69
    var_loc = Location.dummy_loc
70
  }
71

    
72
let mkexpr loc d =
73
  { expr_tag = Utils.new_tag ();
74
    expr_desc = d;
75
    expr_type = Types.new_var ();
76
    expr_clock = Clocks.new_var true;
77
    expr_delay = Delay.new_var ();
78
    expr_annot = None;
79
    expr_loc = loc }
80

    
81
let var_decl_of_const ?(parentid=None) c =
82
  { var_id = c.const_id;
83
    var_orig = true;
84
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
85
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
86
    var_dec_const = true;
87
    var_dec_value = None;
88
    var_parent_nodeid = parentid;
89
    var_type = c.const_type;
90
    var_clock = Clocks.new_var false;
91
    var_loc = c.const_loc }
92

    
93
let mk_new_name used id =
94
  let rec new_name name cpt =
95
    if used name
96
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
97
    else name
98
  in new_name id 1
99

    
100
let mkeq loc (lhs, rhs) =
101
  { eq_lhs = lhs;
102
    eq_rhs = rhs;
103
    eq_loc = loc }
104

    
105
let mkassert loc expr =
106
  { assert_loc = loc;
107
    assert_expr = expr
108
  }
109

    
110
let mktop_decl loc own itf d =
111
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
112

    
113
let mkpredef_call loc funname args =
114
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
115

    
116
let is_clock_dec_type cty =
117
  match cty with
118
  | Tydec_clock _ -> true
119
  | _             -> false
120

    
121
let const_of_top top_decl =
122
  match top_decl.top_decl_desc with
123
  | Const c -> c
124
  | _ -> assert false
125

    
126
let node_of_top top_decl =
127
  match top_decl.top_decl_desc with
128
  | Node nd -> nd
129
  | _ -> raise Not_found
130

    
131
let imported_node_of_top top_decl =
132
  match top_decl.top_decl_desc with
133
  | ImportedNode ind -> ind
134
  | _ -> assert false
135

    
136
let typedef_of_top top_decl =
137
  match top_decl.top_decl_desc with
138
  | TypeDef tdef -> tdef
139
  | _ -> assert false
140

    
141
let dependency_of_top top_decl =
142
  match top_decl.top_decl_desc with
143
  | Open (local, dep) -> (local, dep)
144
  | _ -> assert false
145

    
146
let consts_of_enum_type top_decl =
147
  match top_decl.top_decl_desc with
148
  | TypeDef tdef ->
149
    (match tdef.tydef_desc with
150
    | Tydec_enum tags ->
151
       List.map
152
	 (fun tag ->
153
	   let cdecl = {
154
	     const_id = tag;
155
	     const_loc = top_decl.top_decl_loc;
156
	     const_value = Const_tag tag;
157
	     const_type = Type_predef.type_const tdef.tydef_id
158
	   } in
159
	   { top_decl with top_decl_desc = Const cdecl })
160
	 tags
161
     | _               -> [])
162
  | _ -> assert false
163

    
164
(************************************************************)
165
(*   Eexpr functions *)
166
(************************************************************)
167

    
168
let merge_node_annot ann1 ann2 =
169
  { requires = ann1.requires @ ann2.requires;
170
    ensures = ann1.ensures @ ann2.ensures;
171
    behaviors = ann1.behaviors @ ann2.behaviors;
172
    spec_loc = ann1.spec_loc
173
  }
174

    
175
let mkeexpr loc expr =
176
  { eexpr_tag = Utils.new_tag ();
177
    eexpr_qfexpr = expr;
178
    eexpr_quantifiers = [];
179
    eexpr_type = Types.new_var ();
180
    eexpr_clock = Clocks.new_var true;
181
    eexpr_normalized = None;
182
    eexpr_loc = loc }
183

    
184
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
185

    
186
(*
187
let mkepredef_call loc funname args =
188
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
189

    
190
let mkepredef_unary_call loc funname arg =
191
  mkeexpr loc (EExpr_appl (funname, arg, None))
192
*)
193

    
194
let merge_expr_annot ann1 ann2 =
195
  match ann1, ann2 with
196
    | None, None -> assert false
197
    | Some _, None -> ann1
198
    | None, Some _ -> ann2
199
    | Some ann1, Some ann2 -> Some {
200
      annots = ann1.annots @ ann2.annots;
201
      annot_loc = ann1.annot_loc
202
    }
203

    
204
let update_expr_annot node_id e annot =
205
  List.iter (fun (key, _) -> 
206
    Annotations.add_expr_ann node_id e.expr_tag key
207
  ) annot.annots;
208
  e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
209
  e
210

    
211

    
212
let mkinstr ?lustre_expr ?lustre_eq i =
213
  {
214
    instr_desc = i;
215
    (* lustre_expr = lustre_expr; *)
216
    lustre_eq = lustre_eq;
217
  }
218

    
219
let get_instr_desc i = i.instr_desc
220
let update_instr_desc i id = { i with instr_desc = id }
221

    
222
(***********************************************************)
223
(* Fast access to nodes, by name *)
224
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
225
let consts_table = Hashtbl.create 30
226

    
227
let print_node_table fmt () =
228
  begin
229
    Format.fprintf fmt "{ /* node table */@.";
230
    Hashtbl.iter (fun id nd ->
231
      Format.fprintf fmt "%s |-> %a"
232
	id
233
	Printers.pp_short_decl nd
234
    ) node_table;
235
    Format.fprintf fmt "}@."
236
  end
237

    
238
let print_consts_table fmt () =
239
  begin
240
    Format.fprintf fmt "{ /* consts table */@.";
241
    Hashtbl.iter (fun id const ->
242
      Format.fprintf fmt "%s |-> %a"
243
	id
244
	Printers.pp_const_decl (const_of_top const)
245
    ) consts_table;
246
    Format.fprintf fmt "}@."
247
  end
248

    
249
let node_name td =
250
    match td.top_decl_desc with 
251
    | Node nd         -> nd.node_id
252
    | ImportedNode nd -> nd.nodei_id
253
    | _ -> assert false
254

    
255
let is_generic_node td =
256
  match td.top_decl_desc with 
257
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
258
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
259
  | _ -> assert false
260

    
261
let node_inputs td =
262
  match td.top_decl_desc with 
263
  | Node nd         -> nd.node_inputs
264
  | ImportedNode nd -> nd.nodei_inputs
265
  | _ -> assert false
266

    
267
let node_from_name id =
268
  try
269
    Hashtbl.find node_table id
270
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
271
		     assert false)
272

    
273
let is_imported_node td =
274
  match td.top_decl_desc with 
275
  | Node nd         -> false
276
  | ImportedNode nd -> true
277
  | _ -> assert false
278

    
279

    
280
(* alias and type definition table *)
281

    
282
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
283

    
284
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
285
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
286
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
287
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
288

    
289
let type_table =
290
  Utils.create_hashtable 20 [
291
    Tydec_int  , top_int_type;
292
    Tydec_bool , top_bool_type;
293
    (* Tydec_float, top_float_type; *)
294
    Tydec_real , top_real_type
295
  ]
296

    
297
let print_type_table fmt () =
298
  begin
299
    Format.fprintf fmt "{ /* type table */@.";
300
    Hashtbl.iter (fun tydec tdef ->
301
      Format.fprintf fmt "%a |-> %a"
302
	Printers.pp_var_type_dec_desc tydec
303
	Printers.pp_typedef (typedef_of_top tdef)
304
    ) type_table;
305
    Format.fprintf fmt "}@."
306
  end
307

    
308
let rec is_user_type typ =
309
  match typ with
310
  | Tydec_int | Tydec_bool | Tydec_real 
311
  (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
312
  | Tydec_clock typ' -> is_user_type typ'
313
  | _ -> true
314

    
315
let get_repr_type typ =
316
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
317
  if is_user_type typ_def then typ else typ_def
318

    
319
let rec coretype_equal ty1 ty2 =
320
  let res =
321
  match ty1, ty2 with
322
  | Tydec_any           , _
323
  | _                   , Tydec_any             -> assert false
324
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
325
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
326
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
327
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
328
  | Tydec_int           , Tydec_int
329
  | Tydec_real          , Tydec_real
330
  (* | Tydec_float         , Tydec_float *)
331
  | Tydec_bool          , Tydec_bool            -> true
332
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
333
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
334
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
335
  | Tydec_struct fl1    , Tydec_struct fl2      ->
336
       List.length fl1 = List.length fl2
337
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
338
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
339
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
340
  | _                                  -> false
341
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
342

    
343
let tag_true = "true"
344
let tag_false = "false"
345
let tag_default = "default"
346

    
347
let const_is_bool c =
348
 match c with
349
 | Const_tag t -> t = tag_true || t = tag_false
350
 | _           -> false
351

    
352
(* Computes the negation of a boolean constant *)
353
let const_negation c =
354
  assert (const_is_bool c);
355
  match c with
356
  | Const_tag t when t = tag_true  -> Const_tag tag_false
357
  | _                              -> Const_tag tag_true
358

    
359
let const_or c1 c2 =
360
  assert (const_is_bool c1 && const_is_bool c2);
361
  match c1, c2 with
362
  | Const_tag t1, _            when t1 = tag_true -> c1
363
  | _           , Const_tag t2 when t2 = tag_true -> c2
364
  | _                                             -> Const_tag tag_false
365

    
366
let const_and c1 c2 =
367
  assert (const_is_bool c1 && const_is_bool c2);
368
  match c1, c2 with
369
  | Const_tag t1, _            when t1 = tag_false -> c1
370
  | _           , Const_tag t2 when t2 = tag_false -> c2
371
  | _                                              -> Const_tag tag_true
372

    
373
let const_xor c1 c2 =
374
  assert (const_is_bool c1 && const_is_bool c2);
375
   match c1, c2 with
376
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
377
  | _                                         -> Const_tag tag_false
378

    
379
let const_impl c1 c2 =
380
  assert (const_is_bool c1 && const_is_bool c2);
381
  match c1, c2 with
382
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
383
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
384
  | _                                             -> Const_tag tag_false
385

    
386
(* To guarantee uniqueness of tags in enum types *)
387
let tag_table =
388
  Utils.create_hashtable 20 [
389
   tag_true, top_bool_type;
390
   tag_false, top_bool_type
391
  ]
392

    
393
(* To guarantee uniqueness of fields in struct types *)
394
let field_table =
395
  Utils.create_hashtable 20 [
396
  ]
397

    
398
let get_enum_type_tags cty =
399
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
400
 match cty with
401
 | Tydec_bool    -> [tag_true; tag_false]
402
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
403
                     | Tydec_enum tl -> tl
404
                     | _             -> assert false)
405
 | _            -> assert false
406

    
407
let get_struct_type_fields cty =
408
 match cty with
409
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
410
                     | Tydec_struct fl -> fl
411
                     | _               -> assert false)
412
 | _            -> assert false
413

    
414
let const_of_bool b =
415
 Const_tag (if b then tag_true else tag_false)
416

    
417
(* let get_const c = snd (Hashtbl.find consts_table c) *)
418

    
419
let ident_of_expr expr =
420
 match expr.expr_desc with
421
 | Expr_ident id -> id
422
 | _             -> assert false
423

    
424
(* Generate a new ident expression from a declared variable *)
425
let expr_of_vdecl v =
426
  { expr_tag = Utils.new_tag ();
427
    expr_desc = Expr_ident v.var_id;
428
    expr_type = v.var_type;
429
    expr_clock = v.var_clock;
430
    expr_delay = Delay.new_var ();
431
    expr_annot = None;
432
    expr_loc = v.var_loc }
433

    
434
(* Caution, returns an untyped and unclocked expression *)
435
let expr_of_ident id loc =
436
  {expr_tag = Utils.new_tag ();
437
   expr_desc = Expr_ident id;
438
   expr_type = Types.new_var ();
439
   expr_clock = Clocks.new_var true;
440
   expr_delay = Delay.new_var ();
441
   expr_loc = loc;
442
   expr_annot = None}
443

    
444
let is_tuple_expr expr =
445
 match expr.expr_desc with
446
  | Expr_tuple _ -> true
447
  | _            -> false
448

    
449
let expr_list_of_expr expr =
450
  match expr.expr_desc with
451
  | Expr_tuple elist -> elist
452
  | _                -> [expr]
453

    
454
let expr_of_expr_list loc elist =
455
 match elist with
456
 | [t]  -> { t with expr_loc = loc }
457
 | t::_ ->
458
    let tlist = List.map (fun e -> e.expr_type) elist in
459
    let clist = List.map (fun e -> e.expr_clock) elist in
460
    { t with expr_desc = Expr_tuple elist;
461
	     expr_type = Type_predef.type_tuple tlist;
462
	     expr_clock = Clock_predef.ck_tuple clist;
463
	     expr_tag = Utils.new_tag ();
464
	     expr_loc = loc }
465
 | _    -> assert false
466

    
467
let call_of_expr expr =
468
 match expr.expr_desc with
469
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
470
 | _                      -> assert false
471

    
472
    
473
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
474
let rec expr_of_dimension dim =
475
  let open Dimension in
476
  match dim.dim_desc with
477
 | Dbool b        ->
478
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
479
 | Dint i         ->
480
     mkexpr dim.dim_loc (Expr_const (Const_int i))
481
 | Dident id      ->
482
     mkexpr dim.dim_loc (Expr_ident id)
483
 | Dite (c, t, e) ->
484
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
485
 | Dappl (id, args) ->
486
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
487
 | Dlink dim'       -> expr_of_dimension dim'
488
 | Dvar
489
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
490
			assert false)
491

    
492
let dimension_of_const loc const =
493
  let open Dimension in
494
 match const with
495
 | Const_int i                                    -> mkdim_int loc i
496
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
497
 | _                                              -> raise InvalidDimension
498

    
499
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
500
   into dimension expressions *)
501
let rec dimension_of_expr expr =
502
  let open Dimension in
503
  match expr.expr_desc with
504
  | Expr_const c  -> dimension_of_const expr.expr_loc c
505
  | Expr_ident id -> mkdim_ident expr.expr_loc id
506
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
507
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
508
      if k = None then raise InvalidDimension;
509
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
510
  | Expr_ite (i, t, e)        ->
511
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
512
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
513

    
514

    
515
let sort_handlers hl =
516
 List.sort (fun (t, _) (t', _) -> compare t t') hl
517

    
518
let num_10 = Num.num_of_int 10
519

    
520
let cst_real_to_num n i =
521
  Num.(n // (num_10 **/ (num_of_int i)))
522

    
523
let rec is_eq_const c1 c2 =
524
  match c1, c2 with
525
  | Const_real (n1, i1, _), Const_real (n2, i2, _)
526
    -> let n1 = cst_real_to_num n1 i1 in
527
       let n2 = cst_real_to_num n2 i2 in
528
	    Num.eq_num n1 n2
529
  | Const_struct lcl1, Const_struct lcl2
530
    -> List.length lcl1 = List.length lcl2
531
    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
532
  | _  -> c1 = c2
533

    
534
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
535
  | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2
536
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
537
  | Expr_array el1, Expr_array el2 
538
  | Expr_tuple el1, Expr_tuple el2 -> 
539
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
540
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
541
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
542
  | 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
543
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
544
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
545
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
546
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
547
  | 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')
548
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
549
  | Expr_power (e1, i1), Expr_power (e2, i2)
550
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
551
  | _ -> false
552

    
553
let get_node_vars nd =
554
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
555

    
556
let mk_new_node_name nd id =
557
  let used_vars = get_node_vars nd in
558
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
559
  mk_new_name used id
560

    
561
let get_var id var_list =
562
  List.find (fun v -> v.var_id = id) var_list
563

    
564
let get_node_var id node =
565
  try
566
    get_var id (get_node_vars node)
567
  with Not_found -> begin
568
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
569
    raise Not_found
570
  end
571

    
572

    
573
let get_node_eqs =
574
  let get_eqs stmts =
575
    List.fold_right
576
      (fun stmt (res_eq, res_aut) ->
577
	match stmt with
578
	| Eq eq -> eq :: res_eq, res_aut
579
	| Aut aut -> res_eq, aut::res_aut)
580
      stmts
581
      ([], []) in
582
  let table_eqs = Hashtbl.create 23 in
583
  (fun nd ->
584
    try
585
      let (old, res) = Hashtbl.find table_eqs nd.node_id
586
      in if old == nd.node_stmts then res else raise Not_found
587
    with Not_found -> 
588
      let res = get_eqs nd.node_stmts in
589
      begin
590
	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
591
	res
592
      end)
593

    
594
let get_node_eq id node =
595
  let eqs, auts = get_node_eqs node in
596
  try
597
    List.find (fun eq -> List.mem id eq.eq_lhs) eqs
598
  with
599
    Not_found -> (* Shall be defined in automata auts *) raise Not_found
600
      
601
let get_nodes prog = 
602
  List.fold_left (
603
    fun nodes decl ->
604
      match decl.top_decl_desc with
605
	| Node _ -> decl::nodes
606
	| Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes  
607
  ) [] prog
608

    
609
let get_imported_nodes prog = 
610
  List.fold_left (
611
    fun nodes decl ->
612
      match decl.top_decl_desc with
613
	| ImportedNode _ -> decl::nodes
614
	| Const _ | Node _ | Open _ | TypeDef _-> nodes  
615
  ) [] prog
616

    
617
let get_consts prog = 
618
  List.fold_right (
619
    fun decl consts ->
620
      match decl.top_decl_desc with
621
	| Const _ -> decl::consts
622
	| Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts  
623
  ) prog []
624

    
625
let get_typedefs prog = 
626
  List.fold_right (
627
    fun decl types ->
628
      match decl.top_decl_desc with
629
	| TypeDef _ -> decl::types
630
	| Node _ | ImportedNode _ | Open _ | Const _ -> types  
631
  ) prog []
632

    
633
let get_dependencies prog =
634
  List.fold_right (
635
    fun decl deps ->
636
      match decl.top_decl_desc with
637
	| Open _ -> decl::deps
638
	| Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps  
639
  ) prog []
640

    
641
let get_node_interface nd =
642
 {nodei_id = nd.node_id;
643
  nodei_type = nd.node_type;
644
  nodei_clock = nd.node_clock;
645
  nodei_inputs = nd.node_inputs;
646
  nodei_outputs = nd.node_outputs;
647
  nodei_stateless = nd.node_dec_stateless;
648
  nodei_spec = nd.node_spec;
649
  (* nodei_annot = nd.node_annot; *)
650
  nodei_prototype = None;
651
  nodei_in_lib = [];
652
 }
653

    
654
(************************************************************************)
655
(*        Renaming                                                      *)
656

    
657
let rec rename_static rename cty =
658
 match cty with
659
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
660
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
661
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
662
 | _                      -> cty
663

    
664
let rec rename_carrier rename cck =
665
 match cck with
666
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
667
 | _             -> cck
668

    
669
 (*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
670

    
671
(* applies the renaming function [fvar] to all variables of expression [expr] *)
672
 (* let rec expr_replace_var fvar expr = *)
673
 (*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
674

    
675
 (* and expr_desc_replace_var fvar expr_desc = *)
676
 (*   match expr_desc with *)
677
 (*   | Expr_const _ -> expr_desc *)
678
 (*   | Expr_ident i -> Expr_ident (fvar i) *)
679
 (*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
680
 (*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
681
 (*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
682
 (*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
683
 (*   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *)
684
 (*   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)  *)
685
 (*   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
686
 (*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
687
 (*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
688
 (*   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *)
689
 (*   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *)
690

    
691

    
692

    
693
 let rec rename_expr  f_node f_var expr =
694
   { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
695
 and rename_expr_desc f_node f_var expr_desc =
696
   let re = rename_expr  f_node f_var in
697
   match expr_desc with
698
   | Expr_const _ -> expr_desc
699
   | Expr_ident i -> Expr_ident (f_var i)
700
   | Expr_array el -> Expr_array (List.map re el)
701
   | Expr_access (e1, d) -> Expr_access (re e1, d)
702
   | Expr_power (e1, d) -> Expr_power (re e1, d)
703
   | Expr_tuple el -> Expr_tuple (List.map re el)
704
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
705
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
706
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
707
   | Expr_pre e' -> Expr_pre (re e')
708
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
709
   | Expr_merge (i, hl) -> 
710
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
711
   | Expr_appl (i, e', i') -> 
712
     Expr_appl (f_node i, re e', Utils.option_map re i')
713

    
714
 let rename_dec_type f_node f_var t = assert false (*
715
						     Types.rename_dim_type (Dimension.rename f_node f_var) t*)
716

    
717
 let rename_dec_clock f_node f_var c = assert false (* 
718
					  Clocks.rename_clock_expr f_var c*)
719
   
720
 let rename_var f_node f_var v = {
721
   v with
722
     var_id = f_var v.var_id;
723
     var_dec_type = rename_dec_type f_node f_var v.var_type;
724
     var_dec_clock = rename_dec_clock f_node f_var v.var_clock
725
 } 
726

    
727
 let rename_vars f_node f_var = List.map (rename_var f_node f_var) 
728

    
729
 let rec rename_eq f_node f_var eq = { eq with
730
   eq_lhs = List.map f_var eq.eq_lhs; 
731
   eq_rhs = rename_expr f_node f_var eq.eq_rhs
732
 } 
733
 and rename_handler f_node f_var  h = {h with
734
   hand_state = f_var h.hand_state;
735
   hand_unless = List.map (
736
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
737
   ) h.hand_unless;
738
   hand_until = List.map (
739
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
740
   ) h.hand_until;
741
   hand_locals = rename_vars f_node f_var h.hand_locals;
742
   hand_stmts = rename_stmts f_node f_var h.hand_stmts;
743
   hand_annots = rename_annots f_node f_var h.hand_annots;
744
   
745
 } 
746
 and rename_aut f_node f_var  aut = { aut with
747
   aut_id = f_var aut.aut_id;
748
   aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
749
 }
750
 and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with
751
   | Eq eq -> Eq (rename_eq f_node f_var eq)
752
   | Aut at -> Aut (rename_aut f_node f_var at))
753
   stmts
754
 and rename_annotl f_node f_var  annots = 
755
   List.map 
756
     (fun (key, value) -> key, rename_eexpr f_node f_var value) 
757
     annots
758
 and rename_annot f_node f_var annot =
759
   { annot with annots = rename_annotl f_node f_var annot.annots }
760
 and rename_annots f_node f_var annots =
761
   List.map (rename_annot f_node f_var) annots
762
and rename_eexpr f_node f_var ee =
763
   { ee with
764
     eexpr_tag = Utils.new_tag ();
765
     eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
766
     eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
767
     eexpr_normalized = Utils.option_map 
768
       (fun (vdecl, eqs, vdecls) ->
769
	 rename_var f_node f_var vdecl,
770
	 List.map (rename_eq f_node f_var) eqs,
771
	 rename_vars f_node f_var vdecls
772
       ) ee.eexpr_normalized;
773
     
774
   }
775
 
776
     
777
     
778
   
779
 let rename_node f_node f_var nd =
780
   let rename_var = rename_var f_node f_var in
781
   let rename_expr = rename_expr f_node f_var in
782
   let rename_stmts = rename_stmts f_node f_var in
783
   let inputs = List.map rename_var nd.node_inputs in
784
   let outputs = List.map rename_var nd.node_outputs in
785
   let locals = List.map rename_var nd.node_locals in
786
   let gen_calls = List.map rename_expr nd.node_gencalls in
787
   let node_checks = List.map (Dimension.rename f_node f_var)  nd.node_checks in
788
   let node_asserts = List.map 
789
     (fun a -> 
790
       {a with assert_expr = 
791
	   let expr = a.assert_expr in
792
	   rename_expr expr})
793
     nd.node_asserts
794
   in
795
   let node_stmts = rename_stmts nd.node_stmts
796

    
797
     
798
   in
799
   let spec = 
800
     Utils.option_map 
801
       (fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *) 
802
       nd.node_spec 
803
   in
804
   let annot = rename_annots f_node f_var nd.node_annot in
805
   {
806
     node_id = f_node nd.node_id;
807
     node_type = nd.node_type;
808
     node_clock = nd.node_clock;
809
     node_inputs = inputs;
810
     node_outputs = outputs;
811
     node_locals = locals;
812
     node_gencalls = gen_calls;
813
     node_checks = node_checks;
814
     node_asserts = node_asserts;
815
     node_stmts = node_stmts;
816
     node_dec_stateless = nd.node_dec_stateless;
817
     node_stateless = nd.node_stateless;
818
     node_spec = spec;
819
     node_annot = annot;
820
   }
821

    
822

    
823
let rename_const f_const c =
824
  { c with const_id = f_const c.const_id }
825

    
826
let rename_typedef f_var t =
827
  match t.tydef_desc with
828
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
829
  | _               -> t
830

    
831
let rename_prog f_node f_var f_const prog =
832
  List.rev (
833
    List.fold_left (fun accu top ->
834
      (match top.top_decl_desc with
835
      | Node nd -> 
836
	 { top with top_decl_desc = Node (rename_node f_node f_var nd) }
837
      | Const c -> 
838
	 { top with top_decl_desc = Const (rename_const f_const c) }
839
      | TypeDef tdef ->
840
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
841
      | ImportedNode _
842
      | Open _       -> top)
843
      ::accu
844
) [] prog
845
		   )
846

    
847
(* Applies the renaming function [fvar] to every rhs
848
   only when the corresponding lhs satisfies predicate [pvar] *)
849
 let eq_replace_rhs_var pvar fvar eq =
850
   let pvar l = List.exists pvar l in
851
   let rec replace lhs rhs =
852
     { rhs with expr_desc =
853
     match lhs with
854
     | []  -> assert false
855
     | [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc
856
     | _   ->
857
       (match rhs.expr_desc with
858
       | Expr_tuple tl ->
859
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
860
       | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
861
	 let args = expr_list_of_expr arg in
862
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
863
       | Expr_array _
864
       | Expr_access _
865
       | Expr_power _
866
       | Expr_const _
867
       | Expr_ident _
868
       | Expr_appl _   ->
869
	 if pvar lhs
870
	 then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
871
	 else rhs.expr_desc
872
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
873
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
874
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
875
       | Expr_pre e'          -> Expr_pre (replace lhs e')
876
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
877
				 in Expr_when (replace lhs e', i', l)
878
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
879
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
880
       )
881
     }
882
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
883

    
884
    
885
(**********************************************************************)
886
(* Pretty printers *)
887

    
888
let pp_decl_type fmt tdecl =
889
  match tdecl.top_decl_desc with
890
  | Node nd ->
891
    fprintf fmt "%s: " nd.node_id;
892
    Utils.reset_names ();
893
    fprintf fmt "%a@ " Types.print_ty nd.node_type
894
  | ImportedNode ind ->
895
    fprintf fmt "%s: " ind.nodei_id;
896
    Utils.reset_names ();
897
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
898
  | Const _ | Open _ | TypeDef _ -> ()
899

    
900
let pp_prog_type fmt tdecl_list =
901
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
902

    
903
let pp_decl_clock fmt cdecl =
904
  match cdecl.top_decl_desc with
905
  | Node nd ->
906
    fprintf fmt "%s: " nd.node_id;
907
    Utils.reset_names ();
908
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
909
  | ImportedNode ind ->
910
    fprintf fmt "%s: " ind.nodei_id;
911
    Utils.reset_names ();
912
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
913
  | Const _ | Open _ | TypeDef _ -> ()
914

    
915
let pp_prog_clock fmt prog =
916
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
917

    
918

    
919
(* filling node table with internal functions *)
920
let vdecls_of_typ_ck cpt ty =
921
  let loc = Location.dummy_loc in
922
  List.map
923
    (fun _ -> incr cpt;
924
              let name = sprintf "_var_%d" !cpt in
925
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
926
    (Types.type_list_of_type ty)
927

    
928
let mk_internal_node id =
929
  let spec = None in
930
  let ty = Env.lookup_value Basic_library.type_env id in
931
  let ck = Env.lookup_value Basic_library.clock_env id in
932
  let (tin, tout) = Types.split_arrow ty in
933
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
934
  let cpt = ref (-1) in
935
  mktop
936
    (ImportedNode
937
       {nodei_id = id;
938
	nodei_type = ty;
939
	nodei_clock = ck;
940
	nodei_inputs = vdecls_of_typ_ck cpt tin;
941
	nodei_outputs = vdecls_of_typ_ck cpt tout;
942
	nodei_stateless = Types.get_static_value ty <> None;
943
	nodei_spec = spec;
944
	(* nodei_annot = []; *)
945
	nodei_prototype = None;
946
       	nodei_in_lib = [];
947
       })
948

    
949
let add_internal_funs () =
950
  List.iter
951
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
952
    Basic_library.internal_funs
953

    
954

    
955

    
956
(* Replace any occurence of a var in vars_to_replace by its associated
957
   expression in defs until e does not contain any such variables *)
958
let rec substitute_expr vars_to_replace defs e =
959
  let se = substitute_expr vars_to_replace defs in
960
  { e with expr_desc = 
961
      let ed = e.expr_desc in
962
      match ed with
963
      | Expr_const _ -> ed
964
      | Expr_array el -> Expr_array (List.map se el)
965
      | Expr_access (e1, d) -> Expr_access (se e1, d)
966
      | Expr_power (e1, d) -> Expr_power (se e1, d)
967
      | Expr_tuple el -> Expr_tuple (List.map se el)
968
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
969
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
970
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
971
      | Expr_pre e' -> Expr_pre (se e')
972
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
973
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
974
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
975
      | Expr_ident i -> 
976
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
977
	  let eq_i eq = eq.eq_lhs = [i] in
978
	  if List.exists eq_i defs then
979
	    let sub = List.find eq_i defs in
980
	    let sub' = se sub.eq_rhs in
981
	    sub'.expr_desc
982
	  else 
983
	    assert false
984
	)
985
	else
986
	  ed
987

    
988
  }
989
  
990
 let rec expr_to_eexpr  expr =
991
   { eexpr_tag = expr.expr_tag;
992
     eexpr_qfexpr = expr;
993
     eexpr_quantifiers = [];
994
     eexpr_type = expr.expr_type;
995
     eexpr_clock = expr.expr_clock;
996
     eexpr_loc = expr.expr_loc;
997
     eexpr_normalized = None
998
   }
999
 (* and expr_desc_to_eexpr_desc expr_desc = *)
1000
 (*   let conv = expr_to_eexpr in *)
1001
 (*   match expr_desc with *)
1002
 (*   | Expr_const c -> EExpr_const (match c with *)
1003
 (*     | Const_int x -> EConst_int x  *)
1004
 (*     | Const_real x -> EConst_real x  *)
1005
 (*     | Const_float x -> EConst_float x  *)
1006
 (*     | Const_tag x -> EConst_tag x  *)
1007
 (*     | _ -> assert false *)
1008

    
1009
 (*   ) *)
1010
 (*   | Expr_ident i -> EExpr_ident i *)
1011
 (*   | Expr_tuple el -> EExpr_tuple (List.map conv el) *)
1012

    
1013
 (*   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)  *)
1014
 (*   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *)
1015
 (*   | Expr_pre e' -> EExpr_pre (conv e') *)
1016
 (*   | Expr_appl (i, e', i') ->  *)
1017
 (*     EExpr_appl  *)
1018
 (*       (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *)
1019

    
1020
 (*   | Expr_when _ *)
1021
 (*   | Expr_merge _ -> assert false *)
1022
 (*   | Expr_array _  *)
1023
 (*   | Expr_access _  *)
1024
 (*   | Expr_power _  -> assert false *)
1025
 (*   | Expr_ite (c, t, e) -> assert false  *)
1026
 (*   | _ -> assert false *)
1027
      
1028
     
1029
let rec get_expr_calls nodes e =
1030
  let get_calls = get_expr_calls nodes in
1031
  match e.expr_desc with
1032
  | Expr_const _ 
1033
   | Expr_ident _ -> Utils.ISet.empty
1034
   | Expr_tuple el
1035
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
1036
   | Expr_pre e1 
1037
   | Expr_when (e1, _, _) 
1038
   | Expr_access (e1, _) 
1039
   | Expr_power (e1, _) -> get_calls e1
1040
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
1041
   | Expr_arrow (e1, e2) 
1042
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
1043
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
1044
   | Expr_appl (i, e', i') -> 
1045
     if Basic_library.is_expr_internal_fun e then 
1046
       (get_calls e') 
1047
     else
1048
       let calls =  Utils.ISet.add i (get_calls e') in
1049
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
1050
       if List.exists test nodes then
1051
	 match (List.find test nodes).top_decl_desc with
1052
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
1053
	 | _ -> assert false
1054
       else 
1055
	 calls
1056

    
1057
and get_eq_calls nodes eq =
1058
  get_expr_calls nodes eq.eq_rhs
1059
and get_aut_handler_calls nodes h =
1060
  List.fold_left (fun accu stmt -> match stmt with
1061
  | Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu
1062
  | Aut aut' ->  Utils.ISet.union (get_aut_calls nodes aut') accu
1063
  ) Utils.ISet.empty h.hand_stmts 
1064
and get_aut_calls nodes aut =
1065
  List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)
1066
    Utils.ISet.empty aut.aut_handlers
1067
and get_node_calls nodes node =
1068
  let eqs, auts = get_node_eqs node in
1069
  let aut_calls =
1070
    List.fold_left
1071
      (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)
1072
      Utils.ISet.empty auts
1073
  in
1074
  List.fold_left
1075
    (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)
1076
    aut_calls eqs
1077

    
1078
let get_expr_vars e =
1079
  let rec get_expr_vars vars e =
1080
    get_expr_desc_vars vars e.expr_desc
1081
  and get_expr_desc_vars vars expr_desc =
1082
    (*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);*)
1083
  match expr_desc with
1084
  | Expr_const _ -> vars
1085
  | Expr_ident x -> Utils.ISet.add x vars
1086
  | Expr_tuple el
1087
  | Expr_array el -> List.fold_left get_expr_vars vars el
1088
  | Expr_pre e1 -> get_expr_vars vars e1
1089
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
1090
  | Expr_access (e1, d) 
1091
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
1092
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
1093
  | Expr_arrow (e1, e2) 
1094
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
1095
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
1096
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
1097
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
1098
  in
1099
  get_expr_vars Utils.ISet.empty e 
1100

    
1101
let rec expr_has_arrows e =
1102
  expr_desc_has_arrows e.expr_desc
1103
and expr_desc_has_arrows expr_desc =
1104
  match expr_desc with
1105
  | Expr_const _ 
1106
  | Expr_ident _ -> false
1107
  | Expr_tuple el
1108
  | Expr_array el -> List.exists expr_has_arrows el
1109
  | Expr_pre e1 
1110
  | Expr_when (e1, _, _) 
1111
  | Expr_access (e1, _) 
1112
  | Expr_power (e1, _) -> expr_has_arrows e1
1113
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
1114
  | Expr_arrow (e1, e2) 
1115
  | Expr_fby (e1, e2) -> true
1116
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1117
  | Expr_appl (i, e', i') -> expr_has_arrows e'
1118

    
1119
and eq_has_arrows eq =
1120
  expr_has_arrows eq.eq_rhs
1121
and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers 
1122
and node_has_arrows node =
1123
  let eqs, auts = get_node_eqs node in
1124
  List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts
1125

    
1126

    
1127

    
1128
let copy_var_decl vdecl =
1129
  mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid)
1130

    
1131
let copy_const cdecl =
1132
  { cdecl with const_type = Types.new_var () }
1133

    
1134
let copy_node nd =
1135
  { nd with
1136
    node_type     = Types.new_var ();
1137
    node_clock    = Clocks.new_var true;
1138
    node_inputs   = List.map copy_var_decl nd.node_inputs;
1139
    node_outputs  = List.map copy_var_decl nd.node_outputs;
1140
    node_locals   = List.map copy_var_decl nd.node_locals;
1141
    node_gencalls = [];
1142
    node_checks   = [];
1143
    node_stateless = None;
1144
  }
1145

    
1146
let copy_top top =
1147
  match top.top_decl_desc with
1148
  | Node nd -> { top with top_decl_desc = Node (copy_node nd)  }
1149
  | Const c -> { top with top_decl_desc = Const (copy_const c) }
1150
  | _       -> top
1151

    
1152
let copy_prog top_list =
1153
  List.map copy_top top_list
1154

    
1155

    
1156
let rec expr_contains_expr expr_tag expr  =
1157
  let search = expr_contains_expr expr_tag in
1158
  expr.expr_tag = expr_tag ||
1159
      (
1160
	match expr.expr_desc with
1161
	| Expr_const _ -> false
1162
	| Expr_array el -> List.exists search el
1163
	| Expr_access (e1, _) 
1164
	| Expr_power (e1, _) -> search e1
1165
	| Expr_tuple el -> List.exists search el
1166
	| Expr_ite (c, t, e) -> List.exists search [c;t;e]
1167
	| Expr_arrow (e1, e2)
1168
	| Expr_fby (e1, e2) -> List.exists search [e1; e2]
1169
	| Expr_pre e' 
1170
	| Expr_when (e', _, _) -> search e'
1171
	| Expr_merge (_, hl) -> List.exists (fun (_, h) -> search h) hl
1172
	| Expr_appl (_, e', None) -> search e' 
1173
	| Expr_appl (_, e', Some e'') -> List.exists search [e'; e''] 
1174
	| Expr_ident _ -> false
1175
      )
1176

    
1177

    
1178

    
1179
(* Generate a new local [node] variable *)
1180
let cpt_fresh = ref 0
1181

    
1182
let reset_cpt_fresh () =
1183
    cpt_fresh := 0
1184
    
1185
let mk_fresh_var node loc ty ck =
1186
  let vars = get_node_vars node in
1187
  let rec aux () =
1188
  incr cpt_fresh;
1189
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
1190
  if List.exists (fun v -> v.var_id = s) vars then aux () else
1191
  {
1192
    var_id = s;
1193
    var_orig = false;
1194
    var_dec_type = dummy_type_dec;
1195
    var_dec_clock = dummy_clock_dec;
1196
    var_dec_const = false;
1197
    var_dec_value = None;
1198
    var_parent_nodeid = Some node.node_id;
1199
    var_type = ty;
1200
    var_clock = ck;
1201
    var_loc = loc
1202
  }
1203
  in aux ()
1204

    
1205
(* Local Variables: *)
1206
(* compile-command:"make -C .." *)
1207
(* End: *)