Project

General

Profile

Download (48.1 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Format
13
open Lustre_types
14
open Machine_code_types
15
(*open Dimension*)
16

    
17

    
18
module VDeclModule =
19
struct (* Node module *)
20
  type t = var_decl
21
  let compare v1 v2 = compare v1.var_id v2.var_id
22
end
23

    
24
module VMap = Map.Make(VDeclModule)
25

    
26
module VSet: sig
27
  include Set.S
28
  val pp: Format.formatter -> t -> unit
29
  val get: ident -> t -> elt
30
end with type elt = var_decl =
31
  struct
32
    include Set.Make(VDeclModule)
33
    let pp fmt s =
34
      Format.fprintf fmt "{@[%a}@]" (Utils.fprintf_list ~sep:",@ " Printers.pp_var) (elements s)
35
    (* Strangley the find_first function of Set.Make is incorrect (at
36
       the current time of writting this comment. Had to switch to
37
       lists *)
38
    let get id s = List.find (fun v -> v.var_id = id) (elements s)
39
  end
40
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
41

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

    
44

    
45

    
46
(************************************************************)
47
(* *)
48

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

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

    
55
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) =
56
  assert (value = None || is_const);
57
  { var_id = id;
58
    var_orig = orig;
59
    var_dec_type = ty_dec;
60
    var_dec_clock = ck_dec;
61
    var_dec_const = is_const;
62
    var_dec_value = value;
63
    var_parent_nodeid = parentid;
64
    var_type = Types.new_var ();
65
    var_clock = Clocks.new_var true;
66
    var_loc = loc }
67

    
68
let dummy_var_decl name typ =
69
  {
70
    var_id = name;
71
    var_orig = false;
72
    var_dec_type = dummy_type_dec;
73
    var_dec_clock = dummy_clock_dec;
74
    var_dec_const = false;
75
    var_dec_value = None;
76
    var_parent_nodeid = None;
77
    var_type =  typ;
78
    var_clock = Clocks.new_ck Clocks.Cvar true;
79
    var_loc = Location.dummy_loc
80
  }
81

    
82
let mkexpr loc d =
83
  { expr_tag = Utils.new_tag ();
84
    expr_desc = d;
85
    expr_type = Types.new_var ();
86
    expr_clock = Clocks.new_var true;
87
    expr_delay = Delay.new_var ();
88
    expr_annot = None;
89
    expr_loc = loc }
90

    
91
let var_decl_of_const ?(parentid=None) c =
92
  { var_id = c.const_id;
93
    var_orig = true;
94
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
95
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
96
    var_dec_const = true;
97
    var_dec_value = None;
98
    var_parent_nodeid = parentid;
99
    var_type = c.const_type;
100
    var_clock = Clocks.new_var false;
101
    var_loc = c.const_loc }
102

    
103
let mk_new_name used id =
104
  let rec new_name name cpt =
105
    if used name
106
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
107
    else name
108
  in new_name id 1
109

    
110
let mkeq loc (lhs, rhs) =
111
  { eq_lhs = lhs;
112
    eq_rhs = rhs;
113
    eq_loc = loc }
114

    
115
let mkassert loc expr =
116
  { assert_loc = loc;
117
    assert_expr = expr
118
  }
119

    
120
let mktop_decl loc own itf d =
121
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
122

    
123
let mkpredef_call loc funname args =
124
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
125

    
126
let is_clock_dec_type cty =
127
  match cty with
128
  | Tydec_clock _ -> true
129
  | _             -> false
130

    
131
let const_of_top top_decl =
132
  match top_decl.top_decl_desc with
133
  | Const c -> c
134
  | _ -> assert false
135

    
136
let node_of_top top_decl =
137
  match top_decl.top_decl_desc with
138
  | Node nd -> nd
139
  | _ -> raise Not_found
140

    
141
let imported_node_of_top top_decl =
142
  match top_decl.top_decl_desc with
143
  | ImportedNode ind -> ind
144
  | _ -> assert false
145

    
146
let typedef_of_top top_decl =
147
  match top_decl.top_decl_desc with
148
  | TypeDef tdef -> tdef
149
  | _ -> assert false
150

    
151
let dependency_of_top top_decl =
152
  match top_decl.top_decl_desc with
153
  | Open (local, dep) -> (local, dep)
154
  | _ -> assert false
155

    
156
let consts_of_enum_type top_decl =
157
  match top_decl.top_decl_desc with
158
  | TypeDef tdef ->
159
    (match tdef.tydef_desc with
160
    | Tydec_enum tags ->
161
       List.map
162
	 (fun tag ->
163
	   let cdecl = {
164
	     const_id = tag;
165
	     const_loc = top_decl.top_decl_loc;
166
	     const_value = Const_tag tag;
167
	     const_type = Type_predef.type_const tdef.tydef_id
168
	   } in
169
	   { top_decl with top_decl_desc = Const cdecl })
170
	 tags
171
     | _               -> [])
172
  | _ -> assert false
173

    
174
(************************************************************)
175
(*   Eexpr functions *)
176
(************************************************************)
177

    
178

    
179
let empty_contract =
180
  {
181
    consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
182
  }
183

    
184
(* For const declaration we do as for regular lustre node.
185
But for local flows we registered the variable and the lustre flow definition *)
186
let mk_contract_var id is_const type_opt expr loc =
187
  let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
188
  if is_const then
189
  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
190
  { empty_contract with consts = [v]; spec_loc = loc; }
191
  else
192
    let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
193
    let eq = mkeq loc ([id], expr) in 
194
    { empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
195

    
196
let eexpr_add_name eexpr eexpr_name =
197
  { eexpr with eexpr_name }
198

    
199
let mk_contract_guarantees name eexpr =
200
  { empty_contract with guarantees = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
201

    
202
let mk_contract_assume name eexpr =
203
  { empty_contract with assume = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
204

    
205
let mk_contract_mode id rl el loc =
206
  { empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc }
207

    
208
let mk_contract_import id ins outs loc =
209
  { empty_contract with imports = [{import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc; }]; spec_loc = loc }
210

    
211
    
212
let merge_contracts ann1 ann2 = (* keeping the first item loc *)
213
  { consts = ann1.consts @ ann2.consts;
214
    locals = ann1.locals @ ann2.locals;
215
    stmts = ann1.stmts @ ann2.stmts;
216
    assume = ann1.assume @ ann2.assume;
217
    guarantees = ann1.guarantees @ ann2.guarantees;
218
    modes = ann1.modes @ ann2.modes;
219
    imports = ann1.imports @ ann2.imports;
220
    spec_loc = ann1.spec_loc
221
  }
222

    
223
let mkeexpr loc expr =
224
  { eexpr_tag = Utils.new_tag ();
225
    eexpr_qfexpr = expr;
226
    eexpr_quantifiers = [];
227
    eexpr_name = None;
228
    eexpr_type = Types.new_var ();
229
    eexpr_clock = Clocks.new_var true;
230
    eexpr_loc = loc }
231

    
232
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
233

    
234
(*
235
let mkepredef_call loc funname args =
236
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
237

    
238
let mkepredef_unary_call loc funname arg =
239
  mkeexpr loc (EExpr_appl (funname, arg, None))
240
*)
241

    
242
let merge_expr_annot ann1 ann2 =
243
  match ann1, ann2 with
244
    | None, None -> assert false
245
    | Some _, None -> ann1
246
    | None, Some _ -> ann2
247
    | Some ann1, Some ann2 -> Some {
248
      annots = ann1.annots @ ann2.annots;
249
      annot_loc = ann1.annot_loc
250
    }
251

    
252
let update_expr_annot node_id e annot =
253
  List.iter (fun (key, _) -> 
254
    Annotations.add_expr_ann node_id e.expr_tag key
255
  ) annot.annots;
256
  e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
257
  e
258

    
259

    
260
let mkinstr ?lustre_eq ?(instr_spec=[]) instr_desc = {
261
  instr_desc;
262
  (* lustre_expr = lustre_expr; *)
263
  instr_spec;
264
  lustre_eq;
265
}
266

    
267
let get_instr_desc i = i.instr_desc
268
let update_instr_desc i id = { i with instr_desc = id }
269

    
270
(***********************************************************)
271
(* Fast access to nodes, by name *)
272
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
273
let consts_table = Hashtbl.create 30
274

    
275
let print_node_table fmt () =
276
  begin
277
    Format.fprintf fmt "{ /* node table */@.";
278
    Hashtbl.iter (fun id nd ->
279
      Format.fprintf fmt "%s |-> %a"
280
	id
281
	Printers.pp_short_decl nd
282
    ) node_table;
283
    Format.fprintf fmt "}@."
284
  end
285

    
286
let print_consts_table fmt () =
287
  begin
288
    Format.fprintf fmt "{ /* consts table */@.";
289
    Hashtbl.iter (fun id const ->
290
      Format.fprintf fmt "%s |-> %a"
291
	id
292
	Printers.pp_const_decl (const_of_top const)
293
    ) consts_table;
294
    Format.fprintf fmt "}@."
295
  end
296

    
297
let node_name td =
298
    match td.top_decl_desc with 
299
    | Node nd         -> nd.node_id
300
    | ImportedNode nd -> nd.nodei_id
301
    | _ -> assert false
302

    
303
let is_generic_node td =
304
  match td.top_decl_desc with 
305
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
306
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
307
  | _ -> assert false
308

    
309
let node_inputs td =
310
  match td.top_decl_desc with 
311
  | Node nd         -> nd.node_inputs
312
  | ImportedNode nd -> nd.nodei_inputs
313
  | _ -> assert false
314

    
315
let node_from_name id =
316
      Hashtbl.find node_table id
317
      
318
let update_node id top =
319
  Hashtbl.replace node_table id top
320

    
321
let is_imported_node td =
322
  match td.top_decl_desc with 
323
  | Node _         -> false
324
  | ImportedNode _ -> true
325
  | _ -> assert false
326

    
327
let is_node_contract nd =
328
  match nd.node_spec with
329
  | Some (Contract _) -> true
330
  | _ -> false
331
  
332
let get_node_contract nd =
333
  match nd.node_spec with
334
  | Some (Contract c) -> c
335
  | _ -> assert false
336
  
337
let is_contract td =
338
  match td.top_decl_desc with 
339
  | Node nd -> is_node_contract nd
340
  | _ -> false
341

    
342
(* alias and type definition table *)
343

    
344
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
345

    
346
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
347
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
348
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
349
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
350

    
351
let type_table =
352
  Utils.create_hashtable 20 [
353
    Tydec_int  , top_int_type;
354
    Tydec_bool , top_bool_type;
355
    (* Tydec_float, top_float_type; *)
356
    Tydec_real , top_real_type
357
  ]
358

    
359
let print_type_table fmt () =
360
  begin
361
    Format.fprintf fmt "{ /* type table */@.";
362
    Hashtbl.iter (fun tydec tdef ->
363
      Format.fprintf fmt "%a |-> %a"
364
	Printers.pp_var_type_dec_desc tydec
365
	Printers.pp_typedef (typedef_of_top tdef)
366
    ) type_table;
367
    Format.fprintf fmt "}@."
368
  end
369

    
370
let rec is_user_type typ =
371
  match typ with
372
  | Tydec_int | Tydec_bool | Tydec_real 
373
  (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
374
  | Tydec_clock typ' -> is_user_type typ'
375
  | _ -> true
376

    
377
let get_repr_type typ =
378
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
379
  if is_user_type typ_def then typ else typ_def
380

    
381
let rec coretype_equal ty1 ty2 =
382
  let res =
383
  match ty1, ty2 with
384
  | Tydec_any           , _
385
  | _                   , Tydec_any             -> assert false
386
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
387
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
388
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
389
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
390
  | Tydec_int           , Tydec_int
391
  | Tydec_real          , Tydec_real
392
  (* | Tydec_float         , Tydec_float *)
393
  | Tydec_bool          , Tydec_bool            -> true
394
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
395
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
396
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
397
  | Tydec_struct fl1    , Tydec_struct fl2      ->
398
       List.length fl1 = List.length fl2
399
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
400
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
401
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
402
  | _                                  -> false
403
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
404

    
405
let tag_default = "default"
406

    
407
let const_is_bool c =
408
 match c with
409
 | Const_tag t -> t = tag_true || t = tag_false
410
 | _           -> false
411

    
412
(* Computes the negation of a boolean constant *)
413
let const_negation c =
414
  assert (const_is_bool c);
415
  match c with
416
  | Const_tag t when t = tag_true  -> Const_tag tag_false
417
  | _                              -> Const_tag tag_true
418

    
419
let const_or c1 c2 =
420
  assert (const_is_bool c1 && const_is_bool c2);
421
  match c1, c2 with
422
  | Const_tag t1, _            when t1 = tag_true -> c1
423
  | _           , Const_tag t2 when t2 = tag_true -> c2
424
  | _                                             -> Const_tag tag_false
425

    
426
let const_and c1 c2 =
427
  assert (const_is_bool c1 && const_is_bool c2);
428
  match c1, c2 with
429
  | Const_tag t1, _            when t1 = tag_false -> c1
430
  | _           , Const_tag t2 when t2 = tag_false -> c2
431
  | _                                              -> Const_tag tag_true
432

    
433
let const_xor c1 c2 =
434
  assert (const_is_bool c1 && const_is_bool c2);
435
   match c1, c2 with
436
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
437
  | _                                         -> Const_tag tag_false
438

    
439
let const_impl c1 c2 =
440
  assert (const_is_bool c1 && const_is_bool c2);
441
  match c1, c2 with
442
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
443
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
444
  | _                                             -> Const_tag tag_false
445

    
446
(* To guarantee uniqueness of tags in enum types *)
447
let tag_table =
448
  Utils.create_hashtable 20 [
449
   tag_true, top_bool_type;
450
   tag_false, top_bool_type
451
  ]
452

    
453
(* To guarantee uniqueness of fields in struct types *)
454
let field_table =
455
  Utils.create_hashtable 20 [
456
  ]
457

    
458
let get_enum_type_tags cty =
459
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
460
 match cty with
461
 | Tydec_bool    -> [tag_true; tag_false]
462
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
463
                     | Tydec_enum tl -> tl
464
                     | _             -> assert false)
465
 | _            -> assert false
466

    
467
let get_struct_type_fields cty =
468
 match cty with
469
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
470
                     | Tydec_struct fl -> fl
471
                     | _               -> assert false)
472
 | _            -> assert false
473

    
474
let const_of_bool b =
475
 Const_tag (if b then tag_true else tag_false)
476

    
477
(* let get_const c = snd (Hashtbl.find consts_table c) *)
478

    
479
let ident_of_expr expr =
480
 match expr.expr_desc with
481
 | Expr_ident id -> id
482
 | _             -> assert false
483

    
484
(* Generate a new ident expression from a declared variable *)
485
let expr_of_vdecl v =
486
  { expr_tag = Utils.new_tag ();
487
    expr_desc = Expr_ident v.var_id;
488
    expr_type = v.var_type;
489
    expr_clock = v.var_clock;
490
    expr_delay = Delay.new_var ();
491
    expr_annot = None;
492
    expr_loc = v.var_loc }
493

    
494
(* Caution, returns an untyped and unclocked expression *)
495
let expr_of_ident id loc =
496
  {expr_tag = Utils.new_tag ();
497
   expr_desc = Expr_ident id;
498
   expr_type = Types.new_var ();
499
   expr_clock = Clocks.new_var true;
500
   expr_delay = Delay.new_var ();
501
   expr_loc = loc;
502
   expr_annot = None}
503

    
504
let is_tuple_expr expr =
505
 match expr.expr_desc with
506
  | Expr_tuple _ -> true
507
  | _            -> false
508

    
509
let expr_list_of_expr expr =
510
  match expr.expr_desc with
511
  | Expr_tuple elist -> elist
512
  | _                -> [expr]
513

    
514
let expr_of_expr_list loc elist =
515
 match elist with
516
 | [t]  -> { t with expr_loc = loc }
517
 | t::_ ->
518
    let tlist = List.map (fun e -> e.expr_type) elist in
519
    let clist = List.map (fun e -> e.expr_clock) elist in
520
    { t with expr_desc = Expr_tuple elist;
521
	     expr_type = Type_predef.type_tuple tlist;
522
	     expr_clock = Clock_predef.ck_tuple clist;
523
	     expr_tag = Utils.new_tag ();
524
	     expr_loc = loc }
525
 | _    -> assert false
526

    
527
let call_of_expr expr =
528
 match expr.expr_desc with
529
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
530
 | _                      -> assert false
531

    
532
    
533
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
534
let rec expr_of_dimension dim =
535
  let open Dimension in
536
  let expr =
537
  match dim.dim_desc with
538
 | Dbool b        ->
539
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
540
 | Dint i         ->
541
     mkexpr dim.dim_loc (Expr_const (Const_int i))
542
 | Dident id      ->
543
     mkexpr dim.dim_loc (Expr_ident id)
544
 | Dite (c, t, e) ->
545
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
546
 | Dappl (id, args) ->
547
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
548
 | Dlink dim'       -> expr_of_dimension dim'
549
 | Dvar
550
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
551
			assert false)
552
  in
553
  { expr
554
  with
555
    expr_type = Types.new_ty Types.type_int;
556
  }
557
  
558
let dimension_of_const loc const =
559
  let open Dimension in
560
 match const with
561
 | Const_int i                                    -> mkdim_int loc i
562
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
563
 | _                                              -> raise InvalidDimension
564

    
565
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
566
   into dimension expressions *)
567
let rec dimension_of_expr expr =
568
  let open Dimension in
569
  match expr.expr_desc with
570
  | Expr_const c  -> dimension_of_const expr.expr_loc c
571
  | Expr_ident id -> mkdim_ident expr.expr_loc id
572
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
573
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
574
      if k = None then raise InvalidDimension;
575
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
576
  | Expr_ite (i, t, e)        ->
577
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
578
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
579

    
580

    
581
let sort_handlers hl =
582
 List.sort (fun (t, _) (t', _) -> compare t t') hl
583

    
584
  
585
let rec is_eq_const c1 c2 =
586
  match c1, c2 with
587
  | Const_real r1, Const_real _
588
    -> Real.eq r1 r1 
589
  | Const_struct lcl1, Const_struct lcl2
590
    -> List.length lcl1 = List.length lcl2
591
    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
592
  | _  -> c1 = c2
593

    
594
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
595
  | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2
596
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
597
  | Expr_array el1, Expr_array el2 
598
  | Expr_tuple el1, Expr_tuple el2 -> 
599
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
600
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
601
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
602
  | 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
603
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
604
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
605
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
606
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
607
  | 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')
608
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
609
  | Expr_power (e1, i1), Expr_power (e2, i2)
610
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
611
  | _ -> false
612

    
613
let get_node_vars nd =
614
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
615

    
616
let mk_new_node_name nd id =
617
  let used_vars = get_node_vars nd in
618
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
619
  mk_new_name used id
620

    
621
let get_var id var_list =
622
  List.find (fun v -> v.var_id = id) var_list
623

    
624
let get_node_var id node =
625
  try
626
    get_var id (get_node_vars node)
627
  with Not_found -> begin
628
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
629
    raise Not_found
630
  end
631

    
632

    
633
let get_node_eqs =
634
  let get_eqs stmts =
635
    List.fold_right
636
      (fun stmt (res_eq, res_aut) ->
637
	match stmt with
638
	| Eq eq -> eq :: res_eq, res_aut
639
	| Aut aut -> res_eq, aut::res_aut)
640
      stmts
641
      ([], []) in
642
  let table_eqs = Hashtbl.create 23 in
643
  (fun nd ->
644
    try
645
      let (old, res) = Hashtbl.find table_eqs nd.node_id
646
      in if old == nd.node_stmts then res else raise Not_found
647
    with Not_found -> 
648
      let res = get_eqs nd.node_stmts in
649
      begin
650
	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
651
	res
652
      end)
653

    
654
let get_node_eq id node =
655
  let eqs, _ = get_node_eqs node in
656
  try
657
    List.find (fun eq -> List.mem id eq.eq_lhs) eqs
658
  with
659
    Not_found -> (* Shall be defined in automata auts *) raise Not_found
660
      
661
let get_nodes prog = 
662
  List.fold_left (
663
    fun nodes decl ->
664
      match decl.top_decl_desc with
665
      | Node _ -> decl::nodes
666
      | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes
667
  ) [] prog
668
  |> List.rev
669

    
670
let get_imported_nodes prog = 
671
  List.fold_left (
672
    fun nodes decl ->
673
      match decl.top_decl_desc with
674
	| ImportedNode _ -> decl::nodes
675
	| Const _ | Node _ | Include _ | Open _ | TypeDef _-> nodes  
676
  ) [] prog
677

    
678
let get_consts prog = 
679
  List.fold_right (
680
    fun decl consts ->
681
      match decl.top_decl_desc with
682
	| Const _ -> decl::consts
683
	| Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> consts  
684
  ) prog []
685

    
686
let get_typedefs prog = 
687
  List.fold_right (
688
    fun decl types ->
689
      match decl.top_decl_desc with
690
	| TypeDef _ -> decl::types
691
	| Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> types  
692
  ) prog []
693

    
694
let get_dependencies prog =
695
  List.fold_right (
696
    fun decl deps ->
697
      match decl.top_decl_desc with
698
	| Open _ -> decl::deps
699
	| Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> deps  
700
  ) prog []
701

    
702
let get_node_interface nd =
703
 {nodei_id = nd.node_id;
704
  nodei_type = nd.node_type;
705
  nodei_clock = nd.node_clock;
706
  nodei_inputs = nd.node_inputs;
707
  nodei_outputs = nd.node_outputs;
708
  nodei_stateless = nd.node_dec_stateless;
709
  nodei_spec = nd.node_spec;
710
  (* nodei_annot = nd.node_annot; *)
711
  nodei_prototype = None;
712
  nodei_in_lib = [];
713
 }
714

    
715
(************************************************************************)
716
(*        Renaming / Copying                                                      *)
717

    
718
let copy_var_decl vdecl =
719
  mkvar_decl
720
    vdecl.var_loc
721
    ~orig:vdecl.var_orig
722
    (
723
      vdecl.var_id,
724
      vdecl.var_dec_type,
725
      vdecl.var_dec_clock,
726
      vdecl.var_dec_const,
727
      vdecl.var_dec_value,
728
      vdecl.var_parent_nodeid
729
    )
730

    
731
let copy_const cdecl =
732
  { cdecl with const_type = Types.new_var () }
733

    
734
let copy_node nd =
735
  { nd with
736
    node_type     = Types.new_var ();
737
    node_clock    = Clocks.new_var true;
738
    node_inputs   = List.map copy_var_decl nd.node_inputs;
739
    node_outputs  = List.map copy_var_decl nd.node_outputs;
740
    node_locals   = List.map copy_var_decl nd.node_locals;
741
    node_gencalls = [];
742
    node_checks   = [];
743
    node_stateless = None;
744
  }
745

    
746
let copy_top top =
747
  match top.top_decl_desc with
748
  | Node nd -> { top with top_decl_desc = Node (copy_node nd)  }
749
  | Const c -> { top with top_decl_desc = Const (copy_const c) }
750
  | _       -> top
751

    
752
let copy_prog top_list =
753
  List.map copy_top top_list
754

    
755
  
756
let rec rename_static rename cty =
757
 match cty with
758
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
759
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
760
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
761
 | _                      -> cty
762

    
763
let rename_carrier rename cck =
764
 match cck with
765
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
766
 | _             -> cck
767

    
768
 (*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
769

    
770
(* applies the renaming function [fvar] to all variables of expression [expr] *)
771
 (* let rec expr_replace_var fvar expr = *)
772
 (*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
773

    
774
 (* and expr_desc_replace_var fvar expr_desc = *)
775
 (*   match expr_desc with *)
776
 (*   | Expr_const _ -> expr_desc *)
777
 (*   | Expr_ident i -> Expr_ident (fvar i) *)
778
 (*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
779
 (*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
780
 (*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
781
 (*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
782
 (*   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *)
783
 (*   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)  *)
784
 (*   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
785
 (*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
786
 (*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
787
 (*   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *)
788
 (*   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *)
789

    
790

    
791

    
792
 let rec rename_expr  f_node f_var expr =
793
   { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
794
 and rename_expr_desc f_node f_var expr_desc =
795
   let re = rename_expr  f_node f_var in
796
   match expr_desc with
797
   | Expr_const _ -> expr_desc
798
   | Expr_ident i -> Expr_ident (f_var i)
799
   | Expr_array el -> Expr_array (List.map re el)
800
   | Expr_access (e1, d) -> Expr_access (re e1, d)
801
   | Expr_power (e1, d) -> Expr_power (re e1, d)
802
   | Expr_tuple el -> Expr_tuple (List.map re el)
803
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
804
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
805
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
806
   | Expr_pre e' -> Expr_pre (re e')
807
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
808
   | Expr_merge (i, hl) -> 
809
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
810
   | Expr_appl (i, e', i') -> 
811
     Expr_appl (f_node i, re e', Utils.option_map re i')
812
   
813
 let rename_var f_var v = {
814
     (copy_var_decl v) with
815
     var_id = f_var v.var_id;
816
     var_type = v.var_type;
817
     var_clock = v.var_clock;
818
 } 
819

    
820
 let rename_vars f_var = List.map (rename_var f_var)
821

    
822
 let rec rename_eq f_node f_var eq = { eq with
823
   eq_lhs = List.map f_var eq.eq_lhs; 
824
   eq_rhs = rename_expr f_node f_var eq.eq_rhs
825
 } 
826
 and rename_handler f_node f_var  h = {h with
827
   hand_state = f_var h.hand_state;
828
   hand_unless = List.map (
829
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
830
   ) h.hand_unless;
831
   hand_until = List.map (
832
     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
833
   ) h.hand_until;
834
   hand_locals = rename_vars f_var h.hand_locals;
835
   hand_stmts = rename_stmts f_node f_var h.hand_stmts;
836
   hand_annots = rename_annots f_node f_var h.hand_annots;
837
   
838
 } 
839
 and rename_aut f_node f_var  aut = { aut with
840
   aut_id = f_var aut.aut_id;
841
   aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
842
 }
843
 and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with
844
   | Eq eq -> Eq (rename_eq f_node f_var eq)
845
   | Aut at -> Aut (rename_aut f_node f_var at))
846
   stmts
847
 and rename_annotl f_node f_var  annots = 
848
   List.map 
849
     (fun (key, value) -> key, rename_eexpr f_node f_var value) 
850
     annots
851
 and rename_annot f_node f_var annot =
852
   { annot with annots = rename_annotl f_node f_var annot.annots }
853
 and rename_annots f_node f_var annots =
854
   List.map (rename_annot f_node f_var) annots
855
and rename_eexpr f_node f_var ee =
856
   { ee with
857
     eexpr_tag = Utils.new_tag ();
858
     eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
859
     eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_var vdecls) ee.eexpr_quantifiers;
860
   }
861
and rename_mode f_node f_var m =
862
  let rename_ee = rename_eexpr f_node f_var in
863
  {
864
    m with
865
    require = List.map rename_ee m.require;
866
    ensure = List.map rename_ee m.ensure
867
  }
868
     
869
 let rename_import f_node f_var imp =
870
   let rename_expr = rename_expr f_node f_var in
871
   {
872
     imp with
873
     import_nodeid = f_node imp.import_nodeid;
874
     inputs = rename_expr imp.inputs;
875
     outputs =  rename_expr imp.outputs;
876
   }
877
   
878
 let rename_node f_node f_var nd =
879
   let f_var x = (* checking that this is actually a local variable *)
880
     if List.exists (fun v -> v.var_id = x) (get_node_vars nd) then
881
       f_var x
882
     else
883
       x
884
   in
885
   let rename_var = rename_var f_var in
886
   let rename_vars = List.map rename_var in
887
   let rename_expr = rename_expr f_node f_var in
888
   let rename_eexpr = rename_eexpr f_node f_var in
889
   let rename_stmts = rename_stmts f_node f_var in
890
   let inputs = rename_vars nd.node_inputs in
891
   let outputs = rename_vars nd.node_outputs in
892
   let locals = rename_vars nd.node_locals in
893
   let gen_calls = List.map rename_expr nd.node_gencalls in
894
   let node_checks = List.map (Dimension.rename f_node f_var)  nd.node_checks in
895
   let node_asserts = List.map 
896
     (fun a -> 
897
       {a with assert_expr = 
898
	   let expr = a.assert_expr in
899
	   rename_expr expr})
900
     nd.node_asserts
901
   in
902
   let node_stmts = rename_stmts nd.node_stmts
903

    
904
     
905
   in
906
   let spec = 
907
     Utils.option_map 
908
       (fun s -> match s with
909
                   NodeSpec id -> NodeSpec (f_node id)
910
                 | Contract c -> Contract {
911
                     c with
912
                     consts = rename_vars c.consts;
913
                     locals = rename_vars c.locals;
914
                     stmts = rename_stmts c.stmts;
915
                     assume = List.map rename_eexpr c.assume;
916
                     guarantees = List.map rename_eexpr c.guarantees;
917
                     modes = List.map (rename_mode f_node f_var) c.modes;
918
                     imports = List.map (rename_import f_node f_var) c.imports;
919
                   }
920
       )
921
       nd.node_spec 
922
   in
923
   let annot = rename_annots f_node f_var nd.node_annot in
924
   {
925
     node_id = f_node nd.node_id;
926
     node_type = nd.node_type;
927
     node_clock = nd.node_clock;
928
     node_inputs = inputs;
929
     node_outputs = outputs;
930
     node_locals = locals;
931
     node_gencalls = gen_calls;
932
     node_checks = node_checks;
933
     node_asserts = node_asserts;
934
     node_stmts = node_stmts;
935
     node_dec_stateless = nd.node_dec_stateless;
936
     node_stateless = nd.node_stateless;
937
     node_spec = spec;
938
     node_annot = annot;
939
     node_iscontract = nd.node_iscontract;
940
   }
941

    
942

    
943
let rename_const f_const c =
944
  { c with const_id = f_const c.const_id }
945

    
946
let rename_typedef f_var t =
947
  match t.tydef_desc with
948
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
949
  | _               -> t
950

    
951
let rename_prog f_node f_var f_const prog =
952
  List.rev (
953
    List.fold_left (fun accu top ->
954
      (match top.top_decl_desc with
955
      | Node nd -> 
956
	 { top with top_decl_desc = Node (rename_node f_node f_var nd) }
957
      | Const c -> 
958
	 { top with top_decl_desc = Const (rename_const f_const c) }
959
      | TypeDef tdef ->
960
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
961
      | ImportedNode _
962
        | Include _ | Open _       -> top)
963
      ::accu
964
) [] prog
965
		   )
966

    
967
(* Applies the renaming function [fvar] to every rhs
968
   only when the corresponding lhs satisfies predicate [pvar] *)
969
 let eq_replace_rhs_var pvar fvar eq =
970
   let pvar l = List.exists pvar l in
971
   let rec replace lhs rhs =
972
     { rhs with expr_desc =
973
     match lhs with
974
     | []  -> assert false
975
     | [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc
976
     | _   ->
977
       (match rhs.expr_desc with
978
       | Expr_tuple tl ->
979
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
980
       | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
981
	 let args = expr_list_of_expr arg in
982
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
983
       | Expr_array _
984
       | Expr_access _
985
       | Expr_power _
986
       | Expr_const _
987
       | Expr_ident _
988
       | Expr_appl _   ->
989
	 if pvar lhs
990
	 then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
991
	 else rhs.expr_desc
992
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
993
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
994
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
995
       | Expr_pre e'          -> Expr_pre (replace lhs e')
996
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
997
				 in Expr_when (replace lhs e', i', l)
998
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
999
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
1000
       )
1001
     }
1002
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
1003

    
1004
    
1005
(**********************************************************************)
1006
(* Pretty printers *)
1007

    
1008
let pp_decl_type fmt tdecl =
1009
  match tdecl.top_decl_desc with
1010
  | Node nd ->
1011
    fprintf fmt "%s: " nd.node_id;
1012
    Utils.reset_names ();
1013
    fprintf fmt "%a" Types.print_ty nd.node_type
1014
  | ImportedNode ind ->
1015
    fprintf fmt "%s: " ind.nodei_id;
1016
    Utils.reset_names ();
1017
    fprintf fmt "%a" Types.print_ty ind.nodei_type
1018
  | Const _ | Include _ | Open _ | TypeDef _ -> ()
1019

    
1020
let pp_prog_type fmt tdecl_list =
1021
  Utils.Format.(pp_print_list
1022
                  ~pp_open_box:pp_open_vbox0
1023
                  pp_decl_type fmt tdecl_list)
1024

    
1025
let pp_decl_clock fmt cdecl =
1026
  match cdecl.top_decl_desc with
1027
  | Node nd ->
1028
    fprintf fmt "%s: " nd.node_id;
1029
    Utils.reset_names ();
1030
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
1031
  | ImportedNode ind ->
1032
    fprintf fmt "%s: " ind.nodei_id;
1033
    Utils.reset_names ();
1034
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
1035
  | Const _ | Include _ | Open _ | TypeDef _ -> ()
1036

    
1037
let pp_prog_clock fmt prog =
1038
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
1039

    
1040

    
1041
(* filling node table with internal functions *)
1042
let vdecls_of_typ_ck cpt ty =
1043
  let loc = Location.dummy_loc in
1044
  List.map
1045
    (fun _ -> incr cpt;
1046
              let name = sprintf "_var_%d" !cpt in
1047
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
1048
    (Types.type_list_of_type ty)
1049

    
1050
let mk_internal_node id =
1051
  let spec = None in
1052
  let ty = Env.lookup_value Basic_library.type_env id in
1053
  let ck = Env.lookup_value Basic_library.clock_env id in
1054
  let (tin, tout) = Types.split_arrow ty in
1055
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
1056
  let cpt = ref (-1) in
1057
  mktop
1058
    (ImportedNode
1059
       {nodei_id = id;
1060
	nodei_type = ty;
1061
	nodei_clock = ck;
1062
	nodei_inputs = vdecls_of_typ_ck cpt tin;
1063
	nodei_outputs = vdecls_of_typ_ck cpt tout;
1064
	nodei_stateless = Types.get_static_value ty <> None;
1065
	nodei_spec = spec;
1066
	(* nodei_annot = []; *)
1067
	nodei_prototype = None;
1068
       	nodei_in_lib = [];
1069
       })
1070

    
1071
let add_internal_funs () =
1072
  List.iter
1073
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
1074
    Basic_library.internal_funs
1075

    
1076

    
1077

    
1078
(* Replace any occurence of a var in vars_to_replace by its associated
1079
   expression in defs until e does not contain any such variables *)
1080
let rec substitute_expr vars_to_replace defs e =
1081
  let se = substitute_expr vars_to_replace defs in
1082
  { e with expr_desc = 
1083
      let ed = e.expr_desc in
1084
      match ed with
1085
      | Expr_const _ -> ed
1086
      | Expr_array el -> Expr_array (List.map se el)
1087
      | Expr_access (e1, d) -> Expr_access (se e1, d)
1088
      | Expr_power (e1, d) -> Expr_power (se e1, d)
1089
      | Expr_tuple el -> Expr_tuple (List.map se el)
1090
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
1091
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
1092
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
1093
      | Expr_pre e' -> Expr_pre (se e')
1094
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
1095
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
1096
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
1097
      | Expr_ident i -> 
1098
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
1099
	  let eq_i eq = eq.eq_lhs = [i] in
1100
	  if List.exists eq_i defs then
1101
	    let sub = List.find eq_i defs in
1102
	    let sub' = se sub.eq_rhs in
1103
	    sub'.expr_desc
1104
	  else 
1105
	    assert false
1106
	)
1107
	else
1108
	  ed
1109

    
1110
  }
1111
  
1112
 let expr_to_eexpr  expr =
1113
   { eexpr_tag = expr.expr_tag;
1114
     eexpr_qfexpr = expr;
1115
     eexpr_quantifiers = [];
1116
     eexpr_name = None;
1117
     eexpr_type = expr.expr_type;
1118
     eexpr_clock = expr.expr_clock;
1119
     eexpr_loc = expr.expr_loc;
1120
     (*eexpr_normalized = None*)
1121
   }
1122
 (* and expr_desc_to_eexpr_desc expr_desc = *)
1123
 (*   let conv = expr_to_eexpr in *)
1124
 (*   match expr_desc with *)
1125
 (*   | Expr_const c -> EExpr_const (match c with *)
1126
 (*     | Const_int x -> EConst_int x  *)
1127
 (*     | Const_real x -> EConst_real x  *)
1128
 (*     | Const_float x -> EConst_float x  *)
1129
 (*     | Const_tag x -> EConst_tag x  *)
1130
 (*     | _ -> assert false *)
1131

    
1132
 (*   ) *)
1133
 (*   | Expr_ident i -> EExpr_ident i *)
1134
 (*   | Expr_tuple el -> EExpr_tuple (List.map conv el) *)
1135

    
1136
 (*   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)  *)
1137
 (*   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *)
1138
 (*   | Expr_pre e' -> EExpr_pre (conv e') *)
1139
 (*   | Expr_appl (i, e', i') ->  *)
1140
 (*     EExpr_appl  *)
1141
 (*       (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *)
1142

    
1143
 (*   | Expr_when _ *)
1144
 (*   | Expr_merge _ -> assert false *)
1145
 (*   | Expr_array _  *)
1146
 (*   | Expr_access _  *)
1147
 (*   | Expr_power _  -> assert false *)
1148
 (*   | Expr_ite (c, t, e) -> assert false  *)
1149
 (*   | _ -> assert false *)
1150
      
1151
     
1152
let rec get_expr_calls nodes e =
1153
  let get_calls = get_expr_calls nodes in
1154
  match e.expr_desc with
1155
  | Expr_const _ 
1156
   | Expr_ident _ -> Utils.ISet.empty
1157
   | Expr_tuple el
1158
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
1159
   | Expr_pre e1 
1160
   | Expr_when (e1, _, _) 
1161
   | Expr_access (e1, _) 
1162
   | Expr_power (e1, _) -> get_calls e1
1163
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
1164
   | Expr_arrow (e1, e2) 
1165
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
1166
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
1167
   | Expr_appl (i, e', _) ->
1168
     if Basic_library.is_expr_internal_fun e then 
1169
       (get_calls e') 
1170
     else
1171
       let calls =  Utils.ISet.add i (get_calls e') in
1172
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
1173
       if List.exists test nodes then
1174
	 match (List.find test nodes).top_decl_desc with
1175
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
1176
	 | _ -> assert false
1177
       else 
1178
	 calls
1179

    
1180
and get_eq_calls nodes eq =
1181
  get_expr_calls nodes eq.eq_rhs
1182
and get_aut_handler_calls nodes h =
1183
  List.fold_left (fun accu stmt -> match stmt with
1184
  | Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu
1185
  | Aut aut' ->  Utils.ISet.union (get_aut_calls nodes aut') accu
1186
  ) Utils.ISet.empty h.hand_stmts 
1187
and get_aut_calls nodes aut =
1188
  List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)
1189
    Utils.ISet.empty aut.aut_handlers
1190
and get_node_calls nodes node =
1191
  let eqs, auts = get_node_eqs node in
1192
  let aut_calls =
1193
    List.fold_left
1194
      (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)
1195
      Utils.ISet.empty auts
1196
  in
1197
  List.fold_left
1198
    (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)
1199
    aut_calls eqs
1200

    
1201
let get_expr_vars e =
1202
  let rec get_expr_vars vars e =
1203
    get_expr_desc_vars vars e.expr_desc
1204
  and get_expr_desc_vars vars expr_desc =
1205
    (*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);*)
1206
  match expr_desc with
1207
  | Expr_const _ -> vars
1208
  | Expr_ident x -> Utils.ISet.add x vars
1209
  | Expr_tuple el
1210
  | Expr_array el -> List.fold_left get_expr_vars vars el
1211
  | Expr_pre e1 -> get_expr_vars vars e1
1212
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
1213
  | Expr_access (e1, d) 
1214
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
1215
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
1216
  | Expr_arrow (e1, e2) 
1217
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
1218
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
1219
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
1220
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
1221
  in
1222
  get_expr_vars Utils.ISet.empty e 
1223

    
1224
(* let rec expr_has_arrows e =
1225
 *   expr_desc_has_arrows e.expr_desc
1226
 * and expr_desc_has_arrows expr_desc =
1227
 *   match expr_desc with
1228
 *   | Expr_const _
1229
 *   | Expr_ident _ -> false
1230
 *   | Expr_tuple el
1231
 *   | Expr_array el -> List.exists expr_has_arrows el
1232
 *   | Expr_pre e1
1233
 *   | Expr_when (e1, _, _)
1234
 *   | Expr_access (e1, _)
1235
 *   | Expr_power (e1, _) -> expr_has_arrows e1
1236
 *   | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
1237
 *   | Expr_arrow _
1238
 *   | Expr_fby _ -> true
1239
 *   | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1240
 *   | Expr_appl (_, e', _) -> expr_has_arrows e'
1241
 *
1242
 * and eq_has_arrows eq =
1243
 *   expr_has_arrows eq.eq_rhs
1244
 * and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers
1245
 * and node_has_arrows node =
1246
 *   let eqs, auts = get_node_eqs node in
1247
 *   List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts *)
1248

    
1249

    
1250

    
1251

    
1252

    
1253
let rec expr_contains_expr expr_tag expr  =
1254
  let search = expr_contains_expr expr_tag in
1255
  expr.expr_tag = expr_tag ||
1256
      (
1257
	match expr.expr_desc with
1258
	| Expr_const _ -> false
1259
	| Expr_array el -> List.exists search el
1260
	| Expr_access (e1, _) 
1261
	| Expr_power (e1, _) -> search e1
1262
	| Expr_tuple el -> List.exists search el
1263
	| Expr_ite (c, t, e) -> List.exists search [c;t;e]
1264
	| Expr_arrow (e1, e2)
1265
	| Expr_fby (e1, e2) -> List.exists search [e1; e2]
1266
	| Expr_pre e' 
1267
	| Expr_when (e', _, _) -> search e'
1268
	| Expr_merge (_, hl) -> List.exists (fun (_, h) -> search h) hl
1269
	| Expr_appl (_, e', None) -> search e' 
1270
	| Expr_appl (_, e', Some e'') -> List.exists search [e'; e''] 
1271
	| Expr_ident _ -> false
1272
      )
1273

    
1274

    
1275

    
1276
(* Generate a new local [node] variable *)
1277
let cpt_fresh = ref 0
1278

    
1279
let reset_cpt_fresh () =
1280
    cpt_fresh := 0
1281
    
1282
let mk_fresh_var (parentid, ctx_env) loc ty ck =
1283
  let rec aux () =
1284
  incr cpt_fresh;
1285
  let s = Printf.sprintf "__%s_%d" parentid !cpt_fresh in
1286
  if List.exists (fun v -> v.var_id = s) ctx_env then aux () else
1287
  {
1288
    var_id = s;
1289
    var_orig = false;
1290
    var_dec_type = dummy_type_dec;
1291
    var_dec_clock = dummy_clock_dec;
1292
    var_dec_const = false;
1293
    var_dec_value = None;
1294
    var_parent_nodeid = Some parentid;
1295
    var_type = ty;
1296
    var_clock = ck;
1297
    var_loc = loc
1298
  }
1299
  in aux ()
1300

    
1301

    
1302
let find_eq xl eqs =
1303
  let rec aux accu eqs =
1304
    match eqs with
1305
	| [] ->
1306
	  begin
1307
	    Format.eprintf "Looking for variables %a in the following equations@.%a@."
1308
	      (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl
1309
	      Printers.pp_node_eqs eqs;
1310
	    assert false
1311
	  end
1312
	| hd::tl ->
1313
	  if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl
1314
    in
1315
    aux [] eqs
1316

    
1317
       
1318
let get_node name prog =
1319
  let node_opt = List.fold_left
1320
    (fun res top -> 
1321
      match res, top.top_decl_desc with
1322
      | Some _, _ -> res
1323
      | None, Node nd -> 
1324
	(* Format.eprintf "Checking node %s = %s: %b@." nd.node_id name (nd.node_id = name); *)
1325
	if nd.node_id = name then Some nd else res
1326
      | _ -> None) 
1327
    None prog 
1328
  in
1329
  try 
1330
    Utils.desome node_opt
1331
  with Utils.DeSome -> raise Not_found
1332

    
1333
(* Pushing negations in expression. Subtitute operators whenever possible *)
1334
let rec push_negations ?(neg=false) e =
1335
  let res =
1336
    let pn = push_negations in
1337
    let map desc =
1338
      (* Keeping clock and type info *)
1339
      let new_e = mkexpr e.expr_loc desc in
1340
      {
1341
        new_e
1342
      with
1343
        expr_type = e.expr_type;
1344
        expr_clock = e.expr_clock
1345
      }
1346
    in
1347
    match e.expr_desc with
1348
    | Expr_ite (g,t,e) ->
1349
       if neg then
1350
         map (Expr_ite(pn g, pn e, pn t))
1351
       else
1352
         map (Expr_ite(pn g, pn t, pn e)) 
1353
    | Expr_tuple t ->
1354
       map (Expr_tuple (List.map (pn ~neg) t))
1355
    | Expr_arrow (e1, e2) ->
1356
       map (Expr_arrow (pn ~neg e1, pn ~neg e2)) 
1357
    | Expr_fby (e1, e2) ->
1358
       map (Expr_fby (pn ~neg e1, pn ~neg e2))
1359
    | Expr_pre e ->
1360
       map (Expr_pre (pn ~neg e))
1361
    | Expr_appl (op, e', None) when op = "not" ->
1362
       if neg then
1363
         push_negations ~neg:false e'
1364
       else
1365
         push_negations ~neg:true e'
1366
    | Expr_appl (op, e', None) when List.mem op (Basic_library.bool_funs @ Basic_library.rel_funs) -> (
1367
      match op with
1368
      | "&&" -> map (Expr_appl((if neg then "||" else op), pn ~neg e', None))
1369
      | "||" -> map (Expr_appl((if neg then "&&" else op), pn ~neg e', None))
1370
      (* TODO xor/equi/impl *)
1371
      | "<" -> map (Expr_appl((if neg then ">=" else op), pn e', None))
1372
      | ">" -> map (Expr_appl((if neg then "<=" else op), pn e', None))
1373
      | "<=" -> map (Expr_appl((if neg then ">" else op), pn e', None))
1374
      | ">=" -> map (Expr_appl((if neg then "<" else op), pn e', None))
1375
      | "!=" -> map (Expr_appl((if neg then "=" else op), pn e', None))
1376
      | "=" -> map (Expr_appl((if neg then "!=" else op), pn e', None))
1377
             
1378
      | _ -> assert false                     
1379
    )
1380
    | Expr_const c -> if neg then map (Expr_const (const_negation c)) else e
1381
    | Expr_ident _ -> 
1382
       if neg then
1383
                         mkpredef_call e.expr_loc "not" [e]
1384
                       else
1385
                         e
1386
    | Expr_appl _ ->
1387
       if neg then
1388
         mkpredef_call e.expr_loc "not" [e]
1389
       else
1390
         e
1391
    | _ -> assert false (* no array, array access, power or merge/when *)
1392
  in
1393
  res
1394

    
1395
let rec add_pre_expr vars e =
1396
  let ap = add_pre_expr vars in
1397
  let desc =
1398
    match e.expr_desc with
1399
    | Expr_ite (g,t,e) ->
1400
       Expr_ite (ap g, ap t,ap e)
1401
    | Expr_tuple t ->
1402
       Expr_tuple (List.map ap t)
1403
    | Expr_arrow (e1, e2) ->
1404
       Expr_arrow (ap e1, ap e2) 
1405
    | Expr_fby (e1, e2) ->
1406
       Expr_fby (ap e1, ap e2)
1407
    | Expr_pre e ->
1408
       Expr_pre (ap e)
1409
    | Expr_appl (op, e, opt) ->
1410
       Expr_appl (op, ap e, opt)
1411
    | Expr_const _ -> e.expr_desc 
1412
    | Expr_ident id ->
1413
       if List.mem id vars then
1414
         Expr_pre e
1415
       else
1416
         e.expr_desc
1417
    | _ -> assert false (* no array, array access, power or merge/when yet *)
1418
  in
1419
  let new_e = mkexpr e.expr_loc desc in
1420
  { new_e with
1421
    expr_type = e.expr_type;
1422
    expr_clock = e.expr_clock
1423
  }
1424

    
1425

    
1426
        
1427
let mk_eq l e1 e2 =
1428
  mkpredef_call l "=" [e1; e2]
1429

    
1430

    
1431
let rec partial_eval e =
1432
  let pa = partial_eval in
1433
  let edesc =
1434
    match e.expr_desc with
1435
    | Expr_const _ -> e.expr_desc 
1436
    | Expr_ident _ -> e.expr_desc
1437
    | Expr_ite (g,t,e) -> (
1438
       let g, t, e = pa g, pa t, pa e in
1439
       match g.expr_desc with
1440
       | Expr_const (Const_tag tag) when (tag = tag_true) -> t.expr_desc
1441
       | Expr_const (Const_tag tag) when (tag = tag_false) -> e.expr_desc
1442
       | _ -> Expr_ite (g, t, e)
1443
    )
1444
    | Expr_tuple t ->
1445
       Expr_tuple (List.map pa t)
1446
    | Expr_arrow (e1, e2) ->
1447
       Expr_arrow (pa e1, pa e2) 
1448
    | Expr_fby (e1, e2) ->
1449
       Expr_fby (pa e1, pa e2)
1450
    | Expr_pre e ->
1451
       Expr_pre (pa e)
1452
    | Expr_appl (op, args, opt) ->
1453
       let args = pa args in
1454
       if Basic_library.is_expr_internal_fun e then
1455
         Basic_library.partial_eval op args opt
1456
       else
1457
         Expr_appl (op, args, opt)
1458
    | Expr_array el ->
1459
       Expr_array (List.map pa el)
1460
    | Expr_access (e, d) ->
1461
       Expr_access (pa e, d)
1462
    | Expr_power (e, d) ->
1463
       Expr_power (pa e, d)
1464
    | Expr_when (e, id, l) ->
1465
       Expr_when (pa e, id, l)
1466
    | Expr_merge (id, gl) -> 
1467
       Expr_merge(id, List.map (fun (l, e) -> l, pa e) gl)
1468
  in
1469
  { e with expr_desc = edesc }
1470

    
1471
    (* Local Variables: *)
1472
    (* compile-command:"make -C .." *)
1473
    (* End: *)
(15-15/66)