Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 12af4908

History | View | Annotate | Download (25.5 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
(** The core language and its ast. Every element of the ast contains its
27
    location in the program text. The type and clock of an ast element
28
    is mutable (and initialized to dummy values). This avoids to have to
29
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
30

    
31
type ident = Utils.ident
32
type label = Utils.ident
33
type rat = Utils.rat
34
type tag = Utils.tag
35

    
36
type constant =
37
  | Const_int of int
38
  | Const_real of string
39
  | Const_float of float
40
  | Const_array of constant list
41
  | Const_tag of label
42
  | Const_struct of (label * constant) list
43

    
44
type type_dec = LustreSpec.type_dec
45

    
46
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
47

    
48

    
49
type clock_dec = LustreSpec.clock_dec
50

    
51
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
52

    
53
type var_decl = LustreSpec.var_decl
54

    
55
(* The tag of an expression is a unique identifier used to distinguish
56
   different instances of the same node *)
57
type expr =
58
    {expr_tag: tag;
59
     expr_desc: expr_desc;
60
     mutable expr_type: Types.type_expr;
61
     mutable expr_clock: Clocks.clock_expr;
62
     mutable expr_delay: Delay.delay_expr;
63
     mutable expr_annot: LustreSpec.expr_annot option;
64
     expr_loc: Location.t}
65

    
66
and expr_desc =
67
  | Expr_const of constant
68
  | Expr_ident of ident
69
  | Expr_tuple of expr list
70
  | Expr_ite   of expr * expr * expr
71
  | Expr_arrow of expr * expr
72
  | Expr_fby of expr * expr
73
  | Expr_array of expr list
74
  | Expr_access of expr * Dimension.dim_expr
75
  | Expr_power of expr * Dimension.dim_expr
76
  | Expr_pre of expr
77
  | Expr_when of expr * ident * label
78
  | Expr_merge of ident * (label * expr) list
79
  | Expr_appl of call_t
80
  | Expr_uclock of expr * int
81
  | Expr_dclock of expr * int
82
  | Expr_phclock of expr * rat
83
 and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
84

    
85
type eq =
86
    {eq_lhs: ident list;
87
     eq_rhs: expr;
88
     eq_loc: Location.t}
89

    
90
type assert_t = 
91
    {
92
      assert_expr: expr;
93
      assert_loc: Location.t
94
    } 
95

    
96
type node_desc =
97
    {node_id: ident;
98
     mutable node_type: Types.type_expr;
99
     mutable node_clock: Clocks.clock_expr;
100
     node_inputs: var_decl list;
101
     node_outputs: var_decl list;
102
     node_locals: var_decl list;
103
     mutable node_gencalls: expr list;
104
     mutable node_checks: Dimension.dim_expr list;
105
     node_asserts: assert_t list; 
106
     node_eqs: eq list;
107
     node_spec: LustreSpec.node_annot option;
108
     node_annot: LustreSpec.expr_annot option;
109
    }
110

    
111
type imported_node_desc =
112
    {nodei_id: ident;
113
     mutable nodei_type: Types.type_expr;
114
     mutable nodei_clock: Clocks.clock_expr;
115
     nodei_inputs: var_decl list;
116
     nodei_outputs: var_decl list;
117
     nodei_stateless: bool;
118
     nodei_spec: LustreSpec.node_annot option;
119
    }
120

    
121
type imported_fun_desc =
122
    {fun_id: ident;
123
     mutable fun_type: Types.type_expr;
124
     fun_inputs: var_decl list;
125
     fun_outputs: var_decl list;
126
     fun_spec: LustreSpec.node_annot option;}
127

    
128
type const_desc = 
129
    {const_id: ident; 
130
     const_loc: Location.t; 
131
     const_value: constant;      
132
     mutable const_type: Types.type_expr;
133
    }
134

    
135
type top_decl_desc =
136
  | Node of node_desc
137
  | Consts of const_desc list
138
  | ImportedNode of imported_node_desc
139
  | ImportedFun of imported_fun_desc
140
  | Open of string
141

    
142
type top_decl =
143
    {top_decl_desc: top_decl_desc;
144
     top_decl_loc: Location.t}
145

    
146
type program = top_decl list
147

    
148
type error =
149
    Main_not_found
150
  | Main_wrong_kind
151
  | No_main_specified
152

    
153

    
154
module VDeclModule =
155
struct (* Node module *)
156
  type t = var_decl
157
  let compare v1 v2 = compare v1 v2
158
  let hash n = Hashtbl.hash n
159
  let equal n1 n2 = n1 = n2
160
end
161

    
162
module VMap = Map.Make(VDeclModule)
163

    
164
module VSet = Set.Make(VDeclModule)
165

    
166
(************************************************************)
167
(* *)
168

    
169
let mktyp loc d =
170
  { ty_dec_desc = d; ty_dec_loc = loc }
171

    
172
let mkclock loc d =
173
  { ck_dec_desc = d; ck_dec_loc = loc }
174

    
175
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) =
176
  { var_id = id;
177
    var_dec_type = ty_dec;
178
    var_dec_clock = ck_dec;
179
    var_dec_const = is_const;
180
    var_type = Types.new_var ();
181
    var_clock = Clocks.new_var true;
182
    var_loc = loc }
183

    
184
let mkexpr loc d =
185
  { expr_tag = Utils.new_tag ();
186
    expr_desc = d;
187
    expr_type = Types.new_var ();
188
    expr_clock = Clocks.new_var true;
189
    expr_delay = Delay.new_var ();
190
    expr_annot = None;
191
    expr_loc = loc }
192

    
193
let var_decl_of_const c =
194
  { var_id = c.const_id;
195
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
196
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
197
    var_dec_const = true;
198
    var_type = c.const_type;
199
    var_clock = Clocks.new_var false;
200
    var_loc = c.const_loc }
201

    
202
let mk_new_name vdecl_list id =
203
  let rec new_name name cpt =
204
    if List.exists (fun v -> v.var_id = name) vdecl_list
205
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
206
    else name
207
  in new_name id 1
208

    
209
let update_expr_annot e annot =
210
  { e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) }
211

    
212
let mkeq loc (lhs, rhs) =
213
  { eq_lhs = lhs;
214
    eq_rhs = rhs;
215
    eq_loc = loc }
216

    
217
let mkassert loc expr =
218
  { assert_loc = loc;
219
    assert_expr = expr
220
  }
221

    
222
let mktop_decl loc d =
223
  { top_decl_desc = d; top_decl_loc = loc }
224

    
225
let mkpredef_call loc funname args =
226
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
227

    
228
let mkpredef_unary_call loc funname arg =
229
  mkexpr loc (Expr_appl (funname, arg, None))
230

    
231

    
232
(***********************************************************)
233
exception Error of error
234
exception Unbound_type of type_dec_desc*Location.t
235
exception Already_bound_label of label*type_dec_desc*Location.t
236

    
237
(* Fast access to nodes, by name *)
238
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
239
let consts_table = Hashtbl.create 30
240

    
241
let node_name td =
242
    match td.top_decl_desc with 
243
    | Node nd         -> nd.node_id
244
    | ImportedNode nd -> nd.nodei_id
245
    | _ -> assert false
246

    
247
let is_generic_node td =
248
  match td.top_decl_desc with 
249
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
250
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
251
  | _ -> assert false
252

    
253
let node_inputs td =
254
  match td.top_decl_desc with 
255
  | Node nd         -> nd.node_inputs
256
  | ImportedNode nd -> nd.nodei_inputs
257
  | _ -> assert false
258

    
259
let node_from_name id =
260
  try
261
    Hashtbl.find node_table id
262
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
263
		     assert false)
264

    
265
let is_imported_node td =
266
  match td.top_decl_desc with 
267
  | Node nd         -> false
268
  | ImportedNode nd -> true
269
  | _ -> assert false
270

    
271
(* alias and type definition table *)
272
let type_table =
273
  Utils.create_hashtable 20 [
274
    Tydec_int  , Tydec_int;
275
    Tydec_bool , Tydec_bool;
276
    Tydec_float, Tydec_float;
277
    Tydec_real , Tydec_real
278
  ]
279

    
280
let rec is_user_type typ =
281
  match typ with
282
  | Tydec_int | Tydec_bool | Tydec_real 
283
  | Tydec_float | Tydec_any | Tydec_const _ -> false
284
  | Tydec_clock typ' -> is_user_type typ'
285
  | _ -> true
286

    
287
let get_repr_type typ =
288
  let typ_def = Hashtbl.find type_table typ in
289
  if is_user_type typ_def then typ else typ_def
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, Tydec_bool;
337
   tag_false, Tydec_bool
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
 match cty with
347
 | Tydec_bool    -> [tag_true; tag_false]
348
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
349
                     | Tydec_enum tl -> tl
350
                     | _             -> assert false)
351
 | _            -> assert false
352

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

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

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

    
365
(* Caution, returns an untyped and unclocked expression *)
366
let expr_of_ident id loc =
367
  {expr_tag = Utils.new_tag ();
368
   expr_desc = Expr_ident id;
369
   expr_type = Types.new_var ();
370
   expr_clock = Clocks.new_var true;
371
   expr_delay = Delay.new_var ();
372
   expr_loc = loc;
373
   expr_annot = None}
374

    
375
let expr_list_of_expr expr =
376
  match expr.expr_desc with
377
  | Expr_tuple elist ->
378
      elist
379
  | _ -> [expr]
380

    
381
let expr_of_expr_list loc elist =
382
 match elist with
383
 | [t]  -> { t with expr_loc = loc }
384
 | t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc }
385
 | _    -> assert false
386

    
387
let call_of_expr expr =
388
 match expr.expr_desc with
389
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
390
 | _                      -> assert false
391

    
392
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
393
let rec expr_of_dimension dim =
394
 match dim.dim_desc with
395
 | Dbool b        ->
396
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
397
 | Dint i         ->
398
     mkexpr dim.dim_loc (Expr_const (Const_int i))
399
 | Dident id      ->
400
     mkexpr dim.dim_loc (Expr_ident id)
401
 | Dite (c, t, e) ->
402
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
403
 | Dappl (id, args) ->
404
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
405
 | Dlink dim'       -> expr_of_dimension dim'
406
 | Dvar
407
 | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
408
			assert false)
409

    
410
let dimension_of_const loc const =
411
 match const with
412
 | Const_int i                                    -> mkdim_int loc i
413
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
414
 | _                                              -> raise InvalidDimension
415

    
416
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
417
   into dimension expressions *)
418
let rec dimension_of_expr expr =
419
  match expr.expr_desc with
420
  | Expr_const c  -> dimension_of_const expr.expr_loc c
421
  | Expr_ident id -> mkdim_ident expr.expr_loc id
422
  | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
423
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
424
      if k = None then raise InvalidDimension;
425
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
426
  | Expr_ite (i, t, e)        ->
427
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
428
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
429

    
430

    
431
let sort_handlers hl =
432
 List.sort (fun (t, _) (t', _) -> compare t t') hl
433

    
434
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
435
  | Expr_const c1, Expr_const c2 -> c1 = c2
436
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
437
  | Expr_array el1, Expr_array el2 
438
  | Expr_tuple el1, Expr_tuple el2 -> 
439
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
440
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
441
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
442
  | 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
443
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
444
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
445
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
446
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
447
  | 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')
448
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
449
  | Expr_uclock(e, i), Expr_uclock(e', i') -> i=i' && is_eq_expr e e'
450
  | Expr_dclock(e, i), Expr_dclock(e', i') -> i=i' && is_eq_expr e e'
451
  | Expr_phclock(e, r), Expr_phclock(e', r') -> r=r' && is_eq_expr e e'
452
  | Expr_power (e1, i1), Expr_power (e2, i2)
453
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
454
  | _ -> false
455

    
456
let node_vars nd =
457
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
458

    
459
let node_var id node =
460
 List.find (fun v -> v.var_id = id) (node_vars node)
461

    
462
let node_eq id node =
463
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
464

    
465
(* Consts unfoooolding *)
466
let is_const i consts = 
467
  List.exists (fun c -> c.const_id = i) consts
468

    
469
let get_const i consts =
470
  let c = List.find (fun c -> c.const_id = i) consts in
471
  c.const_value
472

    
473
let rec expr_unfold_consts consts e = 
474
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }
475

    
476
and expr_desc_unfold_consts consts e =
477
  let unfold = expr_unfold_consts consts in
478
  match e with
479
  | Expr_const _ -> e
480
  | Expr_ident i -> if is_const i consts then Expr_const (get_const i consts) else e
481
  | Expr_array el -> Expr_array (List.map unfold el)
482
  | Expr_access (e1, d) -> Expr_access (unfold e1, d)
483
  | Expr_power (e1, d) -> Expr_power (unfold e1, d)
484
  | Expr_tuple el -> Expr_tuple (List.map unfold el)
485
  | Expr_ite (c, t, e) -> Expr_ite (unfold c, unfold t, unfold e)
486
  | Expr_arrow (e1, e2)-> Expr_arrow (unfold e1, unfold e2) 
487
  | Expr_fby (e1, e2) -> Expr_fby (unfold e1, unfold e2)
488
  (* | Expr_concat (e1, e2) -> Expr_concat (unfold e1, unfold e2) *)
489
  (* | Expr_tail e' -> Expr_tail (unfold e') *)
490
  | Expr_pre e' -> Expr_pre (unfold e')
491
  | Expr_when (e', i, l)-> Expr_when (unfold e', i, l)
492
  | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl)
493
  | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i')
494
  | Expr_uclock (e', i) -> Expr_uclock (unfold e', i) 
495
  | Expr_dclock (e', i) -> Expr_dclock (unfold e', i)
496
  | Expr_phclock _ -> e  
497

    
498
let eq_unfold_consts consts eq =
499
  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
500

    
501
let node_unfold_consts consts node = 
502
  { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
503

    
504
let get_consts prog = 
505
  List.fold_left (
506
    fun consts decl ->
507
      match decl.top_decl_desc with
508
	| Consts clist -> clist@consts
509
	| Node _ | ImportedNode _ | ImportedFun _ | Open _ -> consts  
510
  ) [] prog
511

    
512

    
513
let get_nodes prog = 
514
  List.fold_left (
515
    fun nodes decl ->
516
      match decl.top_decl_desc with
517
	| Node nd -> nd::nodes
518
	| Consts _ | ImportedNode _ | ImportedFun _ | Open _ -> nodes  
519
  ) [] prog
520

    
521
let prog_unfold_consts prog =
522
  let consts = get_consts prog in
523
    List.map (
524
      fun decl -> match decl.top_decl_desc with 
525
	| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)}
526
	| _       -> decl
527
    ) prog 
528

    
529

    
530

    
531
(************************************************************************)
532
(*        Renaming                                                      *)
533

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

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

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

    
592

    
593
 let rec rename_expr  f_node f_var f_const expr =
594
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
595
 and rename_expr_desc f_node f_var f_const expr_desc =
596
   let re = rename_expr  f_node f_var f_const in
597
   match expr_desc with
598
   | Expr_const _ -> expr_desc
599
   | Expr_ident i -> Expr_ident (f_var i)
600
   | Expr_array el -> Expr_array (List.map re el)
601
   | Expr_access (e1, d) -> Expr_access (re e1, d)
602
   | Expr_power (e1, d) -> Expr_power (re e1, d)
603
   | Expr_tuple el -> Expr_tuple (List.map re el)
604
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
605
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
606
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
607
   | Expr_pre e' -> Expr_pre (re e')
608
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
609
   | Expr_merge (i, hl) -> 
610
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
611
   | Expr_appl (i, e', i') -> 
612
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
613
   | _ -> assert false
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 inputs = List.map rename_var nd.node_inputs in
626
  let outputs = List.map rename_var nd.node_outputs in
627
  let locals = List.map rename_var nd.node_locals in
628
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
629
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
630
  let node_asserts = List.map 
631
    (fun a -> 
632
      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
633
    ) nd.node_asserts
634
  in
635
  let eqs = List.map 
636
    (fun eq -> { eq with
637
      eq_lhs = List.map f_var eq.eq_lhs; 
638
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
639
    } ) nd.node_eqs
640
  in
641
  let spec = 
642
    Utils.option_map 
643
      (fun s -> rename_node_annot f_node f_var f_const s) 
644
      nd.node_spec 
645
  in
646
  let annot =
647
    Utils.option_map
648
      (fun s -> rename_expr_annot f_node f_var f_const s) 
649
      nd.node_annot
650
  in
651
  {
652
    node_id = f_node nd.node_id;
653
    node_type = nd.node_type;
654
    node_clock = nd.node_clock;
655
    node_inputs = inputs;
656
    node_outputs = outputs;
657
    node_locals = locals;
658
    node_gencalls = gen_calls;
659
    node_checks = node_checks;
660
    node_asserts = node_asserts;
661
    node_eqs = eqs;
662
    node_spec = spec;
663
    node_annot = annot;
664
  }
665

    
666

    
667
let rename_const f_const c =
668
  { c with const_id = f_const c.const_id }
669
    
670
let rename_prog f_node f_var f_const prog =
671
  List.rev (
672
    List.fold_left (fun accu top ->
673
      (match top.top_decl_desc with
674
      | Node nd -> 
675
	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
676
      | Consts c -> 
677
	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
678
      | ImportedNode _
679
      | ImportedFun _
680
      | Open _ -> top)
681
      ::accu
682
) [] prog
683
  )
684

    
685
(**********************************************************************)
686
(* Pretty printers *)
687

    
688
let pp_decl_type fmt tdecl =
689
  match tdecl.top_decl_desc with
690
  | Node nd ->
691
    fprintf fmt "%s: " nd.node_id;
692
    Utils.reset_names ();
693
    fprintf fmt "%a@ " Types.print_ty nd.node_type
694
  | ImportedNode ind ->
695
    fprintf fmt "%s: " ind.nodei_id;
696
    Utils.reset_names ();
697
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
698
  | ImportedFun ind ->
699
    fprintf fmt "%s: " ind.fun_id;
700
    Utils.reset_names ();
701
    fprintf fmt "%a@ " Types.print_ty ind.fun_type
702
  | Consts _ | Open _ -> ()
703

    
704
let pp_prog_type fmt tdecl_list =
705
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
706

    
707
let pp_decl_clock fmt cdecl =
708
  match cdecl.top_decl_desc with
709
  | Node nd ->
710
    fprintf fmt "%s: " nd.node_id;
711
    Utils.reset_names ();
712
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
713
  | ImportedNode ind ->
714
    fprintf fmt "%s: " ind.nodei_id;
715
    Utils.reset_names ();
716
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
717
  | ImportedFun _ | Consts _ | Open _ -> ()
718

    
719
let pp_prog_clock fmt prog =
720
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
721

    
722
let pp_error fmt = function
723
    Main_not_found ->
724
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
725
	!Options.main_node
726
  | Main_wrong_kind ->
727
    fprintf fmt
728
      "Name %s does not correspond to a (non-imported) node definition.@." 
729
      !Options.main_node
730
  | No_main_specified ->
731
    fprintf fmt "No main node specified@."
732

    
733
(* filling node table with internal functions *)
734
let vdecls_of_typ_ck cpt ty =
735
  let loc = Location.dummy_loc in
736
  List.map
737
    (fun _ -> incr cpt;
738
              let name = sprintf "_var_%d" !cpt in
739
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
740
    (Types.type_list_of_type ty)
741

    
742
let mk_internal_node id =
743
  let spec = None in
744
  let ty = Env.lookup_value Basic_library.type_env id in
745
  let ck = Env.lookup_value Basic_library.clock_env id in
746
  let (tin, tout) = Types.split_arrow ty in
747
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
748
  let cpt = ref (-1) in
749
  mktop_decl Location.dummy_loc
750
    (ImportedNode
751
       {nodei_id = id;
752
	nodei_type = ty;
753
	nodei_clock = ck;
754
	nodei_inputs = vdecls_of_typ_ck cpt tin;
755
	nodei_outputs = vdecls_of_typ_ck cpt tout;
756
	nodei_stateless = Types.get_static_value ty <> None;
757
	nodei_spec = spec})
758

    
759
let add_internal_funs () =
760
  List.iter
761
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
762
    Basic_library.internal_funs
763

    
764
(* Local Variables: *)
765
(* compile-command:"make -C .." *)
766
(* End: *)