Project

General

Profile

Download (48.7 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
module VDeclModule = struct
18
  (* Node module *)
19
  type t = var_decl
20

    
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

    
29
  val pp : Format.formatter -> t -> unit
30

    
31
  val get : ident -> t -> elt
32
end
33
with type elt = var_decl = struct
34
  include Set.Make (VDeclModule)
35

    
36
  let pp fmt s =
37
    Format.fprintf fmt "{@[%a}@]"
38
      (Utils.fprintf_list ~sep:",@ " Printers.pp_var)
39
      (elements s)
40

    
41
  (* Strangley the find_first function of Set.Make is incorrect (at the current
42
     time of writting this comment. Had to switch to lists *)
43
  let get id s = List.find (fun v -> v.var_id = id) (elements s)
44
end
45

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

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

    
52
(************************************************************)
53
(* *)
54

    
55
let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc }
56

    
57
let mkclock loc d = { ck_dec_desc = d; ck_dec_loc = loc }
58

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

    
75
let dummy_var_decl name typ =
76
  {
77
    var_id = name;
78
    var_orig = false;
79
    var_dec_type = dummy_type_dec;
80
    var_dec_clock = dummy_clock_dec;
81
    var_dec_const = false;
82
    var_dec_value = None;
83
    var_parent_nodeid = None;
84
    var_type = typ;
85
    var_clock = Clocks.new_ck Clocks.Cvar true;
86
    var_loc = Location.dummy_loc;
87
  }
88

    
89
let mkexpr loc d =
90
  {
91
    expr_tag = Utils.new_tag ();
92
    expr_desc = d;
93
    expr_type = Types.new_var ();
94
    expr_clock = Clocks.new_var true;
95
    expr_delay = Delay.new_var ();
96
    expr_annot = None;
97
    expr_loc = loc;
98
  }
99

    
100
let var_decl_of_const ?(parentid = None) c =
101
  {
102
    var_id = c.const_id;
103
    var_orig = true;
104
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
105
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
106
    var_dec_const = true;
107
    var_dec_value = None;
108
    var_parent_nodeid = parentid;
109
    var_type = c.const_type;
110
    var_clock = Clocks.new_var false;
111
    var_loc = c.const_loc;
112
  }
113

    
114
let mk_new_name used id =
115
  let rec new_name name cpt =
116
    if used name then new_name (sprintf "_%s_%i" id cpt) (cpt + 1) else name
117
  in
118
  new_name id 1
119

    
120
let mkeq loc (lhs, rhs) = { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc }
121

    
122
let mkassert loc expr = { assert_loc = loc; assert_expr = expr }
123

    
124
let mktop_decl loc own itf d =
125
  {
126
    top_decl_desc = d;
127
    top_decl_loc = loc;
128
    top_decl_owner = own;
129
    top_decl_itf = itf;
130
  }
131

    
132
let mkpredef_call loc funname args =
133
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
134

    
135
let is_clock_dec_type cty = match cty with Tydec_clock _ -> true | _ -> false
136

    
137
let const_of_top top_decl =
138
  match top_decl.top_decl_desc with Const c -> c | _ -> assert false
139

    
140
let node_of_top top_decl =
141
  match top_decl.top_decl_desc with Node nd -> nd | _ -> raise Not_found
142

    
143
let imported_node_of_top top_decl =
144
  match top_decl.top_decl_desc with
145
  | ImportedNode ind ->
146
    ind
147
  | _ ->
148
    assert false
149

    
150
let typedef_of_top top_decl =
151
  match top_decl.top_decl_desc with TypeDef tdef -> tdef | _ -> assert false
152

    
153
let dependency_of_top top_decl =
154
  match top_decl.top_decl_desc with
155
  | Open (local, dep) ->
156
    local, dep
157
  | _ ->
158
    assert false
159

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

    
182
(************************************************************)
183
(*   Eexpr functions *)
184
(************************************************************)
185

    
186
let empty_contract =
187
  {
188
    consts = [];
189
    locals = [];
190
    stmts = [];
191
    assume = [];
192
    guarantees = [];
193
    modes = [];
194
    imports = [];
195
    spec_loc = Location.dummy_loc;
196
  }
197

    
198
(* For const declaration we do as for regular lustre node. But for local flows
199
   we registered the variable and the lustre flow definition *)
200
let mk_contract_var id is_const type_opt expr loc =
201
  let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
202
  if is_const then
203
    let v =
204
      mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None)
205
    in
206
    { empty_contract with consts = [ v ]; spec_loc = loc }
207
  else
208
    let v =
209
      mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None)
210
    in
211
    let eq = mkeq loc ([ id ], expr) in
212
    { empty_contract with locals = [ v ]; stmts = [ Eq eq ]; spec_loc = loc }
213

    
214
let eexpr_add_name eexpr eexpr_name = { eexpr with eexpr_name }
215

    
216
let mk_contract_guarantees name eexpr =
217
  {
218
    empty_contract with
219
    guarantees = [ eexpr_add_name eexpr name ];
220
    spec_loc = eexpr.eexpr_loc;
221
  }
222

    
223
let mk_contract_assume name eexpr =
224
  {
225
    empty_contract with
226
    assume = [ eexpr_add_name eexpr name ];
227
    spec_loc = eexpr.eexpr_loc;
228
  }
229

    
230
let mk_contract_mode id rl el loc =
231
  {
232
    empty_contract with
233
    modes = [ { mode_id = id; require = rl; ensure = el; mode_loc = loc } ];
234
    spec_loc = loc;
235
  }
236

    
237
let mk_contract_import id ins outs loc =
238
  {
239
    empty_contract with
240
    imports =
241
      [ { import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc } ];
242
    spec_loc = loc;
243
  }
244

    
245
let merge_contracts ann1 ann2 =
246
  (* keeping the first item loc *)
247
  {
248
    consts = ann1.consts @ ann2.consts;
249
    locals = ann1.locals @ ann2.locals;
250
    stmts = ann1.stmts @ ann2.stmts;
251
    assume = ann1.assume @ ann2.assume;
252
    guarantees = ann1.guarantees @ ann2.guarantees;
253
    modes = ann1.modes @ ann2.modes;
254
    imports = ann1.imports @ ann2.imports;
255
    spec_loc = ann1.spec_loc;
256
  }
257

    
258
let mkeexpr loc expr =
259
  {
260
    eexpr_tag = Utils.new_tag ();
261
    eexpr_qfexpr = expr;
262
    eexpr_quantifiers = [];
263
    eexpr_name = None;
264
    eexpr_type = Types.new_var ();
265
    eexpr_clock = Clocks.new_var true;
266
    eexpr_loc = loc;
267
  }
268

    
269
let extend_eexpr q e = { e with eexpr_quantifiers = q @ e.eexpr_quantifiers }
270

    
271
(* let mkepredef_call loc funname args = mkeexpr loc (EExpr_appl (funname,
272
   mkeexpr loc (EExpr_tuple args), None))
273

    
274
   let mkepredef_unary_call loc funname arg = mkeexpr loc (EExpr_appl (funname,
275
   arg, None)) *)
276

    
277
let merge_expr_annot ann1 ann2 =
278
  match ann1, ann2 with
279
  | None, None ->
280
    assert false
281
  | Some _, None ->
282
    ann1
283
  | None, Some _ ->
284
    ann2
285
  | Some ann1, Some ann2 ->
286
    Some { annots = ann1.annots @ ann2.annots; annot_loc = ann1.annot_loc }
287

    
288
let update_expr_annot node_id e annot =
289
  List.iter
290
    (fun (key, _) -> Annotations.add_expr_ann node_id e.expr_tag key)
291
    annot.annots;
292
  e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
293
  e
294

    
295
let mkinstr ?lustre_eq ?(instr_spec = []) instr_desc =
296
  { instr_desc; (* lustre_expr = lustre_expr; *)
297
                instr_spec; lustre_eq }
298

    
299
let get_instr_desc i = i.instr_desc
300

    
301
let update_instr_desc i id = { i with instr_desc = id }
302

    
303
(***********************************************************)
304
(* Fast access to nodes, by name *)
305
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
306

    
307
let consts_table = Hashtbl.create 30
308

    
309
let print_node_table fmt () =
310
  Format.fprintf fmt "{ /* node table */@.";
311
  Hashtbl.iter
312
    (fun id nd -> Format.fprintf fmt "%s |-> %a" id Printers.pp_short_decl nd)
313
    node_table;
314
  Format.fprintf fmt "}@."
315

    
316
let print_consts_table fmt () =
317
  Format.fprintf fmt "{ /* consts table */@.";
318
  Hashtbl.iter
319
    (fun id const ->
320
      Format.fprintf fmt "%s |-> %a" id Printers.pp_const_decl
321
        (const_of_top const))
322
    consts_table;
323
  Format.fprintf fmt "}@."
324

    
325
let node_name td =
326
  match td.top_decl_desc with
327
  | Node nd ->
328
    nd.node_id
329
  | ImportedNode nd ->
330
    nd.nodei_id
331
  | _ ->
332
    assert false
333

    
334
let is_generic_node td =
335
  match td.top_decl_desc with
336
  | Node nd ->
337
    List.exists (fun v -> v.var_dec_const) nd.node_inputs
338
  | ImportedNode nd ->
339
    List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
340
  | _ ->
341
    assert false
342

    
343
let node_inputs td =
344
  match td.top_decl_desc with
345
  | Node nd ->
346
    nd.node_inputs
347
  | ImportedNode nd ->
348
    nd.nodei_inputs
349
  | _ ->
350
    assert false
351

    
352
let node_from_name id = Hashtbl.find node_table id
353

    
354
let update_node id top = Hashtbl.replace node_table id top
355

    
356
let is_imported_node td =
357
  match td.top_decl_desc with
358
  | Node _ ->
359
    false
360
  | ImportedNode _ ->
361
    true
362
  | _ ->
363
    assert false
364

    
365
let is_node_contract nd =
366
  match nd.node_spec with Some (Contract _) -> true | _ -> false
367

    
368
let get_node_contract nd =
369
  match nd.node_spec with Some (Contract c) -> c | _ -> assert false
370

    
371
let is_contract td =
372
  match td.top_decl_desc with Node nd -> is_node_contract nd | _ -> false
373

    
374
(* alias and type definition table *)
375

    
376
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
377

    
378
let top_int_type = mktop (TypeDef { tydef_id = "int"; tydef_desc = Tydec_int })
379

    
380
let top_bool_type =
381
  mktop (TypeDef { tydef_id = "bool"; tydef_desc = Tydec_bool })
382

    
383
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc =
384
   Tydec_float}) *)
385
let top_real_type =
386
  mktop (TypeDef { tydef_id = "real"; tydef_desc = Tydec_real })
387

    
388
let type_table =
389
  Utils.create_hashtable 20
390
    [
391
      Tydec_int, top_int_type;
392
      Tydec_bool, top_bool_type;
393
      (* Tydec_float, top_float_type; *)
394
      Tydec_real, top_real_type;
395
    ]
396

    
397
let print_type_table fmt () =
398
  Format.fprintf fmt "{ /* type table */@.";
399
  Hashtbl.iter
400
    (fun tydec tdef ->
401
      Format.fprintf fmt "%a |-> %a" Printers.pp_var_type_dec_desc tydec
402
        Printers.pp_typedef (typedef_of_top tdef))
403
    type_table;
404
  Format.fprintf fmt "}@."
405

    
406
let rec is_user_type typ =
407
  match typ with
408
  | Tydec_int
409
  | Tydec_bool
410
  | Tydec_real (* | Tydec_float *)
411
  | Tydec_any
412
  | Tydec_const _ ->
413
    false
414
  | Tydec_clock typ' ->
415
    is_user_type typ'
416
  | _ ->
417
    true
418

    
419
let get_repr_type typ =
420
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
421
  if is_user_type typ_def then typ else typ_def
422

    
423
let rec coretype_equal ty1 ty2 =
424
  let res =
425
    match ty1, ty2 with
426
    | Tydec_any, _ | _, Tydec_any ->
427
      assert false
428
    | Tydec_const _, Tydec_const _ ->
429
      get_repr_type ty1 = get_repr_type ty2
430
    | Tydec_const _, _ ->
431
      let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc in
432
      (not (is_user_type ty1')) && coretype_equal ty1' ty2
433
    | _, Tydec_const _ ->
434
      coretype_equal ty2 ty1
435
    | Tydec_int, Tydec_int
436
    | Tydec_real, Tydec_real
437
    (* | Tydec_float , Tydec_float *)
438
    | Tydec_bool, Tydec_bool ->
439
      true
440
    | Tydec_clock ty1, Tydec_clock ty2 ->
441
      coretype_equal ty1 ty2
442
    | Tydec_array (d1, ty1), Tydec_array (d2, ty2) ->
443
      Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
444
    | Tydec_enum tl1, Tydec_enum tl2 ->
445
      List.sort compare tl1 = List.sort compare tl2
446
    | Tydec_struct fl1, Tydec_struct fl2 ->
447
      List.length fl1 = List.length fl2
448
      && List.for_all2
449
           (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
450
           (List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl1)
451
           (List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl2)
452
    | _ ->
453
      false
454
  in
455
  (*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc
456
    ty1 Printers.pp_var_type_dec_desc ty2 res;*)
457
  res
458

    
459
let tag_default = "default"
460

    
461
let const_is_bool c =
462
  match c with Const_tag t -> t = tag_true || t = tag_false | _ -> false
463

    
464
(* Computes the negation of a boolean constant *)
465
let const_negation c =
466
  assert (const_is_bool c);
467
  match c with
468
  | Const_tag t when t = tag_true ->
469
    Const_tag tag_false
470
  | _ ->
471
    Const_tag tag_true
472

    
473
let const_or c1 c2 =
474
  assert (const_is_bool c1 && const_is_bool c2);
475
  match c1, c2 with
476
  | Const_tag t1, _ when t1 = tag_true ->
477
    c1
478
  | _, Const_tag t2 when t2 = tag_true ->
479
    c2
480
  | _ ->
481
    Const_tag tag_false
482

    
483
let const_and c1 c2 =
484
  assert (const_is_bool c1 && const_is_bool c2);
485
  match c1, c2 with
486
  | Const_tag t1, _ when t1 = tag_false ->
487
    c1
488
  | _, Const_tag t2 when t2 = tag_false ->
489
    c2
490
  | _ ->
491
    Const_tag tag_true
492

    
493
let const_xor c1 c2 =
494
  assert (const_is_bool c1 && const_is_bool c2);
495
  match c1, c2 with
496
  | Const_tag t1, Const_tag t2 when t1 <> t2 ->
497
    Const_tag tag_true
498
  | _ ->
499
    Const_tag tag_false
500

    
501
let const_impl c1 c2 =
502
  assert (const_is_bool c1 && const_is_bool c2);
503
  match c1, c2 with
504
  | Const_tag t1, _ when t1 = tag_false ->
505
    Const_tag tag_true
506
  | _, Const_tag t2 when t2 = tag_true ->
507
    Const_tag tag_true
508
  | _ ->
509
    Const_tag tag_false
510

    
511
(* To guarantee uniqueness of tags in enum types *)
512
let tag_table =
513
  Utils.create_hashtable 20
514
    [ tag_true, top_bool_type; tag_false, top_bool_type ]
515

    
516
(* To guarantee uniqueness of fields in struct types *)
517
let field_table = Utils.create_hashtable 20 []
518

    
519
let get_enum_type_tags cty =
520
  (*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
521
  match cty with
522
  | Tydec_bool ->
523
    [ tag_true; tag_false ]
524
  | Tydec_const _ -> (
525
    match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
526
    | Tydec_enum tl ->
527
      tl
528
    | _ ->
529
      assert false)
530
  | _ ->
531
    assert false
532

    
533
let get_struct_type_fields cty =
534
  match cty with
535
  | Tydec_const _ -> (
536
    match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
537
    | Tydec_struct fl ->
538
      fl
539
    | _ ->
540
      assert false)
541
  | _ ->
542
    assert false
543

    
544
let const_of_bool b = Const_tag (if b then tag_true else tag_false)
545

    
546
(* let get_const c = snd (Hashtbl.find consts_table c) *)
547

    
548
let ident_of_expr expr =
549
  match expr.expr_desc with Expr_ident id -> id | _ -> assert false
550

    
551
(* Generate a new ident expression from a declared variable *)
552
let expr_of_vdecl v =
553
  {
554
    expr_tag = Utils.new_tag ();
555
    expr_desc = Expr_ident v.var_id;
556
    expr_type = v.var_type;
557
    expr_clock = v.var_clock;
558
    expr_delay = Delay.new_var ();
559
    expr_annot = None;
560
    expr_loc = v.var_loc;
561
  }
562

    
563
(* Caution, returns an untyped and unclocked expression *)
564
let expr_of_ident id loc =
565
  {
566
    expr_tag = Utils.new_tag ();
567
    expr_desc = Expr_ident id;
568
    expr_type = Types.new_var ();
569
    expr_clock = Clocks.new_var true;
570
    expr_delay = Delay.new_var ();
571
    expr_loc = loc;
572
    expr_annot = None;
573
  }
574

    
575
let is_tuple_expr expr =
576
  match expr.expr_desc with Expr_tuple _ -> true | _ -> false
577

    
578
let expr_list_of_expr expr =
579
  match expr.expr_desc with Expr_tuple elist -> elist | _ -> [ expr ]
580

    
581
let expr_of_expr_list loc elist =
582
  match elist with
583
  | [ t ] ->
584
    { t with expr_loc = loc }
585
  | t :: _ ->
586
    let tlist = List.map (fun e -> e.expr_type) elist in
587
    let clist = List.map (fun e -> e.expr_clock) elist in
588
    {
589
      t with
590
      expr_desc = Expr_tuple elist;
591
      expr_type = Type_predef.type_tuple tlist;
592
      expr_clock = Clock_predef.ck_tuple clist;
593
      expr_tag = Utils.new_tag ();
594
      expr_loc = loc;
595
    }
596
  | _ ->
597
    assert false
598

    
599
let call_of_expr expr =
600
  match expr.expr_desc with
601
  | Expr_appl (f, args, r) ->
602
    f, expr_list_of_expr args, r
603
  | _ ->
604
    assert false
605

    
606
(* Conversion from dimension expr to standard expr, for the purpose of printing,
607
   typing, etc... *)
608
let rec expr_of_dimension dim =
609
  let open Dimension in
610
  let expr =
611
    match dim.dim_desc with
612
    | Dbool b ->
613
      mkexpr dim.dim_loc (Expr_const (const_of_bool b))
614
    | Dint i ->
615
      mkexpr dim.dim_loc (Expr_const (Const_int i))
616
    | Dident id ->
617
      mkexpr dim.dim_loc (Expr_ident id)
618
    | Dite (c, t, e) ->
619
      mkexpr dim.dim_loc
620
        (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
621
    | Dappl (id, args) ->
622
      mkexpr dim.dim_loc
623
        (Expr_appl
624
           ( id,
625
             expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args),
626
             None ))
627
    | Dlink dim' ->
628
      expr_of_dimension dim'
629
    | Dvar | Dunivar ->
630
      Format.eprintf "internal error: Corelang.expr_of_dimension %a@."
631
        Dimension.pp_dimension dim;
632
      assert false
633
  in
634
  { expr with expr_type = Types.new_ty Types.type_int }
635

    
636
let dimension_of_const loc const =
637
  let open Dimension in
638
  match const with
639
  | Const_int i ->
640
    mkdim_int loc i
641
  | Const_tag t when t = tag_true || t = tag_false ->
642
    mkdim_bool loc (t = tag_true)
643
  | _ ->
644
    raise InvalidDimension
645

    
646
(* Conversion from standard expr to dimension expr, for the purpose of injecting
647
   static call arguments into dimension expressions *)
648
let rec dimension_of_expr expr =
649
  let open Dimension in
650
  match expr.expr_desc with
651
  | Expr_const c ->
652
    dimension_of_const expr.expr_loc c
653
  | Expr_ident id ->
654
    mkdim_ident expr.expr_loc id
655
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
656
    let k =
657
      Types.get_static_value (Env.lookup_value Basic_library.type_env f)
658
    in
659
    if k = None then raise InvalidDimension;
660
    mkdim_appl expr.expr_loc f
661
      (List.map dimension_of_expr (expr_list_of_expr args))
662
  | Expr_ite (i, t, e) ->
663
    mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t)
664
      (dimension_of_expr e)
665
  | _ ->
666
    raise InvalidDimension
667
(* not a simple dimension expression *)
668

    
669
let sort_handlers hl = List.sort (fun (t, _) (t', _) -> compare t t') hl
670

    
671
let rec is_eq_const c1 c2 =
672
  match c1, c2 with
673
  | Const_real r1, Const_real _ ->
674
    Real.eq r1 r1
675
  | Const_struct lcl1, Const_struct lcl2 ->
676
    List.length lcl1 = List.length lcl2
677
    && List.for_all2
678
         (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2)
679
         lcl1 lcl2
680
  | _ ->
681
    c1 = c2
682

    
683
let rec is_eq_expr e1 e2 =
684
  match e1.expr_desc, e2.expr_desc with
685
  | Expr_const c1, Expr_const c2 ->
686
    is_eq_const c1 c2
687
  | Expr_ident i1, Expr_ident i2 ->
688
    i1 = i2
689
  | Expr_array el1, Expr_array el2 | Expr_tuple el1, Expr_tuple el2 ->
690
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2
691
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') ->
692
    is_eq_expr e1 e1' && is_eq_expr e2 e2'
693
  | Expr_fby (e1, e2), Expr_fby (e1', e2') ->
694
    is_eq_expr e1 e1' && is_eq_expr e2 e2'
695
  | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) ->
696
    is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2
697
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' &&
698
     is_eq_expr e2 e2' *)
699
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
700
  | Expr_pre e, Expr_pre e' ->
701
    is_eq_expr e e'
702
  | Expr_when (e, i, l), Expr_when (e', i', l') ->
703
    l = l' && i = i' && is_eq_expr e e'
704
  | Expr_merge (i, hl), Expr_merge (i', hl') ->
705
    i = i'
706
    && List.for_all2
707
         (fun (t, h) (t', h') -> t = t' && is_eq_expr h h')
708
         (sort_handlers hl) (sort_handlers hl')
709
  | Expr_appl (i, e, r), Expr_appl (i', e', r') ->
710
    i = i' && r = r' && is_eq_expr e e'
711
  | Expr_power (e1, i1), Expr_power (e2, i2)
712
  | Expr_access (e1, i1), Expr_access (e2, i2) ->
713
    is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
714
  | _ ->
715
    false
716

    
717
let get_node_vars nd = nd.node_inputs @ nd.node_locals @ nd.node_outputs
718

    
719
let mk_new_node_name nd id =
720
  let used_vars = get_node_vars nd in
721
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
722
  mk_new_name used id
723

    
724
let get_var id var_list = List.find (fun v -> v.var_id = id) var_list
725

    
726
let get_node_var id node =
727
  try get_var id (get_node_vars node)
728
  with Not_found ->
729
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id
730
       node.node_id; *)
731
    raise Not_found
732

    
733
let get_node_eqs =
734
  let get_eqs stmts =
735
    List.fold_right
736
      (fun stmt (res_eq, res_aut) ->
737
        match stmt with
738
        | Eq eq ->
739
          eq :: res_eq, res_aut
740
        | Aut aut ->
741
          res_eq, aut :: res_aut)
742
      stmts ([], [])
743
  in
744
  let table_eqs = Hashtbl.create 23 in
745
  fun nd ->
746
    try
747
      let old, res = Hashtbl.find table_eqs nd.node_id in
748
      if old == nd.node_stmts then res else raise Not_found
749
    with Not_found ->
750
      let res = get_eqs nd.node_stmts in
751
      Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
752
      res
753

    
754
let get_node_eq id node =
755
  let eqs, _ = get_node_eqs node in
756
  try List.find (fun eq -> List.mem id eq.eq_lhs) eqs
757
  with Not_found -> (* Shall be defined in automata auts *)
758
                    raise Not_found
759

    
760
let get_nodes prog =
761
  List.fold_left
762
    (fun nodes decl ->
763
      match decl.top_decl_desc with
764
      | Node _ ->
765
        decl :: nodes
766
      | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ ->
767
        nodes)
768
    [] prog
769
  |> List.rev
770

    
771
let get_imported_nodes prog =
772
  List.fold_left
773
    (fun nodes decl ->
774
      match decl.top_decl_desc with
775
      | ImportedNode _ ->
776
        decl :: nodes
777
      | Const _ | Node _ | Include _ | Open _ | TypeDef _ ->
778
        nodes)
779
    [] prog
780

    
781
let get_consts prog =
782
  List.fold_right
783
    (fun decl consts ->
784
      match decl.top_decl_desc with
785
      | Const _ ->
786
        decl :: consts
787
      | Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ ->
788
        consts)
789
    prog []
790

    
791
let get_typedefs prog =
792
  List.fold_right
793
    (fun decl types ->
794
      match decl.top_decl_desc with
795
      | TypeDef _ ->
796
        decl :: types
797
      | Node _ | ImportedNode _ | Include _ | Open _ | Const _ ->
798
        types)
799
    prog []
800

    
801
let get_dependencies prog =
802
  List.fold_right
803
    (fun decl deps ->
804
      match decl.top_decl_desc with
805
      | Open _ ->
806
        decl :: deps
807
      | Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ ->
808
        deps)
809
    prog []
810

    
811
let get_node_interface nd =
812
  {
813
    nodei_id = nd.node_id;
814
    nodei_type = nd.node_type;
815
    nodei_clock = nd.node_clock;
816
    nodei_inputs = nd.node_inputs;
817
    nodei_outputs = nd.node_outputs;
818
    nodei_stateless = nd.node_dec_stateless;
819
    nodei_spec = nd.node_spec;
820
    (* nodei_annot = nd.node_annot; *)
821
    nodei_prototype = None;
822
    nodei_in_lib = [];
823
  }
824

    
825
(************************************************************************)
826
(* Renaming / Copying *)
827

    
828
let copy_var_decl vdecl =
829
  mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig
830
    ( vdecl.var_id,
831
      vdecl.var_dec_type,
832
      vdecl.var_dec_clock,
833
      vdecl.var_dec_const,
834
      vdecl.var_dec_value,
835
      vdecl.var_parent_nodeid )
836

    
837
let copy_const cdecl = { cdecl with const_type = Types.new_var () }
838

    
839
let copy_node nd =
840
  {
841
    nd with
842
    node_type = Types.new_var ();
843
    node_clock = Clocks.new_var true;
844
    node_inputs = List.map copy_var_decl nd.node_inputs;
845
    node_outputs = List.map copy_var_decl nd.node_outputs;
846
    node_locals = List.map copy_var_decl nd.node_locals;
847
    node_gencalls = [];
848
    node_checks = [];
849
    node_stateless = None;
850
  }
851

    
852
let copy_top top =
853
  match top.top_decl_desc with
854
  | Node nd ->
855
    { top with top_decl_desc = Node (copy_node nd) }
856
  | Const c ->
857
    { top with top_decl_desc = Const (copy_const c) }
858
  | _ ->
859
    top
860

    
861
let copy_prog top_list = List.map copy_top top_list
862

    
863
let rec rename_static rename cty =
864
  match cty with
865
  | Tydec_array (d, cty') ->
866
    Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
867
  | Tydec_clock cty ->
868
    Tydec_clock (rename_static rename cty)
869
  | Tydec_struct fl ->
870
    Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
871
  | _ ->
872
    cty
873

    
874
let rename_carrier rename cck =
875
  match cck with
876
  | Ckdec_bool cl ->
877
    Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
878
  | _ ->
879
    cck
880

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

    
883
(* applies the renaming function [fvar] to all variables of expression [expr] *)
884
(* let rec expr_replace_var fvar expr = *)
885
(*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
886

    
887
(* and expr_desc_replace_var fvar expr_desc = *)
888
(*   match expr_desc with *)
889
(*   | Expr_const _ -> expr_desc *)
890
(*   | Expr_ident i -> Expr_ident (fvar i) *)
891
(*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
892
(*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
893
(*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
894
(*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
895
(* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var
896
   fvar t, expr_replace_var fvar e) *)
897
(* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1,
898
   expr_replace_var fvar e2) *)
899
(* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var
900
   fvar e2) *)
901
(*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
902
(*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
903
(* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t,
904
   expr_replace_var fvar h)) hl) *)
905
(* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e',
906
   Utils.option_map (expr_replace_var fvar) i') *)
907

    
908
let rec rename_expr f_node f_var expr =
909
  { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
910

    
911
and rename_expr_desc f_node f_var expr_desc =
912
  let re = rename_expr f_node f_var in
913
  match expr_desc with
914
  | Expr_const _ ->
915
    expr_desc
916
  | Expr_ident i ->
917
    Expr_ident (f_var i)
918
  | Expr_array el ->
919
    Expr_array (List.map re el)
920
  | Expr_access (e1, d) ->
921
    Expr_access (re e1, d)
922
  | Expr_power (e1, d) ->
923
    Expr_power (re e1, d)
924
  | Expr_tuple el ->
925
    Expr_tuple (List.map re el)
926
  | Expr_ite (c, t, e) ->
927
    Expr_ite (re c, re t, re e)
928
  | Expr_arrow (e1, e2) ->
929
    Expr_arrow (re e1, re e2)
930
  | Expr_fby (e1, e2) ->
931
    Expr_fby (re e1, re e2)
932
  | Expr_pre e' ->
933
    Expr_pre (re e')
934
  | Expr_when (e', i, l) ->
935
    Expr_when (re e', f_var i, l)
936
  | Expr_merge (i, hl) ->
937
    Expr_merge (f_var i, List.map (fun (t, h) -> t, re h) hl)
938
  | Expr_appl (i, e', i') ->
939
    Expr_appl (f_node i, re e', Utils.option_map re i')
940

    
941
let rename_var f_var v =
942
  {
943
    (copy_var_decl v) with
944
    var_id = f_var v.var_id;
945
    var_type = v.var_type;
946
    var_clock = v.var_clock;
947
  }
948

    
949
let rename_vars f_var = List.map (rename_var f_var)
950

    
951
let rec rename_eq f_node f_var eq =
952
  {
953
    eq with
954
    eq_lhs = List.map f_var eq.eq_lhs;
955
    eq_rhs = rename_expr f_node f_var eq.eq_rhs;
956
  }
957

    
958
and rename_handler f_node f_var h =
959
  {
960
    h with
961
    hand_state = f_var h.hand_state;
962
    hand_unless =
963
      List.map
964
        (fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id)
965
        h.hand_unless;
966
    hand_until =
967
      List.map
968
        (fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id)
969
        h.hand_until;
970
    hand_locals = rename_vars f_var h.hand_locals;
971
    hand_stmts = rename_stmts f_node f_var h.hand_stmts;
972
    hand_annots = rename_annots f_node f_var h.hand_annots;
973
  }
974

    
975
and rename_aut f_node f_var aut =
976
  {
977
    aut with
978
    aut_id = f_var aut.aut_id;
979
    aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
980
  }
981

    
982
and rename_stmts f_node f_var stmts =
983
  List.map
984
    (fun stmt ->
985
      match stmt with
986
      | Eq eq ->
987
        Eq (rename_eq f_node f_var eq)
988
      | Aut at ->
989
        Aut (rename_aut f_node f_var at))
990
    stmts
991

    
992
and rename_annotl f_node f_var annots =
993
  List.map (fun (key, value) -> key, rename_eexpr f_node f_var value) annots
994

    
995
and rename_annot f_node f_var annot =
996
  { annot with annots = rename_annotl f_node f_var annot.annots }
997

    
998
and rename_annots f_node f_var annots =
999
  List.map (rename_annot f_node f_var) annots
1000

    
1001
and rename_eexpr f_node f_var ee =
1002
  {
1003
    ee with
1004
    eexpr_tag = Utils.new_tag ();
1005
    eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
1006
    eexpr_quantifiers =
1007
      List.map
1008
        (fun (typ, vdecls) -> typ, rename_vars f_var vdecls)
1009
        ee.eexpr_quantifiers;
1010
  }
1011

    
1012
and rename_mode f_node f_var m =
1013
  let rename_ee = rename_eexpr f_node f_var in
1014
  {
1015
    m with
1016
    require = List.map rename_ee m.require;
1017
    ensure = List.map rename_ee m.ensure;
1018
  }
1019

    
1020
let rename_import f_node f_var imp =
1021
  let rename_expr = rename_expr f_node f_var in
1022
  {
1023
    imp with
1024
    import_nodeid = f_node imp.import_nodeid;
1025
    inputs = rename_expr imp.inputs;
1026
    outputs = rename_expr imp.outputs;
1027
  }
1028

    
1029
let rename_node f_node f_var nd =
1030
  let f_var x =
1031
    (* checking that this is actually a local variable *)
1032
    if List.exists (fun v -> v.var_id = x) (get_node_vars nd) then f_var x
1033
    else x
1034
  in
1035
  let rename_var = rename_var f_var in
1036
  let rename_vars = List.map rename_var in
1037
  let rename_expr = rename_expr f_node f_var in
1038
  let rename_eexpr = rename_eexpr f_node f_var in
1039
  let rename_stmts = rename_stmts f_node f_var in
1040
  let inputs = rename_vars nd.node_inputs in
1041
  let outputs = rename_vars nd.node_outputs in
1042
  let locals = rename_vars nd.node_locals in
1043
  let gen_calls = List.map rename_expr nd.node_gencalls in
1044
  let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in
1045
  let node_asserts =
1046
    List.map
1047
      (fun a ->
1048
        {
1049
          a with
1050
          assert_expr =
1051
            (let expr = a.assert_expr in
1052
             rename_expr expr);
1053
        })
1054
      nd.node_asserts
1055
  in
1056
  let node_stmts = rename_stmts nd.node_stmts in
1057

    
1058
  let spec =
1059
    Utils.option_map
1060
      (fun s ->
1061
        match s with
1062
        | NodeSpec id ->
1063
          NodeSpec (f_node id)
1064
        | Contract c ->
1065
          Contract
1066
            {
1067
              c with
1068
              consts = rename_vars c.consts;
1069
              locals = rename_vars c.locals;
1070
              stmts = rename_stmts c.stmts;
1071
              assume = List.map rename_eexpr c.assume;
1072
              guarantees = List.map rename_eexpr c.guarantees;
1073
              modes = List.map (rename_mode f_node f_var) c.modes;
1074
              imports = List.map (rename_import f_node f_var) c.imports;
1075
            })
1076
      nd.node_spec
1077
  in
1078
  let annot = rename_annots f_node f_var nd.node_annot in
1079
  {
1080
    node_id = f_node nd.node_id;
1081
    node_type = nd.node_type;
1082
    node_clock = nd.node_clock;
1083
    node_inputs = inputs;
1084
    node_outputs = outputs;
1085
    node_locals = locals;
1086
    node_gencalls = gen_calls;
1087
    node_checks;
1088
    node_asserts;
1089
    node_stmts;
1090
    node_dec_stateless = nd.node_dec_stateless;
1091
    node_stateless = nd.node_stateless;
1092
    node_spec = spec;
1093
    node_annot = annot;
1094
    node_iscontract = nd.node_iscontract;
1095
  }
1096

    
1097
let rename_const f_const c = { c with const_id = f_const c.const_id }
1098

    
1099
let rename_typedef f_var t =
1100
  match t.tydef_desc with
1101
  | Tydec_enum tags ->
1102
    { t with tydef_desc = Tydec_enum (List.map f_var tags) }
1103
  | _ ->
1104
    t
1105

    
1106
let rename_prog f_node f_var f_const prog =
1107
  List.rev
1108
    (List.fold_left
1109
       (fun accu top ->
1110
         (match top.top_decl_desc with
1111
         | Node nd ->
1112
           { top with top_decl_desc = Node (rename_node f_node f_var nd) }
1113
         | Const c ->
1114
           { top with top_decl_desc = Const (rename_const f_const c) }
1115
         | TypeDef tdef ->
1116
           { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
1117
         | ImportedNode _ | Include _ | Open _ ->
1118
           top)
1119
         :: accu)
1120
       [] prog)
1121

    
1122
(* Applies the renaming function [fvar] to every rhs only when the corresponding
1123
   lhs satisfies predicate [pvar] *)
1124
let eq_replace_rhs_var pvar fvar eq =
1125
  let pvar l = List.exists pvar l in
1126
  let rec replace lhs rhs =
1127
    {
1128
      rhs with
1129
      expr_desc =
1130
        (match lhs with
1131
        | [] ->
1132
          assert false
1133
        | [ _ ] ->
1134
          if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
1135
          else rhs.expr_desc
1136
        | _ -> (
1137
          match rhs.expr_desc with
1138
          | Expr_tuple tl ->
1139
            Expr_tuple (List.map2 (fun v e -> replace [ v ] e) lhs tl)
1140
          | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs
1141
            ->
1142
            let args = expr_list_of_expr arg in
1143
            Expr_appl
1144
              ( f,
1145
                expr_of_expr_list arg.expr_loc (List.map (replace lhs) args),
1146
                None )
1147
          | Expr_array _
1148
          | Expr_access _
1149
          | Expr_power _
1150
          | Expr_const _
1151
          | Expr_ident _
1152
          | Expr_appl _ ->
1153
            if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
1154
            else rhs.expr_desc
1155
          | Expr_ite (c, t, e) ->
1156
            Expr_ite (replace lhs c, replace lhs t, replace lhs e)
1157
          | Expr_arrow (e1, e2) ->
1158
            Expr_arrow (replace lhs e1, replace lhs e2)
1159
          | Expr_fby (e1, e2) ->
1160
            Expr_fby (replace lhs e1, replace lhs e2)
1161
          | Expr_pre e' ->
1162
            Expr_pre (replace lhs e')
1163
          | Expr_when (e', i, l) ->
1164
            let i' = if pvar lhs then fvar i else i in
1165
            Expr_when (replace lhs e', i', l)
1166
          | Expr_merge (i, hl) ->
1167
            let i' = if pvar lhs then fvar i else i in
1168
            Expr_merge (i', List.map (fun (t, h) -> t, replace lhs h) hl)));
1169
    }
1170
  in
1171
  { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
1172

    
1173
(**********************************************************************)
1174
(* Pretty printers *)
1175

    
1176
let pp_decl_type fmt tdecl =
1177
  match tdecl.top_decl_desc with
1178
  | Node nd ->
1179
    fprintf fmt "%s: " nd.node_id;
1180
    Utils.reset_names ();
1181
    fprintf fmt "%a" Types.print_ty nd.node_type
1182
  | ImportedNode ind ->
1183
    fprintf fmt "%s: " ind.nodei_id;
1184
    Utils.reset_names ();
1185
    fprintf fmt "%a" Types.print_ty ind.nodei_type
1186
  | Const _ | Include _ | Open _ | TypeDef _ ->
1187
    ()
1188

    
1189
let pp_prog_type fmt tdecl_list =
1190
  Utils.Format.(
1191
    pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_type fmt tdecl_list)
1192

    
1193
let pp_decl_clock fmt cdecl =
1194
  match cdecl.top_decl_desc with
1195
  | Node nd ->
1196
    fprintf fmt "%s: " nd.node_id;
1197
    Utils.reset_names ();
1198
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
1199
  | ImportedNode ind ->
1200
    fprintf fmt "%s: " ind.nodei_id;
1201
    Utils.reset_names ();
1202
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
1203
  | Const _ | Include _ | Open _ | TypeDef _ ->
1204
    ()
1205

    
1206
let pp_prog_clock fmt prog = Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
1207

    
1208
(* filling node table with internal functions *)
1209
let vdecls_of_typ_ck cpt ty =
1210
  let loc = Location.dummy_loc in
1211
  List.map
1212
    (fun _ ->
1213
      incr cpt;
1214
      let name = sprintf "_var_%d" !cpt in
1215
      mkvar_decl loc
1216
        (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
1217
    (Types.type_list_of_type ty)
1218

    
1219
let mk_internal_node id =
1220
  let spec = None in
1221
  let ty = Env.lookup_value Basic_library.type_env id in
1222
  let ck = Env.lookup_value Basic_library.clock_env id in
1223
  let tin, tout = Types.split_arrow ty in
1224
  (*eprintf "internal fun %s: %d -> %d@." id (List.length
1225
    (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
1226
  let cpt = ref (-1) in
1227
  mktop
1228
    (ImportedNode
1229
       {
1230
         nodei_id = id;
1231
         nodei_type = ty;
1232
         nodei_clock = ck;
1233
         nodei_inputs = vdecls_of_typ_ck cpt tin;
1234
         nodei_outputs = vdecls_of_typ_ck cpt tout;
1235
         nodei_stateless = Types.get_static_value ty <> None;
1236
         nodei_spec = spec;
1237
         (* nodei_annot = []; *)
1238
         nodei_prototype = None;
1239
         nodei_in_lib = [];
1240
       })
1241

    
1242
let add_internal_funs () =
1243
  List.iter
1244
    (fun id ->
1245
      let nd = mk_internal_node id in
1246
      Hashtbl.add node_table id nd)
1247
    Basic_library.internal_funs
1248

    
1249
(* Replace any occurence of a var in vars_to_replace by its associated
1250
   expression in defs until e does not contain any such variables *)
1251
let rec substitute_expr vars_to_replace defs e =
1252
  let se = substitute_expr vars_to_replace defs in
1253
  {
1254
    e with
1255
    expr_desc =
1256
      (let ed = e.expr_desc in
1257
       match ed with
1258
       | Expr_const _ ->
1259
         ed
1260
       | Expr_array el ->
1261
         Expr_array (List.map se el)
1262
       | Expr_access (e1, d) ->
1263
         Expr_access (se e1, d)
1264
       | Expr_power (e1, d) ->
1265
         Expr_power (se e1, d)
1266
       | Expr_tuple el ->
1267
         Expr_tuple (List.map se el)
1268
       | Expr_ite (c, t, e) ->
1269
         Expr_ite (se c, se t, se e)
1270
       | Expr_arrow (e1, e2) ->
1271
         Expr_arrow (se e1, se e2)
1272
       | Expr_fby (e1, e2) ->
1273
         Expr_fby (se e1, se e2)
1274
       | Expr_pre e' ->
1275
         Expr_pre (se e')
1276
       | Expr_when (e', i, l) ->
1277
         Expr_when (se e', i, l)
1278
       | Expr_merge (i, hl) ->
1279
         Expr_merge (i, List.map (fun (t, h) -> t, se h) hl)
1280
       | Expr_appl (i, e', i') ->
1281
         Expr_appl (i, se e', i')
1282
       | Expr_ident i ->
1283
         if List.exists (fun v -> v.var_id = i) vars_to_replace then
1284
           let eq_i eq = eq.eq_lhs = [ i ] in
1285
           if List.exists eq_i defs then
1286
             let sub = List.find eq_i defs in
1287
             let sub' = se sub.eq_rhs in
1288
             sub'.expr_desc
1289
           else assert false
1290
         else ed);
1291
  }
1292

    
1293
let expr_to_eexpr expr =
1294
  {
1295
    eexpr_tag = expr.expr_tag;
1296
    eexpr_qfexpr = expr;
1297
    eexpr_quantifiers = [];
1298
    eexpr_name = None;
1299
    eexpr_type = expr.expr_type;
1300
    eexpr_clock = expr.expr_clock;
1301
    eexpr_loc = expr.expr_loc (*eexpr_normalized = None*);
1302
  }
1303

    
1304
(* and expr_desc_to_eexpr_desc expr_desc = *)
1305
(*   let conv = expr_to_eexpr in *)
1306
(*   match expr_desc with *)
1307
(*   | Expr_const c -> EExpr_const (match c with *)
1308
(*     | Const_int x -> EConst_int x  *)
1309
(*     | Const_real x -> EConst_real x  *)
1310
(*     | Const_float x -> EConst_float x  *)
1311
(*     | Const_tag x -> EConst_tag x  *)
1312
(*     | _ -> assert false *)
1313

    
1314
(*   ) *)
1315
(*   | Expr_ident i -> EExpr_ident i *)
1316
(*   | Expr_tuple el -> EExpr_tuple (List.map conv el) *)
1317

    
1318
(*   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)  *)
1319
(*   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *)
1320
(*   | Expr_pre e' -> EExpr_pre (conv e') *)
1321
(*   | Expr_appl (i, e', i') ->  *)
1322
(*     EExpr_appl  *)
1323
(*       (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *)
1324

    
1325
(*   | Expr_when _ *)
1326
(*   | Expr_merge _ -> assert false *)
1327
(*   | Expr_array _  *)
1328
(*   | Expr_access _  *)
1329
(*   | Expr_power _  -> assert false *)
1330
(*   | Expr_ite (c, t, e) -> assert false  *)
1331
(*   | _ -> assert false *)
1332

    
1333
let rec get_expr_calls nodes e =
1334
  let get_calls = get_expr_calls nodes in
1335
  match e.expr_desc with
1336
  | Expr_const _ | Expr_ident _ ->
1337
    Utils.ISet.empty
1338
  | Expr_tuple el | Expr_array el ->
1339
    List.fold_left
1340
      (fun accu e -> Utils.ISet.union accu (get_calls e))
1341
      Utils.ISet.empty el
1342
  | Expr_pre e1 | Expr_when (e1, _, _) | Expr_access (e1, _) | Expr_power (e1, _)
1343
    ->
1344
    get_calls e1
1345
  | Expr_ite (c, t, e) ->
1346
    Utils.ISet.union
1347
      (Utils.ISet.union (get_calls c) (get_calls t))
1348
      (get_calls e)
1349
  | Expr_arrow (e1, e2) | Expr_fby (e1, e2) ->
1350
    Utils.ISet.union (get_calls e1) (get_calls e2)
1351
  | Expr_merge (_, hl) ->
1352
    List.fold_left
1353
      (fun accu (_, h) -> Utils.ISet.union accu (get_calls h))
1354
      Utils.ISet.empty hl
1355
  | Expr_appl (i, e', _) ->
1356
    if Basic_library.is_expr_internal_fun e then get_calls e'
1357
    else
1358
      let calls = Utils.ISet.add i (get_calls e') in
1359
      let test n =
1360
        match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false
1361
      in
1362
      if List.exists test nodes then
1363
        match (List.find test nodes).top_decl_desc with
1364
        | Node nd ->
1365
          Utils.ISet.union (get_node_calls nodes nd) calls
1366
        | _ ->
1367
          assert false
1368
      else calls
1369

    
1370
and get_eq_calls nodes eq = get_expr_calls nodes eq.eq_rhs
1371

    
1372
and get_aut_handler_calls nodes h =
1373
  List.fold_left
1374
    (fun accu stmt ->
1375
      match stmt with
1376
      | Eq eq ->
1377
        Utils.ISet.union (get_eq_calls nodes eq) accu
1378
      | Aut aut' ->
1379
        Utils.ISet.union (get_aut_calls nodes aut') accu)
1380
    Utils.ISet.empty h.hand_stmts
1381

    
1382
and get_aut_calls nodes aut =
1383
  List.fold_left
1384
    (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)
1385
    Utils.ISet.empty aut.aut_handlers
1386

    
1387
and get_node_calls nodes node =
1388
  let eqs, auts = get_node_eqs node in
1389
  let aut_calls =
1390
    List.fold_left
1391
      (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)
1392
      Utils.ISet.empty auts
1393
  in
1394
  List.fold_left
1395
    (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)
1396
    aut_calls eqs
1397

    
1398
let get_expr_vars e =
1399
  let rec get_expr_vars vars e = get_expr_desc_vars vars e.expr_desc
1400
  and get_expr_desc_vars vars expr_desc =
1401
    (*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr
1402
      Location.dummy_loc expr_desc);*)
1403
    match expr_desc with
1404
    | Expr_const _ ->
1405
      vars
1406
    | Expr_ident x ->
1407
      Utils.ISet.add x vars
1408
    | Expr_tuple el | Expr_array el ->
1409
      List.fold_left get_expr_vars vars el
1410
    | Expr_pre e1 ->
1411
      get_expr_vars vars e1
1412
    | Expr_when (e1, c, _) ->
1413
      get_expr_vars (Utils.ISet.add c vars) e1
1414
    | Expr_access (e1, d) | Expr_power (e1, d) ->
1415
      List.fold_left get_expr_vars vars [ e1; expr_of_dimension d ]
1416
    | Expr_ite (c, t, e) ->
1417
      List.fold_left get_expr_vars vars [ c; t; e ]
1418
    | Expr_arrow (e1, e2) | Expr_fby (e1, e2) ->
1419
      List.fold_left get_expr_vars vars [ e1; e2 ]
1420
    | Expr_merge (c, hl) ->
1421
      List.fold_left
1422
        (fun vars (_, h) -> get_expr_vars vars h)
1423
        (Utils.ISet.add c vars) hl
1424
    | Expr_appl (_, arg, None) ->
1425
      get_expr_vars vars arg
1426
    | Expr_appl (_, arg, Some r) ->
1427
      List.fold_left get_expr_vars vars [ arg; r ]
1428
  in
1429
  get_expr_vars Utils.ISet.empty e
1430

    
1431
(* let rec expr_has_arrows e =
1432
 *   expr_desc_has_arrows e.expr_desc
1433
 * and expr_desc_has_arrows expr_desc =
1434
 *   match expr_desc with
1435
 *   | Expr_const _
1436
 *   | Expr_ident _ -> false
1437
 *   | Expr_tuple el
1438
 *   | Expr_array el -> List.exists expr_has_arrows el
1439
 *   | Expr_pre e1
1440
 *   | Expr_when (e1, _, _)
1441
 *   | Expr_access (e1, _)
1442
 *   | Expr_power (e1, _) -> expr_has_arrows e1
1443
 *   | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
1444
 *   | Expr_arrow _
1445
 *   | Expr_fby _ -> true
1446
 *   | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1447
 *   | Expr_appl (_, e', _) -> expr_has_arrows e'
1448
 *
1449
 * and eq_has_arrows eq =
1450
 *   expr_has_arrows eq.eq_rhs
1451
 * 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
1452
 * and node_has_arrows node =
1453
 *   let eqs, auts = get_node_eqs node in
1454
 *   List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts *)
1455

    
1456
let rec expr_contains_expr expr_tag expr =
1457
  let search = expr_contains_expr expr_tag in
1458
  expr.expr_tag = expr_tag
1459
  ||
1460
  match expr.expr_desc with
1461
  | Expr_const _ ->
1462
    false
1463
  | Expr_array el ->
1464
    List.exists search el
1465
  | Expr_access (e1, _) | Expr_power (e1, _) ->
1466
    search e1
1467
  | Expr_tuple el ->
1468
    List.exists search el
1469
  | Expr_ite (c, t, e) ->
1470
    List.exists search [ c; t; e ]
1471
  | Expr_arrow (e1, e2) | Expr_fby (e1, e2) ->
1472
    List.exists search [ e1; e2 ]
1473
  | Expr_pre e' | Expr_when (e', _, _) ->
1474
    search e'
1475
  | Expr_merge (_, hl) ->
1476
    List.exists (fun (_, h) -> search h) hl
1477
  | Expr_appl (_, e', None) ->
1478
    search e'
1479
  | Expr_appl (_, e', Some e'') ->
1480
    List.exists search [ e'; e'' ]
1481
  | Expr_ident _ ->
1482
    false
1483

    
1484
(* Generate a new local [node] variable *)
1485
let cpt_fresh = ref 0
1486

    
1487
let reset_cpt_fresh () = cpt_fresh := 0
1488

    
1489
let mk_fresh_var (parentid, ctx_env) loc ty ck =
1490
  let rec aux () =
1491
    incr cpt_fresh;
1492
    let s = Printf.sprintf "__%s_%d" parentid !cpt_fresh in
1493
    if List.exists (fun v -> v.var_id = s) ctx_env then aux ()
1494
    else
1495
      {
1496
        var_id = s;
1497
        var_orig = false;
1498
        var_dec_type = dummy_type_dec;
1499
        var_dec_clock = dummy_clock_dec;
1500
        var_dec_const = false;
1501
        var_dec_value = None;
1502
        var_parent_nodeid = Some parentid;
1503
        var_type = ty;
1504
        var_clock = ck;
1505
        var_loc = loc;
1506
      }
1507
  in
1508
  aux ()
1509

    
1510
let find_eq xl eqs =
1511
  let rec aux accu eqs =
1512
    match eqs with
1513
    | [] ->
1514
      Format.eprintf "Looking for variables %a in the following equations@.%a@."
1515
        (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v))
1516
        xl Printers.pp_node_eqs eqs;
1517
      assert false
1518
    | hd :: tl ->
1519
      if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu @ tl
1520
      else aux (hd :: accu) tl
1521
  in
1522
  aux [] eqs
1523

    
1524
let get_node name prog =
1525
  let node_opt =
1526
    List.fold_left
1527
      (fun res top ->
1528
        match res, top.top_decl_desc with
1529
        | Some _, _ ->
1530
          res
1531
        | None, Node nd ->
1532
          (* Format.eprintf "Checking node %s = %s: %b@." nd.node_id name
1533
             (nd.node_id = name); *)
1534
          if nd.node_id = name then Some nd else res
1535
        | _ ->
1536
          None)
1537
      None prog
1538
  in
1539
  try Utils.desome node_opt with Utils.DeSome -> raise Not_found
1540

    
1541
(* Pushing negations in expression. Subtitute operators whenever possible *)
1542
let rec push_negations ?(neg = false) e =
1543
  let res =
1544
    let pn = push_negations in
1545
    let map desc =
1546
      (* Keeping clock and type info *)
1547
      let new_e = mkexpr e.expr_loc desc in
1548
      { new_e with expr_type = e.expr_type; expr_clock = e.expr_clock }
1549
    in
1550
    match e.expr_desc with
1551
    | Expr_ite (g, t, e) ->
1552
      if neg then map (Expr_ite (pn g, pn e, pn t))
1553
      else map (Expr_ite (pn g, pn t, pn e))
1554
    | Expr_tuple t ->
1555
      map (Expr_tuple (List.map (pn ~neg) t))
1556
    | Expr_arrow (e1, e2) ->
1557
      map (Expr_arrow (pn ~neg e1, pn ~neg e2))
1558
    | Expr_fby (e1, e2) ->
1559
      map (Expr_fby (pn ~neg e1, pn ~neg e2))
1560
    | Expr_pre e ->
1561
      map (Expr_pre (pn ~neg e))
1562
    | Expr_appl (op, e', None) when op = "not" ->
1563
      if neg then push_negations ~neg:false e' else push_negations ~neg:true e'
1564
    | Expr_appl (op, e', None)
1565
      when List.mem op (Basic_library.bool_funs @ Basic_library.rel_funs) -> (
1566
      match op with
1567
      | "&&" ->
1568
        map (Expr_appl ((if neg then "||" else op), pn ~neg e', None))
1569
      | "||" ->
1570
        map (Expr_appl ((if neg then "&&" else op), pn ~neg e', None))
1571
      (* TODO xor/equi/impl *)
1572
      | "<" ->
1573
        map (Expr_appl ((if neg then ">=" else op), pn e', None))
1574
      | ">" ->
1575
        map (Expr_appl ((if neg then "<=" else op), pn e', None))
1576
      | "<=" ->
1577
        map (Expr_appl ((if neg then ">" else op), pn e', None))
1578
      | ">=" ->
1579
        map (Expr_appl ((if neg then "<" else op), pn e', None))
1580
      | "!=" ->
1581
        map (Expr_appl ((if neg then "=" else op), pn e', None))
1582
      | "=" ->
1583
        map (Expr_appl ((if neg then "!=" else op), pn e', None))
1584
      | _ ->
1585
        assert false)
1586
    | Expr_const c ->
1587
      if neg then map (Expr_const (const_negation c)) else e
1588
    | Expr_ident _ ->
1589
      if neg then mkpredef_call e.expr_loc "not" [ e ] else e
1590
    | Expr_appl _ ->
1591
      if neg then mkpredef_call e.expr_loc "not" [ e ] else e
1592
    | _ ->
1593
      assert false
1594
    (* no array, array access, power or merge/when *)
1595
  in
1596
  res
1597

    
1598
let rec add_pre_expr vars e =
1599
  let ap = add_pre_expr vars in
1600
  let desc =
1601
    match e.expr_desc with
1602
    | Expr_ite (g, t, e) ->
1603
      Expr_ite (ap g, ap t, ap e)
1604
    | Expr_tuple t ->
1605
      Expr_tuple (List.map ap t)
1606
    | Expr_arrow (e1, e2) ->
1607
      Expr_arrow (ap e1, ap e2)
1608
    | Expr_fby (e1, e2) ->
1609
      Expr_fby (ap e1, ap e2)
1610
    | Expr_pre e ->
1611
      Expr_pre (ap e)
1612
    | Expr_appl (op, e, opt) ->
1613
      Expr_appl (op, ap e, opt)
1614
    | Expr_const _ ->
1615
      e.expr_desc
1616
    | Expr_ident id ->
1617
      if List.mem id vars then Expr_pre e else e.expr_desc
1618
    | _ ->
1619
      assert false
1620
    (* no array, array access, power or merge/when yet *)
1621
  in
1622
  let new_e = mkexpr e.expr_loc desc in
1623
  { new_e with expr_type = e.expr_type; expr_clock = e.expr_clock }
1624

    
1625
let mk_eq l e1 e2 = mkpredef_call l "=" [ e1; e2 ]
1626

    
1627
let rec partial_eval e =
1628
  let pa = partial_eval in
1629
  let edesc =
1630
    match e.expr_desc with
1631
    | Expr_const _ ->
1632
      e.expr_desc
1633
    | Expr_ident _ ->
1634
      e.expr_desc
1635
    | Expr_ite (g, t, e) -> (
1636
      let g, t, e = pa g, pa t, pa e in
1637
      match g.expr_desc with
1638
      | Expr_const (Const_tag tag) when tag = tag_true ->
1639
        t.expr_desc
1640
      | Expr_const (Const_tag tag) when tag = tag_false ->
1641
        e.expr_desc
1642
      | _ ->
1643
        Expr_ite (g, t, e))
1644
    | Expr_tuple t ->
1645
      Expr_tuple (List.map pa t)
1646
    | Expr_arrow (e1, e2) ->
1647
      Expr_arrow (pa e1, pa e2)
1648
    | Expr_fby (e1, e2) ->
1649
      Expr_fby (pa e1, pa e2)
1650
    | Expr_pre e ->
1651
      Expr_pre (pa e)
1652
    | Expr_appl (op, args, opt) ->
1653
      let args = pa args in
1654
      if Basic_library.is_expr_internal_fun e then
1655
        Basic_library.partial_eval op args opt
1656
      else Expr_appl (op, args, opt)
1657
    | Expr_array el ->
1658
      Expr_array (List.map pa el)
1659
    | Expr_access (e, d) ->
1660
      Expr_access (pa e, d)
1661
    | Expr_power (e, d) ->
1662
      Expr_power (pa e, d)
1663
    | Expr_when (e, id, l) ->
1664
      Expr_when (pa e, id, l)
1665
    | Expr_merge (id, gl) ->
1666
      Expr_merge (id, List.map (fun (l, e) -> l, pa e) gl)
1667
  in
1668
  { e with expr_desc = edesc }
1669

    
1670
(* Local Variables: *)
1671
(* compile-command:"make -C .." *)
1672
(* End: *)
(15-15/66)