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: *)
|