Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / corelang.ml @ d3e4c22f

History | View | Annotate | Download (26.8 KB)

1 0cbf0839 ploc
(* ----------------------------------------------------------------------------
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 aa223e69 xthirioux
  | Const_struct of (label * constant) list
43 0cbf0839 ploc
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 c02d255e ploc
  | Expr_appl of call_t
80 0cbf0839 ploc
  | Expr_uclock of expr * int
81
  | Expr_dclock of expr * int
82
  | Expr_phclock of expr * rat
83 c02d255e ploc
 and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
84 0cbf0839 ploc
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 d3e4c22f xthirioux
     node_dec_stateless: bool;
108
     mutable node_stateless: bool option;
109 0cbf0839 ploc
     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 f22632aa ploc
  | Open of string
135 0cbf0839 ploc
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 6affc9f5 xthirioux
  | Unbound_symbol of ident
147
  | Already_bound_symbol of ident
148 d3e4c22f xthirioux
  | Stateful of ident
149 0cbf0839 ploc
150 d3e4c22f xthirioux
exception Error of Location.t * error
151 0cbf0839 ploc
152
module VDeclModule =
153
struct (* Node module *)
154
  type t = var_decl
155
  let compare v1 v2 = compare v1 v2
156
  let hash n = Hashtbl.hash n
157
  let equal n1 n2 = n1 = n2
158
end
159
160
module VMap = Map.Make(VDeclModule)
161
162
module VSet = Set.Make(VDeclModule)
163
164
(************************************************************)
165
(* *)
166
167
let mktyp loc d =
168
  { ty_dec_desc = d; ty_dec_loc = loc }
169
170
let mkclock loc d =
171
  { ck_dec_desc = d; ck_dec_loc = loc }
172
173
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) =
174
  { var_id = id;
175
    var_dec_type = ty_dec;
176
    var_dec_clock = ck_dec;
177
    var_dec_const = is_const;
178
    var_type = Types.new_var ();
179
    var_clock = Clocks.new_var true;
180
    var_loc = loc }
181
182
let mkexpr loc d =
183
  { expr_tag = Utils.new_tag ();
184
    expr_desc = d;
185
    expr_type = Types.new_var ();
186
    expr_clock = Clocks.new_var true;
187
    expr_delay = Delay.new_var ();
188
    expr_annot = None;
189
    expr_loc = loc }
190
191
let var_decl_of_const c =
192
  { var_id = c.const_id;
193
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
194
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
195
    var_dec_const = true;
196
    var_type = c.const_type;
197
    var_clock = Clocks.new_var false;
198
    var_loc = c.const_loc }
199
200
let mk_new_name vdecl_list id =
201
  let rec new_name name cpt =
202
    if List.exists (fun v -> v.var_id = name) vdecl_list
203
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
204
    else name
205
  in new_name id 1
206
207
let update_expr_annot e annot =
208
  { e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) }
209
210
let mkeq loc (lhs, rhs) =
211
  { eq_lhs = lhs;
212
    eq_rhs = rhs;
213
    eq_loc = loc }
214
215
let mkassert loc expr =
216
  { assert_loc = loc;
217
    assert_expr = expr
218
  }
219
220
let mktop_decl loc d =
221
  { top_decl_desc = d; top_decl_loc = loc }
222
223
let mkpredef_call loc funname args =
224
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
225
226
let mkpredef_unary_call loc funname arg =
227
  mkexpr loc (Expr_appl (funname, arg, None))
228
229
230
(***********************************************************)
231
(* Fast access to nodes, by name *)
232
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
233
let consts_table = Hashtbl.create 30
234
235
let node_name td =
236
    match td.top_decl_desc with 
237
    | Node nd         -> nd.node_id
238
    | ImportedNode nd -> nd.nodei_id
239
    | _ -> assert false
240
241
let is_generic_node td =
242
  match td.top_decl_desc with 
243
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
244
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
245
  | _ -> assert false
246
247
let node_inputs td =
248
  match td.top_decl_desc with 
249
  | Node nd         -> nd.node_inputs
250
  | ImportedNode nd -> nd.nodei_inputs
251
  | _ -> assert false
252
253
let node_from_name id =
254
  try
255
    Hashtbl.find node_table id
256
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
257
		     assert false)
258
259
let is_imported_node td =
260
  match td.top_decl_desc with 
261
  | Node nd         -> false
262
  | ImportedNode nd -> true
263
  | _ -> assert false
264
265 d3e4c22f xthirioux
let rec is_stateless_expr expr =
266
  match expr.expr_desc with
267
  | Expr_const _ 
268
  | Expr_ident _ -> true
269
  | Expr_tuple el
270
  | Expr_array el -> List.for_all is_stateless_expr el
271
  | Expr_access (e1, _)
272
  | Expr_power (e1, _) -> is_stateless_expr e1
273
  | Expr_ite (c, t, e) -> is_stateless_expr c && is_stateless_expr t && is_stateless_expr e
274
  | Expr_arrow (e1, e2)
275
  | Expr_fby (e1, e2) -> is_stateless_expr e1 && is_stateless_expr e2
276
  | Expr_pre e' -> is_stateless_expr e'
277
  | Expr_when (e', i, l)-> is_stateless_expr e'
278
  | Expr_merge (i, hl) -> List.for_all (fun (t, h) -> is_stateless_expr h) hl 
279
  | Expr_appl (i, e', i') ->
280
    is_stateless_expr e' &&
281
      (Basic_library.is_internal_fun i || check_stateless_node (node_from_name i))
282
  | Expr_uclock _
283
  | Expr_dclock _
284
  | Expr_phclock _ -> assert false
285
and compute_stateless_node nd =
286
 List.for_all (fun eq -> is_stateless_expr eq.eq_rhs) nd.node_eqs
287
and check_stateless_node td =
288
  match td.top_decl_desc with 
289
  | Node nd         -> (
290
    match nd.node_stateless with
291
    | None     -> 
292
      begin
293
	let stateless = compute_stateless_node nd in
294
	nd.node_stateless <- Some (false && stateless);
295
	if nd.node_dec_stateless && (not stateless)
296
	then raise (Error (td.top_decl_loc, Stateful nd.node_id))
297
	else stateless
298
      end
299
    | Some stl -> stl)
300
  | ImportedNode nd -> nd.nodei_stateless
301
  | _ -> true
302
303 0cbf0839 ploc
(* alias and type definition table *)
304
let type_table =
305
  Utils.create_hashtable 20 [
306
    Tydec_int  , Tydec_int;
307
    Tydec_bool , Tydec_bool;
308
    Tydec_float, Tydec_float;
309
    Tydec_real , Tydec_real
310
  ]
311
312
let rec is_user_type typ =
313
  match typ with
314
  | Tydec_int | Tydec_bool | Tydec_real 
315
  | Tydec_float | Tydec_any | Tydec_const _ -> false
316
  | Tydec_clock typ' -> is_user_type typ'
317
  | _ -> true
318
319
let get_repr_type typ =
320
  let typ_def = Hashtbl.find type_table typ in
321
  if is_user_type typ_def then typ else typ_def
322
323
let tag_true = "true"
324
let tag_false = "false"
325
326
let const_is_bool c =
327
 match c with
328
 | Const_tag t -> t = tag_true || t = tag_false
329
 | _           -> false
330
331
(* Computes the negation of a boolean constant *)
332
let const_negation c =
333
  assert (const_is_bool c);
334
  match c with
335
  | Const_tag t when t = tag_true  -> Const_tag tag_false
336
  | _                              -> Const_tag tag_true
337
338
let const_or c1 c2 =
339
  assert (const_is_bool c1 && const_is_bool c2);
340
  match c1, c2 with
341
  | Const_tag t1, _            when t1 = tag_true -> c1
342
  | _           , Const_tag t2 when t2 = tag_true -> c2
343
  | _                                             -> Const_tag tag_false
344
345
let const_and c1 c2 =
346
  assert (const_is_bool c1 && const_is_bool c2);
347
  match c1, c2 with
348
  | Const_tag t1, _            when t1 = tag_false -> c1
349
  | _           , Const_tag t2 when t2 = tag_false -> c2
350
  | _                                              -> Const_tag tag_true
351
352
let const_xor c1 c2 =
353
  assert (const_is_bool c1 && const_is_bool c2);
354
   match c1, c2 with
355
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
356
  | _                                         -> Const_tag tag_false
357
358
let const_impl c1 c2 =
359
  assert (const_is_bool c1 && const_is_bool c2);
360
  match c1, c2 with
361
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
362
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
363
  | _                                             -> Const_tag tag_false
364
365
(* To guarantee uniqueness of tags in enum types *)
366
let tag_table =
367
  Utils.create_hashtable 20 [
368
   tag_true, Tydec_bool;
369
   tag_false, Tydec_bool
370
  ]
371
372 9bdfc99f xthirioux
(* To guarantee uniqueness of fields in struct types *)
373
let field_table =
374
  Utils.create_hashtable 20 [
375
  ]
376
377 0cbf0839 ploc
let get_enum_type_tags cty =
378
 match cty with
379
 | Tydec_bool    -> [tag_true; tag_false]
380
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
381
                     | Tydec_enum tl -> tl
382
                     | _             -> assert false)
383
 | _            -> assert false
384 6560bb94 xthirioux
385 9bdfc99f xthirioux
let get_struct_type_fields cty =
386
 match cty with
387
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
388
                     | Tydec_struct fl -> fl
389
                     | _               -> assert false)
390
 | _            -> assert false
391 6560bb94 xthirioux
392 0cbf0839 ploc
let const_of_bool b =
393
 Const_tag (if b then tag_true else tag_false)
394
395
(* let get_const c = snd (Hashtbl.find consts_table c) *)
396
397
(* Caution, returns an untyped and unclocked expression *)
398
let expr_of_ident id loc =
399
  {expr_tag = Utils.new_tag ();
400
   expr_desc = Expr_ident id;
401
   expr_type = Types.new_var ();
402
   expr_clock = Clocks.new_var true;
403
   expr_delay = Delay.new_var ();
404
   expr_loc = loc;
405
   expr_annot = None}
406
407
let expr_list_of_expr expr =
408
  match expr.expr_desc with
409
  | Expr_tuple elist ->
410
      elist
411
  | _ -> [expr]
412
413
let expr_of_expr_list loc elist =
414
 match elist with
415
 | [t]  -> { t with expr_loc = loc }
416
 | t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc }
417
 | _    -> assert false
418
419
let call_of_expr expr =
420
 match expr.expr_desc with
421
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
422
 | _                      -> assert false
423
424
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
425
let rec expr_of_dimension dim =
426
 match dim.dim_desc with
427
 | Dbool b        ->
428
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
429
 | Dint i         ->
430
     mkexpr dim.dim_loc (Expr_const (Const_int i))
431
 | Dident id      ->
432
     mkexpr dim.dim_loc (Expr_ident id)
433
 | Dite (c, t, e) ->
434
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
435
 | Dappl (id, args) ->
436
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
437
 | Dlink dim'       -> expr_of_dimension dim'
438
 | Dvar
439
 | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
440
			assert false)
441
442
let dimension_of_const loc const =
443
 match const with
444
 | Const_int i                                    -> mkdim_int loc i
445
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
446
 | _                                              -> raise InvalidDimension
447
448
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
449
   into dimension expressions *)
450
let rec dimension_of_expr expr =
451
  match expr.expr_desc with
452
  | Expr_const c  -> dimension_of_const expr.expr_loc c
453
  | Expr_ident id -> mkdim_ident expr.expr_loc id
454
  | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
455
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
456
      if k = None then raise InvalidDimension;
457
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
458
  | Expr_ite (i, t, e)        ->
459
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
460
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
461
462
463
let sort_handlers hl =
464
 List.sort (fun (t, _) (t', _) -> compare t t') hl
465
466
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
467
  | Expr_const c1, Expr_const c2 -> c1 = c2
468
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
469
  | Expr_array el1, Expr_array el2 
470
  | Expr_tuple el1, Expr_tuple el2 -> 
471
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
472
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
473
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
474
  | 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
475
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
476
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
477
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
478
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
479
  | 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')
480
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
481
  | Expr_uclock(e, i), Expr_uclock(e', i') -> i=i' && is_eq_expr e e'
482
  | Expr_dclock(e, i), Expr_dclock(e', i') -> i=i' && is_eq_expr e e'
483
  | Expr_phclock(e, r), Expr_phclock(e', r') -> r=r' && is_eq_expr e e'
484
  | Expr_power (e1, i1), Expr_power (e2, i2)
485
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
486
  | _ -> false
487
488
let node_vars nd =
489
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
490
491
let node_var id node =
492
 List.find (fun v -> v.var_id = id) (node_vars node)
493
494
let node_eq id node =
495
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
496
497
(* Consts unfoooolding *)
498
let is_const i consts = 
499
  List.exists (fun c -> c.const_id = i) consts
500
501
let get_const i consts =
502
  let c = List.find (fun c -> c.const_id = i) consts in
503
  c.const_value
504
505
let rec expr_unfold_consts consts e = 
506
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }
507
508
and expr_desc_unfold_consts consts e =
509
  let unfold = expr_unfold_consts consts in
510
  match e with
511
  | Expr_const _ -> e
512
  | Expr_ident i -> if is_const i consts then Expr_const (get_const i consts) else e
513
  | Expr_array el -> Expr_array (List.map unfold el)
514
  | Expr_access (e1, d) -> Expr_access (unfold e1, d)
515
  | Expr_power (e1, d) -> Expr_power (unfold e1, d)
516
  | Expr_tuple el -> Expr_tuple (List.map unfold el)
517
  | Expr_ite (c, t, e) -> Expr_ite (unfold c, unfold t, unfold e)
518
  | Expr_arrow (e1, e2)-> Expr_arrow (unfold e1, unfold e2) 
519
  | Expr_fby (e1, e2) -> Expr_fby (unfold e1, unfold e2)
520
  (* | Expr_concat (e1, e2) -> Expr_concat (unfold e1, unfold e2) *)
521
  (* | Expr_tail e' -> Expr_tail (unfold e') *)
522
  | Expr_pre e' -> Expr_pre (unfold e')
523
  | Expr_when (e', i, l)-> Expr_when (unfold e', i, l)
524
  | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl)
525
  | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i')
526
  | Expr_uclock (e', i) -> Expr_uclock (unfold e', i) 
527
  | Expr_dclock (e', i) -> Expr_dclock (unfold e', i)
528
  | Expr_phclock _ -> e  
529
530
let eq_unfold_consts consts eq =
531
  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
532
533
let node_unfold_consts consts node = 
534
  { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
535
536
let get_consts prog = 
537
  List.fold_left (
538
    fun consts decl ->
539
      match decl.top_decl_desc with
540
	| Consts clist -> clist@consts
541 d3e4c22f xthirioux
	| Node _ | ImportedNode _ | Open _ -> consts  
542 0cbf0839 ploc
  ) [] prog
543
544
545
let get_nodes prog = 
546
  List.fold_left (
547
    fun nodes decl ->
548
      match decl.top_decl_desc with
549
	| Node nd -> nd::nodes
550 d3e4c22f xthirioux
	| Consts _ | ImportedNode _ | Open _ -> nodes  
551 0cbf0839 ploc
  ) [] prog
552
553
let prog_unfold_consts prog =
554
  let consts = get_consts prog in
555
    List.map (
556
      fun decl -> match decl.top_decl_desc with 
557
	| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)}
558
	| _       -> decl
559
    ) prog 
560
561 c02d255e ploc
562
563
(************************************************************************)
564
(*        Renaming                                                      *)
565
566 0cbf0839 ploc
(* applies the renaming function [fvar] to all variables of expression [expr] *)
567
 let rec expr_replace_var fvar expr =
568
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
569
570
 and expr_desc_replace_var fvar expr_desc =
571
   match expr_desc with
572
   | Expr_const _ -> expr_desc
573
   | Expr_ident i -> Expr_ident (fvar i)
574
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
575
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
576
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
577
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
578
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
579
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
580
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
581
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
582
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
583
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
584
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
585
   | _ -> assert false
586
587
(* Applies the renaming function [fvar] to every rhs
588
   only when the corresponding lhs satisfies predicate [pvar] *)
589
 let eq_replace_rhs_var pvar fvar eq =
590
   let pvar l = List.exists pvar l in
591
   let rec replace lhs rhs =
592
     { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
593
   and replace_desc lhs rhs_desc =
594
     match lhs with
595
     | []  -> assert false
596
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
597
     | _   ->
598
       (match rhs_desc with
599
       | Expr_tuple tl ->
600
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
601
       | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
602
	 let args = expr_list_of_expr arg in
603
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
604
       | Expr_array _
605
       | Expr_access _
606
       | Expr_power _
607
       | Expr_const _
608
       | Expr_ident _
609
       | Expr_appl _   ->
610
	 if pvar lhs
611
	 then expr_desc_replace_var fvar rhs_desc
612
	 else rhs_desc
613
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
614
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
615
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
616
       | Expr_pre e'          -> Expr_pre (replace lhs e')
617
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
618
				 in Expr_when (replace lhs e', i', l)
619
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
620
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
621
       | _                    -> assert false)
622
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
623
624 c02d255e ploc
625
 let rec rename_expr  f_node f_var f_const expr =
626
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
627
 and rename_expr_desc f_node f_var f_const expr_desc =
628
   let re = rename_expr  f_node f_var f_const in
629
   match expr_desc with
630
   | Expr_const _ -> expr_desc
631
   | Expr_ident i -> Expr_ident (f_var i)
632
   | Expr_array el -> Expr_array (List.map re el)
633
   | Expr_access (e1, d) -> Expr_access (re e1, d)
634
   | Expr_power (e1, d) -> Expr_power (re e1, d)
635
   | Expr_tuple el -> Expr_tuple (List.map re el)
636
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
637
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
638
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
639
   | Expr_pre e' -> Expr_pre (re e')
640
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
641
   | Expr_merge (i, hl) -> 
642
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
643
   | Expr_appl (i, e', i') -> 
644
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
645
   | _ -> assert false
646
647
 let rename_node_annot f_node f_var f_const expr  =
648 2842f7ca ploc
   expr
649
 (* TODO assert false *)
650 c02d255e ploc
651
 let rename_expr_annot f_node f_var f_const annot =
652 2842f7ca ploc
   annot
653
 (* TODO assert false *)
654 c02d255e ploc
655
let rename_node f_node f_var f_const nd =
656
  let rename_var v = { v with var_id = f_var v.var_id } in
657
  let inputs = List.map rename_var nd.node_inputs in
658
  let outputs = List.map rename_var nd.node_outputs in
659
  let locals = List.map rename_var nd.node_locals in
660
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
661
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
662
  let node_asserts = List.map 
663
    (fun a -> 
664
      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
665
    ) nd.node_asserts
666
  in
667
  let eqs = List.map 
668
    (fun eq -> { eq with
669
      eq_lhs = List.map f_var eq.eq_lhs; 
670
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
671
    } ) nd.node_eqs
672
  in
673
  let spec = 
674
    Utils.option_map 
675
      (fun s -> rename_node_annot f_node f_var f_const s) 
676
      nd.node_spec 
677
  in
678
  let annot =
679
    Utils.option_map
680
      (fun s -> rename_expr_annot f_node f_var f_const s) 
681
      nd.node_annot
682
  in
683
  {
684
    node_id = f_node nd.node_id;
685
    node_type = nd.node_type;
686
    node_clock = nd.node_clock;
687
    node_inputs = inputs;
688
    node_outputs = outputs;
689
    node_locals = locals;
690
    node_gencalls = gen_calls;
691
    node_checks = node_checks;
692
    node_asserts = node_asserts;
693
    node_eqs = eqs;
694 d3e4c22f xthirioux
    node_dec_stateless = nd.node_dec_stateless;
695
    node_stateless = nd.node_stateless;
696 c02d255e ploc
    node_spec = spec;
697
    node_annot = annot;
698
  }
699
700
701
let rename_const f_const c =
702
  { c with const_id = f_const c.const_id }
703
    
704
let rename_prog f_node f_var f_const prog =
705
  List.rev (
706
    List.fold_left (fun accu top ->
707
      (match top.top_decl_desc with
708
      | Node nd -> 
709
	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
710
      | Consts c -> 
711
	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
712
      | ImportedNode _
713
      | Open _ -> top)
714
      ::accu
715
) [] prog
716
  )
717
718
(**********************************************************************)
719 0cbf0839 ploc
(* Pretty printers *)
720
721
let pp_decl_type fmt tdecl =
722
  match tdecl.top_decl_desc with
723
  | Node nd ->
724
    fprintf fmt "%s: " nd.node_id;
725
    Utils.reset_names ();
726
    fprintf fmt "%a@ " Types.print_ty nd.node_type
727
  | ImportedNode ind ->
728
    fprintf fmt "%s: " ind.nodei_id;
729
    Utils.reset_names ();
730
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
731 f22632aa ploc
  | Consts _ | Open _ -> ()
732 0cbf0839 ploc
733
let pp_prog_type fmt tdecl_list =
734
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
735
736
let pp_decl_clock fmt cdecl =
737
  match cdecl.top_decl_desc with
738
  | Node nd ->
739
    fprintf fmt "%s: " nd.node_id;
740
    Utils.reset_names ();
741
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
742
  | ImportedNode ind ->
743
    fprintf fmt "%s: " ind.nodei_id;
744 f22632aa ploc
    Utils.reset_names ();
745
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
746 d3e4c22f xthirioux
  | Consts _ | Open _ -> ()
747 0cbf0839 ploc
748
let pp_prog_clock fmt prog =
749
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
750
751
let pp_error fmt = function
752
    Main_not_found ->
753
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
754
	!Options.main_node
755
  | Main_wrong_kind ->
756
    fprintf fmt
757
      "Name %s does not correspond to a (non-imported) node definition.@." 
758
      !Options.main_node
759
  | No_main_specified ->
760
    fprintf fmt "No main node specified@."
761 6affc9f5 xthirioux
  | Unbound_symbol sym ->
762
    fprintf fmt
763
      "%s is undefined.@."
764
      sym
765
  | Already_bound_symbol sym -> 
766
    fprintf fmt
767
      "%s is already defined.@."
768
      sym
769 d3e4c22f xthirioux
  | Stateful nd ->
770
    fprintf fmt
771
      "node %s is declared stateless, but it is stateful.@."
772
      nd
773 0cbf0839 ploc
774
(* filling node table with internal functions *)
775
let vdecls_of_typ_ck cpt ty =
776
  let loc = Location.dummy_loc in
777
  List.map
778
    (fun _ -> incr cpt;
779
              let name = sprintf "_var_%d" !cpt in
780
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
781
    (Types.type_list_of_type ty)
782
783
let mk_internal_node id =
784
  let spec = None in
785
  let ty = Env.lookup_value Basic_library.type_env id in
786
  let ck = Env.lookup_value Basic_library.clock_env id in
787
  let (tin, tout) = Types.split_arrow ty in
788
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
789
  let cpt = ref (-1) in
790
  mktop_decl Location.dummy_loc
791
    (ImportedNode
792
       {nodei_id = id;
793
	nodei_type = ty;
794
	nodei_clock = ck;
795
	nodei_inputs = vdecls_of_typ_ck cpt tin;
796
	nodei_outputs = vdecls_of_typ_ck cpt tout;
797
	nodei_stateless = Types.get_static_value ty <> None;
798
	nodei_spec = spec})
799
800
let add_internal_funs () =
801
  List.iter
802
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
803
    Basic_library.internal_funs
804
805
(* Local Variables: *)
806
(* compile-command:"make -C .." *)
807
(* End: *)