Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 14d694c7

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
(***********************************************************)
229
(* Fast access to nodes, by name *)
230
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
231
let consts_table = Hashtbl.create 30
232

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

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

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

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

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

    
263

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
368
let is_tuple_expr expr =
369
 match expr.expr_desc with
370
  | Expr_tuple _ -> true
371
  | _            -> false
372

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

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

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

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

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

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

    
428

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

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

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

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

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

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

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

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

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

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

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

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

    
510

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

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

    
527

    
528

    
529
(************************************************************************)
530
(*        Renaming                                                      *)
531

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

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

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

    
590

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

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

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

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

    
684
(**********************************************************************)
685
(* Pretty printers *)
686

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

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

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

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

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

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

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

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

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