Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 0038002e

History | View | Annotate | Download (23.6 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- *)
22
open Format
23
open LustreSpec
24
open Dimension
25

    
26

    
27
exception Error of Location.t * error
28

    
29
module VDeclModule =
30
struct (* Node module *)
31
  type t = var_decl
32
  let compare v1 v2 = compare v1 v2
33
  let hash n = Hashtbl.hash n
34
  let equal n1 n2 = n1 = n2
35
end
36

    
37
module VMap = Map.Make(VDeclModule)
38

    
39
module VSet = Set.Make(VDeclModule)
40

    
41
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
42

    
43

    
44

    
45
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
46

    
47

    
48

    
49
(************************************************************)
50
(* *)
51

    
52
let mktyp loc d =
53
  { ty_dec_desc = d; ty_dec_loc = loc }
54

    
55
let mkclock loc d =
56
  { ck_dec_desc = d; ck_dec_loc = loc }
57

    
58
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) =
59
  { var_id = id;
60
    var_dec_type = ty_dec;
61
    var_dec_clock = ck_dec;
62
    var_dec_const = is_const;
63
    var_type = Types.new_var ();
64
    var_clock = Clocks.new_var true;
65
    var_loc = loc }
66

    
67
let mkexpr loc d =
68
  { expr_tag = Utils.new_tag ();
69
    expr_desc = d;
70
    expr_type = Types.new_var ();
71
    expr_clock = Clocks.new_var true;
72
    expr_delay = Delay.new_var ();
73
    expr_annot = None;
74
    expr_loc = loc }
75

    
76
let var_decl_of_const c =
77
  { var_id = c.const_id;
78
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
79
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
80
    var_dec_const = true;
81
    var_type = c.const_type;
82
    var_clock = Clocks.new_var false;
83
    var_loc = c.const_loc }
84

    
85
let mk_new_name vdecl_list id =
86
  let rec new_name name cpt =
87
    if List.exists (fun v -> v.var_id = name) vdecl_list
88
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
89
    else name
90
  in new_name id 1
91

    
92
let mkeq loc (lhs, rhs) =
93
  { eq_lhs = lhs;
94
    eq_rhs = rhs;
95
    eq_loc = loc }
96

    
97
let mkassert loc expr =
98
  { assert_loc = loc;
99
    assert_expr = expr
100
  }
101

    
102
let mktop_decl loc d =
103
  { top_decl_desc = d; top_decl_loc = loc }
104

    
105
let mkpredef_call loc funname args =
106
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
107

    
108
(************************************************************)
109
(*   Eexpr functions *)
110
(************************************************************)
111

    
112
let merge_node_annot ann1 ann2 =
113
  { requires = ann1.requires @ ann2.requires;
114
    ensures = ann1.ensures @ ann2.ensures;
115
    behaviors = ann1.behaviors @ ann2.behaviors;
116
    spec_loc = ann1.spec_loc
117
  }
118

    
119
let mkeexpr loc expr =
120
  { eexpr_tag = Utils.new_tag ();
121
    eexpr_qfexpr = expr;
122
    eexpr_quantifiers = [];
123
    eexpr_type = Types.new_var ();
124
    eexpr_clock = Clocks.new_var true;
125
    eexpr_normalized = None;
126
    eexpr_loc = loc }
127

    
128
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
129

    
130
(*
131
let mkepredef_call loc funname args =
132
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
133

    
134
let mkepredef_unary_call loc funname arg =
135
  mkeexpr loc (EExpr_appl (funname, arg, None))
136
*)
137

    
138
let merge_expr_annot ann1 ann2 =
139
  match ann1, ann2 with
140
    | None, None -> assert false
141
    | Some _, None -> ann1
142
    | None, Some _ -> ann2
143
    | Some ann1, Some ann2 -> Some {
144
      annots = ann1.annots @ ann2.annots;
145
      annot_loc = ann1.annot_loc
146
    }
147

    
148
let update_expr_annot e annot =
149
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
150

    
151

    
152
(***********************************************************)
153
(* Fast access to nodes, by name *)
154
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
155
let consts_table = Hashtbl.create 30
156

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

    
163
let is_generic_node td =
164
  match td.top_decl_desc with 
165
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
166
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
167
  | _ -> assert false
168

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

    
175
let node_from_name id =
176
  try
177
    Hashtbl.find node_table id
178
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
179
		     assert false)
180

    
181
let is_imported_node td =
182
  match td.top_decl_desc with 
183
  | Node nd         -> false
184
  | ImportedNode nd -> true
185
  | _ -> assert false
186

    
187

    
188
(* alias and type definition table *)
189
let type_table =
190
  Utils.create_hashtable 20 [
191
    Tydec_int  , Tydec_int;
192
    Tydec_bool , Tydec_bool;
193
    Tydec_float, Tydec_float;
194
    Tydec_real , Tydec_real
195
  ]
196

    
197
let rec is_user_type typ =
198
  match typ with
199
  | Tydec_int | Tydec_bool | Tydec_real 
200
  | Tydec_float | Tydec_any | Tydec_const _ -> false
201
  | Tydec_clock typ' -> is_user_type typ'
202
  | _ -> true
203

    
204
let get_repr_type typ =
205
  let typ_def = Hashtbl.find type_table typ in
206
  if is_user_type typ_def then typ else typ_def
207

    
208
let tag_true = "true"
209
let tag_false = "false"
210

    
211
let const_is_bool c =
212
 match c with
213
 | Const_tag t -> t = tag_true || t = tag_false
214
 | _           -> false
215

    
216
(* Computes the negation of a boolean constant *)
217
let const_negation c =
218
  assert (const_is_bool c);
219
  match c with
220
  | Const_tag t when t = tag_true  -> Const_tag tag_false
221
  | _                              -> Const_tag tag_true
222

    
223
let const_or c1 c2 =
224
  assert (const_is_bool c1 && const_is_bool c2);
225
  match c1, c2 with
226
  | Const_tag t1, _            when t1 = tag_true -> c1
227
  | _           , Const_tag t2 when t2 = tag_true -> c2
228
  | _                                             -> Const_tag tag_false
229

    
230
let const_and c1 c2 =
231
  assert (const_is_bool c1 && const_is_bool c2);
232
  match c1, c2 with
233
  | Const_tag t1, _            when t1 = tag_false -> c1
234
  | _           , Const_tag t2 when t2 = tag_false -> c2
235
  | _                                              -> Const_tag tag_true
236

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

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

    
250
(* To guarantee uniqueness of tags in enum types *)
251
let tag_table =
252
  Utils.create_hashtable 20 [
253
   tag_true, Tydec_bool;
254
   tag_false, Tydec_bool
255
  ]
256

    
257
(* To guarantee uniqueness of fields in struct types *)
258
let field_table =
259
  Utils.create_hashtable 20 [
260
  ]
261

    
262
let get_enum_type_tags cty =
263
 match cty with
264
 | Tydec_bool    -> [tag_true; tag_false]
265
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
266
                     | Tydec_enum tl -> tl
267
                     | _             -> assert false)
268
 | _            -> assert false
269

    
270
let get_struct_type_fields cty =
271
 match cty with
272
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
273
                     | Tydec_struct fl -> fl
274
                     | _               -> assert false)
275
 | _            -> assert false
276

    
277
let const_of_bool b =
278
 Const_tag (if b then tag_true else tag_false)
279

    
280
(* let get_const c = snd (Hashtbl.find consts_table c) *)
281

    
282
let ident_of_expr expr =
283
 match expr.expr_desc with
284
 | Expr_ident id -> id
285
 | _             -> assert false
286

    
287
(* Caution, returns an untyped and unclocked expression *)
288
let expr_of_ident id loc =
289
  {expr_tag = Utils.new_tag ();
290
   expr_desc = Expr_ident id;
291
   expr_type = Types.new_var ();
292
   expr_clock = Clocks.new_var true;
293
   expr_delay = Delay.new_var ();
294
   expr_loc = loc;
295
   expr_annot = None}
296

    
297
let is_tuple_expr expr =
298
 match expr.expr_desc with
299
  | Expr_tuple _ -> true
300
  | _            -> false
301

    
302
let expr_list_of_expr expr =
303
  match expr.expr_desc with
304
  | Expr_tuple elist ->
305
      elist
306
  | _ -> [expr]
307

    
308
let expr_of_expr_list loc elist =
309
 match elist with
310
 | [t]  -> { t with expr_loc = loc }
311
 | t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc }
312
 | _    -> assert false
313

    
314
let call_of_expr expr =
315
 match expr.expr_desc with
316
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
317
 | _                      -> assert false
318

    
319
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
320
let rec expr_of_dimension dim =
321
 match dim.dim_desc with
322
 | Dbool b        ->
323
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
324
 | Dint i         ->
325
     mkexpr dim.dim_loc (Expr_const (Const_int i))
326
 | Dident id      ->
327
     mkexpr dim.dim_loc (Expr_ident id)
328
 | Dite (c, t, e) ->
329
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
330
 | Dappl (id, args) ->
331
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
332
 | Dlink dim'       -> expr_of_dimension dim'
333
 | Dvar
334
 | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
335
			assert false)
336

    
337
let dimension_of_const loc const =
338
 match const with
339
 | Const_int i                                    -> mkdim_int loc i
340
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
341
 | _                                              -> raise InvalidDimension
342

    
343
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
344
   into dimension expressions *)
345
let rec dimension_of_expr expr =
346
  match expr.expr_desc with
347
  | Expr_const c  -> dimension_of_const expr.expr_loc c
348
  | Expr_ident id -> mkdim_ident expr.expr_loc id
349
  | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
350
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
351
      if k = None then raise InvalidDimension;
352
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
353
  | Expr_ite (i, t, e)        ->
354
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
355
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
356

    
357

    
358
let sort_handlers hl =
359
 List.sort (fun (t, _) (t', _) -> compare t t') hl
360

    
361
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
362
  | Expr_const c1, Expr_const c2 -> c1 = c2
363
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
364
  | Expr_array el1, Expr_array el2 
365
  | Expr_tuple el1, Expr_tuple el2 -> 
366
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
367
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
368
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
369
  | 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
370
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
371
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
372
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
373
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
374
  | 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')
375
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
376
  | Expr_power (e1, i1), Expr_power (e2, i2)
377
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
378
  | _ -> false
379

    
380
let get_node_vars nd =
381
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
382

    
383
let get_var id var_list =
384
 List.find (fun v -> v.var_id = id) var_list
385

    
386
let get_node_var id node = get_var id (get_node_vars node)
387

    
388
let get_node_eq id node =
389
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
390

    
391
let get_nodes prog = 
392
  List.fold_left (
393
    fun nodes decl ->
394
      match decl.top_decl_desc with
395
	| Node nd -> nd::nodes
396
	| Consts _ | ImportedNode _ | Open _ -> nodes  
397
  ) [] prog
398

    
399
let get_consts prog = 
400
  List.fold_left (
401
    fun consts decl ->
402
      match decl.top_decl_desc with
403
	| Consts clist -> clist@consts
404
	| Node _ | ImportedNode _ | Open _ -> consts  
405
  ) [] prog
406

    
407

    
408

    
409
(************************************************************************)
410
(*        Renaming                                                      *)
411

    
412
(* applies the renaming function [fvar] to all variables of expression [expr] *)
413
 let rec expr_replace_var fvar expr =
414
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
415

    
416
 and expr_desc_replace_var fvar expr_desc =
417
   match expr_desc with
418
   | Expr_const _ -> expr_desc
419
   | Expr_ident i -> Expr_ident (fvar i)
420
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
421
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
422
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
423
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
424
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
425
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
426
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
427
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
428
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
429
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
430
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
431

    
432
(* Applies the renaming function [fvar] to every rhs
433
   only when the corresponding lhs satisfies predicate [pvar] *)
434
 let eq_replace_rhs_var pvar fvar eq =
435
   let pvar l = List.exists pvar l in
436
   let rec replace lhs rhs =
437
     { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
438
   and replace_desc lhs rhs_desc =
439
     match lhs with
440
     | []  -> assert false
441
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
442
     | _   ->
443
       (match rhs_desc with
444
       | Expr_tuple tl ->
445
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
446
       | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
447
	 let args = expr_list_of_expr arg in
448
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
449
       | Expr_array _
450
       | Expr_access _
451
       | Expr_power _
452
       | Expr_const _
453
       | Expr_ident _
454
       | Expr_appl _   ->
455
	 if pvar lhs
456
	 then expr_desc_replace_var fvar rhs_desc
457
	 else rhs_desc
458
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
459
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
460
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
461
       | Expr_pre e'          -> Expr_pre (replace lhs e')
462
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
463
				 in Expr_when (replace lhs e', i', l)
464
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
465
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
466
       )
467
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
468

    
469

    
470
 let rec rename_expr  f_node f_var f_const expr =
471
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
472
 and rename_expr_desc f_node f_var f_const expr_desc =
473
   let re = rename_expr  f_node f_var f_const in
474
   match expr_desc with
475
   | Expr_const _ -> expr_desc
476
   | Expr_ident i -> Expr_ident (f_var i)
477
   | Expr_array el -> Expr_array (List.map re el)
478
   | Expr_access (e1, d) -> Expr_access (re e1, d)
479
   | Expr_power (e1, d) -> Expr_power (re e1, d)
480
   | Expr_tuple el -> Expr_tuple (List.map re el)
481
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
482
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
483
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
484
   | Expr_pre e' -> Expr_pre (re e')
485
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
486
   | Expr_merge (i, hl) -> 
487
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
488
   | Expr_appl (i, e', i') -> 
489
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
490
  
491
 let rename_node_annot f_node f_var f_const expr  =
492
   expr
493
 (* TODO assert false *)
494

    
495
 let rename_expr_annot f_node f_var f_const annot =
496
   annot
497
 (* TODO assert false *)
498

    
499
let rename_node f_node f_var f_const nd =
500
  let rename_var v = { v with var_id = f_var v.var_id } in
501
  let inputs = List.map rename_var nd.node_inputs in
502
  let outputs = List.map rename_var nd.node_outputs in
503
  let locals = List.map rename_var nd.node_locals in
504
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
505
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
506
  let node_asserts = List.map 
507
    (fun a -> 
508
      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
509
    ) nd.node_asserts
510
  in
511
  let eqs = List.map 
512
    (fun eq -> { eq with
513
      eq_lhs = List.map f_var eq.eq_lhs; 
514
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
515
    } ) nd.node_eqs
516
  in
517
  let spec = 
518
    Utils.option_map 
519
      (fun s -> rename_node_annot f_node f_var f_const s) 
520
      nd.node_spec 
521
  in
522
  let annot =
523
    List.map 
524
      (fun s -> rename_expr_annot f_node f_var f_const s) 
525
      nd.node_annot
526
  in
527
  {
528
    node_id = f_node nd.node_id;
529
    node_type = nd.node_type;
530
    node_clock = nd.node_clock;
531
    node_inputs = inputs;
532
    node_outputs = outputs;
533
    node_locals = locals;
534
    node_gencalls = gen_calls;
535
    node_checks = node_checks;
536
    node_asserts = node_asserts;
537
    node_eqs = eqs;
538
    node_dec_stateless = nd.node_dec_stateless;
539
    node_stateless = nd.node_stateless;
540
    node_spec = spec;
541
    node_annot = annot;
542
  }
543

    
544

    
545
let rename_const f_const c =
546
  { c with const_id = f_const c.const_id }
547
    
548
let rename_prog f_node f_var f_const prog =
549
  List.rev (
550
    List.fold_left (fun accu top ->
551
      (match top.top_decl_desc with
552
      | Node nd -> 
553
	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
554
      | Consts c -> 
555
	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
556
      | ImportedNode _
557
      | Open _ -> top)
558
      ::accu
559
) [] prog
560
  )
561

    
562
(**********************************************************************)
563
(* Pretty printers *)
564

    
565
let pp_decl_type fmt tdecl =
566
  match tdecl.top_decl_desc with
567
  | Node nd ->
568
    fprintf fmt "%s: " nd.node_id;
569
    Utils.reset_names ();
570
    fprintf fmt "%a@ " Types.print_ty nd.node_type
571
  | ImportedNode ind ->
572
    fprintf fmt "%s: " ind.nodei_id;
573
    Utils.reset_names ();
574
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
575
  | Consts _ | Open _ -> ()
576

    
577
let pp_prog_type fmt tdecl_list =
578
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
579

    
580
let pp_decl_clock fmt cdecl =
581
  match cdecl.top_decl_desc with
582
  | Node nd ->
583
    fprintf fmt "%s: " nd.node_id;
584
    Utils.reset_names ();
585
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
586
  | ImportedNode ind ->
587
    fprintf fmt "%s: " ind.nodei_id;
588
    Utils.reset_names ();
589
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
590
  | Consts _ | Open _ -> ()
591

    
592
let pp_prog_clock fmt prog =
593
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
594

    
595
let pp_error fmt = function
596
    Main_not_found ->
597
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
598
	!Options.main_node
599
  | Main_wrong_kind ->
600
    fprintf fmt
601
      "Name %s does not correspond to a (non-imported) node definition.@." 
602
      !Options.main_node
603
  | No_main_specified ->
604
    fprintf fmt "No main node specified@."
605
  | Unbound_symbol sym ->
606
    fprintf fmt
607
      "%s is undefined.@."
608
      sym
609
  | Already_bound_symbol sym -> 
610
    fprintf fmt
611
      "%s is already defined.@."
612
      sym
613

    
614
(* filling node table with internal functions *)
615
let vdecls_of_typ_ck cpt ty =
616
  let loc = Location.dummy_loc in
617
  List.map
618
    (fun _ -> incr cpt;
619
              let name = sprintf "_var_%d" !cpt in
620
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
621
    (Types.type_list_of_type ty)
622

    
623
let mk_internal_node id =
624
  let spec = None in
625
  let ty = Env.lookup_value Basic_library.type_env id in
626
  let ck = Env.lookup_value Basic_library.clock_env id in
627
  let (tin, tout) = Types.split_arrow ty in
628
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
629
  let cpt = ref (-1) in
630
  mktop_decl Location.dummy_loc
631
    (ImportedNode
632
       {nodei_id = id;
633
	nodei_type = ty;
634
	nodei_clock = ck;
635
	nodei_inputs = vdecls_of_typ_ck cpt tin;
636
	nodei_outputs = vdecls_of_typ_ck cpt tout;
637
	nodei_stateless = Types.get_static_value ty <> None;
638
	nodei_spec = spec;
639
	nodei_prototype = None;
640
       	nodei_in_lib = None;
641
       })
642

    
643
let add_internal_funs () =
644
  List.iter
645
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
646
    Basic_library.internal_funs
647

    
648

    
649
let rec get_expr_calls nodes e =
650
  get_calls_expr_desc nodes e.expr_desc
651
and get_calls_expr_desc nodes expr_desc =
652
  let get_calls = get_expr_calls nodes in
653
  match expr_desc with
654
  | Expr_const _ 
655
   | Expr_ident _ -> Utils.ISet.empty
656
   | Expr_tuple el
657
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
658
   | Expr_pre e1 
659
   | Expr_when (e1, _, _) 
660
   | Expr_access (e1, _) 
661
   | Expr_power (e1, _) -> get_calls e1
662
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
663
   | Expr_arrow (e1, e2) 
664
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
665
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
666
   | Expr_appl (i, e', i') -> 
667
     if Basic_library.is_internal_fun i then 
668
       (get_calls e') 
669
     else
670
       let calls =  Utils.ISet.add i (get_calls e') in
671
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
672
       if List.exists test nodes then
673
	 match (List.find test nodes).top_decl_desc with
674
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
675
	 | _ -> assert false
676
       else 
677
	 calls
678

    
679
and get_eq_calls nodes eq =
680
  get_expr_calls nodes eq.eq_rhs
681
and get_node_calls nodes node =
682
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
683

    
684

    
685
let rec expr_has_arrows e =
686
  expr_desc_has_arrows e.expr_desc
687
and expr_desc_has_arrows expr_desc =
688
  match expr_desc with
689
  | Expr_const _ 
690
  | Expr_ident _ -> false
691
  | Expr_tuple el
692
  | Expr_array el -> List.exists expr_has_arrows el
693
  | Expr_pre e1 
694
  | Expr_when (e1, _, _) 
695
  | Expr_access (e1, _) 
696
  | Expr_power (e1, _) -> expr_has_arrows e1
697
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
698
  | Expr_arrow (e1, e2) 
699
  | Expr_fby (e1, e2) -> true
700
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
701
  | Expr_appl (i, e', i') -> expr_has_arrows e'
702

    
703
and eq_has_arrows eq =
704
  expr_has_arrows eq.eq_rhs
705
and node_has_arrows node =
706
  List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
707

    
708
(* Local Variables: *)
709
(* compile-command:"make -C .." *)
710
(* End: *)