Project

General

Profile

Download (25.9 KB) Statistics
| Branch: | Tag: | Revision:
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

    
27
exception Error of Location.t * error
28

    
29
module VDeclModule =
30
struct (* Node module *)
31
  type t = var_decl
32
  let compare v1 v2 = compare v1.var_id v2.var_id
33
end
34

    
35
module VMap = Map.Make(VDeclModule)
36

    
37
module VSet = Set.Make(VDeclModule)
38

    
39
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
40

    
41

    
42

    
43
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
44

    
45

    
46

    
47
(************************************************************)
48
(* *)
49

    
50
let mktyp loc d =
51
  { ty_dec_desc = d; ty_dec_loc = loc }
52

    
53
let mkclock loc d =
54
  { ck_dec_desc = d; ck_dec_loc = loc }
55

    
56
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) =
57
  { var_id = id;
58
    var_dec_type = ty_dec;
59
    var_dec_clock = ck_dec;
60
    var_dec_const = is_const;
61
    var_type = Types.new_var ();
62
    var_clock = Clocks.new_var true;
63
    var_loc = loc }
64

    
65
let mkexpr loc d =
66
  { expr_tag = Utils.new_tag ();
67
    expr_desc = d;
68
    expr_type = Types.new_var ();
69
    expr_clock = Clocks.new_var true;
70
    expr_delay = Delay.new_var ();
71
    expr_annot = None;
72
    expr_loc = loc }
73

    
74
let var_decl_of_const c =
75
  { var_id = c.const_id;
76
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
77
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
78
    var_dec_const = true;
79
    var_type = c.const_type;
80
    var_clock = Clocks.new_var false;
81
    var_loc = c.const_loc }
82

    
83
let mk_new_name vdecl_list id =
84
  let rec new_name name cpt =
85
    if List.exists (fun v -> v.var_id = name) vdecl_list
86
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
87
    else name
88
  in new_name id 1
89

    
90
let mkeq loc (lhs, rhs) =
91
  { eq_lhs = lhs;
92
    eq_rhs = rhs;
93
    eq_loc = loc }
94

    
95
let mkassert loc expr =
96
  { assert_loc = loc;
97
    assert_expr = expr
98
  }
99

    
100
let mktop_decl loc d =
101
  { top_decl_desc = d; top_decl_loc = loc }
102

    
103
let mkpredef_call loc funname args =
104
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
105

    
106
(************************************************************)
107
(*   Eexpr functions *)
108
(************************************************************)
109

    
110
let merge_node_annot ann1 ann2 =
111
  { requires = ann1.requires @ ann2.requires;
112
    ensures = ann1.ensures @ ann2.ensures;
113
    behaviors = ann1.behaviors @ ann2.behaviors;
114
    spec_loc = ann1.spec_loc
115
  }
116

    
117
let mkeexpr loc expr =
118
  { eexpr_tag = Utils.new_tag ();
119
    eexpr_qfexpr = expr;
120
    eexpr_quantifiers = [];
121
    eexpr_type = Types.new_var ();
122
    eexpr_clock = Clocks.new_var true;
123
    eexpr_normalized = None;
124
    eexpr_loc = loc }
125

    
126
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
127

    
128
(*
129
let mkepredef_call loc funname args =
130
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
131

    
132
let mkepredef_unary_call loc funname arg =
133
  mkeexpr loc (EExpr_appl (funname, arg, None))
134
*)
135

    
136
let merge_expr_annot ann1 ann2 =
137
  match ann1, ann2 with
138
    | None, None -> assert false
139
    | Some _, None -> ann1
140
    | None, Some _ -> ann2
141
    | Some ann1, Some ann2 -> Some {
142
      annots = ann1.annots @ ann2.annots;
143
      annot_loc = ann1.annot_loc
144
    }
145

    
146
let update_expr_annot e annot =
147
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
148

    
149

    
150
(***********************************************************)
151
(* Fast access to nodes, by name *)
152
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
153
let consts_table = Hashtbl.create 30
154

    
155
let node_name td =
156
    match td.top_decl_desc with 
157
    | Node nd         -> nd.node_id
158
    | ImportedNode nd -> nd.nodei_id
159
    | _ -> assert false
160

    
161
let is_generic_node td =
162
  match td.top_decl_desc with 
163
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
164
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
165
  | _ -> assert false
166

    
167
let node_inputs td =
168
  match td.top_decl_desc with 
169
  | Node nd         -> nd.node_inputs
170
  | ImportedNode nd -> nd.nodei_inputs
171
  | _ -> assert false
172

    
173
let node_from_name id =
174
  try
175
    Hashtbl.find node_table id
176
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
177
		     assert false)
178

    
179
let is_imported_node td =
180
  match td.top_decl_desc with 
181
  | Node nd         -> false
182
  | ImportedNode nd -> true
183
  | _ -> assert false
184

    
185

    
186
(* alias and type definition table *)
187
let type_table =
188
  Utils.create_hashtable 20 [
189
    Tydec_int  , Tydec_int;
190
    Tydec_bool , Tydec_bool;
191
    Tydec_float, Tydec_float;
192
    Tydec_real , Tydec_real
193
  ]
194

    
195
let rec is_user_type typ =
196
  match typ with
197
  | Tydec_int | Tydec_bool | Tydec_real 
198
  | Tydec_float | Tydec_any | Tydec_const _ -> false
199
  | Tydec_clock typ' -> is_user_type typ'
200
  | _ -> true
201

    
202
let get_repr_type typ =
203
  let typ_def = Hashtbl.find type_table typ in
204
  if is_user_type typ_def then typ else typ_def
205

    
206
let tag_true = "true"
207
let tag_false = "false"
208

    
209
let const_is_bool c =
210
 match c with
211
 | Const_tag t -> t = tag_true || t = tag_false
212
 | _           -> false
213

    
214
(* Computes the negation of a boolean constant *)
215
let const_negation c =
216
  assert (const_is_bool c);
217
  match c with
218
  | Const_tag t when t = tag_true  -> Const_tag tag_false
219
  | _                              -> Const_tag tag_true
220

    
221
let const_or c1 c2 =
222
  assert (const_is_bool c1 && const_is_bool c2);
223
  match c1, c2 with
224
  | Const_tag t1, _            when t1 = tag_true -> c1
225
  | _           , Const_tag t2 when t2 = tag_true -> c2
226
  | _                                             -> Const_tag tag_false
227

    
228
let const_and c1 c2 =
229
  assert (const_is_bool c1 && const_is_bool c2);
230
  match c1, c2 with
231
  | Const_tag t1, _            when t1 = tag_false -> c1
232
  | _           , Const_tag t2 when t2 = tag_false -> c2
233
  | _                                              -> Const_tag tag_true
234

    
235
let const_xor c1 c2 =
236
  assert (const_is_bool c1 && const_is_bool c2);
237
   match c1, c2 with
238
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
239
  | _                                         -> Const_tag tag_false
240

    
241
let const_impl c1 c2 =
242
  assert (const_is_bool c1 && const_is_bool c2);
243
  match c1, c2 with
244
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
245
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
246
  | _                                             -> Const_tag tag_false
247

    
248
(* To guarantee uniqueness of tags in enum types *)
249
let tag_table =
250
  Utils.create_hashtable 20 [
251
   tag_true, Tydec_bool;
252
   tag_false, Tydec_bool
253
  ]
254

    
255
(* To guarantee uniqueness of fields in struct types *)
256
let field_table =
257
  Utils.create_hashtable 20 [
258
  ]
259

    
260
let get_enum_type_tags cty =
261
 match cty with
262
 | Tydec_bool    -> [tag_true; tag_false]
263
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
264
                     | Tydec_enum tl -> tl
265
                     | _             -> assert false)
266
 | _            -> assert false
267

    
268
let get_struct_type_fields cty =
269
 match cty with
270
 | Tydec_const _ -> (match Hashtbl.find type_table cty with
271
                     | Tydec_struct fl -> fl
272
                     | _               -> assert false)
273
 | _            -> assert false
274

    
275
let const_of_bool b =
276
 Const_tag (if b then tag_true else tag_false)
277

    
278
(* let get_const c = snd (Hashtbl.find consts_table c) *)
279

    
280
let ident_of_expr expr =
281
 match expr.expr_desc with
282
 | Expr_ident id -> id
283
 | _             -> assert false
284

    
285
(* Caution, returns an untyped and unclocked expression *)
286
let expr_of_ident id loc =
287
  {expr_tag = Utils.new_tag ();
288
   expr_desc = Expr_ident id;
289
   expr_type = Types.new_var ();
290
   expr_clock = Clocks.new_var true;
291
   expr_delay = Delay.new_var ();
292
   expr_loc = loc;
293
   expr_annot = None}
294

    
295
let is_tuple_expr expr =
296
 match expr.expr_desc with
297
  | Expr_tuple _ -> true
298
  | _            -> false
299

    
300
let expr_list_of_expr expr =
301
  match expr.expr_desc with
302
  | Expr_tuple elist -> elist
303
  | _                -> [expr]
304

    
305
let expr_of_expr_list loc elist =
306
 match elist with
307
 | [t]  -> { t with expr_loc = loc }
308
 | t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc }
309
 | _    -> assert false
310

    
311
let call_of_expr expr =
312
 match expr.expr_desc with
313
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
314
 | _                      -> assert false
315

    
316
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
317
let rec expr_of_dimension dim =
318
 match dim.dim_desc with
319
 | Dbool b        ->
320
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
321
 | Dint i         ->
322
     mkexpr dim.dim_loc (Expr_const (Const_int i))
323
 | Dident id      ->
324
     mkexpr dim.dim_loc (Expr_ident id)
325
 | Dite (c, t, e) ->
326
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
327
 | Dappl (id, args) ->
328
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
329
 | Dlink dim'       -> expr_of_dimension dim'
330
 | Dvar
331
 | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
332
			assert false)
333

    
334
let dimension_of_const loc const =
335
 match const with
336
 | Const_int i                                    -> mkdim_int loc i
337
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
338
 | _                                              -> raise InvalidDimension
339

    
340
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
341
   into dimension expressions *)
342
let rec dimension_of_expr expr =
343
  match expr.expr_desc with
344
  | Expr_const c  -> dimension_of_const expr.expr_loc c
345
  | Expr_ident id -> mkdim_ident expr.expr_loc id
346
  | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
347
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
348
      if k = None then raise InvalidDimension;
349
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
350
  | Expr_ite (i, t, e)        ->
351
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
352
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
353

    
354

    
355
let sort_handlers hl =
356
 List.sort (fun (t, _) (t', _) -> compare t t') hl
357

    
358
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
359
  | Expr_const c1, Expr_const c2 -> c1 = c2
360
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
361
  | Expr_array el1, Expr_array el2 
362
  | Expr_tuple el1, Expr_tuple el2 -> 
363
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
364
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
365
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
366
  | 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
367
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
368
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
369
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
370
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
371
  | 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')
372
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
373
  | Expr_power (e1, i1), Expr_power (e2, i2)
374
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
375
  | _ -> false
376

    
377
let get_node_vars nd =
378
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
379

    
380
let get_var id var_list =
381
 List.find (fun v -> v.var_id = id) var_list
382

    
383
let get_node_var id node = get_var id (get_node_vars node)
384

    
385
let get_node_eq id node =
386
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
387

    
388
let get_nodes prog = 
389
  List.fold_left (
390
    fun nodes decl ->
391
      match decl.top_decl_desc with
392
	| Node nd -> nd::nodes
393
	| Consts _ | ImportedNode _ | Open _ -> nodes  
394
  ) [] prog
395

    
396
let get_consts prog = 
397
  List.fold_left (
398
    fun consts decl ->
399
      match decl.top_decl_desc with
400
	| Consts clist -> clist@consts
401
	| Node _ | ImportedNode _ | Open _ -> consts  
402
  ) [] prog
403

    
404

    
405

    
406
(************************************************************************)
407
(*        Renaming                                                      *)
408

    
409
(* applies the renaming function [fvar] to all variables of expression [expr] *)
410
 let rec expr_replace_var fvar expr =
411
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
412

    
413
 and expr_desc_replace_var fvar expr_desc =
414
   match expr_desc with
415
   | Expr_const _ -> expr_desc
416
   | Expr_ident i -> Expr_ident (fvar i)
417
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
418
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
419
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
420
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
421
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
422
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
423
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
424
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
425
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
426
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
427
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
428

    
429
(* Applies the renaming function [fvar] to every rhs
430
   only when the corresponding lhs satisfies predicate [pvar] *)
431
 let eq_replace_rhs_var pvar fvar eq =
432
   let pvar l = List.exists pvar l in
433
   let rec replace lhs rhs =
434
     { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
435
   and replace_desc lhs rhs_desc =
436
     match lhs with
437
     | []  -> assert false
438
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
439
     | _   ->
440
       (match rhs_desc with
441
       | Expr_tuple tl ->
442
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
443
       | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
444
	 let args = expr_list_of_expr arg in
445
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
446
       | Expr_array _
447
       | Expr_access _
448
       | Expr_power _
449
       | Expr_const _
450
       | Expr_ident _
451
       | Expr_appl _   ->
452
	 if pvar lhs
453
	 then expr_desc_replace_var fvar rhs_desc
454
	 else rhs_desc
455
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
456
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
457
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
458
       | Expr_pre e'          -> Expr_pre (replace lhs e')
459
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
460
				 in Expr_when (replace lhs e', i', l)
461
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
462
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
463
       )
464
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
465

    
466

    
467
 let rec rename_expr  f_node f_var f_const expr =
468
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
469
 and rename_expr_desc f_node f_var f_const expr_desc =
470
   let re = rename_expr  f_node f_var f_const in
471
   match expr_desc with
472
   | Expr_const _ -> expr_desc
473
   | Expr_ident i -> Expr_ident (f_var i)
474
   | Expr_array el -> Expr_array (List.map re el)
475
   | Expr_access (e1, d) -> Expr_access (re e1, d)
476
   | Expr_power (e1, d) -> Expr_power (re e1, d)
477
   | Expr_tuple el -> Expr_tuple (List.map re el)
478
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
479
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
480
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
481
   | Expr_pre e' -> Expr_pre (re e')
482
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
483
   | Expr_merge (i, hl) -> 
484
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
485
   | Expr_appl (i, e', i') -> 
486
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
487
  
488
 let rename_node_annot f_node f_var f_const expr  =
489
   expr
490
 (* TODO assert false *)
491

    
492
 let rename_expr_annot f_node f_var f_const annot =
493
   annot
494
 (* TODO assert false *)
495

    
496
let rename_node f_node f_var f_const nd =
497
  let rename_var v = { v with var_id = f_var v.var_id } in
498
  let rename_eq eq = { eq with
499
      eq_lhs = List.map f_var eq.eq_lhs; 
500
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
501
    } 
502
  in
503
  let inputs = List.map rename_var nd.node_inputs in
504
  let outputs = List.map rename_var nd.node_outputs in
505
  let locals = List.map rename_var nd.node_locals in
506
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
507
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
508
  let node_asserts = List.map 
509
    (fun a -> 
510
      {a with assert_expr = 
511
	  let expr = a.assert_expr in
512
	  rename_expr f_node f_var f_const expr})
513
    nd.node_asserts
514
  in
515
  let eqs = List.map rename_eq nd.node_eqs in
516
  let spec = 
517
    Utils.option_map 
518
      (fun s -> rename_node_annot f_node f_var f_const s) 
519
      nd.node_spec 
520
  in
521
  let annot =
522
    List.map 
523
      (fun s -> rename_expr_annot f_node f_var f_const s) 
524
      nd.node_annot
525
  in
526
  {
527
    node_id = f_node nd.node_id;
528
    node_type = nd.node_type;
529
    node_clock = nd.node_clock;
530
    node_inputs = inputs;
531
    node_outputs = outputs;
532
    node_locals = locals;
533
    node_gencalls = gen_calls;
534
    node_checks = node_checks;
535
    node_asserts = node_asserts;
536
    node_eqs = eqs;
537
    node_dec_stateless = nd.node_dec_stateless;
538
    node_stateless = nd.node_stateless;
539
    node_spec = spec;
540
    node_annot = annot;
541
  }
542

    
543

    
544
let rename_const f_const c =
545
  { c with const_id = f_const c.const_id }
546
    
547
let rename_prog f_node f_var f_const prog =
548
  List.rev (
549
    List.fold_left (fun accu top ->
550
      (match top.top_decl_desc with
551
      | Node nd -> 
552
	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
553
      | Consts c -> 
554
	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
555
      | ImportedNode _
556
      | Open _ -> top)
557
      ::accu
558
) [] prog
559
  )
560

    
561
(**********************************************************************)
562
(* Pretty printers *)
563

    
564
let pp_decl_type fmt tdecl =
565
  match tdecl.top_decl_desc with
566
  | Node nd ->
567
    fprintf fmt "%s: " nd.node_id;
568
    Utils.reset_names ();
569
    fprintf fmt "%a@ " Types.print_ty nd.node_type
570
  | ImportedNode ind ->
571
    fprintf fmt "%s: " ind.nodei_id;
572
    Utils.reset_names ();
573
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
574
  | Consts _ | Open _ -> ()
575

    
576
let pp_prog_type fmt tdecl_list =
577
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
578

    
579
let pp_decl_clock fmt cdecl =
580
  match cdecl.top_decl_desc with
581
  | Node nd ->
582
    fprintf fmt "%s: " nd.node_id;
583
    Utils.reset_names ();
584
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
585
  | ImportedNode ind ->
586
    fprintf fmt "%s: " ind.nodei_id;
587
    Utils.reset_names ();
588
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
589
  | Consts _ | Open _ -> ()
590

    
591
let pp_prog_clock fmt prog =
592
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
593

    
594
let pp_error fmt = function
595
    Main_not_found ->
596
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
597
	!Options.main_node
598
  | Main_wrong_kind ->
599
    fprintf fmt
600
      "Name %s does not correspond to a (non-imported) node definition.@." 
601
      !Options.main_node
602
  | No_main_specified ->
603
    fprintf fmt "No main node specified@."
604
  | Unbound_symbol sym ->
605
    fprintf fmt
606
      "%s is undefined.@."
607
      sym
608
  | Already_bound_symbol sym -> 
609
    fprintf fmt
610
      "%s is already defined.@."
611
      sym
612

    
613
(* filling node table with internal functions *)
614
let vdecls_of_typ_ck cpt ty =
615
  let loc = Location.dummy_loc in
616
  List.map
617
    (fun _ -> incr cpt;
618
              let name = sprintf "_var_%d" !cpt in
619
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
620
    (Types.type_list_of_type ty)
621

    
622
let mk_internal_node id =
623
  let spec = None in
624
  let ty = Env.lookup_value Basic_library.type_env id in
625
  let ck = Env.lookup_value Basic_library.clock_env id in
626
  let (tin, tout) = Types.split_arrow ty in
627
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
628
  let cpt = ref (-1) in
629
  mktop_decl Location.dummy_loc
630
    (ImportedNode
631
       {nodei_id = id;
632
	nodei_type = ty;
633
	nodei_clock = ck;
634
	nodei_inputs = vdecls_of_typ_ck cpt tin;
635
	nodei_outputs = vdecls_of_typ_ck cpt tout;
636
	nodei_stateless = Types.get_static_value ty <> None;
637
	nodei_spec = spec;
638
	nodei_prototype = None;
639
       	nodei_in_lib = None;
640
       })
641

    
642
let add_internal_funs () =
643
  List.iter
644
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
645
    Basic_library.internal_funs
646

    
647

    
648

    
649
(* Replace any occurence of a var in vars_to_replace by its associated
650
   expression in defs until e does not contain any such variables *)
651
let rec substitute_expr vars_to_replace defs e =
652
  let se = substitute_expr vars_to_replace defs in
653
  { e with expr_desc = 
654
      let ed = e.expr_desc in
655
      match ed with
656
      | Expr_const _ -> ed
657
      | Expr_array el -> Expr_array (List.map se el)
658
      | Expr_access (e1, d) -> Expr_access (se e1, d)
659
      | Expr_power (e1, d) -> Expr_power (se e1, d)
660
      | Expr_tuple el -> Expr_tuple (List.map se el)
661
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
662
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
663
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
664
      | Expr_pre e' -> Expr_pre (se e')
665
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
666
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
667
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
668
      | Expr_ident i -> 
669
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
670
	  let eq_i eq = eq.eq_lhs = [i] in
671
	  if List.exists eq_i defs then
672
	    let sub = List.find eq_i defs in
673
	    let sub' = se sub.eq_rhs in
674
	    sub'.expr_desc
675
	  else 
676
	    assert false
677
	)
678
	else
679
	  ed
680

    
681
  }
682
(* FAUT IL RETIRER ?
683
  
684
 let rec expr_to_eexpr  expr =
685
   { eexpr_tag = expr.expr_tag;
686
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
687
     eexpr_type = expr.expr_type;
688
     eexpr_clock = expr.expr_clock;
689
     eexpr_loc = expr.expr_loc
690
   }
691
 and expr_desc_to_eexpr_desc expr_desc =
692
   let conv = expr_to_eexpr in
693
   match expr_desc with
694
   | Expr_const c -> EExpr_const (match c with
695
     | Const_int x -> EConst_int x 
696
     | Const_real x -> EConst_real x 
697
     | Const_float x -> EConst_float x 
698
     | Const_tag x -> EConst_tag x 
699
     | _ -> assert false
700

    
701
   )
702
   | Expr_ident i -> EExpr_ident i
703
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
704

    
705
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
706
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
707
   | Expr_pre e' -> EExpr_pre (conv e')
708
   | Expr_appl (i, e', i') -> 
709
     EExpr_appl 
710
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
711

    
712
   | Expr_when _
713
   | Expr_merge _ -> assert false
714
   | Expr_array _ 
715
   | Expr_access _ 
716
   | Expr_power _  -> assert false
717
   | Expr_ite (c, t, e) -> assert false 
718
   | _ -> assert false
719

    
720
     *)
721
let rec get_expr_calls nodes e =
722
  get_calls_expr_desc nodes e.expr_desc
723
and get_calls_expr_desc nodes expr_desc =
724
  let get_calls = get_expr_calls nodes in
725
  match expr_desc with
726
  | Expr_const _ 
727
   | Expr_ident _ -> Utils.ISet.empty
728
   | Expr_tuple el
729
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
730
   | Expr_pre e1 
731
   | Expr_when (e1, _, _) 
732
   | Expr_access (e1, _) 
733
   | Expr_power (e1, _) -> get_calls e1
734
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
735
   | Expr_arrow (e1, e2) 
736
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
737
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
738
   | Expr_appl (i, e', i') -> 
739
     if Basic_library.is_internal_fun i then 
740
       (get_calls e') 
741
     else
742
       let calls =  Utils.ISet.add i (get_calls e') in
743
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
744
       if List.exists test nodes then
745
	 match (List.find test nodes).top_decl_desc with
746
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
747
	 | _ -> assert false
748
       else 
749
	 calls
750

    
751
and get_eq_calls nodes eq =
752
  get_expr_calls nodes eq.eq_rhs
753
and get_node_calls nodes node =
754
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
755

    
756

    
757
let rec expr_has_arrows e =
758
  expr_desc_has_arrows e.expr_desc
759
and expr_desc_has_arrows expr_desc =
760
  match expr_desc with
761
  | Expr_const _ 
762
  | Expr_ident _ -> false
763
  | Expr_tuple el
764
  | Expr_array el -> List.exists expr_has_arrows el
765
  | Expr_pre e1 
766
  | Expr_when (e1, _, _) 
767
  | Expr_access (e1, _) 
768
  | Expr_power (e1, _) -> expr_has_arrows e1
769
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
770
  | Expr_arrow (e1, e2) 
771
  | Expr_fby (e1, e2) -> true
772
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
773
  | Expr_appl (i, e', i') -> expr_has_arrows e'
774

    
775
and eq_has_arrows eq =
776
  expr_has_arrows eq.eq_rhs
777
and node_has_arrows node =
778
  List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
779

    
780
(* Local Variables: *)
781
(* compile-command:"make -C .." *)
782
(* End: *)
(10-10/49)