Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ c203d676

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