Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ 6affc9f5

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
     node_spec: LustreSpec.node_annot option;
108
     node_annot: LustreSpec.expr_annot option;
109
    }
110

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

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

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

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

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

    
146
type program = top_decl list
147

    
148
type error =
149
    Main_not_found
150
  | Main_wrong_kind
151
  | No_main_specified
152
  | Unbound_symbol of ident
153
  | Already_bound_symbol of ident
154

    
155
exception Error of error * Location.t
156

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

    
165
module VMap = Map.Make(VDeclModule)
166

    
167
module VSet = Set.Make(VDeclModule)
168

    
169
(************************************************************)
170
(* *)
171

    
172
let mktyp loc d =
173
  { ty_dec_desc = d; ty_dec_loc = loc }
174

    
175
let mkclock loc d =
176
  { ck_dec_desc = d; ck_dec_loc = loc }
177

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

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

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

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

    
212
let update_expr_annot e annot =
213
  { e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) }
214

    
215
let mkeq loc (lhs, rhs) =
216
  { eq_lhs = lhs;
217
    eq_rhs = rhs;
218
    eq_loc = loc }
219

    
220
let mkassert loc expr =
221
  { assert_loc = loc;
222
    assert_expr = expr
223
  }
224

    
225
let mktop_decl loc d =
226
  { top_decl_desc = d; top_decl_loc = loc }
227

    
228
let mkpredef_call loc funname args =
229
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
230

    
231
let mkpredef_unary_call loc funname arg =
232
  mkexpr loc (Expr_appl (funname, arg, None))
233

    
234

    
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
(* To guarantee uniqueness of fields in struct types *)
340
let field_table =
341
  Utils.create_hashtable 20 [
342
  ]
343

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

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

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

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

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

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

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

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

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

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

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

    
429

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

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

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

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

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

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

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

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

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

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

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

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

    
511

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

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

    
528

    
529

    
530
(************************************************************************)
531
(*        Renaming                                                      *)
532

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

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

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

    
591

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

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

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

    
622
let rename_node f_node f_var f_const nd =
623
  let rename_var v = { v with var_id = f_var v.var_id } in
624
  let inputs = List.map rename_var nd.node_inputs in
625
  let outputs = List.map rename_var nd.node_outputs in
626
  let locals = List.map rename_var nd.node_locals in
627
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
628
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
629
  let node_asserts = List.map 
630
    (fun a -> 
631
      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
632
    ) nd.node_asserts
633
  in
634
  let eqs = List.map 
635
    (fun eq -> { eq with
636
      eq_lhs = List.map f_var eq.eq_lhs; 
637
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
638
    } ) nd.node_eqs
639
  in
640
  let spec = 
641
    Utils.option_map 
642
      (fun s -> rename_node_annot f_node f_var f_const s) 
643
      nd.node_spec 
644
  in
645
  let annot =
646
    Utils.option_map
647
      (fun s -> rename_expr_annot f_node f_var f_const s) 
648
      nd.node_annot
649
  in
650
  {
651
    node_id = f_node nd.node_id;
652
    node_type = nd.node_type;
653
    node_clock = nd.node_clock;
654
    node_inputs = inputs;
655
    node_outputs = outputs;
656
    node_locals = locals;
657
    node_gencalls = gen_calls;
658
    node_checks = node_checks;
659
    node_asserts = node_asserts;
660
    node_eqs = eqs;
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
      | ImportedFun _
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
  | ImportedFun ind ->
698
    fprintf fmt "%s: " ind.fun_id;
699
    Utils.reset_names ();
700
    fprintf fmt "%a@ " Types.print_ty ind.fun_type
701
  | Consts _ | Open _ -> ()
702

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

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

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

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

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

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

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

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