Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ f4cba4b8

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

    
44
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
45

    
46

    
47

    
48
(************************************************************)
49
(* *)
50

    
51
let mktyp loc d =
52
  { ty_dec_desc = d; ty_dec_loc = loc }
53

    
54
let mkclock loc d =
55
  { ck_dec_desc = d; ck_dec_loc = loc }
56

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

    
70
let dummy_var_decl name typ =
71
  {
72
    var_id = name;
73
    var_orig = false;
74
    var_dec_type = dummy_type_dec;
75
    var_dec_clock = dummy_clock_dec;
76
    var_dec_const = false;
77
    var_dec_value = None;
78
    var_parent_nodeid = None;
79
    var_type =  typ;
80
    var_clock = Clocks.new_ck Clocks.Cvar true;
81
    var_loc = Location.dummy_loc
82
  }
83

    
84
let mkexpr loc d =
85
  { expr_tag = Utils.new_tag ();
86
    expr_desc = d;
87
    expr_type = Types.new_var ();
88
    expr_clock = Clocks.new_var true;
89
    expr_delay = Delay.new_var ();
90
    expr_annot = None;
91
    expr_loc = loc }
92

    
93
let var_decl_of_const ?(parentid=None) c =
94
  { var_id = c.const_id;
95
    var_orig = true;
96
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
97
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
98
    var_dec_const = true;
99
    var_dec_value = None;
100
    var_parent_nodeid = parentid;
101
    var_type = c.const_type;
102
    var_clock = Clocks.new_var false;
103
    var_loc = c.const_loc }
104

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

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

    
117
let mkassert loc expr =
118
  { assert_loc = loc;
119
    assert_expr = expr
120
  }
121

    
122
let mktop_decl loc own itf d =
123
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
124

    
125
let mkpredef_call loc funname args =
126
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
127

    
128
let is_clock_dec_type cty =
129
  match cty with
130
  | Tydec_clock _ -> true
131
  | _             -> false
132

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

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

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

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

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

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

    
176
(************************************************************)
177
(*   Eexpr functions *)
178
(************************************************************)
179

    
180

    
181
let empty_contract =
182
  {
183
    consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
184
  }
185

    
186
(* For const declaration we do as for regular lustre node.
187
But for local flows we registered the variable and the lustre flow definition *)
188
let mk_contract_var id is_const type_opt expr loc =
189
  let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
190
  if is_const then
191
  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
192
  { empty_contract with consts = [v]; spec_loc = loc; }
193
  else
194
    let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
195
    let eq = mkeq loc ([id], expr) in 
196
    { empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
197

    
198
let mk_contract_guarantees eexpr =
199
  { empty_contract with guarantees = [eexpr]; spec_loc = eexpr.eexpr_loc }
200

    
201
let mk_contract_assume eexpr =
202
  { empty_contract with assume = [eexpr]; spec_loc = eexpr.eexpr_loc }
203

    
204
let mk_contract_mode id rl el loc =
205
  { empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc }
206

    
207
let mk_contract_import id ins outs loc =
208
  { empty_contract with imports = [{import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc; }]; spec_loc = loc }
209

    
210
    
211
let merge_contracts ann1 ann2 = (* keeping the first item loc *)
212
  { consts = ann1.consts @ ann2.consts;
213
    locals = ann1.locals @ ann2.locals;
214
    stmts = ann1.stmts @ ann2.stmts;
215
    assume = ann1.assume @ ann2.assume;
216
    guarantees = ann1.guarantees @ ann2.guarantees;
217
    modes = ann1.modes @ ann2.modes;
218
    imports = ann1.imports @ ann2.imports;
219
    spec_loc = ann1.spec_loc
220
  }
221

    
222
let mkeexpr loc expr =
223
  { eexpr_tag = Utils.new_tag ();
224
    eexpr_qfexpr = expr;
225
    eexpr_quantifiers = [];
226
    eexpr_type = Types.new_var ();
227
    eexpr_clock = Clocks.new_var true;
228
    eexpr_loc = loc }
229

    
230
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
231

    
232
(*
233
let mkepredef_call loc funname args =
234
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
235

    
236
let mkepredef_unary_call loc funname arg =
237
  mkeexpr loc (EExpr_appl (funname, arg, None))
238
*)
239

    
240
let merge_expr_annot ann1 ann2 =
241
  match ann1, ann2 with
242
    | None, None -> assert false
243
    | Some _, None -> ann1
244
    | None, Some _ -> ann2
245
    | Some ann1, Some ann2 -> Some {
246
      annots = ann1.annots @ ann2.annots;
247
      annot_loc = ann1.annot_loc
248
    }
249

    
250
let update_expr_annot node_id e annot =
251
  List.iter (fun (key, _) -> 
252
    Annotations.add_expr_ann node_id e.expr_tag key
253
  ) annot.annots;
254
  e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
255
  e
256

    
257

    
258
let mkinstr ?lustre_expr ?lustre_eq i =
259
  {
260
    instr_desc = i;
261
    (* lustre_expr = lustre_expr; *)
262
    lustre_eq = lustre_eq;
263
  }
264

    
265
let get_instr_desc i = i.instr_desc
266
let update_instr_desc i id = { i with instr_desc = id }
267

    
268
(***********************************************************)
269
(* Fast access to nodes, by name *)
270
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
271
let consts_table = Hashtbl.create 30
272

    
273
let print_node_table fmt () =
274
  begin
275
    Format.fprintf fmt "{ /* node table */@.";
276
    Hashtbl.iter (fun id nd ->
277
      Format.fprintf fmt "%s |-> %a"
278
	id
279
	Printers.pp_short_decl nd
280
    ) node_table;
281
    Format.fprintf fmt "}@."
282
  end
283

    
284
let print_consts_table fmt () =
285
  begin
286
    Format.fprintf fmt "{ /* consts table */@.";
287
    Hashtbl.iter (fun id const ->
288
      Format.fprintf fmt "%s |-> %a"
289
	id
290
	Printers.pp_const_decl (const_of_top const)
291
    ) consts_table;
292
    Format.fprintf fmt "}@."
293
  end
294

    
295
let node_name td =
296
    match td.top_decl_desc with 
297
    | Node nd         -> nd.node_id
298
    | ImportedNode nd -> nd.nodei_id
299
    | _ -> assert false
300

    
301
let is_generic_node td =
302
  match td.top_decl_desc with 
303
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
304
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
305
  | _ -> assert false
306

    
307
let node_inputs td =
308
  match td.top_decl_desc with 
309
  | Node nd         -> nd.node_inputs
310
  | ImportedNode nd -> nd.nodei_inputs
311
  | _ -> assert false
312

    
313
let node_from_name id =
314
      Hashtbl.find node_table id
315
  (* with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
316
   *       	     assert false) *)
317

    
318
let update_node id top =
319
  Hashtbl.replace node_table id top
320

    
321
let is_imported_node td =
322
  match td.top_decl_desc with 
323
  | Node nd         -> false
324
  | ImportedNode nd -> true
325
  | _ -> assert false
326

    
327
let is_contract td =
328
  match td.top_decl_desc with 
329
  | Node nd -> (
330
    match nd.node_spec with
331
    | Some (Contract _) -> true
332
    | _ -> false
333
  )                     
334
  | _ -> false
335

    
336

    
337
(* alias and type definition table *)
338

    
339
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
340

    
341
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
342
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
343
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
344
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
345

    
346
let type_table =
347
  Utils.create_hashtable 20 [
348
    Tydec_int  , top_int_type;
349
    Tydec_bool , top_bool_type;
350
    (* Tydec_float, top_float_type; *)
351
    Tydec_real , top_real_type
352
  ]
353

    
354
let print_type_table fmt () =
355
  begin
356
    Format.fprintf fmt "{ /* type table */@.";
357
    Hashtbl.iter (fun tydec tdef ->
358
      Format.fprintf fmt "%a |-> %a"
359
	Printers.pp_var_type_dec_desc tydec
360
	Printers.pp_typedef (typedef_of_top tdef)
361
    ) type_table;
362
    Format.fprintf fmt "}@."
363
  end
364

    
365
let rec is_user_type typ =
366
  match typ with
367
  | Tydec_int | Tydec_bool | Tydec_real 
368
  (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
369
  | Tydec_clock typ' -> is_user_type typ'
370
  | _ -> true
371

    
372
let get_repr_type typ =
373
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
374
  if is_user_type typ_def then typ else typ_def
375

    
376
let rec coretype_equal ty1 ty2 =
377
  let res =
378
  match ty1, ty2 with
379
  | Tydec_any           , _
380
  | _                   , Tydec_any             -> assert false
381
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
382
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
383
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
384
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
385
  | Tydec_int           , Tydec_int
386
  | Tydec_real          , Tydec_real
387
  (* | Tydec_float         , Tydec_float *)
388
  | Tydec_bool          , Tydec_bool            -> true
389
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
390
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
391
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
392
  | Tydec_struct fl1    , Tydec_struct fl2      ->
393
       List.length fl1 = List.length fl2
394
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
395
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
396
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
397
  | _                                  -> false
398
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
399

    
400
let tag_true = "true"
401
let tag_false = "false"
402
let tag_default = "default"
403

    
404
let const_is_bool c =
405
 match c with
406
 | Const_tag t -> t = tag_true || t = tag_false
407
 | _           -> false
408

    
409
(* Computes the negation of a boolean constant *)
410
let const_negation c =
411
  assert (const_is_bool c);
412
  match c with
413
  | Const_tag t when t = tag_true  -> Const_tag tag_false
414
  | _                              -> Const_tag tag_true
415

    
416
let const_or c1 c2 =
417
  assert (const_is_bool c1 && const_is_bool c2);
418
  match c1, c2 with
419
  | Const_tag t1, _            when t1 = tag_true -> c1
420
  | _           , Const_tag t2 when t2 = tag_true -> c2
421
  | _                                             -> Const_tag tag_false
422

    
423
let const_and c1 c2 =
424
  assert (const_is_bool c1 && const_is_bool c2);
425
  match c1, c2 with
426
  | Const_tag t1, _            when t1 = tag_false -> c1
427
  | _           , Const_tag t2 when t2 = tag_false -> c2
428
  | _                                              -> Const_tag tag_true
429

    
430
let const_xor c1 c2 =
431
  assert (const_is_bool c1 && const_is_bool c2);
432
   match c1, c2 with
433
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
434
  | _                                         -> Const_tag tag_false
435

    
436
let const_impl c1 c2 =
437
  assert (const_is_bool c1 && const_is_bool c2);
438
  match c1, c2 with
439
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
440
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
441
  | _                                             -> Const_tag tag_false
442

    
443
(* To guarantee uniqueness of tags in enum types *)
444
let tag_table =
445
  Utils.create_hashtable 20 [
446
   tag_true, top_bool_type;
447
   tag_false, top_bool_type
448
  ]
449

    
450
(* To guarantee uniqueness of fields in struct types *)
451
let field_table =
452
  Utils.create_hashtable 20 [
453
  ]
454

    
455
let get_enum_type_tags cty =
456
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
457
 match cty with
458
 | Tydec_bool    -> [tag_true; tag_false]
459
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
460
                     | Tydec_enum tl -> tl
461
                     | _             -> assert false)
462
 | _            -> assert false
463

    
464
let get_struct_type_fields cty =
465
 match cty with
466
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
467
                     | Tydec_struct fl -> fl
468
                     | _               -> assert false)
469
 | _            -> assert false
470

    
471
let const_of_bool b =
472
 Const_tag (if b then tag_true else tag_false)
473

    
474
(* let get_const c = snd (Hashtbl.find consts_table c) *)
475

    
476
let ident_of_expr expr =
477
 match expr.expr_desc with
478
 | Expr_ident id -> id
479
 | _             -> assert false
480

    
481
(* Generate a new ident expression from a declared variable *)
482
let expr_of_vdecl v =
483
  { expr_tag = Utils.new_tag ();
484
    expr_desc = Expr_ident v.var_id;
485
    expr_type = v.var_type;
486
    expr_clock = v.var_clock;
487
    expr_delay = Delay.new_var ();
488
    expr_annot = None;
489
    expr_loc = v.var_loc }
490

    
491
(* Caution, returns an untyped and unclocked expression *)
492
let expr_of_ident id loc =
493
  {expr_tag = Utils.new_tag ();
494
   expr_desc = Expr_ident id;
495
   expr_type = Types.new_var ();
496
   expr_clock = Clocks.new_var true;
497
   expr_delay = Delay.new_var ();
498
   expr_loc = loc;
499
   expr_annot = None}
500

    
501
let is_tuple_expr expr =
502
 match expr.expr_desc with
503
  | Expr_tuple _ -> true
504
  | _            -> false
505

    
506
let expr_list_of_expr expr =
507
  match expr.expr_desc with
508
  | Expr_tuple elist -> elist
509
  | _                -> [expr]
510

    
511
let expr_of_expr_list loc elist =
512
 match elist with
513
 | [t]  -> { t with expr_loc = loc }
514
 | t::_ ->
515
    let tlist = List.map (fun e -> e.expr_type) elist in
516
    let clist = List.map (fun e -> e.expr_clock) elist in
517
    { t with expr_desc = Expr_tuple elist;
518
	     expr_type = Type_predef.type_tuple tlist;
519
	     expr_clock = Clock_predef.ck_tuple clist;
520
	     expr_tag = Utils.new_tag ();
521
	     expr_loc = loc }
522
 | _    -> assert false
523

    
524
let call_of_expr expr =
525
 match expr.expr_desc with
526
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
527
 | _                      -> assert false
528

    
529
    
530
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
531
let rec expr_of_dimension dim =
532
  let open Dimension in
533
  match dim.dim_desc with
534
 | Dbool b        ->
535
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
536
 | Dint i         ->
537
     mkexpr dim.dim_loc (Expr_const (Const_int i))
538
 | Dident id      ->
539
     mkexpr dim.dim_loc (Expr_ident id)
540
 | Dite (c, t, e) ->
541
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
542
 | Dappl (id, args) ->
543
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
544
 | Dlink dim'       -> expr_of_dimension dim'
545
 | Dvar
546
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
547
			assert false)
548

    
549
let dimension_of_const loc const =
550
  let open Dimension in
551
 match const with
552
 | Const_int i                                    -> mkdim_int loc i
553
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
554
 | _                                              -> raise InvalidDimension
555

    
556
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
557
   into dimension expressions *)
558
let rec dimension_of_expr expr =
559
  let open Dimension in
560
  match expr.expr_desc with
561
  | Expr_const c  -> dimension_of_const expr.expr_loc c
562
  | Expr_ident id -> mkdim_ident expr.expr_loc id
563
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
564
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
565
      if k = None then raise InvalidDimension;
566
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
567
  | Expr_ite (i, t, e)        ->
568
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
569
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
570

    
571

    
572
let sort_handlers hl =
573
 List.sort (fun (t, _) (t', _) -> compare t t') hl
574

    
575
let num_10 = Num.num_of_int 10
576
  
577
let rec is_eq_const c1 c2 =
578
  match c1, c2 with
579
  | Const_real (n1, i1, _), Const_real (n2, i2, _)
580
    -> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in
581
	    let n2 = n2 // (num_10 **/ (num_of_int i2)) in
582
	    eq_num n1 n2)
583
  | Const_struct lcl1, Const_struct lcl2
584
    -> List.length lcl1 = List.length lcl2
585
    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
586
  | _  -> c1 = c2
587

    
588
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
589
  | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2
590
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
591
  | Expr_array el1, Expr_array el2 
592
  | Expr_tuple el1, Expr_tuple el2 -> 
593
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
594
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
595
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
596
  | 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
597
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
598
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
599
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
600
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
601
  | 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')
602
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
603
  | Expr_power (e1, i1), Expr_power (e2, i2)
604
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
605
  | _ -> false
606

    
607
let get_node_vars nd =
608
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
609

    
610
let mk_new_node_name nd id =
611
  let used_vars = get_node_vars nd in
612
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
613
  mk_new_name used id
614

    
615
let get_var id var_list =
616
  List.find (fun v -> v.var_id = id) var_list
617

    
618
let get_node_var id node =
619
  try
620
    get_var id (get_node_vars node)
621
  with Not_found -> begin
622
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
623
    raise Not_found
624
  end
625

    
626

    
627
let get_node_eqs =
628
  let get_eqs stmts =
629
    List.fold_right
630
      (fun stmt (res_eq, res_aut) ->
631
	match stmt with
632
	| Eq eq -> eq :: res_eq, res_aut
633
	| Aut aut -> res_eq, aut::res_aut)
634
      stmts
635
      ([], []) in
636
  let table_eqs = Hashtbl.create 23 in
637
  (fun nd ->
638
    try
639
      let (old, res) = Hashtbl.find table_eqs nd.node_id
640
      in if old == nd.node_stmts then res else raise Not_found
641
    with Not_found -> 
642
      let res = get_eqs nd.node_stmts in
643
      begin
644
	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
645
	res
646
      end)
647

    
648
let get_node_eq id node =
649
  let eqs, auts = get_node_eqs node in
650
  try
651
    List.find (fun eq -> List.mem id eq.eq_lhs) eqs
652
  with
653
    Not_found -> (* Shall be defined in automata auts *) raise Not_found
654
      
655
let get_nodes prog = 
656
  List.fold_left (
657
    fun nodes decl ->
658
      match decl.top_decl_desc with
659
	| Node _ -> decl::nodes
660
	| Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes  
661
  ) [] prog
662

    
663
let get_imported_nodes prog = 
664
  List.fold_left (
665
    fun nodes decl ->
666
      match decl.top_decl_desc with
667
	| ImportedNode _ -> decl::nodes
668
	| Const _ | Node _ | Include _ | Open _ | TypeDef _-> nodes  
669
  ) [] prog
670

    
671
let get_consts prog = 
672
  List.fold_right (
673
    fun decl consts ->
674
      match decl.top_decl_desc with
675
	| Const _ -> decl::consts
676
	| Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> consts  
677
  ) prog []
678

    
679
let get_typedefs prog = 
680
  List.fold_right (
681
    fun decl types ->
682
      match decl.top_decl_desc with
683
	| TypeDef _ -> decl::types
684
	| Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> types  
685
  ) prog []
686

    
687
let get_dependencies prog =
688
  List.fold_right (
689
    fun decl deps ->
690
      match decl.top_decl_desc with
691
	| Open _ -> decl::deps
692
	| Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> deps  
693
  ) prog []
694

    
695
let get_node_interface nd =
696
 {nodei_id = nd.node_id;
697
  nodei_type = nd.node_type;
698
  nodei_clock = nd.node_clock;
699
  nodei_inputs = nd.node_inputs;
700
  nodei_outputs = nd.node_outputs;
701
  nodei_stateless = nd.node_dec_stateless;
702
  nodei_spec = nd.node_spec;
703
  (* nodei_annot = nd.node_annot; *)
704
  nodei_prototype = None;
705
  nodei_in_lib = [];
706
 }
707

    
708
(************************************************************************)
709
(*        Renaming                                                      *)
710

    
711
let rec rename_static rename cty =
712
 match cty with
713
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
714
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
715
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
716
 | _                      -> cty
717

    
718
let rec rename_carrier rename cck =
719
 match cck with
720
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
721
 | _             -> cck
722

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

    
725
(* applies the renaming function [fvar] to all variables of expression [expr] *)
726
 (* let rec expr_replace_var fvar expr = *)
727
 (*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
728

    
729
 (* and expr_desc_replace_var fvar expr_desc = *)
730
 (*   match expr_desc with *)
731
 (*   | Expr_const _ -> expr_desc *)
732
 (*   | Expr_ident i -> Expr_ident (fvar i) *)
733
 (*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
734
 (*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
735
 (*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
736
 (*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
737
 (*   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *)
738
 (*   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)  *)
739
 (*   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
740
 (*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
741
 (*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
742
 (*   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *)
743
 (*   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *)
744

    
745

    
746

    
747
 let rec rename_expr  f_node f_var expr =
748
   { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
749
 and rename_expr_desc f_node f_var expr_desc =
750
   let re = rename_expr  f_node f_var in
751
   match expr_desc with
752
   | Expr_const _ -> expr_desc
753
   | Expr_ident i -> Expr_ident (f_var i)
754
   | Expr_array el -> Expr_array (List.map re el)
755
   | Expr_access (e1, d) -> Expr_access (re e1, d)
756
   | Expr_power (e1, d) -> Expr_power (re e1, d)
757
   | Expr_tuple el -> Expr_tuple (List.map re el)
758
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
759
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
760
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
761
   | Expr_pre e' -> Expr_pre (re e')
762
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
763
   | Expr_merge (i, hl) -> 
764
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
765
   | Expr_appl (i, e', i') -> 
766
     Expr_appl (f_node i, re e', Utils.option_map re i')
767

    
768
 let rename_dec_type f_node f_var t = assert false (*
769
						     Types.rename_dim_type (Dimension.rename f_node f_var) t*)
770

    
771
 let rename_dec_clock f_node f_var c = assert false (* 
772
					  Clocks.rename_clock_expr f_var c*)
773
   
774
 let rename_var f_node f_var v = {
775
   v with
776
     var_id = f_var v.var_id;
777
     var_dec_type = rename_dec_type f_node f_var v.var_type;
778
     var_dec_clock = rename_dec_clock f_node f_var v.var_clock
779
 } 
780

    
781
 let rename_vars f_node f_var = List.map (rename_var f_node f_var) 
782

    
783
 let rec rename_eq f_node f_var eq = { eq with
784
   eq_lhs = List.map f_var eq.eq_lhs; 
785
   eq_rhs = rename_expr f_node f_var eq.eq_rhs
786
 } 
787
 and rename_handler f_node f_var  h = {h with
788
   hand_state = f_var h.hand_state;
789
   hand_unless = List.map (
790
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
791
   ) h.hand_unless;
792
   hand_until = List.map (
793
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
794
   ) h.hand_until;
795
   hand_locals = rename_vars f_node f_var h.hand_locals;
796
   hand_stmts = rename_stmts f_node f_var h.hand_stmts;
797
   hand_annots = rename_annots f_node f_var h.hand_annots;
798
   
799
 } 
800
 and rename_aut f_node f_var  aut = { aut with
801
   aut_id = f_var aut.aut_id;
802
   aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
803
 }
804
 and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with
805
   | Eq eq -> Eq (rename_eq f_node f_var eq)
806
   | Aut at -> Aut (rename_aut f_node f_var at))
807
   stmts
808
 and rename_annotl f_node f_var  annots = 
809
   List.map 
810
     (fun (key, value) -> key, rename_eexpr f_node f_var value) 
811
     annots
812
 and rename_annot f_node f_var annot =
813
   { annot with annots = rename_annotl f_node f_var annot.annots }
814
 and rename_annots f_node f_var annots =
815
   List.map (rename_annot f_node f_var) annots
816
and rename_eexpr f_node f_var ee =
817
   { ee with
818
     eexpr_tag = Utils.new_tag ();
819
     eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
820
     eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
821
   }
822
 
823
     
824
     
825
   
826
 let rename_node f_node f_var nd =
827
   let rename_var = rename_var f_node f_var in
828
   let rename_expr = rename_expr f_node f_var in
829
   let rename_stmts = rename_stmts f_node f_var in
830
   let inputs = List.map rename_var nd.node_inputs in
831
   let outputs = List.map rename_var nd.node_outputs in
832
   let locals = List.map rename_var nd.node_locals in
833
   let gen_calls = List.map rename_expr nd.node_gencalls in
834
   let node_checks = List.map (Dimension.rename f_node f_var)  nd.node_checks in
835
   let node_asserts = List.map 
836
     (fun a -> 
837
       {a with assert_expr = 
838
	   let expr = a.assert_expr in
839
	   rename_expr expr})
840
     nd.node_asserts
841
   in
842
   let node_stmts = rename_stmts nd.node_stmts
843

    
844
     
845
   in
846
   let spec = 
847
     Utils.option_map 
848
       (fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *) 
849
       nd.node_spec 
850
   in
851
   let annot = rename_annots f_node f_var nd.node_annot in
852
   {
853
     node_id = f_node nd.node_id;
854
     node_type = nd.node_type;
855
     node_clock = nd.node_clock;
856
     node_inputs = inputs;
857
     node_outputs = outputs;
858
     node_locals = locals;
859
     node_gencalls = gen_calls;
860
     node_checks = node_checks;
861
     node_asserts = node_asserts;
862
     node_stmts = node_stmts;
863
     node_dec_stateless = nd.node_dec_stateless;
864
     node_stateless = nd.node_stateless;
865
     node_spec = spec;
866
     node_annot = annot;
867
     node_iscontract = nd.node_iscontract;
868
   }
869

    
870

    
871
let rename_const f_const c =
872
  { c with const_id = f_const c.const_id }
873

    
874
let rename_typedef f_var t =
875
  match t.tydef_desc with
876
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
877
  | _               -> t
878

    
879
let rename_prog f_node f_var f_const prog =
880
  List.rev (
881
    List.fold_left (fun accu top ->
882
      (match top.top_decl_desc with
883
      | Node nd -> 
884
	 { top with top_decl_desc = Node (rename_node f_node f_var nd) }
885
      | Const c -> 
886
	 { top with top_decl_desc = Const (rename_const f_const c) }
887
      | TypeDef tdef ->
888
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
889
      | ImportedNode _
890
        | Include _ | Open _       -> top)
891
      ::accu
892
) [] prog
893
		   )
894

    
895
(* Applies the renaming function [fvar] to every rhs
896
   only when the corresponding lhs satisfies predicate [pvar] *)
897
 let eq_replace_rhs_var pvar fvar eq =
898
   let pvar l = List.exists pvar l in
899
   let rec replace lhs rhs =
900
     { rhs with expr_desc =
901
     match lhs with
902
     | []  -> assert false
903
     | [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc
904
     | _   ->
905
       (match rhs.expr_desc with
906
       | Expr_tuple tl ->
907
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
908
       | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
909
	 let args = expr_list_of_expr arg in
910
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
911
       | Expr_array _
912
       | Expr_access _
913
       | Expr_power _
914
       | Expr_const _
915
       | Expr_ident _
916
       | Expr_appl _   ->
917
	 if pvar lhs
918
	 then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
919
	 else rhs.expr_desc
920
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
921
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
922
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
923
       | Expr_pre e'          -> Expr_pre (replace lhs e')
924
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
925
				 in Expr_when (replace lhs e', i', l)
926
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
927
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
928
       )
929
     }
930
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
931

    
932
    
933
(**********************************************************************)
934
(* Pretty printers *)
935

    
936
let pp_decl_type fmt tdecl =
937
  match tdecl.top_decl_desc with
938
  | Node nd ->
939
    fprintf fmt "%s: " nd.node_id;
940
    Utils.reset_names ();
941
    fprintf fmt "%a@ " Types.print_ty nd.node_type
942
  | ImportedNode ind ->
943
    fprintf fmt "%s: " ind.nodei_id;
944
    Utils.reset_names ();
945
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
946
  | Const _ | Include _ | Open _ | TypeDef _ -> ()
947

    
948
let pp_prog_type fmt tdecl_list =
949
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
950

    
951
let pp_decl_clock fmt cdecl =
952
  match cdecl.top_decl_desc with
953
  | Node nd ->
954
    fprintf fmt "%s: " nd.node_id;
955
    Utils.reset_names ();
956
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
957
  | ImportedNode ind ->
958
    fprintf fmt "%s: " ind.nodei_id;
959
    Utils.reset_names ();
960
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
961
  | Const _ | Include _ | Open _ | TypeDef _ -> ()
962

    
963
let pp_prog_clock fmt prog =
964
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
965

    
966

    
967
(* filling node table with internal functions *)
968
let vdecls_of_typ_ck cpt ty =
969
  let loc = Location.dummy_loc in
970
  List.map
971
    (fun _ -> incr cpt;
972
              let name = sprintf "_var_%d" !cpt in
973
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
974
    (Types.type_list_of_type ty)
975

    
976
let mk_internal_node id =
977
  let spec = None in
978
  let ty = Env.lookup_value Basic_library.type_env id in
979
  let ck = Env.lookup_value Basic_library.clock_env id in
980
  let (tin, tout) = Types.split_arrow ty in
981
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
982
  let cpt = ref (-1) in
983
  mktop
984
    (ImportedNode
985
       {nodei_id = id;
986
	nodei_type = ty;
987
	nodei_clock = ck;
988
	nodei_inputs = vdecls_of_typ_ck cpt tin;
989
	nodei_outputs = vdecls_of_typ_ck cpt tout;
990
	nodei_stateless = Types.get_static_value ty <> None;
991
	nodei_spec = spec;
992
	(* nodei_annot = []; *)
993
	nodei_prototype = None;
994
       	nodei_in_lib = [];
995
       })
996

    
997
let add_internal_funs () =
998
  List.iter
999
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
1000
    Basic_library.internal_funs
1001

    
1002

    
1003

    
1004
(* Replace any occurence of a var in vars_to_replace by its associated
1005
   expression in defs until e does not contain any such variables *)
1006
let rec substitute_expr vars_to_replace defs e =
1007
  let se = substitute_expr vars_to_replace defs in
1008
  { e with expr_desc = 
1009
      let ed = e.expr_desc in
1010
      match ed with
1011
      | Expr_const _ -> ed
1012
      | Expr_array el -> Expr_array (List.map se el)
1013
      | Expr_access (e1, d) -> Expr_access (se e1, d)
1014
      | Expr_power (e1, d) -> Expr_power (se e1, d)
1015
      | Expr_tuple el -> Expr_tuple (List.map se el)
1016
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
1017
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
1018
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
1019
      | Expr_pre e' -> Expr_pre (se e')
1020
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
1021
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
1022
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
1023
      | Expr_ident i -> 
1024
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
1025
	  let eq_i eq = eq.eq_lhs = [i] in
1026
	  if List.exists eq_i defs then
1027
	    let sub = List.find eq_i defs in
1028
	    let sub' = se sub.eq_rhs in
1029
	    sub'.expr_desc
1030
	  else 
1031
	    assert false
1032
	)
1033
	else
1034
	  ed
1035

    
1036
  }
1037
  
1038
 let rec expr_to_eexpr  expr =
1039
   { eexpr_tag = expr.expr_tag;
1040
     eexpr_qfexpr = expr;
1041
     eexpr_quantifiers = [];
1042
     eexpr_type = expr.expr_type;
1043
     eexpr_clock = expr.expr_clock;
1044
     eexpr_loc = expr.expr_loc;
1045
     (*eexpr_normalized = None*)
1046
   }
1047
 (* and expr_desc_to_eexpr_desc expr_desc = *)
1048
 (*   let conv = expr_to_eexpr in *)
1049
 (*   match expr_desc with *)
1050
 (*   | Expr_const c -> EExpr_const (match c with *)
1051
 (*     | Const_int x -> EConst_int x  *)
1052
 (*     | Const_real x -> EConst_real x  *)
1053
 (*     | Const_float x -> EConst_float x  *)
1054
 (*     | Const_tag x -> EConst_tag x  *)
1055
 (*     | _ -> assert false *)
1056

    
1057
 (*   ) *)
1058
 (*   | Expr_ident i -> EExpr_ident i *)
1059
 (*   | Expr_tuple el -> EExpr_tuple (List.map conv el) *)
1060

    
1061
 (*   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)  *)
1062
 (*   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *)
1063
 (*   | Expr_pre e' -> EExpr_pre (conv e') *)
1064
 (*   | Expr_appl (i, e', i') ->  *)
1065
 (*     EExpr_appl  *)
1066
 (*       (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *)
1067

    
1068
 (*   | Expr_when _ *)
1069
 (*   | Expr_merge _ -> assert false *)
1070
 (*   | Expr_array _  *)
1071
 (*   | Expr_access _  *)
1072
 (*   | Expr_power _  -> assert false *)
1073
 (*   | Expr_ite (c, t, e) -> assert false  *)
1074
 (*   | _ -> assert false *)
1075
      
1076
     
1077
let rec get_expr_calls nodes e =
1078
  let get_calls = get_expr_calls nodes in
1079
  match e.expr_desc with
1080
  | Expr_const _ 
1081
   | Expr_ident _ -> Utils.ISet.empty
1082
   | Expr_tuple el
1083
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
1084
   | Expr_pre e1 
1085
   | Expr_when (e1, _, _) 
1086
   | Expr_access (e1, _) 
1087
   | Expr_power (e1, _) -> get_calls e1
1088
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
1089
   | Expr_arrow (e1, e2) 
1090
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
1091
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
1092
   | Expr_appl (i, e', i') -> 
1093
     if Basic_library.is_expr_internal_fun e then 
1094
       (get_calls e') 
1095
     else
1096
       let calls =  Utils.ISet.add i (get_calls e') in
1097
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
1098
       if List.exists test nodes then
1099
	 match (List.find test nodes).top_decl_desc with
1100
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
1101
	 | _ -> assert false
1102
       else 
1103
	 calls
1104

    
1105
and get_eq_calls nodes eq =
1106
  get_expr_calls nodes eq.eq_rhs
1107
and get_aut_handler_calls nodes h =
1108
  List.fold_left (fun accu stmt -> match stmt with
1109
  | Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu
1110
  | Aut aut' ->  Utils.ISet.union (get_aut_calls nodes aut') accu
1111
  ) Utils.ISet.empty h.hand_stmts 
1112
and get_aut_calls nodes aut =
1113
  List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)
1114
    Utils.ISet.empty aut.aut_handlers
1115
and get_node_calls nodes node =
1116
  let eqs, auts = get_node_eqs node in
1117
  let aut_calls =
1118
    List.fold_left
1119
      (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)
1120
      Utils.ISet.empty auts
1121
  in
1122
  List.fold_left
1123
    (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)
1124
    aut_calls eqs
1125

    
1126
let get_expr_vars e =
1127
  let rec get_expr_vars vars e =
1128
    get_expr_desc_vars vars e.expr_desc
1129
  and get_expr_desc_vars vars expr_desc =
1130
    (*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);*)
1131
  match expr_desc with
1132
  | Expr_const _ -> vars
1133
  | Expr_ident x -> Utils.ISet.add x vars
1134
  | Expr_tuple el
1135
  | Expr_array el -> List.fold_left get_expr_vars vars el
1136
  | Expr_pre e1 -> get_expr_vars vars e1
1137
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
1138
  | Expr_access (e1, d) 
1139
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
1140
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
1141
  | Expr_arrow (e1, e2) 
1142
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
1143
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
1144
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
1145
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
1146
  in
1147
  get_expr_vars Utils.ISet.empty e 
1148

    
1149
let rec expr_has_arrows e =
1150
  expr_desc_has_arrows e.expr_desc
1151
and expr_desc_has_arrows expr_desc =
1152
  match expr_desc with
1153
  | Expr_const _ 
1154
  | Expr_ident _ -> false
1155
  | Expr_tuple el
1156
  | Expr_array el -> List.exists expr_has_arrows el
1157
  | Expr_pre e1 
1158
  | Expr_when (e1, _, _) 
1159
  | Expr_access (e1, _) 
1160
  | Expr_power (e1, _) -> expr_has_arrows e1
1161
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
1162
  | Expr_arrow (e1, e2) 
1163
  | Expr_fby (e1, e2) -> true
1164
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1165
  | Expr_appl (i, e', i') -> expr_has_arrows e'
1166

    
1167
and eq_has_arrows eq =
1168
  expr_has_arrows eq.eq_rhs
1169
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 
1170
and node_has_arrows node =
1171
  let eqs, auts = get_node_eqs node in
1172
  List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts
1173

    
1174

    
1175

    
1176
let copy_var_decl vdecl =
1177
  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)
1178

    
1179
let copy_const cdecl =
1180
  { cdecl with const_type = Types.new_var () }
1181

    
1182
let copy_node nd =
1183
  { nd with
1184
    node_type     = Types.new_var ();
1185
    node_clock    = Clocks.new_var true;
1186
    node_inputs   = List.map copy_var_decl nd.node_inputs;
1187
    node_outputs  = List.map copy_var_decl nd.node_outputs;
1188
    node_locals   = List.map copy_var_decl nd.node_locals;
1189
    node_gencalls = [];
1190
    node_checks   = [];
1191
    node_stateless = None;
1192
  }
1193

    
1194
let copy_top top =
1195
  match top.top_decl_desc with
1196
  | Node nd -> { top with top_decl_desc = Node (copy_node nd)  }
1197
  | Const c -> { top with top_decl_desc = Const (copy_const c) }
1198
  | _       -> top
1199

    
1200
let copy_prog top_list =
1201
  List.map copy_top top_list
1202

    
1203

    
1204
let rec expr_contains_expr expr_tag expr  =
1205
  let search = expr_contains_expr expr_tag in
1206
  expr.expr_tag = expr_tag ||
1207
      (
1208
	match expr.expr_desc with
1209
	| Expr_const _ -> false
1210
	| Expr_array el -> List.exists search el
1211
	| Expr_access (e1, _) 
1212
	| Expr_power (e1, _) -> search e1
1213
	| Expr_tuple el -> List.exists search el
1214
	| Expr_ite (c, t, e) -> List.exists search [c;t;e]
1215
	| Expr_arrow (e1, e2)
1216
	| Expr_fby (e1, e2) -> List.exists search [e1; e2]
1217
	| Expr_pre e' 
1218
	| Expr_when (e', _, _) -> search e'
1219
	| Expr_merge (_, hl) -> List.exists (fun (_, h) -> search h) hl
1220
	| Expr_appl (_, e', None) -> search e' 
1221
	| Expr_appl (_, e', Some e'') -> List.exists search [e'; e''] 
1222
	| Expr_ident _ -> false
1223
      )
1224

    
1225

    
1226

    
1227
(* Generate a new local [node] variable *)
1228
let cpt_fresh = ref 0
1229

    
1230
let reset_cpt_fresh () =
1231
    cpt_fresh := 0
1232
    
1233
let mk_fresh_var (parentid, ctx_env) loc ty ck =
1234
  let rec aux () =
1235
  incr cpt_fresh;
1236
  let s = Printf.sprintf "__%s_%d" parentid !cpt_fresh in
1237
  if List.exists (fun v -> v.var_id = s) ctx_env then aux () else
1238
  {
1239
    var_id = s;
1240
    var_orig = false;
1241
    var_dec_type = dummy_type_dec;
1242
    var_dec_clock = dummy_clock_dec;
1243
    var_dec_const = false;
1244
    var_dec_value = None;
1245
    var_parent_nodeid = Some parentid;
1246
    var_type = ty;
1247
    var_clock = ck;
1248
    var_loc = loc
1249
  }
1250
  in aux ()
1251

    
1252

    
1253
let find_eq xl eqs =
1254
  let rec aux accu eqs =
1255
    match eqs with
1256
	| [] ->
1257
	  begin
1258
	    Format.eprintf "Looking for variables %a in the following equations@.%a@."
1259
	      (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl
1260
	      Printers.pp_node_eqs eqs;
1261
	    assert false
1262
	  end
1263
	| hd::tl ->
1264
	  if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl
1265
    in
1266
    aux [] eqs
1267

    
1268

    
1269

    
1270
       
1271
(* Local Variables: *)
1272
(* compile-command:"make -C .." *)
1273
(* End: *)