Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 7ecfca04

History | View | Annotate | Download (34.8 KB)

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

    
12
open Format
13
open LustreSpec
14
open Dimension
15

    
16

    
17
exception Error of Location.t * error
18

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

    
25
module VMap = Map.Make(VDeclModule)
26

    
27
module VSet = Set.Make(VDeclModule)
28

    
29
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
(************************************************************)
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
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
45
  assert (value = None || is_const);
46
  { var_id = id;
47
    var_orig = orig;
48
    var_dec_type = ty_dec;
49
    var_dec_clock = ck_dec;
50
    var_dec_const = is_const;
51
    var_dec_value = value;
52
    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
    var_orig = true;
68
    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
    var_dec_value = None;
72
    var_type = c.const_type;
73
    var_clock = Clocks.new_var false;
74
    var_loc = c.const_loc }
75

    
76
let mk_new_name used id =
77
  let rec new_name name cpt =
78
    if used name
79
    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
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

    
96
let mkpredef_call loc funname args =
97
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
98

    
99
let mkpredef_unary_call loc funname arg =
100
  mkexpr loc (Expr_appl (funname, arg, None))
101

    
102
let is_clock_dec_type cty =
103
  match cty with
104
  | Tydec_clock _ -> true
105
  | _             -> false
106

    
107
let const_of_top top_decl =
108
  match top_decl.top_decl_desc with
109
  | Const c -> c
110
  | _ -> assert false
111

    
112
let node_of_top top_decl =
113
  match top_decl.top_decl_desc with
114
  | Node nd -> nd
115
  | _ -> assert false
116

    
117
let imported_node_of_top top_decl =
118
  match top_decl.top_decl_desc with
119
  | ImportedNode ind -> ind
120
  | _ -> assert false
121

    
122
let typedef_of_top top_decl =
123
  match top_decl.top_decl_desc with
124
  | TypeDef tdef -> tdef
125
  | _ -> assert false
126

    
127
let dependency_of_top top_decl =
128
  match top_decl.top_decl_desc with
129
  | Open (local, dep) -> (local, dep)
130
  | _ -> assert false
131

    
132
let consts_of_enum_type top_decl =
133
  match top_decl.top_decl_desc with
134
  | TypeDef tdef ->
135
    (match tdef.tydef_desc with
136
     | 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
137
     | _               -> [])
138
  | _ -> assert false
139

    
140
(************************************************************)
141
(*   Eexpr functions *)
142
(************************************************************)
143

    
144
let merge_node_annot ann1 ann2 =
145
  { requires = ann1.requires @ ann2.requires;
146
    ensures = ann1.ensures @ ann2.ensures;
147
    behaviors = ann1.behaviors @ ann2.behaviors;
148
    spec_loc = ann1.spec_loc
149
  }
150

    
151
let mkeexpr loc expr =
152
  { eexpr_tag = Utils.new_tag ();
153
    eexpr_qfexpr = expr;
154
    eexpr_quantifiers = [];
155
    eexpr_type = Types.new_var ();
156
    eexpr_clock = Clocks.new_var true;
157
    eexpr_normalized = None;
158
    eexpr_loc = loc }
159

    
160
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
161

    
162
(*
163
let mkepredef_call loc funname args =
164
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
165

    
166
let mkepredef_unary_call loc funname arg =
167
  mkeexpr loc (EExpr_appl (funname, arg, None))
168
*)
169

    
170
let merge_expr_annot ann1 ann2 =
171
  match ann1, ann2 with
172
    | None, None -> assert false
173
    | Some _, None -> ann1
174
    | None, Some _ -> ann2
175
    | Some ann1, Some ann2 -> Some {
176
      annots = ann1.annots @ ann2.annots;
177
      annot_loc = ann1.annot_loc
178
    }
179

    
180
let update_expr_annot node_id e annot =
181
  List.iter (fun (key, _) -> 
182
    Annotations.add_expr_ann node_id e.expr_tag key
183
  ) annot.annots;
184
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
185

    
186

    
187
(***********************************************************)
188
(* Fast access to nodes, by name *)
189
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
190
let consts_table = Hashtbl.create 30
191

    
192
let print_node_table fmt () =
193
  begin
194
    Format.fprintf fmt "{ /* node table */@.";
195
    Hashtbl.iter (fun id nd ->
196
      Format.fprintf fmt "%s |-> %a"
197
	id
198
	Printers.pp_short_decl nd
199
    ) node_table;
200
    Format.fprintf fmt "}@."
201
  end
202

    
203
let print_consts_table fmt () =
204
  begin
205
    Format.fprintf fmt "{ /* consts table */@.";
206
    Hashtbl.iter (fun id const ->
207
      Format.fprintf fmt "%s |-> %a"
208
	id
209
	Printers.pp_const_decl (const_of_top const)
210
    ) consts_table;
211
    Format.fprintf fmt "}@."
212
  end
213

    
214
let node_name td =
215
    match td.top_decl_desc with 
216
    | Node nd         -> nd.node_id
217
    | ImportedNode nd -> nd.nodei_id
218
    | _ -> assert false
219

    
220
let is_generic_node td =
221
  match td.top_decl_desc with 
222
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
223
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
224
  | _ -> assert false
225

    
226
let node_inputs td =
227
  match td.top_decl_desc with 
228
  | Node nd         -> nd.node_inputs
229
  | ImportedNode nd -> nd.nodei_inputs
230
  | _ -> assert false
231

    
232
let node_from_name id =
233
  try
234
    Hashtbl.find node_table id
235
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
236
		     assert false)
237

    
238
let is_imported_node td =
239
  match td.top_decl_desc with 
240
  | Node nd         -> false
241
  | ImportedNode nd -> true
242
  | _ -> assert false
243

    
244

    
245
(* alias and type definition table *)
246

    
247
let mktop = mktop_decl Location.dummy_loc !Options.include_dir false
248

    
249
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
250
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
251
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
252
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
253

    
254
let type_table =
255
  Utils.create_hashtable 20 [
256
    Tydec_int  , top_int_type;
257
    Tydec_bool , top_bool_type;
258
    (* Tydec_float, top_float_type; *)
259
    Tydec_real , top_real_type
260
  ]
261

    
262
let print_type_table fmt () =
263
  begin
264
    Format.fprintf fmt "{ /* type table */@.";
265
    Hashtbl.iter (fun tydec tdef ->
266
      Format.fprintf fmt "%a |-> %a"
267
	Printers.pp_var_type_dec_desc tydec
268
	Printers.pp_typedef (typedef_of_top tdef)
269
    ) type_table;
270
    Format.fprintf fmt "}@."
271
  end
272

    
273
let rec is_user_type typ =
274
  match typ with
275
  | Tydec_int | Tydec_bool | Tydec_real 
276
  (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
277
  | Tydec_clock typ' -> is_user_type typ'
278
  | _ -> true
279

    
280
let get_repr_type typ =
281
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
282
  if is_user_type typ_def then typ else typ_def
283

    
284
let rec coretype_equal ty1 ty2 =
285
  let res =
286
  match ty1, ty2 with
287
  | Tydec_any           , _
288
  | _                   , Tydec_any             -> assert false
289
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
290
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
291
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
292
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
293
  | Tydec_int           , Tydec_int
294
  | Tydec_real          , Tydec_real
295
  (* | Tydec_float         , Tydec_float *)
296
  | Tydec_bool          , Tydec_bool            -> true
297
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
298
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
299
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
300
  | Tydec_struct fl1    , Tydec_struct fl2      ->
301
       List.length fl1 = List.length fl2
302
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
303
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
304
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
305
  | _                                  -> false
306
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
307

    
308
let tag_true = "true"
309
let tag_false = "false"
310
let tag_default = "default"
311

    
312
let const_is_bool c =
313
 match c with
314
 | Const_tag t -> t = tag_true || t = tag_false
315
 | _           -> false
316

    
317
(* Computes the negation of a boolean constant *)
318
let const_negation c =
319
  assert (const_is_bool c);
320
  match c with
321
  | Const_tag t when t = tag_true  -> Const_tag tag_false
322
  | _                              -> Const_tag tag_true
323

    
324
let const_or c1 c2 =
325
  assert (const_is_bool c1 && const_is_bool c2);
326
  match c1, c2 with
327
  | Const_tag t1, _            when t1 = tag_true -> c1
328
  | _           , Const_tag t2 when t2 = tag_true -> c2
329
  | _                                             -> Const_tag tag_false
330

    
331
let const_and c1 c2 =
332
  assert (const_is_bool c1 && const_is_bool c2);
333
  match c1, c2 with
334
  | Const_tag t1, _            when t1 = tag_false -> c1
335
  | _           , Const_tag t2 when t2 = tag_false -> c2
336
  | _                                              -> Const_tag tag_true
337

    
338
let const_xor c1 c2 =
339
  assert (const_is_bool c1 && const_is_bool c2);
340
   match c1, c2 with
341
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
342
  | _                                         -> Const_tag tag_false
343

    
344
let const_impl c1 c2 =
345
  assert (const_is_bool c1 && const_is_bool c2);
346
  match c1, c2 with
347
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
348
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
349
  | _                                             -> Const_tag tag_false
350

    
351
(* To guarantee uniqueness of tags in enum types *)
352
let tag_table =
353
  Utils.create_hashtable 20 [
354
   tag_true, top_bool_type;
355
   tag_false, top_bool_type
356
  ]
357

    
358
(* To guarantee uniqueness of fields in struct types *)
359
let field_table =
360
  Utils.create_hashtable 20 [
361
  ]
362

    
363
let get_enum_type_tags cty =
364
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
365
 match cty with
366
 | Tydec_bool    -> [tag_true; tag_false]
367
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
368
                     | Tydec_enum tl -> tl
369
                     | _             -> assert false)
370
 | _            -> assert false
371

    
372
let get_struct_type_fields cty =
373
 match cty with
374
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
375
                     | Tydec_struct fl -> fl
376
                     | _               -> assert false)
377
 | _            -> assert false
378

    
379
let const_of_bool b =
380
 Const_tag (if b then tag_true else tag_false)
381

    
382
(* let get_const c = snd (Hashtbl.find consts_table c) *)
383

    
384
let ident_of_expr expr =
385
 match expr.expr_desc with
386
 | Expr_ident id -> id
387
 | _             -> assert false
388

    
389
(* Generate a new ident expression from a declared variable *)
390
let expr_of_vdecl v =
391
  { expr_tag = Utils.new_tag ();
392
    expr_desc = Expr_ident v.var_id;
393
    expr_type = v.var_type;
394
    expr_clock = v.var_clock;
395
    expr_delay = Delay.new_var ();
396
    expr_annot = None;
397
    expr_loc = v.var_loc }
398

    
399
(* Caution, returns an untyped and unclocked expression *)
400
let expr_of_ident id loc =
401
  {expr_tag = Utils.new_tag ();
402
   expr_desc = Expr_ident id;
403
   expr_type = Types.new_var ();
404
   expr_clock = Clocks.new_var true;
405
   expr_delay = Delay.new_var ();
406
   expr_loc = loc;
407
   expr_annot = None}
408

    
409
let is_tuple_expr expr =
410
 match expr.expr_desc with
411
  | Expr_tuple _ -> true
412
  | _            -> false
413

    
414
let expr_list_of_expr expr =
415
  match expr.expr_desc with
416
  | Expr_tuple elist -> elist
417
  | _                -> [expr]
418

    
419
let expr_of_expr_list loc elist =
420
 match elist with
421
 | [t]  -> { t with expr_loc = loc }
422
 | t::_ ->
423
    let tlist = List.map (fun e -> e.expr_type) elist in
424
    let clist = List.map (fun e -> e.expr_clock) elist in
425
    { t with expr_desc = Expr_tuple elist;
426
	     expr_type = Type_predef.type_tuple tlist;
427
	     expr_clock = Clock_predef.ck_tuple clist;
428
	     expr_tag = Utils.new_tag ();
429
	     expr_loc = loc }
430
 | _    -> assert false
431

    
432
let call_of_expr expr =
433
 match expr.expr_desc with
434
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
435
 | _                      -> assert false
436

    
437
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
438
let rec expr_of_dimension dim =
439
 match dim.dim_desc with
440
 | Dbool b        ->
441
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
442
 | Dint i         ->
443
     mkexpr dim.dim_loc (Expr_const (Const_int i))
444
 | Dident id      ->
445
     mkexpr dim.dim_loc (Expr_ident id)
446
 | Dite (c, t, e) ->
447
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
448
 | Dappl (id, args) ->
449
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
450
 | Dlink dim'       -> expr_of_dimension dim'
451
 | Dvar
452
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
453
			assert false)
454

    
455
let dimension_of_const loc const =
456
 match const with
457
 | Const_int i                                    -> mkdim_int loc i
458
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
459
 | _                                              -> raise InvalidDimension
460

    
461
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
462
   into dimension expressions *)
463
let rec dimension_of_expr expr =
464
  match expr.expr_desc with
465
  | Expr_const c  -> dimension_of_const expr.expr_loc c
466
  | Expr_ident id -> mkdim_ident expr.expr_loc id
467
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
468
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
469
      if k = None then raise InvalidDimension;
470
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
471
  | Expr_ite (i, t, e)        ->
472
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
473
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
474

    
475

    
476
let sort_handlers hl =
477
 List.sort (fun (t, _) (t', _) -> compare t t') hl
478

    
479
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
480
  | Expr_const c1, Expr_const c2 -> c1 = c2
481
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
482
  | Expr_array el1, Expr_array el2 
483
  | Expr_tuple el1, Expr_tuple el2 -> 
484
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
485
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
486
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
487
  | 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
488
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
489
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
490
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
491
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
492
  | 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')
493
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
494
  | Expr_power (e1, i1), Expr_power (e2, i2)
495
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
496
  | _ -> false
497

    
498
let get_node_vars nd =
499
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
500

    
501
let mk_new_node_name nd id =
502
  let used_vars = get_node_vars nd in
503
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
504
  mk_new_name used id
505

    
506
let get_var id var_list =
507
  List.find (fun v -> v.var_id = id) var_list
508

    
509
let get_node_var id node =
510
  get_var id (get_node_vars node)
511

    
512
let get_node_eqs =
513
  let get_eqs stmts =
514
    List.fold_right
515
      (fun stmt res ->
516
	match stmt with
517
	| Eq eq -> eq :: res
518
	| Aut _ -> assert false)
519
      stmts
520
      [] in
521
  let table_eqs = Hashtbl.create 23 in
522
  (fun nd ->
523
    try
524
      let (old, res) = Hashtbl.find table_eqs nd.node_id
525
      in if old == nd.node_stmts then res else raise Not_found
526
    with Not_found -> 
527
      let res = get_eqs nd.node_stmts in
528
      begin
529
	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
530
	res
531
      end)
532

    
533
let get_node_eq id node =
534
 List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node)
535

    
536
let get_nodes prog = 
537
  List.fold_left (
538
    fun nodes decl ->
539
      match decl.top_decl_desc with
540
	| Node _ -> decl::nodes
541
	| Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes  
542
  ) [] prog
543

    
544
let get_imported_nodes prog = 
545
  List.fold_left (
546
    fun nodes decl ->
547
      match decl.top_decl_desc with
548
	| ImportedNode _ -> decl::nodes
549
	| Const _ | Node _ | Open _ | TypeDef _-> nodes  
550
  ) [] prog
551

    
552
let get_consts prog = 
553
  List.fold_right (
554
    fun decl consts ->
555
      match decl.top_decl_desc with
556
	| Const _ -> decl::consts
557
	| Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts  
558
  ) prog []
559

    
560
let get_typedefs prog = 
561
  List.fold_right (
562
    fun decl types ->
563
      match decl.top_decl_desc with
564
	| TypeDef _ -> decl::types
565
	| Node _ | ImportedNode _ | Open _ | Const _ -> types  
566
  ) prog []
567

    
568
let get_dependencies prog =
569
  List.fold_right (
570
    fun decl deps ->
571
      match decl.top_decl_desc with
572
	| Open _ -> decl::deps
573
	| Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps  
574
  ) prog []
575

    
576
let get_node_interface nd =
577
 {nodei_id = nd.node_id;
578
  nodei_type = nd.node_type;
579
  nodei_clock = nd.node_clock;
580
  nodei_inputs = nd.node_inputs;
581
  nodei_outputs = nd.node_outputs;
582
  nodei_stateless = nd.node_dec_stateless;
583
  nodei_spec = nd.node_spec;
584
  nodei_prototype = None;
585
  nodei_in_lib = [];
586
 }
587

    
588
(************************************************************************)
589
(*        Renaming                                                      *)
590

    
591
let rec rename_static rename cty =
592
 match cty with
593
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
594
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
595
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
596
 | _                      -> cty
597

    
598
let rec rename_carrier rename cck =
599
 match cck with
600
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
601
 | _             -> cck
602

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

    
605
(* applies the renaming function [fvar] to all variables of expression [expr] *)
606
 let rec expr_replace_var fvar expr =
607
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
608

    
609
 and expr_desc_replace_var fvar expr_desc =
610
   match expr_desc with
611
   | Expr_const _ -> expr_desc
612
   | Expr_ident i -> Expr_ident (fvar i)
613
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
614
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
615
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
616
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
617
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
618
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
619
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
620
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
621
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
622
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
623
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
624

    
625
(* Applies the renaming function [fvar] to every rhs
626
   only when the corresponding lhs satisfies predicate [pvar] *)
627
 let eq_replace_rhs_var pvar fvar eq =
628
   let pvar l = List.exists pvar l in
629
   let rec replace lhs rhs =
630
     { rhs with expr_desc =
631
     match lhs with
632
     | []  -> assert false
633
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs.expr_desc else rhs.expr_desc
634
     | _   ->
635
       (match rhs.expr_desc with
636
       | Expr_tuple tl ->
637
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
638
       | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
639
	 let args = expr_list_of_expr arg in
640
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
641
       | Expr_array _
642
       | Expr_access _
643
       | Expr_power _
644
       | Expr_const _
645
       | Expr_ident _
646
       | Expr_appl _   ->
647
	 if pvar lhs
648
	 then expr_desc_replace_var fvar rhs.expr_desc
649
	 else rhs.expr_desc
650
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
651
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
652
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
653
       | Expr_pre e'          -> Expr_pre (replace lhs e')
654
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
655
				 in Expr_when (replace lhs e', i', l)
656
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
657
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
658
       )
659
     }
660
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
661

    
662

    
663
 let rec rename_expr  f_node f_var f_const expr =
664
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
665
 and rename_expr_desc f_node f_var f_const expr_desc =
666
   let re = rename_expr  f_node f_var f_const in
667
   match expr_desc with
668
   | Expr_const _ -> expr_desc
669
   | Expr_ident i -> Expr_ident (f_var i)
670
   | Expr_array el -> Expr_array (List.map re el)
671
   | Expr_access (e1, d) -> Expr_access (re e1, d)
672
   | Expr_power (e1, d) -> Expr_power (re e1, d)
673
   | Expr_tuple el -> Expr_tuple (List.map re el)
674
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
675
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
676
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
677
   | Expr_pre e' -> Expr_pre (re e')
678
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
679
   | Expr_merge (i, hl) -> 
680
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
681
   | Expr_appl (i, e', i') -> 
682
     Expr_appl (f_node i, re e', Utils.option_map re i')
683
  
684
 let rename_node_annot f_node f_var f_const expr  =
685
   expr
686
 (* TODO assert false *)
687

    
688
 let rename_expr_annot f_node f_var f_const annot =
689
   annot
690
 (* TODO assert false *)
691

    
692
let rename_node f_node f_var f_const nd =
693
  let rename_var v = { v with var_id = f_var v.var_id } in
694
  let rename_eq eq = { eq with
695
      eq_lhs = List.map f_var eq.eq_lhs; 
696
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
697
    } 
698
  in
699
  let inputs = List.map rename_var nd.node_inputs in
700
  let outputs = List.map rename_var nd.node_outputs in
701
  let locals = List.map rename_var nd.node_locals in
702
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
703
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
704
  let node_asserts = List.map 
705
    (fun a -> 
706
      {a with assert_expr = 
707
	  let expr = a.assert_expr in
708
	  rename_expr f_node f_var f_const expr})
709
    nd.node_asserts
710
  in
711
  let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in
712
  let spec = 
713
    Utils.option_map 
714
      (fun s -> rename_node_annot f_node f_var f_const s) 
715
      nd.node_spec 
716
  in
717
  let annot =
718
    List.map 
719
      (fun s -> rename_expr_annot f_node f_var f_const s) 
720
      nd.node_annot
721
  in
722
  {
723
    node_id = f_node nd.node_id;
724
    node_type = nd.node_type;
725
    node_clock = nd.node_clock;
726
    node_inputs = inputs;
727
    node_outputs = outputs;
728
    node_locals = locals;
729
    node_gencalls = gen_calls;
730
    node_checks = node_checks;
731
    node_asserts = node_asserts;
732
    node_stmts = node_stmts;
733
    node_dec_stateless = nd.node_dec_stateless;
734
    node_stateless = nd.node_stateless;
735
    node_spec = spec;
736
    node_annot = annot;
737
  }
738

    
739

    
740
let rename_const f_const c =
741
  { c with const_id = f_const c.const_id }
742

    
743
let rename_typedef f_var t =
744
  match t.tydef_desc with
745
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
746
  | _               -> t
747

    
748
let rename_prog f_node f_var f_const prog =
749
  List.rev (
750
    List.fold_left (fun accu top ->
751
      (match top.top_decl_desc with
752
      | Node nd -> 
753
	 { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
754
      | Const c -> 
755
	 { top with top_decl_desc = Const (rename_const f_const c) }
756
      | TypeDef tdef ->
757
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
758
      | ImportedNode _
759
      | Open _       -> top)
760
      ::accu
761
) [] prog
762
		   )
763

    
764
(**********************************************************************)
765
(* Pretty printers *)
766

    
767
let pp_decl_type fmt tdecl =
768
  match tdecl.top_decl_desc with
769
  | Node nd ->
770
    fprintf fmt "%s: " nd.node_id;
771
    Utils.reset_names ();
772
    fprintf fmt "%a@ " Types.print_ty nd.node_type
773
  | ImportedNode ind ->
774
    fprintf fmt "%s: " ind.nodei_id;
775
    Utils.reset_names ();
776
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
777
  | Const _ | Open _ | TypeDef _ -> ()
778

    
779
let pp_prog_type fmt tdecl_list =
780
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
781

    
782
let pp_decl_clock fmt cdecl =
783
  match cdecl.top_decl_desc with
784
  | Node nd ->
785
    fprintf fmt "%s: " nd.node_id;
786
    Utils.reset_names ();
787
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
788
  | ImportedNode ind ->
789
    fprintf fmt "%s: " ind.nodei_id;
790
    Utils.reset_names ();
791
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
792
  | Const _ | Open _ | TypeDef _ -> ()
793

    
794
let pp_prog_clock fmt prog =
795
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
796

    
797
let pp_error fmt = function
798
    Main_not_found ->
799
      fprintf fmt "Could not find the definition of main node %s.@."
800
	!Global.main_node
801
  | Main_wrong_kind ->
802
    fprintf fmt
803
      "Node %s does not correspond to a valid main node definition.@." 
804
      !Global.main_node 
805
  | No_main_specified ->
806
    fprintf fmt "No main node specified (use -node option)@."
807
  | Unbound_symbol sym ->
808
    fprintf fmt
809
      "%s is undefined.@."
810
      sym
811
  | Already_bound_symbol sym -> 
812
    fprintf fmt
813
      "%s is already defined.@."
814
      sym
815
  | Unknown_library sym ->
816
    fprintf fmt
817
      "impossible to load library %s.lusic.@.Please compile the corresponding interface or source file.@."
818
      sym
819
  | Wrong_number sym ->
820
    fprintf fmt
821
      "library %s.lusic has a different version number and may crash compiler.@.Please recompile the corresponding interface or source file.@."
822
      sym
823

    
824
(* filling node table with internal functions *)
825
let vdecls_of_typ_ck cpt ty =
826
  let loc = Location.dummy_loc in
827
  List.map
828
    (fun _ -> incr cpt;
829
              let name = sprintf "_var_%d" !cpt in
830
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
831
    (Types.type_list_of_type ty)
832

    
833
let mk_internal_node id =
834
  let spec = None in
835
  let ty = Env.lookup_value Basic_library.type_env id in
836
  let ck = Env.lookup_value Basic_library.clock_env id in
837
  let (tin, tout) = Types.split_arrow ty in
838
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
839
  let cpt = ref (-1) in
840
  mktop
841
    (ImportedNode
842
       {nodei_id = id;
843
	nodei_type = ty;
844
	nodei_clock = ck;
845
	nodei_inputs = vdecls_of_typ_ck cpt tin;
846
	nodei_outputs = vdecls_of_typ_ck cpt tout;
847
	nodei_stateless = Types.get_static_value ty <> None;
848
	nodei_spec = spec;
849
	nodei_prototype = None;
850
       	nodei_in_lib = [];
851
       })
852

    
853
let add_internal_funs () =
854
  List.iter
855
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
856
    Basic_library.internal_funs
857

    
858

    
859

    
860
(* Replace any occurence of a var in vars_to_replace by its associated
861
   expression in defs until e does not contain any such variables *)
862
let rec substitute_expr vars_to_replace defs e =
863
  let se = substitute_expr vars_to_replace defs in
864
  { e with expr_desc = 
865
      let ed = e.expr_desc in
866
      match ed with
867
      | Expr_const _ -> ed
868
      | Expr_array el -> Expr_array (List.map se el)
869
      | Expr_access (e1, d) -> Expr_access (se e1, d)
870
      | Expr_power (e1, d) -> Expr_power (se e1, d)
871
      | Expr_tuple el -> Expr_tuple (List.map se el)
872
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
873
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
874
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
875
      | Expr_pre e' -> Expr_pre (se e')
876
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
877
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
878
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
879
      | Expr_ident i -> 
880
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
881
	  let eq_i eq = eq.eq_lhs = [i] in
882
	  if List.exists eq_i defs then
883
	    let sub = List.find eq_i defs in
884
	    let sub' = se sub.eq_rhs in
885
	    sub'.expr_desc
886
	  else 
887
	    assert false
888
	)
889
	else
890
	  ed
891

    
892
  }
893
(* FAUT IL RETIRER ?
894
  
895
 let rec expr_to_eexpr  expr =
896
   { eexpr_tag = expr.expr_tag;
897
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
898
     eexpr_type = expr.expr_type;
899
     eexpr_clock = expr.expr_clock;
900
     eexpr_loc = expr.expr_loc
901
   }
902
 and expr_desc_to_eexpr_desc expr_desc =
903
   let conv = expr_to_eexpr in
904
   match expr_desc with
905
   | Expr_const c -> EExpr_const (match c with
906
     | Const_int x -> EConst_int x 
907
     | Const_real x -> EConst_real x 
908
     | Const_float x -> EConst_float x 
909
     | Const_tag x -> EConst_tag x 
910
     | _ -> assert false
911

    
912
   )
913
   | Expr_ident i -> EExpr_ident i
914
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
915

    
916
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
917
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
918
   | Expr_pre e' -> EExpr_pre (conv e')
919
   | Expr_appl (i, e', i') -> 
920
     EExpr_appl 
921
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
922

    
923
   | Expr_when _
924
   | Expr_merge _ -> assert false
925
   | Expr_array _ 
926
   | Expr_access _ 
927
   | Expr_power _  -> assert false
928
   | Expr_ite (c, t, e) -> assert false 
929
   | _ -> assert false
930

    
931
     *)
932
let rec get_expr_calls nodes e =
933
  let get_calls = get_expr_calls nodes in
934
  match e.expr_desc with
935
  | Expr_const _ 
936
   | Expr_ident _ -> Utils.ISet.empty
937
   | Expr_tuple el
938
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
939
   | Expr_pre e1 
940
   | Expr_when (e1, _, _) 
941
   | Expr_access (e1, _) 
942
   | Expr_power (e1, _) -> get_calls e1
943
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
944
   | Expr_arrow (e1, e2) 
945
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
946
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
947
   | Expr_appl (i, e', i') -> 
948
     if Basic_library.is_expr_internal_fun e then 
949
       (get_calls e') 
950
     else
951
       let calls =  Utils.ISet.add i (get_calls e') in
952
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
953
       if List.exists test nodes then
954
	 match (List.find test nodes).top_decl_desc with
955
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
956
	 | _ -> assert false
957
       else 
958
	 calls
959

    
960
and get_eq_calls nodes eq =
961
  get_expr_calls nodes eq.eq_rhs
962
and get_node_calls nodes node =
963
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
964

    
965
let rec get_expr_vars vars e =
966
  get_expr_desc_vars vars e.expr_desc
967
and get_expr_desc_vars vars expr_desc =
968
  match expr_desc with
969
  | Expr_const _ -> vars
970
  | Expr_ident x -> Utils.ISet.add x vars
971
  | Expr_tuple el
972
  | Expr_array el -> List.fold_left get_expr_vars vars el
973
  | Expr_pre e1 -> get_expr_vars vars e1
974
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
975
  | Expr_access (e1, d) 
976
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
977
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
978
  | Expr_arrow (e1, e2) 
979
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
980
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
981
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
982
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
983

    
984

    
985
let rec expr_has_arrows e =
986
  expr_desc_has_arrows e.expr_desc
987
and expr_desc_has_arrows expr_desc =
988
  match expr_desc with
989
  | Expr_const _ 
990
  | Expr_ident _ -> false
991
  | Expr_tuple el
992
  | Expr_array el -> List.exists expr_has_arrows el
993
  | Expr_pre e1 
994
  | Expr_when (e1, _, _) 
995
  | Expr_access (e1, _) 
996
  | Expr_power (e1, _) -> expr_has_arrows e1
997
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
998
  | Expr_arrow (e1, e2) 
999
  | Expr_fby (e1, e2) -> true
1000
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1001
  | Expr_appl (i, e', i') -> expr_has_arrows e'
1002

    
1003
and eq_has_arrows eq =
1004
  expr_has_arrows eq.eq_rhs
1005
and node_has_arrows node =
1006
  List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
1007

    
1008

    
1009
let copy_var_decl vdecl =
1010
  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)
1011

    
1012
let copy_const cdecl =
1013
  { cdecl with const_type = Types.new_var () }
1014

    
1015
let copy_node nd =
1016
  { nd with
1017
    node_type     = Types.new_var ();
1018
    node_clock    = Clocks.new_var true;
1019
    node_inputs   = List.map copy_var_decl nd.node_inputs;
1020
    node_outputs  = List.map copy_var_decl nd.node_outputs;
1021
    node_locals   = List.map copy_var_decl nd.node_locals;
1022
    node_gencalls = [];
1023
    node_checks   = [];
1024
    node_stateless = None;
1025
  }
1026

    
1027
let copy_top top =
1028
  match top.top_decl_desc with
1029
  | Node nd -> { top with top_decl_desc = Node (copy_node nd)  }
1030
  | Const c -> { top with top_decl_desc = Const (copy_const c) }
1031
  | _       -> top
1032

    
1033
let copy_prog top_list =
1034
  List.map copy_top top_list
1035

    
1036
(* Local Variables: *)
1037
(* compile-command:"make -C .." *)
1038
(* End: *)