Project

General

Profile

Download (49.5 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 Utils
13
open Format
14
open Lustre_types
15
open Machine_code_types
16
(*open Dimension*)
17

    
18
module VDeclModule = struct
19
  (* Node module *)
20
  type t = var_decl
21

    
22
  let compare v1 v2 = compare v1.var_id v2.var_id
23
end
24

    
25
module VMap = Map.Make (VDeclModule)
26

    
27
module VSet : sig
28
  include Set.S
29

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

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

    
37
  let pp fmt s =
38
    Format.fprintf fmt "{@[%a}@]" (pp_comma_list Printers.pp_var) (elements s)
39

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

    
45
let dummy_type_dec = { ty_dec_desc = Tydec_any; ty_dec_loc = Location.dummy }
46

    
47
let dummy_clock_dec = { ck_dec_desc = Ckdec_any; ck_dec_loc = Location.dummy }
48

    
49
(************************************************************)
50
(* *)
51

    
52
let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc }
53

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

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

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

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

    
99
let var_decl_of_const ?(parentid = None) c =
100
  {
101
    var_id = c.const_id;
102
    var_orig = true;
103
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
104
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
105
    var_dec_const = true;
106
    var_dec_value = None;
107
    var_parent_nodeid = parentid;
108
    var_type = c.const_type;
109
    var_clock = Clocks.new_var false;
110
    var_loc = c.const_loc;
111
    var_is_contract = false;
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 top_decl_loc top_decl_owner top_decl_itf top_decl_desc =
125
  {
126
    top_decl_desc;
127
    top_decl_loc;
128
    top_decl_owner;
129
    top_decl_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;
196
    proof = None
197
  }
198

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

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

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

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

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

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

    
247
let merge_proofs p1 p2 =
248
  let merge_proofs p1 p2 = match p1, p2 with
249
    | Kinduction k1, Kinduction k2 ->
250
      Kinduction (max k1 k2)
251
  in
252
  match p1, p2 with
253
  | Some p1, Some p2 -> Some (merge_proofs p1 p2)
254
  | Some p, None | None, Some p -> Some p
255
  | None, None -> None
256

    
257
let merge_contracts ann1 ann2 =
258
  (* keeping the first item loc *)
259
  {
260
    consts = ann1.consts @ ann2.consts;
261
    locals = ann1.locals @ ann2.locals;
262
    stmts = ann1.stmts @ ann2.stmts;
263
    assume = ann1.assume @ ann2.assume;
264
    guarantees = ann1.guarantees @ ann2.guarantees;
265
    modes = ann1.modes @ ann2.modes;
266
    imports = ann1.imports @ ann2.imports;
267
    spec_loc = ann1.spec_loc;
268
    proof = merge_proofs ann1.proof ann2.proof
269
  }
270

    
271
let mkeexpr loc expr =
272
  {
273
    eexpr_tag = Utils.new_tag ();
274
    eexpr_qfexpr = expr;
275
    eexpr_quantifiers = [];
276
    eexpr_name = None;
277
    eexpr_type = Types.new_var ();
278
    eexpr_clock = Clocks.new_var true;
279
    eexpr_loc = loc;
280
  }
281

    
282
let extend_eexpr q e = { e with eexpr_quantifiers = q @ e.eexpr_quantifiers }
283

    
284
(* let mkepredef_call loc funname args = mkeexpr loc (EExpr_appl (funname,
285
   mkeexpr loc (EExpr_tuple args), None))
286

    
287
   let mkepredef_unary_call loc funname arg = mkeexpr loc (EExpr_appl (funname,
288
   arg, None)) *)
289

    
290
let merge_expr_annot ann1 ann2 =
291
  match ann1, ann2 with
292
  | None, None ->
293
    assert false
294
  | Some _, None ->
295
    ann1
296
  | None, Some _ ->
297
    ann2
298
  | Some ann1, Some ann2 ->
299
    Some { annots = ann1.annots @ ann2.annots; annot_loc = ann1.annot_loc }
300

    
301
let update_expr_annot node_id e annot =
302
  List.iter
303
    (fun (key, _) -> Annotations.add_expr_ann node_id e.expr_tag key)
304
    annot.annots;
305
  e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
306
  e
307

    
308
let mkinstr ?lustre_eq ?(instr_spec = []) instr_desc =
309
  { instr_desc; (* lustre_expr = lustre_expr; *)
310
                instr_spec; lustre_eq }
311

    
312
let get_instr_desc i = i.instr_desc
313

    
314
let update_instr_desc i id = { i with instr_desc = id }
315

    
316
(***********************************************************)
317
(* Fast access to nodes, by name *)
318
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
319

    
320
let consts_table = Hashtbl.create 30
321

    
322
let pp_node_table fmt () =
323
  Format.fprintf fmt "{ /* node table */@.";
324
  Hashtbl.iter
325
    (fun id nd -> Format.fprintf fmt "%s |-> %a" id Printers.pp_short_decl nd)
326
    node_table;
327
  Format.fprintf fmt "}@."
328

    
329
let pp_consts_table fmt () =
330
  Format.fprintf fmt "{ /* consts table */@.";
331
  Hashtbl.iter
332
    (fun id const ->
333
      Format.fprintf
334
        fmt
335
        "%s |-> %a"
336
        id
337
        Printers.pp_const_decl
338
        (const_of_top const))
339
    consts_table;
340
  Format.fprintf fmt "}@."
341

    
342
let node_name td =
343
  match td.top_decl_desc with
344
  | Node nd ->
345
    nd.node_id
346
  | ImportedNode nd ->
347
    nd.nodei_id
348
  | _ ->
349
    assert false
350

    
351
let is_generic_node td =
352
  match td.top_decl_desc with
353
  | Node nd ->
354
    List.exists (fun v -> v.var_dec_const) nd.node_inputs
355
  | ImportedNode nd ->
356
    List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
357
  | _ ->
358
    assert false
359

    
360
let node_inputs td =
361
  match td.top_decl_desc with
362
  | Node nd ->
363
    nd.node_inputs
364
  | ImportedNode nd ->
365
    nd.nodei_inputs
366
  | _ ->
367
    assert false
368

    
369
let node_from_name id = Hashtbl.find node_table id
370

    
371
let update_node id top = Hashtbl.replace node_table id top
372

    
373
let is_imported_node td =
374
  match td.top_decl_desc with
375
  | Node _ ->
376
    false
377
  | ImportedNode _ ->
378
    true
379
  | _ ->
380
    assert false
381

    
382
let is_node_contract nd =
383
  match nd.node_spec with Some (Contract _) -> true | _ -> false
384

    
385
let get_node_contract nd =
386
  match nd.node_spec with Some (Contract c) -> c | _ -> assert false
387

    
388
let is_contract td =
389
  match td.top_decl_desc with Node nd -> is_node_contract nd | _ -> false
390

    
391
(* alias and type definition table *)
392

    
393
let mktop = mktop_decl Location.dummy !Options.dest_dir false
394

    
395
let top_int_type = mktop (TypeDef { tydef_id = "int"; tydef_desc = Tydec_int })
396

    
397
let top_bool_type =
398
  mktop (TypeDef { tydef_id = "bool"; tydef_desc = Tydec_bool })
399

    
400
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc =
401
   Tydec_float}) *)
402
let top_real_type =
403
  mktop (TypeDef { tydef_id = "real"; tydef_desc = Tydec_real })
404

    
405
let type_table =
406
  Utils.create_hashtable
407
    20
408
    [
409
      Tydec_int, top_int_type;
410
      Tydec_bool, top_bool_type;
411
      (* Tydec_float, top_float_type; *)
412
      Tydec_real, top_real_type;
413
    ]
414

    
415
let pp_type_table fmt () =
416
  Format.fprintf fmt "{ /* type table */@.";
417
  Hashtbl.iter
418
    (fun tydec tdef ->
419
      Format.fprintf
420
        fmt
421
        "%a |-> %a"
422
        Printers.pp_var_type_dec_desc
423
        tydec
424
        Printers.pp_typedef
425
        (typedef_of_top tdef))
426
    type_table;
427
  Format.fprintf fmt "}@."
428

    
429
let rec is_user_type typ =
430
  match typ with
431
  | Tydec_int
432
  | Tydec_bool
433
  | Tydec_real (* | Tydec_float *)
434
  | Tydec_any
435
  | Tydec_const _ ->
436
    false
437
  | Tydec_clock typ' ->
438
    is_user_type typ'
439
  | _ ->
440
    true
441

    
442
let get_repr_type typ =
443
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
444
  if is_user_type typ_def then typ else typ_def
445

    
446
let rec coretype_equal ty1 ty2 =
447
  let res =
448
    match ty1, ty2 with
449
    | Tydec_any, _ | _, Tydec_any ->
450
      assert false
451
    | Tydec_const _, Tydec_const _ ->
452
      get_repr_type ty1 = get_repr_type ty2
453
    | Tydec_const _, _ ->
454
      let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc in
455
      (not (is_user_type ty1')) && coretype_equal ty1' ty2
456
    | _, Tydec_const _ ->
457
      coretype_equal ty2 ty1
458
    | Tydec_int, Tydec_int
459
    | Tydec_real, Tydec_real
460
    (* | Tydec_float , Tydec_float *)
461
    | Tydec_bool, Tydec_bool ->
462
      true
463
    | Tydec_clock ty1, Tydec_clock ty2 ->
464
      coretype_equal ty1 ty2
465
    | Tydec_array (d1, ty1), Tydec_array (d2, ty2) ->
466
      Dimension.equal d1 d2 && coretype_equal ty1 ty2
467
    | Tydec_enum tl1, Tydec_enum tl2 ->
468
      List.sort compare tl1 = List.sort compare tl2
469
    | Tydec_struct fl1, Tydec_struct fl2 ->
470
      List.length fl1 = List.length fl2
471
      && List.for_all2
472
           (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
473
           (List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl1)
474
           (List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl2)
475
    | _ ->
476
      false
477
  in
478
  (*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc
479
    ty1 Printers.pp_var_type_dec_desc ty2 res;*)
480
  res
481

    
482
let tag_default = "default"
483

    
484
let const_is_bool c =
485
  match c with Const_tag t -> t = tag_true || t = tag_false | _ -> false
486

    
487
(* Computes the negation of a boolean constant *)
488
let const_negation c =
489
  assert (const_is_bool c);
490
  match c with
491
  | Const_tag t when t = tag_true ->
492
    Const_tag tag_false
493
  | _ ->
494
    Const_tag tag_true
495

    
496
let const_or c1 c2 =
497
  assert (const_is_bool c1 && const_is_bool c2);
498
  match c1, c2 with
499
  | Const_tag t1, _ when t1 = tag_true ->
500
    c1
501
  | _, Const_tag t2 when t2 = tag_true ->
502
    c2
503
  | _ ->
504
    Const_tag tag_false
505

    
506
let const_and c1 c2 =
507
  assert (const_is_bool c1 && const_is_bool c2);
508
  match c1, c2 with
509
  | Const_tag t1, _ when t1 = tag_false ->
510
    c1
511
  | _, Const_tag t2 when t2 = tag_false ->
512
    c2
513
  | _ ->
514
    Const_tag tag_true
515

    
516
let const_xor c1 c2 =
517
  assert (const_is_bool c1 && const_is_bool c2);
518
  match c1, c2 with
519
  | Const_tag t1, Const_tag t2 when t1 <> t2 ->
520
    Const_tag tag_true
521
  | _ ->
522
    Const_tag tag_false
523

    
524
let const_impl c1 c2 =
525
  assert (const_is_bool c1 && const_is_bool c2);
526
  match c1, c2 with
527
  | Const_tag t1, _ when t1 = tag_false ->
528
    Const_tag tag_true
529
  | _, Const_tag t2 when t2 = tag_true ->
530
    Const_tag tag_true
531
  | _ ->
532
    Const_tag tag_false
533

    
534
(* To guarantee uniqueness of tags in enum types *)
535
let tag_table =
536
  Utils.create_hashtable
537
    20
538
    [ tag_true, top_bool_type; tag_false, top_bool_type ]
539

    
540
(* To guarantee uniqueness of fields in struct types *)
541
let field_table = Utils.create_hashtable 20 []
542

    
543
let get_enum_type_tags cty =
544
  (*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
545
  match cty with
546
  | Tydec_bool ->
547
    [ tag_true; tag_false ]
548
  | Tydec_const _ -> (
549
    match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
550
    | Tydec_enum tl ->
551
      tl
552
    | _ ->
553
      assert false)
554
  | _ ->
555
    assert false
556

    
557
let get_struct_type_fields cty =
558
  match cty with
559
  | Tydec_const _ -> (
560
    match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
561
    | Tydec_struct fl ->
562
      fl
563
    | _ ->
564
      assert false)
565
  | _ ->
566
    assert false
567

    
568
let const_of_bool b = Const_tag (if b then tag_true else tag_false)
569

    
570
(* let get_const c = snd (Hashtbl.find consts_table c) *)
571

    
572
let ident_of_expr expr =
573
  match expr.expr_desc with Expr_ident id -> id | _ -> assert false
574

    
575
(* Generate a new ident expression from a declared variable *)
576
let expr_of_vdecl v =
577
  {
578
    expr_tag = Utils.new_tag ();
579
    expr_desc = Expr_ident v.var_id;
580
    expr_type = v.var_type;
581
    expr_clock = v.var_clock;
582
    expr_delay = Delay.new_var ();
583
    expr_annot = None;
584
    expr_loc = v.var_loc;
585
  }
586

    
587
(* Caution, returns an untyped and unclocked expression *)
588
let expr_of_ident id loc =
589
  {
590
    expr_tag = Utils.new_tag ();
591
    expr_desc = Expr_ident id;
592
    expr_type = Types.new_var ();
593
    expr_clock = Clocks.new_var true;
594
    expr_delay = Delay.new_var ();
595
    expr_loc = loc;
596
    expr_annot = None;
597
  }
598

    
599
let is_tuple_expr expr =
600
  match expr.expr_desc with Expr_tuple _ -> true | _ -> false
601

    
602
let expr_list_of_expr expr =
603
  match expr.expr_desc with Expr_tuple elist -> elist | _ -> [ expr ]
604

    
605
let expr_of_expr_list loc elist =
606
  match elist with
607
  | [ t ] ->
608
    { t with expr_loc = loc }
609
  | t :: _ ->
610
    let tlist = List.map (fun e -> e.expr_type) elist in
611
    let clist = List.map (fun e -> e.expr_clock) elist in
612
    {
613
      t with
614
      expr_desc = Expr_tuple elist;
615
      expr_type = Type_predef.type_tuple tlist;
616
      expr_clock = Clock_predef.ck_tuple clist;
617
      expr_tag = Utils.new_tag ();
618
      expr_loc = loc;
619
    }
620
  | _ ->
621
    assert false
622

    
623
let call_of_expr expr =
624
  match expr.expr_desc with
625
  | Expr_appl (f, args, r) ->
626
    f, expr_list_of_expr args, r
627
  | _ ->
628
    assert false
629

    
630
(* Conversion from dimension expr to standard expr, for the purpose of printing,
631
   typing, etc... *)
632
let rec expr_of_dimension dim =
633
  let open Dimension in
634
  let expr =
635
    match dim.dim_desc with
636
    | Dbool b ->
637
      mkexpr dim.dim_loc (Expr_const (const_of_bool b))
638
    | Dint i ->
639
      mkexpr dim.dim_loc (Expr_const (Const_int i))
640
    | Dident id ->
641
      mkexpr dim.dim_loc (Expr_ident id)
642
    | Dite (c, t, e) ->
643
      mkexpr
644
        dim.dim_loc
645
        (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
646
    | Dappl (id, args) ->
647
      mkexpr
648
        dim.dim_loc
649
        (Expr_appl
650
           ( id,
651
             expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args),
652
             None ))
653
    | Dlink dim' ->
654
      expr_of_dimension dim'
655
    | Dvar | Dunivar ->
656
      Format.eprintf
657
        "internal error: Corelang.expr_of_dimension %a@."
658
        Dimension.pp
659
        dim;
660
      assert false
661
  in
662
  { expr with expr_type = Types.new_ty Types.type_int }
663

    
664
let dimension_of_const loc const =
665
  let open Dimension in
666
  match const with
667
  | Const_int i ->
668
    mkdim_int loc i
669
  | Const_tag t when t = tag_true || t = tag_false ->
670
    mkdim_bool loc (t = tag_true)
671
  | _ ->
672
    raise InvalidDimension
673

    
674
(* Conversion from standard expr to dimension expr, for the purpose of injecting
675
   static call arguments into dimension expressions *)
676
let rec dimension_of_expr expr =
677
  let open Dimension in
678
  match expr.expr_desc with
679
  | Expr_const c ->
680
    dimension_of_const expr.expr_loc c
681
  | Expr_ident id ->
682
    mkdim_ident expr.expr_loc id
683
  | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
684
    let k =
685
      Types.get_static_value (Env.lookup_value Basic_library.type_env f)
686
    in
687
    if k = None then raise InvalidDimension;
688
    mkdim_appl
689
      expr.expr_loc
690
      f
691
      (List.map dimension_of_expr (expr_list_of_expr args))
692
  | Expr_ite (i, t, e) ->
693
    mkdim_ite
694
      expr.expr_loc
695
      (dimension_of_expr i)
696
      (dimension_of_expr t)
697
      (dimension_of_expr e)
698
  | _ ->
699
    raise InvalidDimension
700
(* not a simple dimension expression *)
701

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

    
704
let rec is_eq_const c1 c2 =
705
  match c1, c2 with
706
  | Const_real r1, Const_real _ ->
707
    Real.eq r1 r1
708
  | Const_struct lcl1, Const_struct lcl2 ->
709
    List.length lcl1 = List.length lcl2
710
    && List.for_all2
711
         (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2)
712
         lcl1
713
         lcl2
714
  | _ ->
715
    c1 = c2
716

    
717
let rec is_eq_expr e1 e2 =
718
  match e1.expr_desc, e2.expr_desc with
719
  | Expr_const c1, Expr_const c2 ->
720
    is_eq_const c1 c2
721
  | Expr_ident i1, Expr_ident i2 ->
722
    i1 = i2
723
  | Expr_array el1, Expr_array el2 | Expr_tuple el1, Expr_tuple el2 ->
724
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2
725
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') ->
726
    is_eq_expr e1 e1' && is_eq_expr e2 e2'
727
  | Expr_fby (e1, e2), Expr_fby (e1', e2') ->
728
    is_eq_expr e1 e1' && is_eq_expr e2 e2'
729
  | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) ->
730
    is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2
731
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' &&
732
     is_eq_expr e2 e2' *)
733
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
734
  | Expr_pre e, Expr_pre e' ->
735
    is_eq_expr e e'
736
  | Expr_when (e, i, l), Expr_when (e', i', l') ->
737
    l = l' && i = i' && is_eq_expr e e'
738
  | Expr_merge (i, hl), Expr_merge (i', hl') ->
739
    i = i'
740
    && List.for_all2
741
         (fun (t, h) (t', h') -> t = t' && is_eq_expr h h')
742
         (sort_handlers hl)
743
         (sort_handlers hl')
744
  | Expr_appl (i, e, r), Expr_appl (i', e', r') ->
745
    i = i' && r = r' && is_eq_expr e e'
746
  | Expr_power (e1, i1), Expr_power (e2, i2)
747
  | Expr_access (e1, i1), Expr_access (e2, i2) ->
748
    is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
749
  | _ ->
750
    false
751

    
752
let get_node_vars nd = nd.node_inputs @ nd.node_locals @ nd.node_outputs
753

    
754
let mk_new_node_name nd id =
755
  let used_vars = get_node_vars nd in
756
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
757
  mk_new_name used id
758

    
759
let get_var id var_list = List.find (fun v -> v.var_id = id) var_list
760

    
761
let get_node_var id node =
762
  try get_var id (get_node_vars node)
763
  with Not_found ->
764
    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id
765
       node.node_id; *)
766
    raise Not_found
767

    
768
let get_node_eqs =
769
  let get_eqs stmts =
770
    List.fold_right
771
      (fun stmt (res_eq, res_aut) ->
772
        match stmt with
773
        | Eq eq ->
774
          eq :: res_eq, res_aut
775
        | Aut aut ->
776
          res_eq, aut :: res_aut)
777
      stmts
778
      ([], [])
779
  in
780
  let table_eqs = Hashtbl.create 23 in
781
  fun nd ->
782
    try
783
      let old, res = Hashtbl.find table_eqs nd.node_id in
784
      if old == nd.node_stmts then res else raise Not_found
785
    with Not_found ->
786
      let res = get_eqs nd.node_stmts in
787
      Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
788
      res
789

    
790
let get_node_eq id node =
791
  let eqs, _ = get_node_eqs node in
792
  try List.find (fun eq -> List.mem id eq.eq_lhs) eqs
793
  with Not_found -> (* Shall be defined in automata auts *)
794
                    raise Not_found
795

    
796
let get_nodes prog =
797
  List.fold_left
798
    (fun nodes decl ->
799
      match decl.top_decl_desc with
800
      | Node _ ->
801
        decl :: nodes
802
      | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ ->
803
        nodes)
804
    []
805
    prog
806
  |> List.rev
807

    
808
let get_imported_nodes prog =
809
  List.fold_left
810
    (fun nodes decl ->
811
      match decl.top_decl_desc with
812
      | ImportedNode _ ->
813
        decl :: nodes
814
      | Const _ | Node _ | Include _ | Open _ | TypeDef _ ->
815
        nodes)
816
    []
817
    prog
818

    
819
let get_consts prog =
820
  List.fold_right
821
    (fun decl consts ->
822
      match decl.top_decl_desc with
823
      | Const _ ->
824
        decl :: consts
825
      | Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ ->
826
        consts)
827
    prog
828
    []
829

    
830
let get_typedefs prog =
831
  List.fold_right
832
    (fun decl types ->
833
      match decl.top_decl_desc with
834
      | TypeDef _ ->
835
        decl :: types
836
      | Node _ | ImportedNode _ | Include _ | Open _ | Const _ ->
837
        types)
838
    prog
839
    []
840

    
841
let get_dependencies prog =
842
  List.fold_right
843
    (fun decl deps ->
844
      match decl.top_decl_desc with
845
      | Open _ ->
846
        decl :: deps
847
      | Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ ->
848
        deps)
849
    prog
850
    []
851

    
852
let get_node_interface nd =
853
  {
854
    nodei_id = nd.node_id;
855
    nodei_type = nd.node_type;
856
    nodei_clock = nd.node_clock;
857
    nodei_inputs = nd.node_inputs;
858
    nodei_outputs = nd.node_outputs;
859
    nodei_stateless = nd.node_dec_stateless;
860
    nodei_spec = nd.node_spec;
861
    (* nodei_annot = nd.node_annot; *)
862
    nodei_prototype = None;
863
    nodei_in_lib = [];
864
    nodei_iscontract = nd.node_iscontract;
865
  }
866

    
867
(************************************************************************)
868
(* Renaming / Copying *)
869

    
870
let copy_var_decl vdecl =
871
  mkvar_decl
872
    vdecl.var_loc
873
    ~orig:vdecl.var_orig
874
    ( vdecl.var_id,
875
      vdecl.var_dec_type,
876
      vdecl.var_dec_clock,
877
      vdecl.var_dec_const,
878
      vdecl.var_dec_value,
879
      vdecl.var_parent_nodeid )
880

    
881
let copy_const cdecl = { cdecl with const_type = Types.new_var () }
882

    
883
let copy_node nd =
884
  {
885
    nd with
886
    node_type = Types.new_var ();
887
    node_clock = Clocks.new_var true;
888
    node_inputs = List.map copy_var_decl nd.node_inputs;
889
    node_outputs = List.map copy_var_decl nd.node_outputs;
890
    node_locals = List.map copy_var_decl nd.node_locals;
891
    node_gencalls = [];
892
    node_checks = [];
893
    node_stateless = None;
894
  }
895

    
896
let copy_top top =
897
  match top.top_decl_desc with
898
  | Node nd ->
899
    { top with top_decl_desc = Node (copy_node nd) }
900
  | Const c ->
901
    { top with top_decl_desc = Const (copy_const c) }
902
  | _ ->
903
    top
904

    
905
let copy_prog top_list = List.map copy_top top_list
906

    
907
let rec rename_static rename cty =
908
  match cty with
909
  | Tydec_array (d, cty') ->
910
    Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
911
  | Tydec_clock cty ->
912
    Tydec_clock (rename_static rename cty)
913
  | Tydec_struct fl ->
914
    Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
915
  | _ ->
916
    cty
917

    
918
let rename_carrier rename cck =
919
  match cck with
920
  | Ckdec_bool cl ->
921
    Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
922
  | _ ->
923
    cck
924

    
925
(*Format.eprintf "Types.rename_static %a = %a@." pp ty pp res; res*)
926

    
927
(* applies the renaming function [fvar] to all variables of expression [expr] *)
928
(* let rec expr_replace_var fvar expr = *)
929
(*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
930

    
931
(* and expr_desc_replace_var fvar expr_desc = *)
932
(*   match expr_desc with *)
933
(*   | Expr_const _ -> expr_desc *)
934
(*   | Expr_ident i -> Expr_ident (fvar i) *)
935
(*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
936
(*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
937
(*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
938
(*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
939
(* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var
940
   fvar t, expr_replace_var fvar e) *)
941
(* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1,
942
   expr_replace_var fvar e2) *)
943
(* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var
944
   fvar e2) *)
945
(*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
946
(*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
947
(* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t,
948
   expr_replace_var fvar h)) hl) *)
949
(* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e',
950
   Utils.option_map (expr_replace_var fvar) i') *)
951

    
952
let rec rename_expr f_node f_var expr =
953
  { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
954

    
955
and rename_expr_desc f_node f_var expr_desc =
956
  let re = rename_expr f_node f_var in
957
  match expr_desc with
958
  | Expr_const _ ->
959
    expr_desc
960
  | Expr_ident i ->
961
    Expr_ident (f_var i)
962
  | Expr_array el ->
963
    Expr_array (List.map re el)
964
  | Expr_access (e1, d) ->
965
    Expr_access (re e1, d)
966
  | Expr_power (e1, d) ->
967
    Expr_power (re e1, d)
968
  | Expr_tuple el ->
969
    Expr_tuple (List.map re el)
970
  | Expr_ite (c, t, e) ->
971
    Expr_ite (re c, re t, re e)
972
  | Expr_arrow (e1, e2) ->
973
    Expr_arrow (re e1, re e2)
974
  | Expr_fby (e1, e2) ->
975
    Expr_fby (re e1, re e2)
976
  | Expr_pre e' ->
977
    Expr_pre (re e')
978
  | Expr_when (e', i, l) ->
979
    Expr_when (re e', f_var i, l)
980
  | Expr_merge (i, hl) ->
981
    Expr_merge (f_var i, List.map (fun (t, h) -> t, re h) hl)
982
  | Expr_appl (i, e', i') ->
983
    Expr_appl (f_node i, re e', Utils.option_map re i')
984

    
985
let rename_var f_var v =
986
  {
987
    (copy_var_decl v) with
988
    var_id = f_var v.var_id;
989
    var_type = v.var_type;
990
    var_clock = v.var_clock;
991
  }
992

    
993
let rename_vars f_var = List.map (rename_var f_var)
994

    
995
let rec rename_eq f_node f_var eq =
996
  {
997
    eq with
998
    eq_lhs = List.map f_var eq.eq_lhs;
999
    eq_rhs = rename_expr f_node f_var eq.eq_rhs;
1000
  }
1001

    
1002
and rename_handler f_node f_var h =
1003
  {
1004
    h with
1005
    hand_state = f_var h.hand_state;
1006
    hand_unless =
1007
      List.map
1008
        (fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id)
1009
        h.hand_unless;
1010
    hand_until =
1011
      List.map
1012
        (fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id)
1013
        h.hand_until;
1014
    hand_locals = rename_vars f_var h.hand_locals;
1015
    hand_stmts = rename_stmts f_node f_var h.hand_stmts;
1016
    hand_annots = rename_annots f_node f_var h.hand_annots;
1017
  }
1018

    
1019
and rename_aut f_node f_var aut =
1020
  {
1021
    aut with
1022
    aut_id = f_var aut.aut_id;
1023
    aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
1024
  }
1025

    
1026
and rename_stmts f_node f_var stmts =
1027
  List.map
1028
    (fun stmt ->
1029
      match stmt with
1030
      | Eq eq ->
1031
        Eq (rename_eq f_node f_var eq)
1032
      | Aut at ->
1033
        Aut (rename_aut f_node f_var at))
1034
    stmts
1035

    
1036
and rename_annotl f_node f_var annots =
1037
  List.map (fun (key, value) -> key, rename_eexpr f_node f_var value) annots
1038

    
1039
and rename_annot f_node f_var annot =
1040
  { annot with annots = rename_annotl f_node f_var annot.annots }
1041

    
1042
and rename_annots f_node f_var annots =
1043
  List.map (rename_annot f_node f_var) annots
1044

    
1045
and rename_eexpr f_node f_var ee =
1046
  {
1047
    ee with
1048
    eexpr_tag = Utils.new_tag ();
1049
    eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
1050
    eexpr_quantifiers =
1051
      List.map
1052
        (fun (typ, vdecls) -> typ, rename_vars f_var vdecls)
1053
        ee.eexpr_quantifiers;
1054
  }
1055

    
1056
and rename_mode f_node f_var m =
1057
  let rename_ee = rename_eexpr f_node f_var in
1058
  {
1059
    m with
1060
    require = List.map rename_ee m.require;
1061
    ensure = List.map rename_ee m.ensure;
1062
  }
1063

    
1064
let rename_import f_node f_var imp =
1065
  let rename_expr = rename_expr f_node f_var in
1066
  {
1067
    imp with
1068
    import_nodeid = f_node imp.import_nodeid;
1069
    inputs = rename_expr imp.inputs;
1070
    outputs = rename_expr imp.outputs;
1071
  }
1072

    
1073
let rename_contract f_var f_node c =
1074
  let rename_var = rename_var f_var in
1075
  let rename_vars = List.map rename_var in
1076
  let rename_eexpr = rename_eexpr f_node f_var in
1077
  let rename_stmts = rename_stmts f_node f_var in
1078
  {
1079
    c with
1080
    consts = rename_vars c.consts;
1081
    locals = rename_vars c.locals;
1082
    stmts = rename_stmts c.stmts;
1083
    assume = List.map rename_eexpr c.assume;
1084
    guarantees = List.map rename_eexpr c.guarantees;
1085
    modes = List.map (rename_mode f_node f_var) c.modes;
1086
    imports = List.map (rename_import f_node f_var) c.imports;
1087
  }
1088

    
1089
let rename_node f_node f_var nd =
1090
  let f_var x =
1091
    (* checking that this is actually a local variable *)
1092
    if List.exists (fun v -> v.var_id = x) (get_node_vars nd) then f_var x
1093
    else x
1094
  in
1095
  let rename_var = rename_var f_var in
1096
  let rename_vars = List.map rename_var in
1097
  let rename_expr = rename_expr f_node f_var in
1098
  let rename_stmts = rename_stmts f_node f_var in
1099
  let inputs = rename_vars nd.node_inputs in
1100
  let outputs = rename_vars nd.node_outputs in
1101
  let locals = rename_vars nd.node_locals in
1102
  let gen_calls = List.map rename_expr nd.node_gencalls in
1103
  let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in
1104
  let node_asserts =
1105
    List.map
1106
      (fun a ->
1107
        {
1108
          a with
1109
          assert_expr =
1110
            (let expr = a.assert_expr in
1111
             rename_expr expr);
1112
        })
1113
      nd.node_asserts
1114
  in
1115
  let node_stmts = rename_stmts nd.node_stmts in
1116

    
1117
  let spec =
1118
    option_map
1119
      (fun s ->
1120
        match s with
1121
        | NodeSpec id ->
1122
          NodeSpec (f_node id)
1123
        | Contract c ->
1124
          Contract (rename_contract f_var f_node c))
1125
      nd.node_spec
1126
  in
1127
  let annot = rename_annots f_node f_var nd.node_annot in
1128
  {
1129
    node_id = f_node nd.node_id;
1130
    node_type = nd.node_type;
1131
    node_clock = nd.node_clock;
1132
    node_inputs = inputs;
1133
    node_outputs = outputs;
1134
    node_locals = locals;
1135
    node_gencalls = gen_calls;
1136
    node_checks;
1137
    node_asserts;
1138
    node_stmts;
1139
    node_dec_stateless = nd.node_dec_stateless;
1140
    node_stateless = nd.node_stateless;
1141
    node_spec = spec;
1142
    node_annot = annot;
1143
    node_iscontract = nd.node_iscontract;
1144
  }
1145

    
1146
let rename_const f_const c = { c with const_id = f_const c.const_id }
1147

    
1148
let rename_typedef f_var t =
1149
  match t.tydef_desc with
1150
  | Tydec_enum tags ->
1151
    { t with tydef_desc = Tydec_enum (List.map f_var tags) }
1152
  | _ ->
1153
    t
1154

    
1155
let rename_prog f_node f_var f_const prog =
1156
  List.rev
1157
    (List.fold_left
1158
       (fun accu top ->
1159
         (match top.top_decl_desc with
1160
         | Node nd ->
1161
           { top with top_decl_desc = Node (rename_node f_node f_var nd) }
1162
         | Const c ->
1163
           { top with top_decl_desc = Const (rename_const f_const c) }
1164
         | TypeDef tdef ->
1165
           { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
1166
         | ImportedNode _ | Include _ | Open _ ->
1167
           top)
1168
         :: accu)
1169
       []
1170
       prog)
1171

    
1172
(* Applies the renaming function [fvar] to every rhs only when the corresponding
1173
   lhs satisfies predicate [pvar] *)
1174
let eq_replace_rhs_var pvar fvar eq =
1175
  let pvar l = List.exists pvar l in
1176
  let rec replace lhs rhs =
1177
    {
1178
      rhs with
1179
      expr_desc =
1180
        (match lhs with
1181
        | [] ->
1182
          assert false
1183
        | [ _ ] ->
1184
          if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
1185
          else rhs.expr_desc
1186
        | _ -> (
1187
          match rhs.expr_desc with
1188
          | Expr_tuple tl ->
1189
            Expr_tuple (List.map2 (fun v e -> replace [ v ] e) lhs tl)
1190
          | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs
1191
            ->
1192
            let args = expr_list_of_expr arg in
1193
            Expr_appl
1194
              ( f,
1195
                expr_of_expr_list arg.expr_loc (List.map (replace lhs) args),
1196
                None )
1197
          | Expr_array _
1198
          | Expr_access _
1199
          | Expr_power _
1200
          | Expr_const _
1201
          | Expr_ident _
1202
          | Expr_appl _ ->
1203
            if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
1204
            else rhs.expr_desc
1205
          | Expr_ite (c, t, e) ->
1206
            Expr_ite (replace lhs c, replace lhs t, replace lhs e)
1207
          | Expr_arrow (e1, e2) ->
1208
            Expr_arrow (replace lhs e1, replace lhs e2)
1209
          | Expr_fby (e1, e2) ->
1210
            Expr_fby (replace lhs e1, replace lhs e2)
1211
          | Expr_pre e' ->
1212
            Expr_pre (replace lhs e')
1213
          | Expr_when (e', i, l) ->
1214
            let i' = if pvar lhs then fvar i else i in
1215
            Expr_when (replace lhs e', i', l)
1216
          | Expr_merge (i, hl) ->
1217
            let i' = if pvar lhs then fvar i else i in
1218
            Expr_merge (i', List.map (fun (t, h) -> t, replace lhs h) hl)));
1219
    }
1220
  in
1221
  { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
1222

    
1223
(**********************************************************************)
1224
(* Pretty printers *)
1225

    
1226
let pp_decl_type fmt tdecl =
1227
  match tdecl.top_decl_desc with
1228
  | Node nd ->
1229
    fprintf fmt "%s: " nd.node_id;
1230
    Utils.reset_names ();
1231
    fprintf fmt "%a" Types.pp nd.node_type
1232
  | ImportedNode ind ->
1233
    fprintf fmt "%s: " ind.nodei_id;
1234
    Utils.reset_names ();
1235
    fprintf fmt "%a" Types.pp ind.nodei_type
1236
  | Const _ | Include _ | Open _ | TypeDef _ ->
1237
    ()
1238

    
1239
let pp_prog_type fmt tdecl_list =
1240
  Utils.Format.(
1241
    pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_type fmt tdecl_list)
1242

    
1243
let pp_decl_clock fmt cdecl =
1244
  match cdecl.top_decl_desc with
1245
  | Node nd ->
1246
    fprintf fmt "%s: " nd.node_id;
1247
    Utils.reset_names ();
1248
    fprintf fmt "%a@ " Clocks.pp nd.node_clock
1249
  | ImportedNode ind ->
1250
    fprintf fmt "%s: " ind.nodei_id;
1251
    Utils.reset_names ();
1252
    fprintf fmt "%a@ " Clocks.pp ind.nodei_clock
1253
  | Const _ | Include _ | Open _ | TypeDef _ ->
1254
    ()
1255

    
1256
let pp_prog_clock fmt prog =
1257
  pp_print_list ~pp_sep:pp_print_nothing pp_decl_clock fmt prog
1258

    
1259
(* filling node table with internal functions *)
1260
let vdecls_of_typ_ck cpt ty =
1261
  let loc = Location.dummy in
1262
  List.map
1263
    (fun _ ->
1264
      incr cpt;
1265
      let name = sprintf "_var_%d" !cpt in
1266
      mkvar_decl
1267
        loc
1268
        (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
1269
    (Types.type_list_of_type ty)
1270

    
1271
let mk_internal_node id =
1272
  let spec = None in
1273
  let ty = Env.lookup_value Basic_library.type_env id in
1274
  let ck = Env.lookup_value Basic_library.clock_env id in
1275
  let tin, tout = Types.split_arrow ty in
1276
  (*eprintf "internal fun %s: %d -> %d@." id (List.length
1277
    (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
1278
  let cpt = ref (-1) in
1279
  mktop
1280
    (ImportedNode
1281
       {
1282
         nodei_id = id;
1283
         nodei_type = ty;
1284
         nodei_clock = ck;
1285
         nodei_inputs = vdecls_of_typ_ck cpt tin;
1286
         nodei_outputs = vdecls_of_typ_ck cpt tout;
1287
         nodei_stateless = Types.get_static_value ty <> None;
1288
         nodei_spec = spec;
1289
         (* nodei_annot = []; *)
1290
         nodei_prototype = None;
1291
         nodei_in_lib = [];
1292
         nodei_iscontract = false;
1293
       })
1294

    
1295
let add_internal_funs () =
1296
  List.iter
1297
    (fun id ->
1298
      let nd = mk_internal_node id in
1299
      Hashtbl.add node_table id nd)
1300
    Basic_library.internal_funs
1301

    
1302
(* Replace any occurence of a var in vars_to_replace by its associated
1303
   expression in defs until e does not contain any such variables *)
1304
let rec substitute_expr vars_to_replace defs e =
1305
  let se = substitute_expr vars_to_replace defs in
1306
  {
1307
    e with
1308
    expr_desc =
1309
      (let ed = e.expr_desc in
1310
       match ed with
1311
       | Expr_const _ ->
1312
         ed
1313
       | Expr_array el ->
1314
         Expr_array (List.map se el)
1315
       | Expr_access (e1, d) ->
1316
         Expr_access (se e1, d)
1317
       | Expr_power (e1, d) ->
1318
         Expr_power (se e1, d)
1319
       | Expr_tuple el ->
1320
         Expr_tuple (List.map se el)
1321
       | Expr_ite (c, t, e) ->
1322
         Expr_ite (se c, se t, se e)
1323
       | Expr_arrow (e1, e2) ->
1324
         Expr_arrow (se e1, se e2)
1325
       | Expr_fby (e1, e2) ->
1326
         Expr_fby (se e1, se e2)
1327
       | Expr_pre e' ->
1328
         Expr_pre (se e')
1329
       | Expr_when (e', i, l) ->
1330
         Expr_when (se e', i, l)
1331
       | Expr_merge (i, hl) ->
1332
         Expr_merge (i, List.map (fun (t, h) -> t, se h) hl)
1333
       | Expr_appl (i, e', i') ->
1334
         Expr_appl (i, se e', i')
1335
       | Expr_ident i ->
1336
         if List.exists (fun v -> v.var_id = i) vars_to_replace then
1337
           let eq_i eq = eq.eq_lhs = [ i ] in
1338
           if List.exists eq_i defs then
1339
             let sub = List.find eq_i defs in
1340
             let sub' = se sub.eq_rhs in
1341
             sub'.expr_desc
1342
           else assert false
1343
         else ed);
1344
  }
1345

    
1346
let expr_to_eexpr expr =
1347
  {
1348
    eexpr_tag = expr.expr_tag;
1349
    eexpr_qfexpr = expr;
1350
    eexpr_quantifiers = [];
1351
    eexpr_name = None;
1352
    eexpr_type = expr.expr_type;
1353
    eexpr_clock = expr.expr_clock;
1354
    eexpr_loc = expr.expr_loc (*eexpr_normalized = None*);
1355
  }
1356

    
1357
(* and expr_desc_to_eexpr_desc expr_desc = *)
1358
(*   let conv = expr_to_eexpr in *)
1359
(*   match expr_desc with *)
1360
(*   | Expr_const c -> EExpr_const (match c with *)
1361
(*     | Const_int x -> EConst_int x  *)
1362
(*     | Const_real x -> EConst_real x  *)
1363
(*     | Const_float x -> EConst_float x  *)
1364
(*     | Const_tag x -> EConst_tag x  *)
1365
(*     | _ -> assert false *)
1366

    
1367
(*   ) *)
1368
(*   | Expr_ident i -> EExpr_ident i *)
1369
(*   | Expr_tuple el -> EExpr_tuple (List.map conv el) *)
1370

    
1371
(*   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)  *)
1372
(*   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *)
1373
(*   | Expr_pre e' -> EExpr_pre (conv e') *)
1374
(*   | Expr_appl (i, e', i') ->  *)
1375
(*     EExpr_appl  *)
1376
(*       (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *)
1377

    
1378
(*   | Expr_when _ *)
1379
(*   | Expr_merge _ -> assert false *)
1380
(*   | Expr_array _  *)
1381
(*   | Expr_access _  *)
1382
(*   | Expr_power _  -> assert false *)
1383
(*   | Expr_ite (c, t, e) -> assert false  *)
1384
(*   | _ -> assert false *)
1385

    
1386
let rec get_expr_calls nodes e =
1387
  let get_calls = get_expr_calls nodes in
1388
  match e.expr_desc with
1389
  | Expr_const _ | Expr_ident _ ->
1390
    Utils.ISet.empty
1391
  | Expr_tuple el | Expr_array el ->
1392
    List.fold_left
1393
      (fun accu e -> Utils.ISet.union accu (get_calls e))
1394
      Utils.ISet.empty
1395
      el
1396
  | Expr_pre e1 | Expr_when (e1, _, _) | Expr_access (e1, _) | Expr_power (e1, _)
1397
    ->
1398
    get_calls e1
1399
  | Expr_ite (c, t, e) ->
1400
    Utils.ISet.union
1401
      (Utils.ISet.union (get_calls c) (get_calls t))
1402
      (get_calls e)
1403
  | Expr_arrow (e1, e2) | Expr_fby (e1, e2) ->
1404
    Utils.ISet.union (get_calls e1) (get_calls e2)
1405
  | Expr_merge (_, hl) ->
1406
    List.fold_left
1407
      (fun accu (_, h) -> Utils.ISet.union accu (get_calls h))
1408
      Utils.ISet.empty
1409
      hl
1410
  | Expr_appl (i, e', _) ->
1411
    if Basic_library.is_expr_internal_fun e then get_calls e'
1412
    else
1413
      let calls = Utils.ISet.add i (get_calls e') in
1414
      let test n =
1415
        match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false
1416
      in
1417
      if List.exists test nodes then
1418
        match (List.find test nodes).top_decl_desc with
1419
        | Node nd ->
1420
          Utils.ISet.union (get_node_calls nodes nd) calls
1421
        | _ ->
1422
          assert false
1423
      else calls
1424

    
1425
and get_eq_calls nodes eq = get_expr_calls nodes eq.eq_rhs
1426

    
1427
and get_aut_handler_calls nodes h =
1428
  List.fold_left
1429
    (fun accu stmt ->
1430
      match stmt with
1431
      | Eq eq ->
1432
        Utils.ISet.union (get_eq_calls nodes eq) accu
1433
      | Aut aut' ->
1434
        Utils.ISet.union (get_aut_calls nodes aut') accu)
1435
    Utils.ISet.empty
1436
    h.hand_stmts
1437

    
1438
and get_aut_calls nodes aut =
1439
  List.fold_left
1440
    (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)
1441
    Utils.ISet.empty
1442
    aut.aut_handlers
1443

    
1444
and get_node_calls nodes node =
1445
  let eqs, auts = get_node_eqs node in
1446
  let aut_calls =
1447
    List.fold_left
1448
      (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)
1449
      Utils.ISet.empty
1450
      auts
1451
  in
1452
  List.fold_left
1453
    (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)
1454
    aut_calls
1455
    eqs
1456

    
1457
let get_expr_vars e =
1458
  let rec get_expr_vars vars e = get_expr_desc_vars vars e.expr_desc
1459
  and get_expr_desc_vars vars expr_desc =
1460
    (*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr
1461
      Location.dummy expr_desc);*)
1462
    match expr_desc with
1463
    | Expr_const _ ->
1464
      vars
1465
    | Expr_ident x ->
1466
      Utils.ISet.add x vars
1467
    | Expr_tuple el | Expr_array el ->
1468
      List.fold_left get_expr_vars vars el
1469
    | Expr_pre e1 ->
1470
      get_expr_vars vars e1
1471
    | Expr_when (e1, c, _) ->
1472
      get_expr_vars (Utils.ISet.add c vars) e1
1473
    | Expr_access (e1, d) | Expr_power (e1, d) ->
1474
      List.fold_left get_expr_vars vars [ e1; expr_of_dimension d ]
1475
    | Expr_ite (c, t, e) ->
1476
      List.fold_left get_expr_vars vars [ c; t; e ]
1477
    | Expr_arrow (e1, e2) | Expr_fby (e1, e2) ->
1478
      List.fold_left get_expr_vars vars [ e1; e2 ]
1479
    | Expr_merge (c, hl) ->
1480
      List.fold_left
1481
        (fun vars (_, h) -> get_expr_vars vars h)
1482
        (Utils.ISet.add c vars)
1483
        hl
1484
    | Expr_appl (_, arg, None) ->
1485
      get_expr_vars vars arg
1486
    | Expr_appl (_, arg, Some r) ->
1487
      List.fold_left get_expr_vars vars [ arg; r ]
1488
  in
1489
  get_expr_vars Utils.ISet.empty e
1490

    
1491
(* let rec expr_has_arrows e =
1492
 *   expr_desc_has_arrows e.expr_desc
1493
 * and expr_desc_has_arrows expr_desc =
1494
 *   match expr_desc with
1495
 *   | Expr_const _
1496
 *   | Expr_ident _ -> false
1497
 *   | Expr_tuple el
1498
 *   | Expr_array el -> List.exists expr_has_arrows el
1499
 *   | Expr_pre e1
1500
 *   | Expr_when (e1, _, _)
1501
 *   | Expr_access (e1, _)
1502
 *   | Expr_power (e1, _) -> expr_has_arrows e1
1503
 *   | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
1504
 *   | Expr_arrow _
1505
 *   | Expr_fby _ -> true
1506
 *   | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1507
 *   | Expr_appl (_, e', _) -> expr_has_arrows e'
1508
 *
1509
 * and eq_has_arrows eq =
1510
 *   expr_has_arrows eq.eq_rhs
1511
 * 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
1512
 * and node_has_arrows node =
1513
 *   let eqs, auts = get_node_eqs node in
1514
 *   List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts *)
1515

    
1516
let rec expr_contains_expr expr_tag expr =
1517
  let search = expr_contains_expr expr_tag in
1518
  expr.expr_tag = expr_tag
1519
  ||
1520
  match expr.expr_desc with
1521
  | Expr_const _ ->
1522
    false
1523
  | Expr_array el ->
1524
    List.exists search el
1525
  | Expr_access (e1, _) | Expr_power (e1, _) ->
1526
    search e1
1527
  | Expr_tuple el ->
1528
    List.exists search el
1529
  | Expr_ite (c, t, e) ->
1530
    List.exists search [ c; t; e ]
1531
  | Expr_arrow (e1, e2) | Expr_fby (e1, e2) ->
1532
    List.exists search [ e1; e2 ]
1533
  | Expr_pre e' | Expr_when (e', _, _) ->
1534
    search e'
1535
  | Expr_merge (_, hl) ->
1536
    List.exists (fun (_, h) -> search h) hl
1537
  | Expr_appl (_, e', None) ->
1538
    search e'
1539
  | Expr_appl (_, e', Some e'') ->
1540
    List.exists search [ e'; e'' ]
1541
  | Expr_ident _ ->
1542
    false
1543

    
1544
(* Generate a new local [node] variable *)
1545
let cpt_fresh = ref 0
1546

    
1547
let reset_cpt_fresh () = cpt_fresh := 0
1548

    
1549
let mk_fresh_var (parentid, ctx_env) loc ty ck =
1550
  let rec aux () =
1551
    incr cpt_fresh;
1552
    let s = Printf.sprintf "__%s_%d" parentid !cpt_fresh in
1553
    if List.exists (fun v -> v.var_id = s) ctx_env then aux ()
1554
    else
1555
      {
1556
        var_id = s;
1557
        var_orig = false;
1558
        var_dec_type = dummy_type_dec;
1559
        var_dec_clock = dummy_clock_dec;
1560
        var_dec_const = false;
1561
        var_dec_value = None;
1562
        var_parent_nodeid = Some parentid;
1563
        var_type = ty;
1564
        var_clock = ck;
1565
        var_loc = loc;
1566
        var_is_contract = false;
1567
      }
1568
  in
1569
  aux ()
1570

    
1571
let find_eq xl eqs =
1572
  let rec aux accu eqs =
1573
    match eqs with
1574
    | [] ->
1575
      Format.eprintf
1576
        "Looking for variables %a in the following equations@.%a@."
1577
        (pp_comma_list (fun fmt v -> Format.fprintf fmt "%s" v))
1578
        xl
1579
        Printers.pp_node_eqs
1580
        eqs;
1581
      assert false
1582
    | hd :: tl ->
1583
      if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu @ tl
1584
      else aux (hd :: accu) tl
1585
  in
1586
  aux [] eqs
1587

    
1588
let get_node name prog =
1589
  let node_opt =
1590
    List.fold_left
1591
      (fun res top ->
1592
        match res, top.top_decl_desc with
1593
        | Some _, _ ->
1594
          res
1595
        | None, Node nd ->
1596
          (* Format.eprintf "Checking node %s = %s: %b@." nd.node_id name
1597
             (nd.node_id = name); *)
1598
          if nd.node_id = name then Some nd else res
1599
        | _ ->
1600
          None)
1601
      None
1602
      prog
1603
  in
1604
  try Utils.desome node_opt with Utils.DeSome -> raise Not_found
1605

    
1606
(* Pushing negations in expression. Subtitute operators whenever possible *)
1607
let rec push_negations ?(neg = false) e =
1608
  let res =
1609
    let pn = push_negations in
1610
    let map desc =
1611
      (* Keeping clock and type info *)
1612
      let new_e = mkexpr e.expr_loc desc in
1613
      { new_e with expr_type = e.expr_type; expr_clock = e.expr_clock }
1614
    in
1615
    match e.expr_desc with
1616
    | Expr_ite (g, t, e) ->
1617
      if neg then map (Expr_ite (pn g, pn e, pn t))
1618
      else map (Expr_ite (pn g, pn t, pn e))
1619
    | Expr_tuple t ->
1620
      map (Expr_tuple (List.map (pn ~neg) t))
1621
    | Expr_arrow (e1, e2) ->
1622
      map (Expr_arrow (pn ~neg e1, pn ~neg e2))
1623
    | Expr_fby (e1, e2) ->
1624
      map (Expr_fby (pn ~neg e1, pn ~neg e2))
1625
    | Expr_pre e ->
1626
      map (Expr_pre (pn ~neg e))
1627
    | Expr_appl (op, e', None) when op = "not" ->
1628
      if neg then push_negations ~neg:false e' else push_negations ~neg:true e'
1629
    | Expr_appl (op, e', None)
1630
      when List.mem op (Basic_library.bool_funs @ Basic_library.rel_funs) -> (
1631
      match op with
1632
      | "&&" ->
1633
        map (Expr_appl ((if neg then "||" else op), pn ~neg e', None))
1634
      | "||" ->
1635
        map (Expr_appl ((if neg then "&&" else op), pn ~neg e', None))
1636
      (* TODO xor/equi/impl *)
1637
      | "<" ->
1638
        map (Expr_appl ((if neg then ">=" else op), pn e', None))
1639
      | ">" ->
1640
        map (Expr_appl ((if neg then "<=" else op), pn e', None))
1641
      | "<=" ->
1642
        map (Expr_appl ((if neg then ">" else op), pn e', None))
1643
      | ">=" ->
1644
        map (Expr_appl ((if neg then "<" else op), pn e', None))
1645
      | "!=" ->
1646
        map (Expr_appl ((if neg then "=" else op), pn e', None))
1647
      | "=" ->
1648
        map (Expr_appl ((if neg then "!=" else op), pn e', None))
1649
      | _ ->
1650
        assert false)
1651
    | Expr_const c ->
1652
      if neg then map (Expr_const (const_negation c)) else e
1653
    | Expr_ident _ ->
1654
      if neg then mkpredef_call e.expr_loc "not" [ e ] else e
1655
    | Expr_appl _ ->
1656
      if neg then mkpredef_call e.expr_loc "not" [ e ] else e
1657
    | _ ->
1658
      assert false
1659
    (* no array, array access, power or merge/when *)
1660
  in
1661
  res
1662

    
1663
let rec add_pre_expr vars e =
1664
  let ap = add_pre_expr vars in
1665
  let desc =
1666
    match e.expr_desc with
1667
    | Expr_ite (g, t, e) ->
1668
      Expr_ite (ap g, ap t, ap e)
1669
    | Expr_tuple t ->
1670
      Expr_tuple (List.map ap t)
1671
    | Expr_arrow (e1, e2) ->
1672
      Expr_arrow (ap e1, ap e2)
1673
    | Expr_fby (e1, e2) ->
1674
      Expr_fby (ap e1, ap e2)
1675
    | Expr_pre e ->
1676
      Expr_pre (ap e)
1677
    | Expr_appl (op, e, opt) ->
1678
      Expr_appl (op, ap e, opt)
1679
    | Expr_const _ ->
1680
      e.expr_desc
1681
    | Expr_ident id ->
1682
      if List.mem id vars then Expr_pre e else e.expr_desc
1683
    | _ ->
1684
      assert false
1685
    (* no array, array access, power or merge/when yet *)
1686
  in
1687
  let new_e = mkexpr e.expr_loc desc in
1688
  { new_e with expr_type = e.expr_type; expr_clock = e.expr_clock }
1689

    
1690
let mk_eq l e1 e2 = mkpredef_call l "=" [ e1; e2 ]
1691

    
1692
let rec partial_eval e =
1693
  let pa = partial_eval in
1694
  let edesc =
1695
    match e.expr_desc with
1696
    | Expr_const _ ->
1697
      e.expr_desc
1698
    | Expr_ident _ ->
1699
      e.expr_desc
1700
    | Expr_ite (g, t, e) -> (
1701
      let g, t, e = pa g, pa t, pa e in
1702
      match g.expr_desc with
1703
      | Expr_const (Const_tag tag) when tag = tag_true ->
1704
        t.expr_desc
1705
      | Expr_const (Const_tag tag) when tag = tag_false ->
1706
        e.expr_desc
1707
      | _ ->
1708
        Expr_ite (g, t, e))
1709
    | Expr_tuple t ->
1710
      Expr_tuple (List.map pa t)
1711
    | Expr_arrow (e1, e2) ->
1712
      Expr_arrow (pa e1, pa e2)
1713
    | Expr_fby (e1, e2) ->
1714
      Expr_fby (pa e1, pa e2)
1715
    | Expr_pre e ->
1716
      Expr_pre (pa e)
1717
    | Expr_appl (op, args, opt) ->
1718
      let args = pa args in
1719
      if Basic_library.is_expr_internal_fun e then
1720
        Basic_library.partial_eval op args opt
1721
      else Expr_appl (op, args, opt)
1722
    | Expr_array el ->
1723
      Expr_array (List.map pa el)
1724
    | Expr_access (e, d) ->
1725
      Expr_access (pa e, d)
1726
    | Expr_power (e, d) ->
1727
      Expr_power (pa e, d)
1728
    | Expr_when (e, id, l) ->
1729
      Expr_when (pa e, id, l)
1730
    | Expr_merge (id, gl) ->
1731
      Expr_merge (id, List.map (fun (l, e) -> l, pa e) gl)
1732
  in
1733
  { e with expr_desc = edesc }
1734

    
1735
(* Local Variables: *)
1736
(* compile-command:"make -C .." *)
1737
(* End: *)
(24-24/99)