Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ e135421f

History | View | Annotate | Download (25.3 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
    }
122

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

    
130
type top_decl_desc =
131
  | Node of node_desc
132
  | Consts of const_desc list
133
  | ImportedNode of imported_node_desc
134
  | Open of string
135

    
136
type top_decl =
137
    {top_decl_desc: top_decl_desc;
138
     top_decl_loc: Location.t}
139

    
140
type program = top_decl list
141

    
142
type error =
143
    Main_not_found
144
  | Main_wrong_kind
145
  | No_main_specified
146
  | Unbound_symbol of ident
147
  | Already_bound_symbol of ident
148

    
149
exception Error of Location.t * error
150

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

    
159
module VMap = Map.Make(VDeclModule)
160

    
161
module VSet = Set.Make(VDeclModule)
162

    
163
(************************************************************)
164
(* *)
165

    
166
let mktyp loc d =
167
  { ty_dec_desc = d; ty_dec_loc = loc }
168

    
169
let mkclock loc d =
170
  { ck_dec_desc = d; ck_dec_loc = loc }
171

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

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

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

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

    
206
let update_expr_annot e annot =
207
  { e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) }
208

    
209
let mkeq loc (lhs, rhs) =
210
  { eq_lhs = lhs;
211
    eq_rhs = rhs;
212
    eq_loc = loc }
213

    
214
let mkassert loc expr =
215
  { assert_loc = loc;
216
    assert_expr = expr
217
  }
218

    
219
let mktop_decl loc d =
220
  { top_decl_desc = d; top_decl_loc = loc }
221

    
222
let mkpredef_call loc funname args =
223
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
224

    
225
let mkpredef_unary_call loc funname arg =
226
  mkexpr loc (Expr_appl (funname, arg, None))
227

    
228

    
229
(***********************************************************)
230
(* Fast access to nodes, by name *)
231
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
232
let consts_table = Hashtbl.create 30
233

    
234
let node_name td =
235
    match td.top_decl_desc with 
236
    | Node nd         -> nd.node_id
237
    | ImportedNode nd -> nd.nodei_id
238
    | _ -> assert false
239

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

    
246
let node_inputs td =
247
  match td.top_decl_desc with 
248
  | Node nd         -> nd.node_inputs
249
  | ImportedNode nd -> nd.nodei_inputs
250
  | _ -> assert false
251

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

    
258
let is_imported_node td =
259
  match td.top_decl_desc with 
260
  | Node nd         -> false
261
  | ImportedNode nd -> true
262
  | _ -> assert false
263

    
264

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

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

    
281
let get_repr_type typ =
282
  let typ_def = Hashtbl.find type_table typ in
283
  if is_user_type typ_def then typ else typ_def
284

    
285
let tag_true = "true"
286
let tag_false = "false"
287

    
288
let const_is_bool c =
289
 match c with
290
 | Const_tag t -> t = tag_true || t = tag_false
291
 | _           -> false
292

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

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

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

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

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

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

    
334
(* To guarantee uniqueness of fields in struct types *)
335
let field_table =
336
  Utils.create_hashtable 20 [
337
  ]
338

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

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

    
354
let const_of_bool b =
355
 Const_tag (if b then tag_true else tag_false)
356

    
357
(* let get_const c = snd (Hashtbl.find consts_table c) *)
358

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

    
369
let expr_list_of_expr expr =
370
  match expr.expr_desc with
371
  | Expr_tuple elist ->
372
      elist
373
  | _ -> [expr]
374

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

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

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

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

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

    
424

    
425
let sort_handlers hl =
426
 List.sort (fun (t, _) (t', _) -> compare t t') hl
427

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

    
450
let node_vars nd =
451
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
452

    
453
let node_var id node =
454
 List.find (fun v -> v.var_id = id) (node_vars node)
455

    
456
let node_eq id node =
457
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
458

    
459
(* Consts unfoooolding *)
460
let is_const i consts = 
461
  List.exists (fun c -> c.const_id = i) consts
462

    
463
let get_const i consts =
464
  let c = List.find (fun c -> c.const_id = i) consts in
465
  c.const_value
466

    
467
let rec expr_unfold_consts consts e = 
468
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }
469

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

    
492
let eq_unfold_consts consts eq =
493
  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
494

    
495
let node_unfold_consts consts node = 
496
  { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
497

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

    
506

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

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

    
523

    
524

    
525
(************************************************************************)
526
(*        Renaming                                                      *)
527

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

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

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

    
586

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

    
609
 let rename_node_annot f_node f_var f_const expr  =
610
   expr
611
 (* TODO assert false *)
612

    
613
 let rename_expr_annot f_node f_var f_const annot =
614
   annot
615
 (* TODO assert false *)
616

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

    
662

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

    
680
(**********************************************************************)
681
(* Pretty printers *)
682

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

    
695
let pp_prog_type fmt tdecl_list =
696
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
697

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

    
710
let pp_prog_clock fmt prog =
711
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
712

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

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

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

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

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