Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ ed81df06

History | View | Annotate | Download (27.5 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

    
32

    
33
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
34

    
35

    
36

    
37
(************************************************************)
38
(* *)
39

    
40
let mktyp loc d =
41
  { ty_dec_desc = d; ty_dec_loc = loc }
42

    
43
let mkclock loc d =
44
  { ck_dec_desc = d; ck_dec_loc = loc }
45

    
46
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) =
47
  { var_id = id;
48
    var_dec_type = ty_dec;
49
    var_dec_clock = ck_dec;
50
    var_dec_const = is_const;
51
    var_type = Types.new_var ();
52
    var_clock = Clocks.new_var true;
53
    var_loc = loc }
54

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

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

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

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

    
85
let mkassert loc expr =
86
  { assert_loc = loc;
87
    assert_expr = expr
88
  }
89

    
90
let mktop_decl loc d =
91
  { top_decl_desc = d; top_decl_loc = loc }
92

    
93
let mkpredef_call loc funname args =
94
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
95

    
96
(************************************************************)
97
(*   Eexpr functions *)
98
(************************************************************)
99

    
100
let merge_node_annot ann1 ann2 =
101
  { requires = ann1.requires @ ann2.requires;
102
    ensures = ann1.ensures @ ann2.ensures;
103
    behaviors = ann1.behaviors @ ann2.behaviors;
104
    spec_loc = ann1.spec_loc
105
  }
106

    
107
let mkeexpr loc expr =
108
  { eexpr_tag = Utils.new_tag ();
109
    eexpr_qfexpr = expr;
110
    eexpr_quantifiers = [];
111
    eexpr_type = Types.new_var ();
112
    eexpr_clock = Clocks.new_var true;
113
    eexpr_normalized = None;
114
    eexpr_loc = loc }
115

    
116
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
117

    
118
(*
119
let mkepredef_call loc funname args =
120
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
121

    
122
let mkepredef_unary_call loc funname arg =
123
  mkeexpr loc (EExpr_appl (funname, arg, None))
124
*)
125

    
126
let merge_expr_annot ann1 ann2 =
127
  match ann1, ann2 with
128
    | None, None -> assert false
129
    | Some _, None -> ann1
130
    | None, Some _ -> ann2
131
    | Some ann1, Some ann2 -> Some {
132
      annots = ann1.annots @ ann2.annots;
133
      annot_loc = ann1.annot_loc
134
    }
135

    
136
let update_expr_annot e annot =
137
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
138

    
139

    
140
(***********************************************************)
141
(* Fast access to nodes, by name *)
142
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
143
let consts_table = Hashtbl.create 30
144

    
145
let node_name td =
146
    match td.top_decl_desc with 
147
    | Node nd         -> nd.node_id
148
    | ImportedNode nd -> nd.nodei_id
149
    | _ -> assert false
150

    
151
let is_generic_node td =
152
  match td.top_decl_desc with 
153
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
154
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
155
  | _ -> assert false
156

    
157
let node_inputs td =
158
  match td.top_decl_desc with 
159
  | Node nd         -> nd.node_inputs
160
  | ImportedNode nd -> nd.nodei_inputs
161
  | _ -> assert false
162

    
163
let node_from_name id =
164
  try
165
    Hashtbl.find node_table id
166
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
167
		     assert false)
168

    
169
let is_imported_node td =
170
  match td.top_decl_desc with 
171
  | Node nd         -> false
172
  | ImportedNode nd -> true
173
  | _ -> assert false
174

    
175

    
176
(* alias and type definition table *)
177
let type_table =
178
  Utils.create_hashtable 20 [
179
    Tydec_int  , Tydec_int;
180
    Tydec_bool , Tydec_bool;
181
    Tydec_float, Tydec_float;
182
    Tydec_real , Tydec_real
183
  ]
184

    
185
let rec is_user_type typ =
186
  match typ with
187
  | Tydec_int | Tydec_bool | Tydec_real 
188
  | Tydec_float | Tydec_any | Tydec_const _ -> false
189
  | Tydec_clock typ' -> is_user_type typ'
190
  | _ -> true
191

    
192
let get_repr_type typ =
193
  let typ_def = Hashtbl.find type_table typ in
194
  if is_user_type typ_def then typ else typ_def
195

    
196
let rec coretype_equal ty1 ty2 =
197
  (*let res =*) 
198
  match ty1, ty2 with
199
  | Tydec_any           , _
200
  | _                   , Tydec_any             -> assert false
201
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
202
  | Tydec_const _       , _                     -> let ty1' = Hashtbl.find type_table ty1
203
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
204
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
205
  | Tydec_int           , Tydec_int
206
  | Tydec_real          , Tydec_real
207
  | Tydec_float         , Tydec_float
208
  | Tydec_bool          , Tydec_bool            -> true
209
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
210
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
211
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
212
  | Tydec_struct fl1    , Tydec_struct fl2      ->
213
       List.length fl1 = List.length fl2
214
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
215
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
216
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
217
  | _                                  -> false
218
  (*in (Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res; res)*)
219

    
220
let tag_true = "true"
221
let tag_false = "false"
222

    
223
let const_is_bool c =
224
 match c with
225
 | Const_tag t -> t = tag_true || t = tag_false
226
 | _           -> false
227

    
228
(* Computes the negation of a boolean constant *)
229
let const_negation c =
230
  assert (const_is_bool c);
231
  match c with
232
  | Const_tag t when t = tag_true  -> Const_tag tag_false
233
  | _                              -> Const_tag tag_true
234

    
235
let const_or c1 c2 =
236
  assert (const_is_bool c1 && const_is_bool c2);
237
  match c1, c2 with
238
  | Const_tag t1, _            when t1 = tag_true -> c1
239
  | _           , Const_tag t2 when t2 = tag_true -> c2
240
  | _                                             -> Const_tag tag_false
241

    
242
let const_and c1 c2 =
243
  assert (const_is_bool c1 && const_is_bool c2);
244
  match c1, c2 with
245
  | Const_tag t1, _            when t1 = tag_false -> c1
246
  | _           , Const_tag t2 when t2 = tag_false -> c2
247
  | _                                              -> Const_tag tag_true
248

    
249
let const_xor c1 c2 =
250
  assert (const_is_bool c1 && const_is_bool c2);
251
   match c1, c2 with
252
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
253
  | _                                         -> Const_tag tag_false
254

    
255
let const_impl c1 c2 =
256
  assert (const_is_bool c1 && const_is_bool c2);
257
  match c1, c2 with
258
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
259
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
260
  | _                                             -> Const_tag tag_false
261

    
262
(* To guarantee uniqueness of tags in enum types *)
263
let tag_table =
264
  Utils.create_hashtable 20 [
265
   tag_true, Tydec_bool;
266
   tag_false, Tydec_bool
267
  ]
268

    
269
(* To guarantee uniqueness of fields in struct types *)
270
let field_table =
271
  Utils.create_hashtable 20 [
272
  ]
273

    
274
let get_enum_type_tags cty =
275
 match cty with
276
 | Tydec_bool    -> [tag_true; tag_false]
277
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
278
                     | Tydec_enum tl -> tl
279
                     | _             -> assert false)
280
 | _            -> assert false
281

    
282
let get_struct_type_fields cty =
283
 match cty with
284
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
285
                     | Tydec_struct fl -> fl
286
                     | _               -> assert false)
287
 | _            -> assert false
288

    
289
let const_of_bool b =
290
 Const_tag (if b then tag_true else tag_false)
291

    
292
(* let get_const c = snd (Hashtbl.find consts_table c) *)
293

    
294
let ident_of_expr expr =
295
 match expr.expr_desc with
296
 | Expr_ident id -> id
297
 | _             -> assert false
298

    
299
(* Caution, returns an untyped and unclocked expression *)
300
let expr_of_ident id loc =
301
  {expr_tag = Utils.new_tag ();
302
   expr_desc = Expr_ident id;
303
   expr_type = Types.new_var ();
304
   expr_clock = Clocks.new_var true;
305
   expr_delay = Delay.new_var ();
306
   expr_loc = loc;
307
   expr_annot = None}
308

    
309
let is_tuple_expr expr =
310
 match expr.expr_desc with
311
  | Expr_tuple _ -> true
312
  | _            -> false
313

    
314
let expr_list_of_expr expr =
315
  match expr.expr_desc with
316
  | Expr_tuple elist -> elist
317
  | _                -> [expr]
318

    
319
let expr_of_expr_list loc elist =
320
 match elist with
321
 | [t]  -> { t with expr_loc = loc }
322
 | t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc }
323
 | _    -> assert false
324

    
325
let call_of_expr expr =
326
 match expr.expr_desc with
327
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
328
 | _                      -> assert false
329

    
330
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
331
let rec expr_of_dimension dim =
332
 match dim.dim_desc with
333
 | Dbool b        ->
334
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
335
 | Dint i         ->
336
     mkexpr dim.dim_loc (Expr_const (Const_int i))
337
 | Dident id      ->
338
     mkexpr dim.dim_loc (Expr_ident id)
339
 | Dite (c, t, e) ->
340
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
341
 | Dappl (id, args) ->
342
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
343
 | Dlink dim'       -> expr_of_dimension dim'
344
 | Dvar
345
 | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
346
			assert false)
347

    
348
let dimension_of_const loc const =
349
 match const with
350
 | Const_int i                                    -> mkdim_int loc i
351
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
352
 | _                                              -> raise InvalidDimension
353

    
354
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
355
   into dimension expressions *)
356
let rec dimension_of_expr expr =
357
  match expr.expr_desc with
358
  | Expr_const c  -> dimension_of_const expr.expr_loc c
359
  | Expr_ident id -> mkdim_ident expr.expr_loc id
360
  | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
361
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
362
      if k = None then raise InvalidDimension;
363
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
364
  | Expr_ite (i, t, e)        ->
365
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
366
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
367

    
368

    
369
let sort_handlers hl =
370
 List.sort (fun (t, _) (t', _) -> compare t t') hl
371

    
372
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
373
  | Expr_const c1, Expr_const c2 -> c1 = c2
374
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
375
  | Expr_array el1, Expr_array el2 
376
  | Expr_tuple el1, Expr_tuple el2 -> 
377
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
378
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
379
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
380
  | 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
381
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
382
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
383
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
384
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
385
  | 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')
386
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
387
  | Expr_power (e1, i1), Expr_power (e2, i2)
388
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
389
  | _ -> false
390

    
391
let get_node_vars nd =
392
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
393

    
394
let get_var id var_list =
395
 List.find (fun v -> v.var_id = id) var_list
396

    
397
let get_node_var id node = get_var id (get_node_vars node)
398

    
399
let get_node_eq id node =
400
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
401

    
402
let get_nodes prog = 
403
  List.fold_left (
404
    fun nodes decl ->
405
      match decl.top_decl_desc with
406
	| Node nd -> nd::nodes
407
	| Consts _ | ImportedNode _ | Open _ | Type _ -> nodes  
408
  ) [] prog
409

    
410
let get_consts prog = 
411
  List.fold_left (
412
    fun consts decl ->
413
      match decl.top_decl_desc with
414
	| Consts clist -> clist@consts
415
	| Node _ | ImportedNode _ | Open _ | Type _ -> consts  
416
  ) [] prog
417

    
418
let get_types prog = 
419
  List.fold_left (
420
    fun types decl ->
421
      match decl.top_decl_desc with
422
	| Type typ -> typ::types
423
	| Node _ | ImportedNode _ | Open _ | Consts _ -> types  
424
  ) [] prog
425

    
426
let get_node_interface nd =
427
 {nodei_id = nd.node_id;
428
  nodei_type = nd.node_type;
429
  nodei_clock = nd.node_clock;
430
  nodei_inputs = nd.node_inputs;
431
  nodei_outputs = nd.node_outputs;
432
  nodei_stateless = nd.node_dec_stateless;
433
  nodei_spec = nd.node_spec;
434
  nodei_prototype = None;
435
  nodei_in_lib = None;
436
 }
437

    
438
(************************************************************************)
439
(*        Renaming                                                      *)
440

    
441
(* applies the renaming function [fvar] to all variables of expression [expr] *)
442
 let rec expr_replace_var fvar expr =
443
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
444

    
445
 and expr_desc_replace_var fvar expr_desc =
446
   match expr_desc with
447
   | Expr_const _ -> expr_desc
448
   | Expr_ident i -> Expr_ident (fvar i)
449
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
450
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
451
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
452
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
453
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
454
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
455
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
456
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
457
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
458
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
459
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
460

    
461
(* Applies the renaming function [fvar] to every rhs
462
   only when the corresponding lhs satisfies predicate [pvar] *)
463
 let eq_replace_rhs_var pvar fvar eq =
464
   let pvar l = List.exists pvar l in
465
   let rec replace lhs rhs =
466
     { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
467
   and replace_desc lhs rhs_desc =
468
     match lhs with
469
     | []  -> assert false
470
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
471
     | _   ->
472
       (match rhs_desc with
473
       | Expr_tuple tl ->
474
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
475
       | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
476
	 let args = expr_list_of_expr arg in
477
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
478
       | Expr_array _
479
       | Expr_access _
480
       | Expr_power _
481
       | Expr_const _
482
       | Expr_ident _
483
       | Expr_appl _   ->
484
	 if pvar lhs
485
	 then expr_desc_replace_var fvar rhs_desc
486
	 else rhs_desc
487
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
488
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
489
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
490
       | Expr_pre e'          -> Expr_pre (replace lhs e')
491
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
492
				 in Expr_when (replace lhs e', i', l)
493
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
494
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
495
       )
496
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
497

    
498

    
499
 let rec rename_expr  f_node f_var f_const expr =
500
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
501
 and rename_expr_desc f_node f_var f_const expr_desc =
502
   let re = rename_expr  f_node f_var f_const in
503
   match expr_desc with
504
   | Expr_const _ -> expr_desc
505
   | Expr_ident i -> Expr_ident (f_var i)
506
   | Expr_array el -> Expr_array (List.map re el)
507
   | Expr_access (e1, d) -> Expr_access (re e1, d)
508
   | Expr_power (e1, d) -> Expr_power (re e1, d)
509
   | Expr_tuple el -> Expr_tuple (List.map re el)
510
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
511
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
512
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
513
   | Expr_pre e' -> Expr_pre (re e')
514
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
515
   | Expr_merge (i, hl) -> 
516
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
517
   | Expr_appl (i, e', i') -> 
518
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
519
  
520
 let rename_node_annot f_node f_var f_const expr  =
521
   expr
522
 (* TODO assert false *)
523

    
524
 let rename_expr_annot f_node f_var f_const annot =
525
   annot
526
 (* TODO assert false *)
527

    
528
let rename_node f_node f_var f_const nd =
529
  let rename_var v = { v with var_id = f_var v.var_id } in
530
  let rename_eq eq = { eq with
531
      eq_lhs = List.map f_var eq.eq_lhs; 
532
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
533
    } 
534
  in
535
  let inputs = List.map rename_var nd.node_inputs in
536
  let outputs = List.map rename_var nd.node_outputs in
537
  let locals = List.map rename_var nd.node_locals in
538
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
539
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
540
  let node_asserts = List.map 
541
    (fun a -> 
542
      {a with assert_expr = 
543
	  let expr = a.assert_expr in
544
	  rename_expr f_node f_var f_const expr})
545
    nd.node_asserts
546
  in
547
  let eqs = List.map rename_eq nd.node_eqs in
548
  let spec = 
549
    Utils.option_map 
550
      (fun s -> rename_node_annot f_node f_var f_const s) 
551
      nd.node_spec 
552
  in
553
  let annot =
554
    List.map 
555
      (fun s -> rename_expr_annot f_node f_var f_const s) 
556
      nd.node_annot
557
  in
558
  {
559
    node_id = f_node nd.node_id;
560
    node_type = nd.node_type;
561
    node_clock = nd.node_clock;
562
    node_inputs = inputs;
563
    node_outputs = outputs;
564
    node_locals = locals;
565
    node_gencalls = gen_calls;
566
    node_checks = node_checks;
567
    node_asserts = node_asserts;
568
    node_eqs = eqs;
569
    node_dec_stateless = nd.node_dec_stateless;
570
    node_stateless = nd.node_stateless;
571
    node_spec = spec;
572
    node_annot = annot;
573
  }
574

    
575

    
576
let rename_const f_const c =
577
  { c with const_id = f_const c.const_id }
578
    
579
let rename_prog f_node f_var f_const prog =
580
  List.rev (
581
    List.fold_left (fun accu top ->
582
      (match top.top_decl_desc with
583
      | Node nd -> 
584
	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
585
      | Consts c -> 
586
	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
587
      | ImportedNode _
588
      | Open _
589
      | Type _ -> top)
590
      ::accu
591
) [] prog
592
  )
593

    
594
(**********************************************************************)
595
(* Pretty printers *)
596

    
597
let pp_decl_type fmt tdecl =
598
  match tdecl.top_decl_desc with
599
  | Node nd ->
600
    fprintf fmt "%s: " nd.node_id;
601
    Utils.reset_names ();
602
    fprintf fmt "%a@ " Types.print_ty nd.node_type
603
  | ImportedNode ind ->
604
    fprintf fmt "%s: " ind.nodei_id;
605
    Utils.reset_names ();
606
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
607
  | Consts _ | Open _ | Type _ -> ()
608

    
609
let pp_prog_type fmt tdecl_list =
610
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
611

    
612
let pp_decl_clock fmt cdecl =
613
  match cdecl.top_decl_desc with
614
  | Node nd ->
615
    fprintf fmt "%s: " nd.node_id;
616
    Utils.reset_names ();
617
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
618
  | ImportedNode ind ->
619
    fprintf fmt "%s: " ind.nodei_id;
620
    Utils.reset_names ();
621
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
622
  | Consts _ | Open _ | Type _ -> ()
623

    
624
let pp_prog_clock fmt prog =
625
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
626

    
627
let pp_error fmt = function
628
    Main_not_found ->
629
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
630
	!Options.main_node
631
  | Main_wrong_kind ->
632
    fprintf fmt
633
      "Name %s does not correspond to a (non-imported) node definition.@." 
634
      !Options.main_node
635
  | No_main_specified ->
636
    fprintf fmt "No main node specified@."
637
  | Unbound_symbol sym ->
638
    fprintf fmt
639
      "%s is undefined.@."
640
      sym
641
  | Already_bound_symbol sym -> 
642
    fprintf fmt
643
      "%s is already defined.@."
644
      sym
645

    
646
(* filling node table with internal functions *)
647
let vdecls_of_typ_ck cpt ty =
648
  let loc = Location.dummy_loc in
649
  List.map
650
    (fun _ -> incr cpt;
651
              let name = sprintf "_var_%d" !cpt in
652
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
653
    (Types.type_list_of_type ty)
654

    
655
let mk_internal_node id =
656
  let spec = None in
657
  let ty = Env.lookup_value Basic_library.type_env id in
658
  let ck = Env.lookup_value Basic_library.clock_env id in
659
  let (tin, tout) = Types.split_arrow ty in
660
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
661
  let cpt = ref (-1) in
662
  mktop_decl Location.dummy_loc
663
    (ImportedNode
664
       {nodei_id = id;
665
	nodei_type = ty;
666
	nodei_clock = ck;
667
	nodei_inputs = vdecls_of_typ_ck cpt tin;
668
	nodei_outputs = vdecls_of_typ_ck cpt tout;
669
	nodei_stateless = Types.get_static_value ty <> None;
670
	nodei_spec = spec;
671
	nodei_prototype = None;
672
       	nodei_in_lib = None;
673
       })
674

    
675
let add_internal_funs () =
676
  List.iter
677
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
678
    Basic_library.internal_funs
679

    
680

    
681

    
682
(* Replace any occurence of a var in vars_to_replace by its associated
683
   expression in defs until e does not contain any such variables *)
684
let rec substitute_expr vars_to_replace defs e =
685
  let se = substitute_expr vars_to_replace defs in
686
  { e with expr_desc = 
687
      let ed = e.expr_desc in
688
      match ed with
689
      | Expr_const _ -> ed
690
      | Expr_array el -> Expr_array (List.map se el)
691
      | Expr_access (e1, d) -> Expr_access (se e1, d)
692
      | Expr_power (e1, d) -> Expr_power (se e1, d)
693
      | Expr_tuple el -> Expr_tuple (List.map se el)
694
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
695
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
696
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
697
      | Expr_pre e' -> Expr_pre (se e')
698
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
699
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
700
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
701
      | Expr_ident i -> 
702
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
703
	  let eq_i eq = eq.eq_lhs = [i] in
704
	  if List.exists eq_i defs then
705
	    let sub = List.find eq_i defs in
706
	    let sub' = se sub.eq_rhs in
707
	    sub'.expr_desc
708
	  else 
709
	    assert false
710
	)
711
	else
712
	  ed
713

    
714
  }
715
(* FAUT IL RETIRER ?
716
  
717
 let rec expr_to_eexpr  expr =
718
   { eexpr_tag = expr.expr_tag;
719
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
720
     eexpr_type = expr.expr_type;
721
     eexpr_clock = expr.expr_clock;
722
     eexpr_loc = expr.expr_loc
723
   }
724
 and expr_desc_to_eexpr_desc expr_desc =
725
   let conv = expr_to_eexpr in
726
   match expr_desc with
727
   | Expr_const c -> EExpr_const (match c with
728
     | Const_int x -> EConst_int x 
729
     | Const_real x -> EConst_real x 
730
     | Const_float x -> EConst_float x 
731
     | Const_tag x -> EConst_tag x 
732
     | _ -> assert false
733

    
734
   )
735
   | Expr_ident i -> EExpr_ident i
736
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
737

    
738
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
739
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
740
   | Expr_pre e' -> EExpr_pre (conv e')
741
   | Expr_appl (i, e', i') -> 
742
     EExpr_appl 
743
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
744

    
745
   | Expr_when _
746
   | Expr_merge _ -> assert false
747
   | Expr_array _ 
748
   | Expr_access _ 
749
   | Expr_power _  -> assert false
750
   | Expr_ite (c, t, e) -> assert false 
751
   | _ -> assert false
752

    
753
     *)
754
let rec get_expr_calls nodes e =
755
  get_calls_expr_desc nodes e.expr_desc
756
and get_calls_expr_desc nodes expr_desc =
757
  let get_calls = get_expr_calls nodes in
758
  match expr_desc with
759
  | Expr_const _ 
760
   | Expr_ident _ -> Utils.ISet.empty
761
   | Expr_tuple el
762
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
763
   | Expr_pre e1 
764
   | Expr_when (e1, _, _) 
765
   | Expr_access (e1, _) 
766
   | Expr_power (e1, _) -> get_calls e1
767
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
768
   | Expr_arrow (e1, e2) 
769
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
770
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
771
   | Expr_appl (i, e', i') -> 
772
     if Basic_library.is_internal_fun i then 
773
       (get_calls e') 
774
     else
775
       let calls =  Utils.ISet.add i (get_calls e') in
776
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
777
       if List.exists test nodes then
778
	 match (List.find test nodes).top_decl_desc with
779
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
780
	 | _ -> assert false
781
       else 
782
	 calls
783

    
784
and get_eq_calls nodes eq =
785
  get_expr_calls nodes eq.eq_rhs
786
and get_node_calls nodes node =
787
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
788

    
789

    
790
let rec expr_has_arrows e =
791
  expr_desc_has_arrows e.expr_desc
792
and expr_desc_has_arrows expr_desc =
793
  match expr_desc with
794
  | Expr_const _ 
795
  | Expr_ident _ -> false
796
  | Expr_tuple el
797
  | Expr_array el -> List.exists expr_has_arrows el
798
  | Expr_pre e1 
799
  | Expr_when (e1, _, _) 
800
  | Expr_access (e1, _) 
801
  | Expr_power (e1, _) -> expr_has_arrows e1
802
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
803
  | Expr_arrow (e1, e2) 
804
  | Expr_fby (e1, e2) -> true
805
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
806
  | Expr_appl (i, e', i') -> expr_has_arrows e'
807

    
808
and eq_has_arrows eq =
809
  expr_has_arrows eq.eq_rhs
810
and node_has_arrows node =
811
  List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
812

    
813
(* Local Variables: *)
814
(* compile-command:"make -C .." *)
815
(* End: *)