Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ c02d255e

History | View | Annotate | Download (25.1 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

    
43
type type_dec = LustreSpec.type_dec
44

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

    
47

    
48
type clock_dec = LustreSpec.clock_dec
49

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

    
52
type var_decl = LustreSpec.var_decl
53

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

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

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

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

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

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

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

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

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

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

    
145
type program = top_decl list
146

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

    
152

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

    
161
module VMap = Map.Make(VDeclModule)
162

    
163
module VSet = Set.Make(VDeclModule)
164

    
165
(************************************************************)
166
(* *)
167

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

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

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

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

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

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

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

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

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

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

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

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

    
230

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

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

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

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

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

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

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

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

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

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

    
290
let tag_true = "true"
291
let tag_false = "false"
292

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

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

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

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

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

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

    
332
(* To guarantee uniqueness of tags in enum types *)
333
let tag_table =
334
  Utils.create_hashtable 20 [
335
   tag_true, Tydec_bool;
336
   tag_false, Tydec_bool
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 const_of_bool b =
348
 Const_tag (if b then tag_true else tag_false)
349

    
350
(* let get_const c = snd (Hashtbl.find consts_table c) *)
351

    
352
(* Caution, returns an untyped and unclocked expression *)
353
let expr_of_ident id loc =
354
  {expr_tag = Utils.new_tag ();
355
   expr_desc = Expr_ident id;
356
   expr_type = Types.new_var ();
357
   expr_clock = Clocks.new_var true;
358
   expr_delay = Delay.new_var ();
359
   expr_loc = loc;
360
   expr_annot = None}
361

    
362
let expr_list_of_expr expr =
363
  match expr.expr_desc with
364
  | Expr_tuple elist ->
365
      elist
366
  | _ -> [expr]
367

    
368
let expr_of_expr_list loc elist =
369
 match elist with
370
 | [t]  -> { t with expr_loc = loc }
371
 | t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc }
372
 | _    -> assert false
373

    
374
let call_of_expr expr =
375
 match expr.expr_desc with
376
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
377
 | _                      -> assert false
378

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

    
397
let dimension_of_const loc const =
398
 match const with
399
 | Const_int i                                    -> mkdim_int loc i
400
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
401
 | _                                              -> raise InvalidDimension
402

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

    
417

    
418
let sort_handlers hl =
419
 List.sort (fun (t, _) (t', _) -> compare t t') hl
420

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

    
443
let node_vars nd =
444
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
445

    
446
let node_var id node =
447
 List.find (fun v -> v.var_id = id) (node_vars node)
448

    
449
let node_eq id node =
450
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
451

    
452
(* Consts unfoooolding *)
453
let is_const i consts = 
454
  List.exists (fun c -> c.const_id = i) consts
455

    
456
let get_const i consts =
457
  let c = List.find (fun c -> c.const_id = i) consts in
458
  c.const_value
459

    
460
let rec expr_unfold_consts consts e = 
461
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }
462

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

    
485
let eq_unfold_consts consts eq =
486
  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
487

    
488
let node_unfold_consts consts node = 
489
  { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
490

    
491
let get_consts prog = 
492
  List.fold_left (
493
    fun consts decl ->
494
      match decl.top_decl_desc with
495
	| Consts clist -> clist@consts
496
	| Node _ | ImportedNode _ | ImportedFun _ | Open _ -> consts  
497
  ) [] prog
498

    
499

    
500
let get_nodes prog = 
501
  List.fold_left (
502
    fun nodes decl ->
503
      match decl.top_decl_desc with
504
	| Node nd -> nd::nodes
505
	| Consts _ | ImportedNode _ | ImportedFun _ | Open _ -> nodes  
506
  ) [] prog
507

    
508
let prog_unfold_consts prog =
509
  let consts = get_consts prog in
510
    List.map (
511
      fun decl -> match decl.top_decl_desc with 
512
	| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)}
513
	| _       -> decl
514
    ) prog 
515

    
516

    
517

    
518
(************************************************************************)
519
(*        Renaming                                                      *)
520

    
521
(* applies the renaming function [fvar] to all variables of expression [expr] *)
522
 let rec expr_replace_var fvar expr =
523
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
524

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

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

    
579

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

    
602
 let rename_node_annot f_node f_var f_const expr  =
603
   assert false
604

    
605
 let rename_expr_annot f_node f_var f_const annot =
606
   assert false
607

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

    
651

    
652
let rename_const f_const c =
653
  { c with const_id = f_const c.const_id }
654
    
655
let rename_prog f_node f_var f_const prog =
656
  List.rev (
657
    List.fold_left (fun accu top ->
658
      (match top.top_decl_desc with
659
      | Node nd -> 
660
	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
661
      | Consts c -> 
662
	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
663
      | ImportedNode _
664
      | ImportedFun _
665
      | Open _ -> top)
666
      ::accu
667
) [] prog
668
  )
669

    
670
(**********************************************************************)
671
(* Pretty printers *)
672

    
673
let pp_decl_type fmt tdecl =
674
  match tdecl.top_decl_desc with
675
  | Node nd ->
676
    fprintf fmt "%s: " nd.node_id;
677
    Utils.reset_names ();
678
    fprintf fmt "%a@ " Types.print_ty nd.node_type
679
  | ImportedNode ind ->
680
    fprintf fmt "%s: " ind.nodei_id;
681
    Utils.reset_names ();
682
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
683
  | ImportedFun ind ->
684
    fprintf fmt "%s: " ind.fun_id;
685
    Utils.reset_names ();
686
    fprintf fmt "%a@ " Types.print_ty ind.fun_type
687
  | Consts _ | Open _ -> ()
688

    
689
let pp_prog_type fmt tdecl_list =
690
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
691

    
692
let pp_decl_clock fmt cdecl =
693
  match cdecl.top_decl_desc with
694
  | Node nd ->
695
    fprintf fmt "%s: " nd.node_id;
696
    Utils.reset_names ();
697
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
698
  | ImportedNode ind ->
699
    fprintf fmt "%s: " ind.nodei_id;
700
    Utils.reset_names ();
701
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
702
  | ImportedFun _ | Consts _ | Open _ -> ()
703

    
704
let pp_prog_clock fmt prog =
705
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
706

    
707
let pp_error fmt = function
708
    Main_not_found ->
709
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
710
	!Options.main_node
711
  | Main_wrong_kind ->
712
    fprintf fmt
713
      "Name %s does not correspond to a (non-imported) node definition.@." 
714
      !Options.main_node
715
  | No_main_specified ->
716
    fprintf fmt "No main node specified@."
717

    
718
(* filling node table with internal functions *)
719
let vdecls_of_typ_ck cpt ty =
720
  let loc = Location.dummy_loc in
721
  List.map
722
    (fun _ -> incr cpt;
723
              let name = sprintf "_var_%d" !cpt in
724
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
725
    (Types.type_list_of_type ty)
726

    
727
let mk_internal_node id =
728
  let spec = None in
729
  let ty = Env.lookup_value Basic_library.type_env id in
730
  let ck = Env.lookup_value Basic_library.clock_env id in
731
  let (tin, tout) = Types.split_arrow ty in
732
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
733
  let cpt = ref (-1) in
734
  mktop_decl Location.dummy_loc
735
    (ImportedNode
736
       {nodei_id = id;
737
	nodei_type = ty;
738
	nodei_clock = ck;
739
	nodei_inputs = vdecls_of_typ_ck cpt tin;
740
	nodei_outputs = vdecls_of_typ_ck cpt tout;
741
	nodei_stateless = Types.get_static_value ty <> None;
742
	nodei_spec = spec})
743

    
744
let add_internal_funs () =
745
  List.iter
746
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
747
    Basic_library.internal_funs
748

    
749
(* Local Variables: *)
750
(* compile-command:"make -C .." *)
751
(* End: *)