Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 70df2f87

History | View | Annotate | Download (31 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 (id, ty_dec, ck_dec, is_const) =
45
  { var_id = id;
46
    var_dec_type = ty_dec;
47
    var_dec_clock = ck_dec;
48
    var_dec_const = is_const;
49
    var_type = Types.new_var ();
50
    var_clock = Clocks.new_var true;
51
    var_loc = loc }
52

    
53
let mkexpr loc d =
54
  { expr_tag = Utils.new_tag ();
55
    expr_desc = d;
56
    expr_type = Types.new_var ();
57
    expr_clock = Clocks.new_var true;
58
    expr_delay = Delay.new_var ();
59
    expr_annot = None;
60
    expr_loc = loc }
61

    
62
let var_decl_of_const c =
63
  { var_id = c.const_id;
64
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
65
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
66
    var_dec_const = true;
67
    var_type = c.const_type;
68
    var_clock = Clocks.new_var false;
69
    var_loc = c.const_loc }
70

    
71
let mk_new_name vdecl_list id =
72
  let rec new_name name cpt =
73
    if List.exists (fun v -> v.var_id = name) vdecl_list
74
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
75
    else name
76
  in new_name id 1
77

    
78
let mkeq loc (lhs, rhs) =
79
  { eq_lhs = lhs;
80
    eq_rhs = rhs;
81
    eq_loc = loc }
82

    
83
let mkassert loc expr =
84
  { assert_loc = loc;
85
    assert_expr = expr
86
  }
87

    
88
let mktop_decl loc own itf d =
89
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
90

    
91
let mkpredef_call loc funname args =
92
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
93

    
94

    
95
let const_of_top top_decl =
96
  match top_decl.top_decl_desc with
97
  | Const c -> c
98
  | _ -> assert false
99

    
100
let node_of_top top_decl =
101
  match top_decl.top_decl_desc with
102
  | Node nd -> nd
103
  | _ -> assert false
104

    
105
let imported_node_of_top top_decl =
106
  match top_decl.top_decl_desc with
107
  | ImportedNode ind -> ind
108
  | _ -> assert false
109

    
110
let typedef_of_top top_decl =
111
  match top_decl.top_decl_desc with
112
  | TypeDef tdef -> tdef
113
  | _ -> assert false
114

    
115
let dependency_of_top top_decl =
116
  match top_decl.top_decl_desc with
117
  | Open (local, dep) -> (local, dep)
118
  | _ -> assert false
119

    
120
let consts_of_enum_type top_decl =
121
  match top_decl.top_decl_desc with
122
  | TypeDef tdef ->
123
    (match tdef.tydef_desc with
124
     | 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
125
     | _               -> [])
126
  | _ -> assert false
127

    
128
(************************************************************)
129
(*   Eexpr functions *)
130
(************************************************************)
131

    
132
let merge_node_annot ann1 ann2 =
133
  { requires = ann1.requires @ ann2.requires;
134
    ensures = ann1.ensures @ ann2.ensures;
135
    behaviors = ann1.behaviors @ ann2.behaviors;
136
    spec_loc = ann1.spec_loc
137
  }
138

    
139
let mkeexpr loc expr =
140
  { eexpr_tag = Utils.new_tag ();
141
    eexpr_qfexpr = expr;
142
    eexpr_quantifiers = [];
143
    eexpr_type = Types.new_var ();
144
    eexpr_clock = Clocks.new_var true;
145
    eexpr_normalized = None;
146
    eexpr_loc = loc }
147

    
148
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
149

    
150
(*
151
let mkepredef_call loc funname args =
152
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
153

    
154
let mkepredef_unary_call loc funname arg =
155
  mkeexpr loc (EExpr_appl (funname, arg, None))
156
*)
157

    
158
let merge_expr_annot ann1 ann2 =
159
  match ann1, ann2 with
160
    | None, None -> assert false
161
    | Some _, None -> ann1
162
    | None, Some _ -> ann2
163
    | Some ann1, Some ann2 -> Some {
164
      annots = ann1.annots @ ann2.annots;
165
      annot_loc = ann1.annot_loc
166
    }
167

    
168
let update_expr_annot e annot =
169
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
170

    
171

    
172
(***********************************************************)
173
(* Fast access to nodes, by name *)
174
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
175
let consts_table = Hashtbl.create 30
176

    
177
let print_node_table fmt () =
178
  begin
179
    Format.fprintf fmt "{ /* node table */@.";
180
    Hashtbl.iter (fun id nd ->
181
      Format.fprintf fmt "%s |-> %a"
182
	id
183
	Printers.pp_short_decl nd
184
    ) node_table;
185
    Format.fprintf fmt "}@."
186
  end
187

    
188
let print_consts_table fmt () =
189
  begin
190
    Format.fprintf fmt "{ /* consts table */@.";
191
    Hashtbl.iter (fun id const ->
192
      Format.fprintf fmt "%s |-> %a"
193
	id
194
	Printers.pp_const_decl (const_of_top const)
195
    ) consts_table;
196
    Format.fprintf fmt "}@."
197
  end
198

    
199
let node_name td =
200
    match td.top_decl_desc with 
201
    | Node nd         -> nd.node_id
202
    | ImportedNode nd -> nd.nodei_id
203
    | _ -> assert false
204

    
205
let is_generic_node td =
206
  match td.top_decl_desc with 
207
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
208
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
209
  | _ -> assert false
210

    
211
let node_inputs td =
212
  match td.top_decl_desc with 
213
  | Node nd         -> nd.node_inputs
214
  | ImportedNode nd -> nd.nodei_inputs
215
  | _ -> assert false
216

    
217
let node_from_name id =
218
  try
219
    Hashtbl.find node_table id
220
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
221
		     assert false)
222

    
223
let is_imported_node td =
224
  match td.top_decl_desc with 
225
  | Node nd         -> false
226
  | ImportedNode nd -> true
227
  | _ -> assert false
228

    
229

    
230
(* alias and type definition table *)
231

    
232
let top_int_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
233
let top_bool_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
234
let top_float_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float})
235
let top_real_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
236

    
237
let type_table =
238
  Utils.create_hashtable 20 [
239
    Tydec_int  , top_int_type;
240
    Tydec_bool , top_bool_type;
241
    Tydec_float, top_float_type;
242
    Tydec_real , top_real_type
243
  ]
244

    
245
let print_type_table fmt () =
246
  begin
247
    Format.fprintf fmt "{ /* type table */@.";
248
    Hashtbl.iter (fun tydec tdef ->
249
      Format.fprintf fmt "%a |-> %a"
250
	Printers.pp_var_type_dec_desc tydec
251
	Printers.pp_typedef (typedef_of_top tdef)
252
    ) type_table;
253
    Format.fprintf fmt "}@."
254
  end
255

    
256
let rec is_user_type typ =
257
  match typ with
258
  | Tydec_int | Tydec_bool | Tydec_real 
259
  | Tydec_float | Tydec_any | Tydec_const _ -> false
260
  | Tydec_clock typ' -> is_user_type typ'
261
  | _ -> true
262

    
263
let get_repr_type typ =
264
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
265
  if is_user_type typ_def then typ else typ_def
266

    
267
let rec coretype_equal ty1 ty2 =
268
  let res =
269
  match ty1, ty2 with
270
  | Tydec_any           , _
271
  | _                   , Tydec_any             -> assert false
272
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
273
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
274
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
275
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
276
  | Tydec_int           , Tydec_int
277
  | Tydec_real          , Tydec_real
278
  | Tydec_float         , Tydec_float
279
  | Tydec_bool          , Tydec_bool            -> true
280
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
281
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
282
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
283
  | Tydec_struct fl1    , Tydec_struct fl2      ->
284
       List.length fl1 = List.length fl2
285
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
286
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
287
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
288
  | _                                  -> false
289
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
290

    
291
let tag_true = "true"
292
let tag_false = "false"
293

    
294
let const_is_bool c =
295
 match c with
296
 | Const_tag t -> t = tag_true || t = tag_false
297
 | _           -> false
298

    
299
(* Computes the negation of a boolean constant *)
300
let const_negation c =
301
  assert (const_is_bool c);
302
  match c with
303
  | Const_tag t when t = tag_true  -> Const_tag tag_false
304
  | _                              -> Const_tag tag_true
305

    
306
let const_or c1 c2 =
307
  assert (const_is_bool c1 && const_is_bool c2);
308
  match c1, c2 with
309
  | Const_tag t1, _            when t1 = tag_true -> c1
310
  | _           , Const_tag t2 when t2 = tag_true -> c2
311
  | _                                             -> Const_tag tag_false
312

    
313
let const_and c1 c2 =
314
  assert (const_is_bool c1 && const_is_bool c2);
315
  match c1, c2 with
316
  | Const_tag t1, _            when t1 = tag_false -> c1
317
  | _           , Const_tag t2 when t2 = tag_false -> c2
318
  | _                                              -> Const_tag tag_true
319

    
320
let const_xor c1 c2 =
321
  assert (const_is_bool c1 && const_is_bool c2);
322
   match c1, c2 with
323
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
324
  | _                                         -> Const_tag tag_false
325

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

    
333
(* To guarantee uniqueness of tags in enum types *)
334
let tag_table =
335
  Utils.create_hashtable 20 [
336
   tag_true, top_bool_type;
337
   tag_false, top_bool_type
338
  ]
339

    
340
(* To guarantee uniqueness of fields in struct types *)
341
let field_table =
342
  Utils.create_hashtable 20 [
343
  ]
344

    
345
let get_enum_type_tags cty =
346
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
347
 match cty with
348
 | Tydec_bool    -> [tag_true; tag_false]
349
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
350
                     | Tydec_enum tl -> tl
351
                     | _             -> assert false)
352
 | _            -> assert false
353

    
354
let get_struct_type_fields cty =
355
 match cty with
356
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
357
                     | Tydec_struct fl -> fl
358
                     | _               -> assert false)
359
 | _            -> assert false
360

    
361
let const_of_bool b =
362
 Const_tag (if b then tag_true else tag_false)
363

    
364
(* let get_const c = snd (Hashtbl.find consts_table c) *)
365

    
366
let ident_of_expr expr =
367
 match expr.expr_desc with
368
 | Expr_ident id -> id
369
 | _             -> assert false
370

    
371
(* Caution, returns an untyped and unclocked expression *)
372
let expr_of_ident id loc =
373
  {expr_tag = Utils.new_tag ();
374
   expr_desc = Expr_ident id;
375
   expr_type = Types.new_var ();
376
   expr_clock = Clocks.new_var true;
377
   expr_delay = Delay.new_var ();
378
   expr_loc = loc;
379
   expr_annot = None}
380

    
381
let is_tuple_expr expr =
382
 match expr.expr_desc with
383
  | Expr_tuple _ -> true
384
  | _            -> false
385

    
386
let expr_list_of_expr expr =
387
  match expr.expr_desc with
388
  | Expr_tuple elist -> elist
389
  | _                -> [expr]
390

    
391
let expr_of_expr_list loc elist =
392
 match elist with
393
 | [t]  -> { t with expr_loc = loc }
394
 | t::_ ->
395
    let tlist = List.map (fun e -> e.expr_type) elist in
396
    let clist = List.map (fun e -> e.expr_clock) elist in
397
    { t with expr_desc = Expr_tuple elist;
398
	     expr_type = Type_predef.type_tuple tlist;
399
	     expr_clock = Clock_predef.ck_tuple clist;
400
	     expr_tag = Utils.new_tag ();
401
	     expr_loc = loc }
402
 | _    -> assert false
403

    
404
let call_of_expr expr =
405
 match expr.expr_desc with
406
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
407
 | _                      -> assert false
408

    
409
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
410
let rec expr_of_dimension dim =
411
 match dim.dim_desc with
412
 | Dbool b        ->
413
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
414
 | Dint i         ->
415
     mkexpr dim.dim_loc (Expr_const (Const_int i))
416
 | Dident id      ->
417
     mkexpr dim.dim_loc (Expr_ident id)
418
 | Dite (c, t, e) ->
419
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
420
 | Dappl (id, args) ->
421
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
422
 | Dlink dim'       -> expr_of_dimension dim'
423
 | Dvar
424
 | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
425
			assert false)
426

    
427
let dimension_of_const loc const =
428
 match const with
429
 | Const_int i                                    -> mkdim_int loc i
430
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
431
 | _                                              -> raise InvalidDimension
432

    
433
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
434
   into dimension expressions *)
435
let rec dimension_of_expr expr =
436
  match expr.expr_desc with
437
  | Expr_const c  -> dimension_of_const expr.expr_loc c
438
  | Expr_ident id -> mkdim_ident expr.expr_loc id
439
  | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
440
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
441
      if k = None then raise InvalidDimension;
442
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
443
  | Expr_ite (i, t, e)        ->
444
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
445
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
446

    
447

    
448
let sort_handlers hl =
449
 List.sort (fun (t, _) (t', _) -> compare t t') hl
450

    
451
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
452
  | Expr_const c1, Expr_const c2 -> c1 = c2
453
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
454
  | Expr_array el1, Expr_array el2 
455
  | Expr_tuple el1, Expr_tuple el2 -> 
456
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
457
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
458
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
459
  | 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
460
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
461
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
462
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
463
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
464
  | 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')
465
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
466
  | Expr_power (e1, i1), Expr_power (e2, i2)
467
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
468
  | _ -> false
469

    
470
let get_node_vars nd =
471
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
472

    
473
let get_var id var_list =
474
 List.find (fun v -> v.var_id = id) var_list
475

    
476
let get_node_var id node = get_var id (get_node_vars node)
477

    
478
let get_node_eq id node =
479
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
480

    
481
let get_nodes prog = 
482
  List.fold_left (
483
    fun nodes decl ->
484
      match decl.top_decl_desc with
485
	| Node _ -> decl::nodes
486
	| Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes  
487
  ) [] prog
488

    
489
let get_imported_nodes prog = 
490
  List.fold_left (
491
    fun nodes decl ->
492
      match decl.top_decl_desc with
493
	| ImportedNode _ -> decl::nodes
494
	| Const _ | Node _ | Open _ | TypeDef _-> nodes  
495
  ) [] prog
496

    
497
let get_consts prog = 
498
  List.fold_right (
499
    fun decl consts ->
500
      match decl.top_decl_desc with
501
	| Const _ -> decl::consts
502
	| Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts  
503
  ) prog []
504

    
505
let get_typedefs prog = 
506
  List.fold_right (
507
    fun decl types ->
508
      match decl.top_decl_desc with
509
	| TypeDef _ -> decl::types
510
	| Node _ | ImportedNode _ | Open _ | Const _ -> types  
511
  ) prog []
512

    
513
let get_dependencies prog =
514
  List.fold_right (
515
    fun decl deps ->
516
      match decl.top_decl_desc with
517
	| Open _ -> decl::deps
518
	| Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps  
519
  ) prog []
520

    
521
let get_node_interface nd =
522
 {nodei_id = nd.node_id;
523
  nodei_type = nd.node_type;
524
  nodei_clock = nd.node_clock;
525
  nodei_inputs = nd.node_inputs;
526
  nodei_outputs = nd.node_outputs;
527
  nodei_stateless = nd.node_dec_stateless;
528
  nodei_spec = nd.node_spec;
529
  nodei_prototype = None;
530
  nodei_in_lib = None;
531
 }
532

    
533
(************************************************************************)
534
(*        Renaming                                                      *)
535

    
536
(* applies the renaming function [fvar] to all variables of expression [expr] *)
537
 let rec expr_replace_var fvar expr =
538
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
539

    
540
 and expr_desc_replace_var fvar expr_desc =
541
   match expr_desc with
542
   | Expr_const _ -> expr_desc
543
   | Expr_ident i -> Expr_ident (fvar i)
544
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
545
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
546
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
547
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
548
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
549
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
550
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
551
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
552
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
553
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
554
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
555

    
556
(* Applies the renaming function [fvar] to every rhs
557
   only when the corresponding lhs satisfies predicate [pvar] *)
558
 let eq_replace_rhs_var pvar fvar eq =
559
   let pvar l = List.exists pvar l in
560
   let rec replace lhs rhs =
561
     { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
562
   and replace_desc lhs rhs_desc =
563
     match lhs with
564
     | []  -> assert false
565
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
566
     | _   ->
567
       (match rhs_desc with
568
       | Expr_tuple tl ->
569
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
570
       | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
571
	 let args = expr_list_of_expr arg in
572
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
573
       | Expr_array _
574
       | Expr_access _
575
       | Expr_power _
576
       | Expr_const _
577
       | Expr_ident _
578
       | Expr_appl _   ->
579
	 if pvar lhs
580
	 then expr_desc_replace_var fvar rhs_desc
581
	 else rhs_desc
582
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
583
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
584
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
585
       | Expr_pre e'          -> Expr_pre (replace lhs e')
586
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
587
				 in Expr_when (replace lhs e', i', l)
588
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
589
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
590
       )
591
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
592

    
593

    
594
 let rec rename_expr  f_node f_var f_const expr =
595
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
596
 and rename_expr_desc f_node f_var f_const expr_desc =
597
   let re = rename_expr  f_node f_var f_const in
598
   match expr_desc with
599
   | Expr_const _ -> expr_desc
600
   | Expr_ident i -> Expr_ident (f_var i)
601
   | Expr_array el -> Expr_array (List.map re el)
602
   | Expr_access (e1, d) -> Expr_access (re e1, d)
603
   | Expr_power (e1, d) -> Expr_power (re e1, d)
604
   | Expr_tuple el -> Expr_tuple (List.map re el)
605
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
606
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
607
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
608
   | Expr_pre e' -> Expr_pre (re e')
609
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
610
   | Expr_merge (i, hl) -> 
611
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
612
   | Expr_appl (i, e', i') -> 
613
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
614
  
615
 let rename_node_annot f_node f_var f_const expr  =
616
   expr
617
 (* TODO assert false *)
618

    
619
 let rename_expr_annot f_node f_var f_const annot =
620
   annot
621
 (* TODO assert false *)
622

    
623
let rename_node f_node f_var f_const nd =
624
  let rename_var v = { v with var_id = f_var v.var_id } in
625
  let rename_eq eq = { eq with
626
      eq_lhs = List.map f_var eq.eq_lhs; 
627
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
628
    } 
629
  in
630
  let inputs = List.map rename_var nd.node_inputs in
631
  let outputs = List.map rename_var nd.node_outputs in
632
  let locals = List.map rename_var nd.node_locals in
633
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
634
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
635
  let node_asserts = List.map 
636
    (fun a -> 
637
      {a with assert_expr = 
638
	  let expr = a.assert_expr in
639
	  rename_expr f_node f_var f_const expr})
640
    nd.node_asserts
641
  in
642
  let eqs = List.map rename_eq nd.node_eqs in
643
  let spec = 
644
    Utils.option_map 
645
      (fun s -> rename_node_annot f_node f_var f_const s) 
646
      nd.node_spec 
647
  in
648
  let annot =
649
    List.map 
650
      (fun s -> rename_expr_annot f_node f_var f_const s) 
651
      nd.node_annot
652
  in
653
  {
654
    node_id = f_node nd.node_id;
655
    node_type = nd.node_type;
656
    node_clock = nd.node_clock;
657
    node_inputs = inputs;
658
    node_outputs = outputs;
659
    node_locals = locals;
660
    node_gencalls = gen_calls;
661
    node_checks = node_checks;
662
    node_asserts = node_asserts;
663
    node_eqs = eqs;
664
    node_dec_stateless = nd.node_dec_stateless;
665
    node_stateless = nd.node_stateless;
666
    node_spec = spec;
667
    node_annot = annot;
668
  }
669

    
670

    
671
let rename_const f_const c =
672
  { c with const_id = f_const c.const_id }
673

    
674
let rename_typedef f_var t =
675
  match t.tydef_desc with
676
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
677
  | _               -> t
678

    
679
let rename_prog f_node f_var f_const prog =
680
  List.rev (
681
    List.fold_left (fun accu top ->
682
      (match top.top_decl_desc with
683
      | Node nd -> 
684
	 { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
685
      | Const c -> 
686
	 { top with top_decl_desc = Const (rename_const f_const c) }
687
      | TypeDef tdef ->
688
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
689
      | ImportedNode _
690
      | Open _       -> top)
691
      ::accu
692
) [] prog
693
		   )
694

    
695
(**********************************************************************)
696
(* Pretty printers *)
697

    
698
let pp_decl_type fmt tdecl =
699
  match tdecl.top_decl_desc with
700
  | Node nd ->
701
    fprintf fmt "%s: " nd.node_id;
702
    Utils.reset_names ();
703
    fprintf fmt "%a@ " Types.print_ty nd.node_type
704
  | ImportedNode ind ->
705
    fprintf fmt "%s: " ind.nodei_id;
706
    Utils.reset_names ();
707
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
708
  | Const _ | Open _ | TypeDef _ -> ()
709

    
710
let pp_prog_type fmt tdecl_list =
711
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
712

    
713
let pp_decl_clock fmt cdecl =
714
  match cdecl.top_decl_desc with
715
  | Node nd ->
716
    fprintf fmt "%s: " nd.node_id;
717
    Utils.reset_names ();
718
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
719
  | ImportedNode ind ->
720
    fprintf fmt "%s: " ind.nodei_id;
721
    Utils.reset_names ();
722
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
723
  | Const _ | Open _ | TypeDef _ -> ()
724

    
725
let pp_prog_clock fmt prog =
726
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
727

    
728
let pp_error fmt = function
729
    Main_not_found ->
730
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
731
	!Options.main_node
732
  | Main_wrong_kind ->
733
    fprintf fmt
734
      "Name %s does not correspond to a (non-imported) node definition.@." 
735
      !Options.main_node
736
  | No_main_specified ->
737
    fprintf fmt "No main node specified@."
738
  | Unbound_symbol sym ->
739
    fprintf fmt
740
      "%s is undefined.@."
741
      sym
742
  | Already_bound_symbol sym -> 
743
    fprintf fmt
744
      "%s is already defined.@."
745
      sym
746
  | Unknown_library sym ->
747
    fprintf fmt
748
      "impossible to load library %s.@."
749
      sym
750

    
751
(* filling node table with internal functions *)
752
let vdecls_of_typ_ck cpt ty =
753
  let loc = Location.dummy_loc in
754
  List.map
755
    (fun _ -> incr cpt;
756
              let name = sprintf "_var_%d" !cpt in
757
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
758
    (Types.type_list_of_type ty)
759

    
760
let mk_internal_node id =
761
  let spec = None in
762
  let ty = Env.lookup_value Basic_library.type_env id in
763
  let ck = Env.lookup_value Basic_library.clock_env id in
764
  let (tin, tout) = Types.split_arrow ty in
765
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
766
  let cpt = ref (-1) in
767
  mktop_decl Location.dummy_loc Version.prefix false
768
    (ImportedNode
769
       {nodei_id = id;
770
	nodei_type = ty;
771
	nodei_clock = ck;
772
	nodei_inputs = vdecls_of_typ_ck cpt tin;
773
	nodei_outputs = vdecls_of_typ_ck cpt tout;
774
	nodei_stateless = Types.get_static_value ty <> None;
775
	nodei_spec = spec;
776
	nodei_prototype = None;
777
       	nodei_in_lib = None;
778
       })
779

    
780
let add_internal_funs () =
781
  List.iter
782
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
783
    Basic_library.internal_funs
784

    
785

    
786

    
787
(* Replace any occurence of a var in vars_to_replace by its associated
788
   expression in defs until e does not contain any such variables *)
789
let rec substitute_expr vars_to_replace defs e =
790
  let se = substitute_expr vars_to_replace defs in
791
  { e with expr_desc = 
792
      let ed = e.expr_desc in
793
      match ed with
794
      | Expr_const _ -> ed
795
      | Expr_array el -> Expr_array (List.map se el)
796
      | Expr_access (e1, d) -> Expr_access (se e1, d)
797
      | Expr_power (e1, d) -> Expr_power (se e1, d)
798
      | Expr_tuple el -> Expr_tuple (List.map se el)
799
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
800
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
801
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
802
      | Expr_pre e' -> Expr_pre (se e')
803
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
804
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
805
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
806
      | Expr_ident i -> 
807
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
808
	  let eq_i eq = eq.eq_lhs = [i] in
809
	  if List.exists eq_i defs then
810
	    let sub = List.find eq_i defs in
811
	    let sub' = se sub.eq_rhs in
812
	    sub'.expr_desc
813
	  else 
814
	    assert false
815
	)
816
	else
817
	  ed
818

    
819
  }
820
(* FAUT IL RETIRER ?
821
  
822
 let rec expr_to_eexpr  expr =
823
   { eexpr_tag = expr.expr_tag;
824
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
825
     eexpr_type = expr.expr_type;
826
     eexpr_clock = expr.expr_clock;
827
     eexpr_loc = expr.expr_loc
828
   }
829
 and expr_desc_to_eexpr_desc expr_desc =
830
   let conv = expr_to_eexpr in
831
   match expr_desc with
832
   | Expr_const c -> EExpr_const (match c with
833
     | Const_int x -> EConst_int x 
834
     | Const_real x -> EConst_real x 
835
     | Const_float x -> EConst_float x 
836
     | Const_tag x -> EConst_tag x 
837
     | _ -> assert false
838

    
839
   )
840
   | Expr_ident i -> EExpr_ident i
841
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
842

    
843
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
844
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
845
   | Expr_pre e' -> EExpr_pre (conv e')
846
   | Expr_appl (i, e', i') -> 
847
     EExpr_appl 
848
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
849

    
850
   | Expr_when _
851
   | Expr_merge _ -> assert false
852
   | Expr_array _ 
853
   | Expr_access _ 
854
   | Expr_power _  -> assert false
855
   | Expr_ite (c, t, e) -> assert false 
856
   | _ -> assert false
857

    
858
     *)
859
let rec get_expr_calls nodes e =
860
  get_calls_expr_desc nodes e.expr_desc
861
and get_calls_expr_desc nodes expr_desc =
862
  let get_calls = get_expr_calls nodes in
863
  match expr_desc with
864
  | Expr_const _ 
865
   | Expr_ident _ -> Utils.ISet.empty
866
   | Expr_tuple el
867
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
868
   | Expr_pre e1 
869
   | Expr_when (e1, _, _) 
870
   | Expr_access (e1, _) 
871
   | Expr_power (e1, _) -> get_calls e1
872
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
873
   | Expr_arrow (e1, e2) 
874
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
875
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
876
   | Expr_appl (i, e', i') -> 
877
     if Basic_library.is_internal_fun i then 
878
       (get_calls e') 
879
     else
880
       let calls =  Utils.ISet.add i (get_calls e') in
881
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
882
       if List.exists test nodes then
883
	 match (List.find test nodes).top_decl_desc with
884
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
885
	 | _ -> assert false
886
       else 
887
	 calls
888

    
889
and get_eq_calls nodes eq =
890
  get_expr_calls nodes eq.eq_rhs
891
and get_node_calls nodes node =
892
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
893

    
894

    
895
let rec expr_has_arrows e =
896
  expr_desc_has_arrows e.expr_desc
897
and expr_desc_has_arrows expr_desc =
898
  match expr_desc with
899
  | Expr_const _ 
900
  | Expr_ident _ -> false
901
  | Expr_tuple el
902
  | Expr_array el -> List.exists expr_has_arrows el
903
  | Expr_pre e1 
904
  | Expr_when (e1, _, _) 
905
  | Expr_access (e1, _) 
906
  | Expr_power (e1, _) -> expr_has_arrows e1
907
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
908
  | Expr_arrow (e1, e2) 
909
  | Expr_fby (e1, e2) -> true
910
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
911
  | Expr_appl (i, e', i') -> expr_has_arrows e'
912

    
913
and eq_has_arrows eq =
914
  expr_has_arrows eq.eq_rhs
915
and node_has_arrows node =
916
  List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
917

    
918
(* Local Variables: *)
919
(* compile-command:"make -C .." *)
920
(* End: *)