Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 54ae8ac7

History | View | Annotate | Download (25.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
(** 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
     mutable node_dec_stateless: bool;
108
     mutable node_stateless: bool option;
109
     node_spec: LustreSpec.node_annot option;
110
     node_annot: LustreSpec.expr_annot option;
111
    }
112

    
113
type imported_node_desc =
114
    {nodei_id: ident;
115
     mutable nodei_type: Types.type_expr;
116
     mutable nodei_clock: Clocks.clock_expr;
117
     nodei_inputs: var_decl list;
118
     nodei_outputs: var_decl list;
119
     nodei_stateless: bool;
120
     nodei_spec: LustreSpec.node_annot option;
121
     nodei_prototype: string option;
122
     nodei_in_lib: string option;
123
    }
124

    
125
type const_desc = 
126
    {const_id: ident; 
127
     const_loc: Location.t; 
128
     const_value: constant;      
129
     mutable const_type: Types.type_expr;
130
    }
131

    
132
type top_decl_desc =
133
| Node of node_desc
134
| Consts of const_desc list
135
| ImportedNode of imported_node_desc
136
| Open of bool * string (* the boolean set to true denotes a local 
137
			   lusi vs a lusi installed at system level *)
138

    
139
type top_decl =
140
    {top_decl_desc: top_decl_desc;
141
     top_decl_loc: Location.t}
142

    
143
type program = top_decl list
144

    
145
type error =
146
    Main_not_found
147
  | Main_wrong_kind
148
  | No_main_specified
149
  | Unbound_symbol of ident
150
  | Already_bound_symbol of ident
151

    
152
exception Error of Location.t * error
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
(* Fast access to nodes, by name *)
234
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
235
let consts_table = Hashtbl.create 30
236

    
237
let node_name td =
238
    match td.top_decl_desc with 
239
    | Node nd         -> nd.node_id
240
    | ImportedNode nd -> nd.nodei_id
241
    | _ -> assert false
242

    
243
let is_generic_node td =
244
  match td.top_decl_desc with 
245
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
246
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
247
  | _ -> assert false
248

    
249
let node_inputs td =
250
  match td.top_decl_desc with 
251
  | Node nd         -> nd.node_inputs
252
  | ImportedNode nd -> nd.nodei_inputs
253
  | _ -> assert false
254

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

    
261
let is_imported_node td =
262
  match td.top_decl_desc with 
263
  | Node nd         -> false
264
  | ImportedNode nd -> true
265
  | _ -> assert false
266

    
267

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

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

    
284
let get_repr_type typ =
285
  let typ_def = Hashtbl.find type_table typ in
286
  if is_user_type typ_def then typ else typ_def
287

    
288
let tag_true = "true"
289
let tag_false = "false"
290

    
291
let const_is_bool c =
292
 match c with
293
 | Const_tag t -> t = tag_true || t = tag_false
294
 | _           -> false
295

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

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

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

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

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

    
330
(* To guarantee uniqueness of tags in enum types *)
331
let tag_table =
332
  Utils.create_hashtable 20 [
333
   tag_true, Tydec_bool;
334
   tag_false, Tydec_bool
335
  ]
336

    
337
(* To guarantee uniqueness of fields in struct types *)
338
let field_table =
339
  Utils.create_hashtable 20 [
340
  ]
341

    
342
let get_enum_type_tags cty =
343
 match cty with
344
 | Tydec_bool    -> [tag_true; tag_false]
345
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
346
                     | Tydec_enum tl -> tl
347
                     | _             -> assert false)
348
 | _            -> assert false
349

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

    
357
let const_of_bool b =
358
 Const_tag (if b then tag_true else tag_false)
359

    
360
(* let get_const c = snd (Hashtbl.find consts_table c) *)
361

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

    
372
let expr_list_of_expr expr =
373
  match expr.expr_desc with
374
  | Expr_tuple elist ->
375
      elist
376
  | _ -> [expr]
377

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

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

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

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

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

    
427

    
428
let sort_handlers hl =
429
 List.sort (fun (t, _) (t', _) -> compare t t') hl
430

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

    
453
let node_vars nd =
454
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
455

    
456
let node_var id node =
457
 List.find (fun v -> v.var_id = id) (node_vars node)
458

    
459
let node_eq id node =
460
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
461

    
462
(* Consts unfoooolding *)
463
let is_const i consts = 
464
  List.exists (fun c -> c.const_id = i) consts
465

    
466
let get_const i consts =
467
  let c = List.find (fun c -> c.const_id = i) consts in
468
  c.const_value
469

    
470
let rec expr_unfold_consts consts e = 
471
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }
472

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

    
495
let eq_unfold_consts consts eq =
496
  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
497

    
498
let node_unfold_consts consts node = 
499
  { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
500

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

    
509

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

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

    
526

    
527

    
528
(************************************************************************)
529
(*        Renaming                                                      *)
530

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

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

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

    
589

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

    
612
 let rename_node_annot f_node f_var f_const expr  =
613
   expr
614
 (* TODO assert false *)
615

    
616
 let rename_expr_annot f_node f_var f_const annot =
617
   annot
618
 (* TODO assert false *)
619

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

    
665

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

    
683
(**********************************************************************)
684
(* Pretty printers *)
685

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

    
698
let pp_prog_type fmt tdecl_list =
699
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
700

    
701
let pp_decl_clock fmt cdecl =
702
  match cdecl.top_decl_desc with
703
  | Node nd ->
704
    fprintf fmt "%s: " nd.node_id;
705
    Utils.reset_names ();
706
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
707
  | ImportedNode ind ->
708
    fprintf fmt "%s: " ind.nodei_id;
709
    Utils.reset_names ();
710
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
711
  | Consts _ | Open _ -> ()
712

    
713
let pp_prog_clock fmt prog =
714
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
715

    
716
let pp_error fmt = function
717
    Main_not_found ->
718
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
719
	!Options.main_node
720
  | Main_wrong_kind ->
721
    fprintf fmt
722
      "Name %s does not correspond to a (non-imported) node definition.@." 
723
      !Options.main_node
724
  | No_main_specified ->
725
    fprintf fmt "No main node specified@."
726
  | Unbound_symbol sym ->
727
    fprintf fmt
728
      "%s is undefined.@."
729
      sym
730
  | Already_bound_symbol sym -> 
731
    fprintf fmt
732
      "%s is already defined.@."
733
      sym
734

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

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

    
764
let add_internal_funs () =
765
  List.iter
766
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
767
    Basic_library.internal_funs
768

    
769
(* Local Variables: *)
770
(* compile-command:"make -C .." *)
771
(* End: *)