Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 264a4844

History | View | Annotate | Download (35.6 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
open Format
13
open LustreSpec
14 7d640c88 ploc
(*open Dimension*)
15 22fe1c93 ploc
16
17 e7cc5186 ploc
exception Error of Location.t * Error.error_kind
18 22fe1c93 ploc
19
module VDeclModule =
20
struct (* Node module *)
21
  type t = var_decl
22 bb2ca5f4 xthirioux
  let compare v1 v2 = compare v1.var_id v2.var_id
23 22fe1c93 ploc
end
24
25
module VMap = Map.Make(VDeclModule)
26
27
module VSet = Set.Make(VDeclModule)
28
29 01c7d5e1 ploc
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
30
31
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
32
33
34
35 22fe1c93 ploc
(************************************************************)
36
(* *)
37
38
let mktyp loc d =
39
  { ty_dec_desc = d; ty_dec_loc = loc }
40
41
let mkclock loc d =
42
  { ck_dec_desc = d; ck_dec_loc = loc }
43
44 ec433d69 xthirioux
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
45
  assert (value = None || is_const);
46 22fe1c93 ploc
  { var_id = id;
47 54d032f5 xthirioux
    var_orig = orig;
48 22fe1c93 ploc
    var_dec_type = ty_dec;
49
    var_dec_clock = ck_dec;
50
    var_dec_const = is_const;
51 ec433d69 xthirioux
    var_dec_value = value;
52 22fe1c93 ploc
    var_type = Types.new_var ();
53
    var_clock = Clocks.new_var true;
54
    var_loc = loc }
55
56
let mkexpr loc d =
57
  { expr_tag = Utils.new_tag ();
58
    expr_desc = d;
59
    expr_type = Types.new_var ();
60
    expr_clock = Clocks.new_var true;
61
    expr_delay = Delay.new_var ();
62
    expr_annot = None;
63
    expr_loc = loc }
64
65
let var_decl_of_const c =
66
  { var_id = c.const_id;
67 54d032f5 xthirioux
    var_orig = true;
68 22fe1c93 ploc
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
69
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
70
    var_dec_const = true;
71 ec433d69 xthirioux
    var_dec_value = None;
72 22fe1c93 ploc
    var_type = c.const_type;
73
    var_clock = Clocks.new_var false;
74
    var_loc = c.const_loc }
75
76 b08ffca7 xthirioux
let mk_new_name used id =
77 22fe1c93 ploc
  let rec new_name name cpt =
78 b08ffca7 xthirioux
    if used name
79 22fe1c93 ploc
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
80
    else name
81
  in new_name id 1
82
83
let mkeq loc (lhs, rhs) =
84
  { eq_lhs = lhs;
85
    eq_rhs = rhs;
86
    eq_loc = loc }
87
88
let mkassert loc expr =
89
  { assert_loc = loc;
90
    assert_expr = expr
91
  }
92
93 ef34b4ae xthirioux
let mktop_decl loc own itf d =
94
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
95 22fe1c93 ploc
96
let mkpredef_call loc funname args =
97
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
98
99 ec433d69 xthirioux
let is_clock_dec_type cty =
100
  match cty with
101
  | Tydec_clock _ -> true
102
  | _             -> false
103 ef34b4ae xthirioux
104
let const_of_top top_decl =
105
  match top_decl.top_decl_desc with
106
  | Const c -> c
107
  | _ -> assert false
108
109
let node_of_top top_decl =
110
  match top_decl.top_decl_desc with
111
  | Node nd -> nd
112 2475c9e8 ploc
  | _ -> raise Not_found
113 ef34b4ae xthirioux
114
let imported_node_of_top top_decl =
115
  match top_decl.top_decl_desc with
116
  | ImportedNode ind -> ind
117
  | _ -> assert false
118
119
let typedef_of_top top_decl =
120
  match top_decl.top_decl_desc with
121
  | TypeDef tdef -> tdef
122
  | _ -> assert false
123
124
let dependency_of_top top_decl =
125
  match top_decl.top_decl_desc with
126
  | Open (local, dep) -> (local, dep)
127
  | _ -> assert false
128
129
let consts_of_enum_type top_decl =
130
  match top_decl.top_decl_desc with
131
  | TypeDef tdef ->
132
    (match tdef.tydef_desc with
133
     | Tydec_enum tags -> List.map (fun tag -> let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags
134
     | _               -> [])
135
  | _ -> assert false
136
137 01c7d5e1 ploc
(************************************************************)
138
(*   Eexpr functions *)
139
(************************************************************)
140
141
let merge_node_annot ann1 ann2 =
142
  { requires = ann1.requires @ ann2.requires;
143
    ensures = ann1.ensures @ ann2.ensures;
144
    behaviors = ann1.behaviors @ ann2.behaviors;
145
    spec_loc = ann1.spec_loc
146
  }
147
148
let mkeexpr loc expr =
149
  { eexpr_tag = Utils.new_tag ();
150
    eexpr_qfexpr = expr;
151
    eexpr_quantifiers = [];
152
    eexpr_type = Types.new_var ();
153
    eexpr_clock = Clocks.new_var true;
154
    eexpr_normalized = None;
155
    eexpr_loc = loc }
156
157
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
158
159
(*
160
let mkepredef_call loc funname args =
161
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
162
163
let mkepredef_unary_call loc funname arg =
164
  mkeexpr loc (EExpr_appl (funname, arg, None))
165
*)
166
167
let merge_expr_annot ann1 ann2 =
168
  match ann1, ann2 with
169
    | None, None -> assert false
170
    | Some _, None -> ann1
171
    | None, Some _ -> ann2
172
    | Some ann1, Some ann2 -> Some {
173
      annots = ann1.annots @ ann2.annots;
174
      annot_loc = ann1.annot_loc
175
    }
176
177 566dbf49 ploc
let update_expr_annot node_id e annot =
178
  List.iter (fun (key, _) -> 
179
    Annotations.add_expr_ann node_id e.expr_tag key
180
  ) annot.annots;
181 264a4844 ploc
  e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
182
  e
183 01c7d5e1 ploc
184
185 1b683c9a ploc
let mkinstr ?lustre_expr ?lustre_eq i =
186 3ca27bc7 ploc
  {
187
    instr_desc = i;
188 1bff14ac ploc
    (* lustre_expr = lustre_expr; *)
189
    lustre_eq = lustre_eq;
190 3ca27bc7 ploc
  }
191
192
let get_instr_desc i = i.instr_desc
193
let update_instr_desc i id = { i with instr_desc = id }
194
195 22fe1c93 ploc
(***********************************************************)
196
(* Fast access to nodes, by name *)
197
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
198
let consts_table = Hashtbl.create 30
199
200 ef34b4ae xthirioux
let print_node_table fmt () =
201
  begin
202
    Format.fprintf fmt "{ /* node table */@.";
203
    Hashtbl.iter (fun id nd ->
204
      Format.fprintf fmt "%s |-> %a"
205
	id
206
	Printers.pp_short_decl nd
207
    ) node_table;
208
    Format.fprintf fmt "}@."
209
  end
210
211
let print_consts_table fmt () =
212
  begin
213
    Format.fprintf fmt "{ /* consts table */@.";
214
    Hashtbl.iter (fun id const ->
215
      Format.fprintf fmt "%s |-> %a"
216
	id
217
	Printers.pp_const_decl (const_of_top const)
218
    ) consts_table;
219
    Format.fprintf fmt "}@."
220
  end
221
222 22fe1c93 ploc
let node_name td =
223
    match td.top_decl_desc with 
224
    | Node nd         -> nd.node_id
225
    | ImportedNode nd -> nd.nodei_id
226
    | _ -> assert false
227
228
let is_generic_node td =
229
  match td.top_decl_desc with 
230
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
231
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
232
  | _ -> assert false
233
234
let node_inputs td =
235
  match td.top_decl_desc with 
236
  | Node nd         -> nd.node_inputs
237
  | ImportedNode nd -> nd.nodei_inputs
238
  | _ -> assert false
239
240
let node_from_name id =
241
  try
242
    Hashtbl.find node_table id
243
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
244
		     assert false)
245
246
let is_imported_node td =
247
  match td.top_decl_desc with 
248
  | Node nd         -> false
249
  | ImportedNode nd -> true
250
  | _ -> assert false
251
252 52cfee34 xthirioux
253 22fe1c93 ploc
(* alias and type definition table *)
254 ef34b4ae xthirioux
255 990210f3 ploc
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
256 1e48ef45 ploc
257
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
258
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
259 04a63d25 xthirioux
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
260 1e48ef45 ploc
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
261 ef34b4ae xthirioux
262 22fe1c93 ploc
let type_table =
263
  Utils.create_hashtable 20 [
264 ef34b4ae xthirioux
    Tydec_int  , top_int_type;
265
    Tydec_bool , top_bool_type;
266 04a63d25 xthirioux
    (* Tydec_float, top_float_type; *)
267 ef34b4ae xthirioux
    Tydec_real , top_real_type
268 22fe1c93 ploc
  ]
269
270 ef34b4ae xthirioux
let print_type_table fmt () =
271
  begin
272
    Format.fprintf fmt "{ /* type table */@.";
273
    Hashtbl.iter (fun tydec tdef ->
274
      Format.fprintf fmt "%a |-> %a"
275
	Printers.pp_var_type_dec_desc tydec
276
	Printers.pp_typedef (typedef_of_top tdef)
277
    ) type_table;
278
    Format.fprintf fmt "}@."
279
  end
280
281 22fe1c93 ploc
let rec is_user_type typ =
282
  match typ with
283
  | Tydec_int | Tydec_bool | Tydec_real 
284 04a63d25 xthirioux
  (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
285 22fe1c93 ploc
  | Tydec_clock typ' -> is_user_type typ'
286
  | _ -> true
287
288
let get_repr_type typ =
289 ef34b4ae xthirioux
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
290 22fe1c93 ploc
  if is_user_type typ_def then typ else typ_def
291
292 b1655a21 xthirioux
let rec coretype_equal ty1 ty2 =
293 ef34b4ae xthirioux
  let res =
294 b1655a21 xthirioux
  match ty1, ty2 with
295 ed81df06 xthirioux
  | Tydec_any           , _
296
  | _                   , Tydec_any             -> assert false
297
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
298 ef34b4ae xthirioux
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
299 ed81df06 xthirioux
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
300
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
301
  | Tydec_int           , Tydec_int
302
  | Tydec_real          , Tydec_real
303 04a63d25 xthirioux
  (* | Tydec_float         , Tydec_float *)
304 ed81df06 xthirioux
  | Tydec_bool          , Tydec_bool            -> true
305
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
306
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
307
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
308
  | Tydec_struct fl1    , Tydec_struct fl2      ->
309 b1655a21 xthirioux
       List.length fl1 = List.length fl2
310
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
311
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
312
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
313
  | _                                  -> false
314 ef34b4ae xthirioux
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
315 b1655a21 xthirioux
316 22fe1c93 ploc
let tag_true = "true"
317
let tag_false = "false"
318 77a61575 xthirioux
let tag_default = "default"
319 22fe1c93 ploc
320
let const_is_bool c =
321
 match c with
322
 | Const_tag t -> t = tag_true || t = tag_false
323
 | _           -> false
324
325
(* Computes the negation of a boolean constant *)
326
let const_negation c =
327
  assert (const_is_bool c);
328
  match c with
329
  | Const_tag t when t = tag_true  -> Const_tag tag_false
330
  | _                              -> Const_tag tag_true
331
332
let const_or c1 c2 =
333
  assert (const_is_bool c1 && const_is_bool c2);
334
  match c1, c2 with
335
  | Const_tag t1, _            when t1 = tag_true -> c1
336
  | _           , Const_tag t2 when t2 = tag_true -> c2
337
  | _                                             -> Const_tag tag_false
338
339
let const_and c1 c2 =
340
  assert (const_is_bool c1 && const_is_bool c2);
341
  match c1, c2 with
342
  | Const_tag t1, _            when t1 = tag_false -> c1
343
  | _           , Const_tag t2 when t2 = tag_false -> c2
344
  | _                                              -> Const_tag tag_true
345
346
let const_xor c1 c2 =
347
  assert (const_is_bool c1 && const_is_bool c2);
348
   match c1, c2 with
349
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
350
  | _                                         -> Const_tag tag_false
351
352
let const_impl c1 c2 =
353
  assert (const_is_bool c1 && const_is_bool c2);
354
  match c1, c2 with
355
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
356
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
357
  | _                                             -> Const_tag tag_false
358
359
(* To guarantee uniqueness of tags in enum types *)
360
let tag_table =
361
  Utils.create_hashtable 20 [
362 ef34b4ae xthirioux
   tag_true, top_bool_type;
363
   tag_false, top_bool_type
364 22fe1c93 ploc
  ]
365
366 fa090c4e xthirioux
(* To guarantee uniqueness of fields in struct types *)
367
let field_table =
368
  Utils.create_hashtable 20 [
369
  ]
370
371 22fe1c93 ploc
let get_enum_type_tags cty =
372 ef34b4ae xthirioux
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
373 22fe1c93 ploc
 match cty with
374
 | Tydec_bool    -> [tag_true; tag_false]
375 ef34b4ae xthirioux
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
376 22fe1c93 ploc
                     | Tydec_enum tl -> tl
377
                     | _             -> assert false)
378
 | _            -> assert false
379 6a6abd76 xthirioux
380 fa090c4e xthirioux
let get_struct_type_fields cty =
381
 match cty with
382 ef34b4ae xthirioux
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
383 fa090c4e xthirioux
                     | Tydec_struct fl -> fl
384
                     | _               -> assert false)
385
 | _            -> assert false
386 6a6abd76 xthirioux
387 22fe1c93 ploc
let const_of_bool b =
388
 Const_tag (if b then tag_true else tag_false)
389
390
(* let get_const c = snd (Hashtbl.find consts_table c) *)
391
392 add75bcb xthirioux
let ident_of_expr expr =
393
 match expr.expr_desc with
394
 | Expr_ident id -> id
395
 | _             -> assert false
396
397 fc886259 xthirioux
(* Generate a new ident expression from a declared variable *)
398
let expr_of_vdecl v =
399
  { expr_tag = Utils.new_tag ();
400
    expr_desc = Expr_ident v.var_id;
401
    expr_type = v.var_type;
402
    expr_clock = v.var_clock;
403
    expr_delay = Delay.new_var ();
404
    expr_annot = None;
405
    expr_loc = v.var_loc }
406
407 22fe1c93 ploc
(* Caution, returns an untyped and unclocked expression *)
408
let expr_of_ident id loc =
409
  {expr_tag = Utils.new_tag ();
410
   expr_desc = Expr_ident id;
411
   expr_type = Types.new_var ();
412
   expr_clock = Clocks.new_var true;
413
   expr_delay = Delay.new_var ();
414
   expr_loc = loc;
415
   expr_annot = None}
416
417 b616fe7a xthirioux
let is_tuple_expr expr =
418
 match expr.expr_desc with
419
  | Expr_tuple _ -> true
420
  | _            -> false
421
422 22fe1c93 ploc
let expr_list_of_expr expr =
423
  match expr.expr_desc with
424 bb2ca5f4 xthirioux
  | Expr_tuple elist -> elist
425
  | _                -> [expr]
426 22fe1c93 ploc
427
let expr_of_expr_list loc elist =
428
 match elist with
429
 | [t]  -> { t with expr_loc = loc }
430 70df2f87 xthirioux
 | t::_ ->
431
    let tlist = List.map (fun e -> e.expr_type) elist in
432
    let clist = List.map (fun e -> e.expr_clock) elist in
433
    { t with expr_desc = Expr_tuple elist;
434
	     expr_type = Type_predef.type_tuple tlist;
435
	     expr_clock = Clock_predef.ck_tuple clist;
436
	     expr_tag = Utils.new_tag ();
437
	     expr_loc = loc }
438 22fe1c93 ploc
 | _    -> assert false
439
440
let call_of_expr expr =
441
 match expr.expr_desc with
442
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
443
 | _                      -> assert false
444
445 7d640c88 ploc
    
446 22fe1c93 ploc
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
447
let rec expr_of_dimension dim =
448 7d640c88 ploc
  let open Dimension in
449
  match dim.dim_desc with
450 22fe1c93 ploc
 | Dbool b        ->
451
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
452
 | Dint i         ->
453
     mkexpr dim.dim_loc (Expr_const (Const_int i))
454
 | Dident id      ->
455
     mkexpr dim.dim_loc (Expr_ident id)
456
 | Dite (c, t, e) ->
457
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
458
 | Dappl (id, args) ->
459
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
460
 | Dlink dim'       -> expr_of_dimension dim'
461
 | Dvar
462 fc886259 xthirioux
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
463 22fe1c93 ploc
			assert false)
464
465
let dimension_of_const loc const =
466 7d640c88 ploc
  let open Dimension in
467 22fe1c93 ploc
 match const with
468
 | Const_int i                                    -> mkdim_int loc i
469
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
470
 | _                                              -> raise InvalidDimension
471
472
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
473
   into dimension expressions *)
474
let rec dimension_of_expr expr =
475 7d640c88 ploc
  let open Dimension in
476 22fe1c93 ploc
  match expr.expr_desc with
477
  | Expr_const c  -> dimension_of_const expr.expr_loc c
478
  | Expr_ident id -> mkdim_ident expr.expr_loc id
479 04a63d25 xthirioux
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
480 22fe1c93 ploc
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
481
      if k = None then raise InvalidDimension;
482
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
483
  | Expr_ite (i, t, e)        ->
484
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
485
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
486
487
488
let sort_handlers hl =
489
 List.sort (fun (t, _) (t', _) -> compare t t') hl
490
491 e49b6d55 xavier.thirioux
let num_10 = Num.num_of_int 10
492
  
493
let rec is_eq_const c1 c2 =
494
  match c1, c2 with
495
  | Const_real (n1, i1, _), Const_real (n2, i2, _)
496
    -> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in
497
	    let n2 = n2 // (num_10 **/ (num_of_int i2)) in
498
	    eq_num n1 n2)
499
  | Const_struct lcl1, Const_struct lcl2
500
    -> List.length lcl1 = List.length lcl2
501
    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
502
  | _  -> c1 = c2
503
504 22fe1c93 ploc
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
505 e49b6d55 xavier.thirioux
  | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2
506 22fe1c93 ploc
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
507
  | Expr_array el1, Expr_array el2 
508
  | Expr_tuple el1, Expr_tuple el2 -> 
509
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
510
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
511
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
512
  | 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
513
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
514
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
515
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
516
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
517
  | 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')
518
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
519
  | Expr_power (e1, i1), Expr_power (e2, i2)
520
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
521
  | _ -> false
522
523 01c7d5e1 ploc
let get_node_vars nd =
524 22fe1c93 ploc
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
525
526 fc886259 xthirioux
let mk_new_node_name nd id =
527
  let used_vars = get_node_vars nd in
528
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
529
  mk_new_name used id
530
531 01c7d5e1 ploc
let get_var id var_list =
532 04a63d25 xthirioux
  List.find (fun v -> v.var_id = id) var_list
533 22fe1c93 ploc
534 df39e35a xthirioux
let get_node_var id node =
535 76c7023b ploc
  try
536
    get_var id (get_node_vars node)
537
  with Not_found -> begin
538 63f10e14 ploc
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
539 76c7023b ploc
    raise Not_found
540
  end
541
    
542 b08ffca7 xthirioux
let get_node_eqs =
543
  let get_eqs stmts =
544
    List.fold_right
545
      (fun stmt res ->
546
	match stmt with
547
	| Eq eq -> eq :: res
548
	| Aut _ -> assert false)
549
      stmts
550
      [] in
551
  let table_eqs = Hashtbl.create 23 in
552
  (fun nd ->
553
    try
554
      let (old, res) = Hashtbl.find table_eqs nd.node_id
555
      in if old == nd.node_stmts then res else raise Not_found
556
    with Not_found -> 
557
      let res = get_eqs nd.node_stmts in
558
      begin
559
	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
560
	res
561
      end)
562
563 01c7d5e1 ploc
let get_node_eq id node =
564 b08ffca7 xthirioux
 List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node)
565 22fe1c93 ploc
566
let get_nodes prog = 
567
  List.fold_left (
568
    fun nodes decl ->
569
      match decl.top_decl_desc with
570 ef34b4ae xthirioux
	| Node _ -> decl::nodes
571
	| Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes  
572 22fe1c93 ploc
  ) [] prog
573
574 ef34b4ae xthirioux
let get_imported_nodes prog = 
575 c1adf235 ploc
  List.fold_left (
576 ef34b4ae xthirioux
    fun nodes decl ->
577 c1adf235 ploc
      match decl.top_decl_desc with
578 ef34b4ae xthirioux
	| ImportedNode _ -> decl::nodes
579
	| Const _ | Node _ | Open _ | TypeDef _-> nodes  
580 c1adf235 ploc
  ) [] prog
581 22fe1c93 ploc
582 ef34b4ae xthirioux
let get_consts prog = 
583
  List.fold_right (
584
    fun decl consts ->
585 b1655a21 xthirioux
      match decl.top_decl_desc with
586 ef34b4ae xthirioux
	| Const _ -> decl::consts
587
	| Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts  
588
  ) prog []
589
590
let get_typedefs prog = 
591
  List.fold_right (
592
    fun decl types ->
593
      match decl.top_decl_desc with
594
	| TypeDef _ -> decl::types
595
	| Node _ | ImportedNode _ | Open _ | Const _ -> types  
596
  ) prog []
597
598
let get_dependencies prog =
599
  List.fold_right (
600
    fun decl deps ->
601
      match decl.top_decl_desc with
602
	| Open _ -> decl::deps
603
	| Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps  
604
  ) prog []
605 e2380d4d ploc
606 ed81df06 xthirioux
let get_node_interface nd =
607
 {nodei_id = nd.node_id;
608
  nodei_type = nd.node_type;
609
  nodei_clock = nd.node_clock;
610
  nodei_inputs = nd.node_inputs;
611
  nodei_outputs = nd.node_outputs;
612
  nodei_stateless = nd.node_dec_stateless;
613
  nodei_spec = nd.node_spec;
614
  nodei_prototype = None;
615 04a63d25 xthirioux
  nodei_in_lib = [];
616 ed81df06 xthirioux
 }
617
618 e2380d4d ploc
(************************************************************************)
619
(*        Renaming                                                      *)
620
621 ec433d69 xthirioux
let rec rename_static rename cty =
622
 match cty with
623
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
624
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
625
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
626
 | _                      -> cty
627
628
let rec rename_carrier rename cck =
629
 match cck with
630
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
631
 | _             -> cck
632
633
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
634
635
(* applies the renaming function [fvar] to all variables of expression [expr] *)
636
 let rec expr_replace_var fvar expr =
637
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
638
639
 and expr_desc_replace_var fvar expr_desc =
640
   match expr_desc with
641
   | Expr_const _ -> expr_desc
642
   | Expr_ident i -> Expr_ident (fvar i)
643
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
644
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
645
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
646
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
647
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
648
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
649
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
650
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
651
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
652
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
653
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
654
655
(* Applies the renaming function [fvar] to every rhs
656
   only when the corresponding lhs satisfies predicate [pvar] *)
657
 let eq_replace_rhs_var pvar fvar eq =
658
   let pvar l = List.exists pvar l in
659
   let rec replace lhs rhs =
660 04a63d25 xthirioux
     { rhs with expr_desc =
661 ec433d69 xthirioux
     match lhs with
662
     | []  -> assert false
663 04a63d25 xthirioux
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs.expr_desc else rhs.expr_desc
664 ec433d69 xthirioux
     | _   ->
665 04a63d25 xthirioux
       (match rhs.expr_desc with
666 ec433d69 xthirioux
       | Expr_tuple tl ->
667
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
668 04a63d25 xthirioux
       | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
669 ec433d69 xthirioux
	 let args = expr_list_of_expr arg in
670
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
671
       | Expr_array _
672
       | Expr_access _
673
       | Expr_power _
674
       | Expr_const _
675
       | Expr_ident _
676
       | Expr_appl _   ->
677
	 if pvar lhs
678 04a63d25 xthirioux
	 then expr_desc_replace_var fvar rhs.expr_desc
679
	 else rhs.expr_desc
680 ec433d69 xthirioux
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
681
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
682
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
683
       | Expr_pre e'          -> Expr_pre (replace lhs e')
684
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
685
				 in Expr_when (replace lhs e', i', l)
686
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
687
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
688
       )
689 04a63d25 xthirioux
     }
690 ec433d69 xthirioux
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
691
692
693
 let rec rename_expr  f_node f_var f_const expr =
694
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
695
 and rename_expr_desc f_node f_var f_const expr_desc =
696
   let re = rename_expr  f_node f_var f_const 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_node_annot f_node f_var f_const expr  =
715
   expr
716
 (* TODO assert false *)
717
718
 let rename_expr_annot f_node f_var f_const annot =
719
   annot
720
 (* TODO assert false *)
721
722
let rename_node f_node f_var f_const nd =
723
  let rename_var v = { v with var_id = f_var v.var_id } in
724
  let rename_eq eq = { eq with
725
      eq_lhs = List.map f_var eq.eq_lhs; 
726
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
727
    } 
728
  in
729
  let inputs = List.map rename_var nd.node_inputs in
730
  let outputs = List.map rename_var nd.node_outputs in
731
  let locals = List.map rename_var nd.node_locals in
732
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
733
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
734
  let node_asserts = List.map 
735
    (fun a -> 
736
      {a with assert_expr = 
737
	  let expr = a.assert_expr in
738
	  rename_expr f_node f_var f_const expr})
739
    nd.node_asserts
740
  in
741
  let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in
742
  let spec = 
743
    Utils.option_map 
744
      (fun s -> rename_node_annot f_node f_var f_const s) 
745
      nd.node_spec 
746
  in
747
  let annot =
748
    List.map 
749
      (fun s -> rename_expr_annot f_node f_var f_const s) 
750
      nd.node_annot
751
  in
752
  {
753
    node_id = f_node nd.node_id;
754
    node_type = nd.node_type;
755
    node_clock = nd.node_clock;
756
    node_inputs = inputs;
757
    node_outputs = outputs;
758
    node_locals = locals;
759
    node_gencalls = gen_calls;
760
    node_checks = node_checks;
761
    node_asserts = node_asserts;
762
    node_stmts = node_stmts;
763
    node_dec_stateless = nd.node_dec_stateless;
764
    node_stateless = nd.node_stateless;
765
    node_spec = spec;
766
    node_annot = annot;
767
  }
768
769
770
let rename_const f_const c =
771
  { c with const_id = f_const c.const_id }
772
773
let rename_typedef f_var t =
774
  match t.tydef_desc with
775
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
776
  | _               -> t
777
778
let rename_prog f_node f_var f_const prog =
779
  List.rev (
780
    List.fold_left (fun accu top ->
781
      (match top.top_decl_desc with
782
      | Node nd -> 
783
	 { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
784
      | Const c -> 
785
	 { top with top_decl_desc = Const (rename_const f_const c) }
786
      | TypeDef tdef ->
787
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
788
      | ImportedNode _
789
      | Open _       -> top)
790
      ::accu
791
) [] prog
792
		   )
793
794
(**********************************************************************)
795
(* Pretty printers *)
796
797
let pp_decl_type fmt tdecl =
798
  match tdecl.top_decl_desc with
799
  | Node nd ->
800
    fprintf fmt "%s: " nd.node_id;
801
    Utils.reset_names ();
802
    fprintf fmt "%a@ " Types.print_ty nd.node_type
803
  | ImportedNode ind ->
804
    fprintf fmt "%s: " ind.nodei_id;
805
    Utils.reset_names ();
806
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
807
  | Const _ | Open _ | TypeDef _ -> ()
808
809
let pp_prog_type fmt tdecl_list =
810
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
811
812
let pp_decl_clock fmt cdecl =
813
  match cdecl.top_decl_desc with
814
  | Node nd ->
815
    fprintf fmt "%s: " nd.node_id;
816
    Utils.reset_names ();
817
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
818
  | ImportedNode ind ->
819
    fprintf fmt "%s: " ind.nodei_id;
820
    Utils.reset_names ();
821
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
822
  | Const _ | Open _ | TypeDef _ -> ()
823
824
let pp_prog_clock fmt prog =
825
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
826
827
828
(* filling node table with internal functions *)
829
let vdecls_of_typ_ck cpt ty =
830
  let loc = Location.dummy_loc in
831
  List.map
832
    (fun _ -> incr cpt;
833
              let name = sprintf "_var_%d" !cpt in
834
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
835
    (Types.type_list_of_type ty)
836
837
let mk_internal_node id =
838
  let spec = None in
839
  let ty = Env.lookup_value Basic_library.type_env id in
840
  let ck = Env.lookup_value Basic_library.clock_env id in
841
  let (tin, tout) = Types.split_arrow ty in
842
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
843
  let cpt = ref (-1) in
844
  mktop
845
    (ImportedNode
846
       {nodei_id = id;
847
	nodei_type = ty;
848
	nodei_clock = ck;
849
	nodei_inputs = vdecls_of_typ_ck cpt tin;
850
	nodei_outputs = vdecls_of_typ_ck cpt tout;
851
	nodei_stateless = Types.get_static_value ty <> None;
852
	nodei_spec = spec;
853
	nodei_prototype = None;
854 04a63d25 xthirioux
       	nodei_in_lib = [];
855 ec433d69 xthirioux
       })
856
857
let add_internal_funs () =
858
  List.iter
859
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
860
    Basic_library.internal_funs
861
862
863
864
(* Replace any occurence of a var in vars_to_replace by its associated
865
   expression in defs until e does not contain any such variables *)
866
let rec substitute_expr vars_to_replace defs e =
867
  let se = substitute_expr vars_to_replace defs in
868
  { e with expr_desc = 
869
      let ed = e.expr_desc in
870
      match ed with
871
      | Expr_const _ -> ed
872
      | Expr_array el -> Expr_array (List.map se el)
873
      | Expr_access (e1, d) -> Expr_access (se e1, d)
874
      | Expr_power (e1, d) -> Expr_power (se e1, d)
875
      | Expr_tuple el -> Expr_tuple (List.map se el)
876
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
877
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
878
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
879
      | Expr_pre e' -> Expr_pre (se e')
880
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
881
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
882
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
883
      | Expr_ident i -> 
884
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
885
	  let eq_i eq = eq.eq_lhs = [i] in
886
	  if List.exists eq_i defs then
887
	    let sub = List.find eq_i defs in
888
	    let sub' = se sub.eq_rhs in
889
	    sub'.expr_desc
890
	  else 
891
	    assert false
892
	)
893
	else
894
	  ed
895
896
  }
897
(* FAUT IL RETIRER ?
898
  
899
 let rec expr_to_eexpr  expr =
900
   { eexpr_tag = expr.expr_tag;
901
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
902
     eexpr_type = expr.expr_type;
903
     eexpr_clock = expr.expr_clock;
904
     eexpr_loc = expr.expr_loc
905
   }
906
 and expr_desc_to_eexpr_desc expr_desc =
907
   let conv = expr_to_eexpr in
908
   match expr_desc with
909
   | Expr_const c -> EExpr_const (match c with
910
     | Const_int x -> EConst_int x 
911
     | Const_real x -> EConst_real x 
912
     | Const_float x -> EConst_float x 
913
     | Const_tag x -> EConst_tag x 
914
     | _ -> assert false
915
916
   )
917
   | Expr_ident i -> EExpr_ident i
918
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
919
920
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
921
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
922
   | Expr_pre e' -> EExpr_pre (conv e')
923
   | Expr_appl (i, e', i') -> 
924
     EExpr_appl 
925
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
926
927
   | Expr_when _
928
   | Expr_merge _ -> assert false
929
   | Expr_array _ 
930
   | Expr_access _ 
931
   | Expr_power _  -> assert false
932
   | Expr_ite (c, t, e) -> assert false 
933
   | _ -> assert false
934
935
     *)
936
let rec get_expr_calls nodes e =
937
  let get_calls = get_expr_calls nodes in
938 04a63d25 xthirioux
  match e.expr_desc with
939 ec433d69 xthirioux
  | Expr_const _ 
940
   | Expr_ident _ -> Utils.ISet.empty
941
   | Expr_tuple el
942
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
943
   | Expr_pre e1 
944
   | Expr_when (e1, _, _) 
945
   | Expr_access (e1, _) 
946
   | Expr_power (e1, _) -> get_calls e1
947
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
948
   | Expr_arrow (e1, e2) 
949
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
950
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
951
   | Expr_appl (i, e', i') -> 
952 04a63d25 xthirioux
     if Basic_library.is_expr_internal_fun e then 
953 ec433d69 xthirioux
       (get_calls e') 
954
     else
955
       let calls =  Utils.ISet.add i (get_calls e') in
956
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
957
       if List.exists test nodes then
958
	 match (List.find test nodes).top_decl_desc with
959
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
960
	 | _ -> assert false
961
       else 
962
	 calls
963
964
and get_eq_calls nodes eq =
965
  get_expr_calls nodes eq.eq_rhs
966
and get_node_calls nodes node =
967
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
968
969 a6df3992 Ploc
let get_expr_vars e =
970
  let rec get_expr_vars vars e =
971
    get_expr_desc_vars vars e.expr_desc
972
  and get_expr_desc_vars vars expr_desc =
973 a85ca7df ploc
    (*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);*)
974 ec433d69 xthirioux
  match expr_desc with
975
  | Expr_const _ -> vars
976 a85ca7df ploc
  | Expr_ident x -> Utils.ISet.add x vars
977 ec433d69 xthirioux
  | Expr_tuple el
978
  | Expr_array el -> List.fold_left get_expr_vars vars el
979
  | Expr_pre e1 -> get_expr_vars vars e1
980
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
981
  | Expr_access (e1, d) 
982
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
983
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
984
  | Expr_arrow (e1, e2) 
985
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
986
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
987
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
988
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
989 a6df3992 Ploc
  in
990
  get_expr_vars Utils.ISet.empty e 
991 ec433d69 xthirioux
992
let rec expr_has_arrows e =
993
  expr_desc_has_arrows e.expr_desc
994
and expr_desc_has_arrows expr_desc =
995
  match expr_desc with
996
  | Expr_const _ 
997
  | Expr_ident _ -> false
998
  | Expr_tuple el
999
  | Expr_array el -> List.exists expr_has_arrows el
1000
  | Expr_pre e1 
1001
  | Expr_when (e1, _, _) 
1002
  | Expr_access (e1, _) 
1003
  | Expr_power (e1, _) -> expr_has_arrows e1
1004
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
1005
  | Expr_arrow (e1, e2) 
1006
  | Expr_fby (e1, e2) -> true
1007
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1008
  | Expr_appl (i, e', i') -> expr_has_arrows e'
1009
1010
and eq_has_arrows eq =
1011
  expr_has_arrows eq.eq_rhs
1012
and node_has_arrows node =
1013
  List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
1014
1015 01c7d5e1 ploc
1016 ec433d69 xthirioux
let copy_var_decl vdecl =
1017
  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)
1018
1019
let copy_const cdecl =
1020
  { cdecl with const_type = Types.new_var () }
1021
1022
let copy_node nd =
1023
  { nd with
1024
    node_type     = Types.new_var ();
1025
    node_clock    = Clocks.new_var true;
1026
    node_inputs   = List.map copy_var_decl nd.node_inputs;
1027
    node_outputs  = List.map copy_var_decl nd.node_outputs;
1028
    node_locals   = List.map copy_var_decl nd.node_locals;
1029
    node_gencalls = [];
1030
    node_checks   = [];
1031
    node_stateless = None;
1032
  }
1033
1034
let copy_top top =
1035
  match top.top_decl_desc with
1036
  | Node nd -> { top with top_decl_desc = Node (copy_node nd)  }
1037
  | Const c -> { top with top_decl_desc = Const (copy_const c) }
1038
  | _       -> top
1039
1040
let copy_prog top_list =
1041
  List.map copy_top top_list
1042
1043 e7cc5186 ploc
1044
let rec expr_contains_expr expr_tag expr  =
1045
  let search = expr_contains_expr expr_tag in
1046
  expr.expr_tag = expr_tag ||
1047
      (
1048
	match expr.expr_desc with
1049
	| Expr_const _ -> false
1050
	| Expr_array el -> List.exists search el
1051
	| Expr_access (e1, _) 
1052
	| Expr_power (e1, _) -> search e1
1053
	| Expr_tuple el -> List.exists search el
1054
	| Expr_ite (c, t, e) -> List.exists search [c;t;e]
1055
	| Expr_arrow (e1, e2)
1056
	| Expr_fby (e1, e2) -> List.exists search [e1; e2]
1057
	| Expr_pre e' 
1058
	| Expr_when (e', _, _) -> search e'
1059
	| Expr_merge (_, hl) -> List.exists (fun (_, h) -> search h) hl
1060
	| Expr_appl (_, e', None) -> search e' 
1061
	| Expr_appl (_, e', Some e'') -> List.exists search [e'; e''] 
1062
	| Expr_ident _ -> false
1063
      )
1064
1065 22fe1c93 ploc
(* Local Variables: *)
1066
(* compile-command:"make -C .." *)
1067
(* End: *)