1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Format
|
13
|
open Lustre_types
|
14
|
open Machine_code_types
|
15
|
(*open Dimension*)
|
16
|
|
17
|
|
18
|
exception Error of Location.t * Error.error_kind
|
19
|
|
20
|
module VDeclModule =
|
21
|
struct (* Node module *)
|
22
|
type t = var_decl
|
23
|
let compare v1 v2 = compare v1.var_id v2.var_id
|
24
|
end
|
25
|
|
26
|
module VMap = Map.Make(VDeclModule)
|
27
|
|
28
|
module VSet: sig
|
29
|
include Set.S
|
30
|
val pp: Format.formatter -> t -> unit
|
31
|
end with type elt = var_decl =
|
32
|
struct
|
33
|
include Set.Make(VDeclModule)
|
34
|
let pp fmt s =
|
35
|
Format.fprintf fmt "{@[%a}@]" (Utils.fprintf_list ~sep:",@ " Printers.pp_var) (elements s)
|
36
|
end
|
37
|
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
|
38
|
|
39
|
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
|
40
|
|
41
|
|
42
|
|
43
|
(************************************************************)
|
44
|
(* *)
|
45
|
|
46
|
let mktyp loc d =
|
47
|
{ ty_dec_desc = d; ty_dec_loc = loc }
|
48
|
|
49
|
let mkclock loc d =
|
50
|
{ ck_dec_desc = d; ck_dec_loc = loc }
|
51
|
|
52
|
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) =
|
53
|
assert (value = None || is_const);
|
54
|
{ var_id = id;
|
55
|
var_orig = orig;
|
56
|
var_dec_type = ty_dec;
|
57
|
var_dec_clock = ck_dec;
|
58
|
var_dec_const = is_const;
|
59
|
var_dec_value = value;
|
60
|
var_parent_nodeid = parentid;
|
61
|
var_type = Types.new_var ();
|
62
|
var_clock = Clocks.new_var true;
|
63
|
var_loc = loc }
|
64
|
|
65
|
let dummy_var_decl name typ =
|
66
|
{
|
67
|
var_id = name;
|
68
|
var_orig = false;
|
69
|
var_dec_type = dummy_type_dec;
|
70
|
var_dec_clock = dummy_clock_dec;
|
71
|
var_dec_const = false;
|
72
|
var_dec_value = None;
|
73
|
var_parent_nodeid = None;
|
74
|
var_type = typ;
|
75
|
var_clock = Clocks.new_ck Clocks.Cvar true;
|
76
|
var_loc = Location.dummy_loc
|
77
|
}
|
78
|
|
79
|
let mkexpr loc d =
|
80
|
{ expr_tag = Utils.new_tag ();
|
81
|
expr_desc = d;
|
82
|
expr_type = Types.new_var ();
|
83
|
expr_clock = Clocks.new_var true;
|
84
|
expr_delay = Delay.new_var ();
|
85
|
expr_annot = None;
|
86
|
expr_loc = loc }
|
87
|
|
88
|
let var_decl_of_const ?(parentid=None) c =
|
89
|
{ var_id = c.const_id;
|
90
|
var_orig = true;
|
91
|
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
|
92
|
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
|
93
|
var_dec_const = true;
|
94
|
var_dec_value = None;
|
95
|
var_parent_nodeid = parentid;
|
96
|
var_type = c.const_type;
|
97
|
var_clock = Clocks.new_var false;
|
98
|
var_loc = c.const_loc }
|
99
|
|
100
|
let mk_new_name used id =
|
101
|
let rec new_name name cpt =
|
102
|
if used name
|
103
|
then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
|
104
|
else name
|
105
|
in new_name id 1
|
106
|
|
107
|
let mkeq loc (lhs, rhs) =
|
108
|
{ eq_lhs = lhs;
|
109
|
eq_rhs = rhs;
|
110
|
eq_loc = loc }
|
111
|
|
112
|
let mkassert loc expr =
|
113
|
{ assert_loc = loc;
|
114
|
assert_expr = expr
|
115
|
}
|
116
|
|
117
|
let mktop_decl loc own itf d =
|
118
|
{ top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
|
119
|
|
120
|
let mkpredef_call loc funname args =
|
121
|
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
|
122
|
|
123
|
let is_clock_dec_type cty =
|
124
|
match cty with
|
125
|
| Tydec_clock _ -> true
|
126
|
| _ -> false
|
127
|
|
128
|
let const_of_top top_decl =
|
129
|
match top_decl.top_decl_desc with
|
130
|
| Const c -> c
|
131
|
| _ -> assert false
|
132
|
|
133
|
let node_of_top top_decl =
|
134
|
match top_decl.top_decl_desc with
|
135
|
| Node nd -> nd
|
136
|
| _ -> raise Not_found
|
137
|
|
138
|
let imported_node_of_top top_decl =
|
139
|
match top_decl.top_decl_desc with
|
140
|
| ImportedNode ind -> ind
|
141
|
| _ -> assert false
|
142
|
|
143
|
let typedef_of_top top_decl =
|
144
|
match top_decl.top_decl_desc with
|
145
|
| TypeDef tdef -> tdef
|
146
|
| _ -> assert false
|
147
|
|
148
|
let dependency_of_top top_decl =
|
149
|
match top_decl.top_decl_desc with
|
150
|
| Open (local, dep) -> (local, dep)
|
151
|
| _ -> assert false
|
152
|
|
153
|
let consts_of_enum_type top_decl =
|
154
|
match top_decl.top_decl_desc with
|
155
|
| TypeDef tdef ->
|
156
|
(match tdef.tydef_desc with
|
157
|
| Tydec_enum tags ->
|
158
|
List.map
|
159
|
(fun tag ->
|
160
|
let cdecl = {
|
161
|
const_id = tag;
|
162
|
const_loc = top_decl.top_decl_loc;
|
163
|
const_value = Const_tag tag;
|
164
|
const_type = Type_predef.type_const tdef.tydef_id
|
165
|
} in
|
166
|
{ top_decl with top_decl_desc = Const cdecl })
|
167
|
tags
|
168
|
| _ -> [])
|
169
|
| _ -> assert false
|
170
|
|
171
|
(************************************************************)
|
172
|
(* Eexpr functions *)
|
173
|
(************************************************************)
|
174
|
|
175
|
|
176
|
let empty_contract =
|
177
|
{
|
178
|
consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
|
179
|
}
|
180
|
|
181
|
(* For const declaration we do as for regular lustre node.
|
182
|
But for local flows we registered the variable and the lustre flow definition *)
|
183
|
let mk_contract_var id is_const type_opt expr loc =
|
184
|
let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
|
185
|
if is_const then
|
186
|
let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
|
187
|
{ empty_contract with consts = [v]; spec_loc = loc; }
|
188
|
else
|
189
|
let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
|
190
|
let eq = mkeq loc ([id], expr) in
|
191
|
{ empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
|
192
|
|
193
|
let mk_contract_guarantees eexpr =
|
194
|
{ empty_contract with guarantees = [eexpr]; spec_loc = eexpr.eexpr_loc }
|
195
|
|
196
|
let mk_contract_assume eexpr =
|
197
|
{ empty_contract with assume = [eexpr]; spec_loc = eexpr.eexpr_loc }
|
198
|
|
199
|
let mk_contract_mode id rl el loc =
|
200
|
{ empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc }
|
201
|
|
202
|
let mk_contract_import id ins outs loc =
|
203
|
{ empty_contract with imports = [{import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc; }]; spec_loc = loc }
|
204
|
|
205
|
|
206
|
let merge_contracts ann1 ann2 = (* keeping the first item loc *)
|
207
|
{ consts = ann1.consts @ ann2.consts;
|
208
|
locals = ann1.locals @ ann2.locals;
|
209
|
stmts = ann1.stmts @ ann2.stmts;
|
210
|
assume = ann1.assume @ ann2.assume;
|
211
|
guarantees = ann1.guarantees @ ann2.guarantees;
|
212
|
modes = ann1.modes @ ann2.modes;
|
213
|
imports = ann1.imports @ ann2.imports;
|
214
|
spec_loc = ann1.spec_loc
|
215
|
}
|
216
|
|
217
|
let mkeexpr loc expr =
|
218
|
{ eexpr_tag = Utils.new_tag ();
|
219
|
eexpr_qfexpr = expr;
|
220
|
eexpr_quantifiers = [];
|
221
|
eexpr_type = Types.new_var ();
|
222
|
eexpr_clock = Clocks.new_var true;
|
223
|
eexpr_loc = loc }
|
224
|
|
225
|
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
|
226
|
|
227
|
(*
|
228
|
let mkepredef_call loc funname args =
|
229
|
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
|
230
|
|
231
|
let mkepredef_unary_call loc funname arg =
|
232
|
mkeexpr loc (EExpr_appl (funname, arg, None))
|
233
|
*)
|
234
|
|
235
|
let merge_expr_annot ann1 ann2 =
|
236
|
match ann1, ann2 with
|
237
|
| None, None -> assert false
|
238
|
| Some _, None -> ann1
|
239
|
| None, Some _ -> ann2
|
240
|
| Some ann1, Some ann2 -> Some {
|
241
|
annots = ann1.annots @ ann2.annots;
|
242
|
annot_loc = ann1.annot_loc
|
243
|
}
|
244
|
|
245
|
let update_expr_annot node_id e annot =
|
246
|
List.iter (fun (key, _) ->
|
247
|
Annotations.add_expr_ann node_id e.expr_tag key
|
248
|
) annot.annots;
|
249
|
e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
|
250
|
e
|
251
|
|
252
|
|
253
|
let mkinstr ?lustre_expr ?lustre_eq i =
|
254
|
{
|
255
|
instr_desc = i;
|
256
|
(* lustre_expr = lustre_expr; *)
|
257
|
lustre_eq = lustre_eq;
|
258
|
}
|
259
|
|
260
|
let get_instr_desc i = i.instr_desc
|
261
|
let update_instr_desc i id = { i with instr_desc = id }
|
262
|
|
263
|
(***********************************************************)
|
264
|
(* Fast access to nodes, by name *)
|
265
|
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
|
266
|
let consts_table = Hashtbl.create 30
|
267
|
|
268
|
let print_node_table fmt () =
|
269
|
begin
|
270
|
Format.fprintf fmt "{ /* node table */@.";
|
271
|
Hashtbl.iter (fun id nd ->
|
272
|
Format.fprintf fmt "%s |-> %a"
|
273
|
id
|
274
|
Printers.pp_short_decl nd
|
275
|
) node_table;
|
276
|
Format.fprintf fmt "}@."
|
277
|
end
|
278
|
|
279
|
let print_consts_table fmt () =
|
280
|
begin
|
281
|
Format.fprintf fmt "{ /* consts table */@.";
|
282
|
Hashtbl.iter (fun id const ->
|
283
|
Format.fprintf fmt "%s |-> %a"
|
284
|
id
|
285
|
Printers.pp_const_decl (const_of_top const)
|
286
|
) consts_table;
|
287
|
Format.fprintf fmt "}@."
|
288
|
end
|
289
|
|
290
|
let node_name td =
|
291
|
match td.top_decl_desc with
|
292
|
| Node nd -> nd.node_id
|
293
|
| ImportedNode nd -> nd.nodei_id
|
294
|
| _ -> assert false
|
295
|
|
296
|
let is_generic_node td =
|
297
|
match td.top_decl_desc with
|
298
|
| Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
|
299
|
| ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
|
300
|
| _ -> assert false
|
301
|
|
302
|
let node_inputs td =
|
303
|
match td.top_decl_desc with
|
304
|
| Node nd -> nd.node_inputs
|
305
|
| ImportedNode nd -> nd.nodei_inputs
|
306
|
| _ -> assert false
|
307
|
|
308
|
let node_from_name id =
|
309
|
Hashtbl.find node_table id
|
310
|
(* with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
|
311
|
* assert false) *)
|
312
|
|
313
|
let update_node id top =
|
314
|
Hashtbl.replace node_table id top
|
315
|
|
316
|
let is_imported_node td =
|
317
|
match td.top_decl_desc with
|
318
|
| Node nd -> false
|
319
|
| ImportedNode nd -> true
|
320
|
| _ -> assert false
|
321
|
|
322
|
|
323
|
(* alias and type definition table *)
|
324
|
|
325
|
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
|
326
|
|
327
|
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
|
328
|
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
|
329
|
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
|
330
|
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
|
331
|
|
332
|
let type_table =
|
333
|
Utils.create_hashtable 20 [
|
334
|
Tydec_int , top_int_type;
|
335
|
Tydec_bool , top_bool_type;
|
336
|
(* Tydec_float, top_float_type; *)
|
337
|
Tydec_real , top_real_type
|
338
|
]
|
339
|
|
340
|
let print_type_table fmt () =
|
341
|
begin
|
342
|
Format.fprintf fmt "{ /* type table */@.";
|
343
|
Hashtbl.iter (fun tydec tdef ->
|
344
|
Format.fprintf fmt "%a |-> %a"
|
345
|
Printers.pp_var_type_dec_desc tydec
|
346
|
Printers.pp_typedef (typedef_of_top tdef)
|
347
|
) type_table;
|
348
|
Format.fprintf fmt "}@."
|
349
|
end
|
350
|
|
351
|
let rec is_user_type typ =
|
352
|
match typ with
|
353
|
| Tydec_int | Tydec_bool | Tydec_real
|
354
|
(* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
|
355
|
| Tydec_clock typ' -> is_user_type typ'
|
356
|
| _ -> true
|
357
|
|
358
|
let get_repr_type typ =
|
359
|
let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
|
360
|
if is_user_type typ_def then typ else typ_def
|
361
|
|
362
|
let rec coretype_equal ty1 ty2 =
|
363
|
let res =
|
364
|
match ty1, ty2 with
|
365
|
| Tydec_any , _
|
366
|
| _ , Tydec_any -> assert false
|
367
|
| Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2
|
368
|
| Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
|
369
|
in (not (is_user_type ty1')) && coretype_equal ty1' ty2
|
370
|
| _ , Tydec_const _ -> coretype_equal ty2 ty1
|
371
|
| Tydec_int , Tydec_int
|
372
|
| Tydec_real , Tydec_real
|
373
|
(* | Tydec_float , Tydec_float *)
|
374
|
| Tydec_bool , Tydec_bool -> true
|
375
|
| Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2
|
376
|
| Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
|
377
|
| Tydec_enum tl1 , Tydec_enum tl2 -> List.sort compare tl1 = List.sort compare tl2
|
378
|
| Tydec_struct fl1 , Tydec_struct fl2 ->
|
379
|
List.length fl1 = List.length fl2
|
380
|
&& List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
|
381
|
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
|
382
|
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
|
383
|
| _ -> false
|
384
|
in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
|
385
|
|
386
|
let tag_true = "true"
|
387
|
let tag_false = "false"
|
388
|
let tag_default = "default"
|
389
|
|
390
|
let const_is_bool c =
|
391
|
match c with
|
392
|
| Const_tag t -> t = tag_true || t = tag_false
|
393
|
| _ -> false
|
394
|
|
395
|
(* Computes the negation of a boolean constant *)
|
396
|
let const_negation c =
|
397
|
assert (const_is_bool c);
|
398
|
match c with
|
399
|
| Const_tag t when t = tag_true -> Const_tag tag_false
|
400
|
| _ -> Const_tag tag_true
|
401
|
|
402
|
let const_or c1 c2 =
|
403
|
assert (const_is_bool c1 && const_is_bool c2);
|
404
|
match c1, c2 with
|
405
|
| Const_tag t1, _ when t1 = tag_true -> c1
|
406
|
| _ , Const_tag t2 when t2 = tag_true -> c2
|
407
|
| _ -> Const_tag tag_false
|
408
|
|
409
|
let const_and c1 c2 =
|
410
|
assert (const_is_bool c1 && const_is_bool c2);
|
411
|
match c1, c2 with
|
412
|
| Const_tag t1, _ when t1 = tag_false -> c1
|
413
|
| _ , Const_tag t2 when t2 = tag_false -> c2
|
414
|
| _ -> Const_tag tag_true
|
415
|
|
416
|
let const_xor c1 c2 =
|
417
|
assert (const_is_bool c1 && const_is_bool c2);
|
418
|
match c1, c2 with
|
419
|
| Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true
|
420
|
| _ -> Const_tag tag_false
|
421
|
|
422
|
let const_impl c1 c2 =
|
423
|
assert (const_is_bool c1 && const_is_bool c2);
|
424
|
match c1, c2 with
|
425
|
| Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true
|
426
|
| _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
|
427
|
| _ -> Const_tag tag_false
|
428
|
|
429
|
(* To guarantee uniqueness of tags in enum types *)
|
430
|
let tag_table =
|
431
|
Utils.create_hashtable 20 [
|
432
|
tag_true, top_bool_type;
|
433
|
tag_false, top_bool_type
|
434
|
]
|
435
|
|
436
|
(* To guarantee uniqueness of fields in struct types *)
|
437
|
let field_table =
|
438
|
Utils.create_hashtable 20 [
|
439
|
]
|
440
|
|
441
|
let get_enum_type_tags cty =
|
442
|
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
|
443
|
match cty with
|
444
|
| Tydec_bool -> [tag_true; tag_false]
|
445
|
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
|
446
|
| Tydec_enum tl -> tl
|
447
|
| _ -> assert false)
|
448
|
| _ -> assert false
|
449
|
|
450
|
let get_struct_type_fields cty =
|
451
|
match cty with
|
452
|
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
|
453
|
| Tydec_struct fl -> fl
|
454
|
| _ -> assert false)
|
455
|
| _ -> assert false
|
456
|
|
457
|
let const_of_bool b =
|
458
|
Const_tag (if b then tag_true else tag_false)
|
459
|
|
460
|
(* let get_const c = snd (Hashtbl.find consts_table c) *)
|
461
|
|
462
|
let ident_of_expr expr =
|
463
|
match expr.expr_desc with
|
464
|
| Expr_ident id -> id
|
465
|
| _ -> assert false
|
466
|
|
467
|
(* Generate a new ident expression from a declared variable *)
|
468
|
let expr_of_vdecl v =
|
469
|
{ expr_tag = Utils.new_tag ();
|
470
|
expr_desc = Expr_ident v.var_id;
|
471
|
expr_type = v.var_type;
|
472
|
expr_clock = v.var_clock;
|
473
|
expr_delay = Delay.new_var ();
|
474
|
expr_annot = None;
|
475
|
expr_loc = v.var_loc }
|
476
|
|
477
|
(* Caution, returns an untyped and unclocked expression *)
|
478
|
let expr_of_ident id loc =
|
479
|
{expr_tag = Utils.new_tag ();
|
480
|
expr_desc = Expr_ident id;
|
481
|
expr_type = Types.new_var ();
|
482
|
expr_clock = Clocks.new_var true;
|
483
|
expr_delay = Delay.new_var ();
|
484
|
expr_loc = loc;
|
485
|
expr_annot = None}
|
486
|
|
487
|
let is_tuple_expr expr =
|
488
|
match expr.expr_desc with
|
489
|
| Expr_tuple _ -> true
|
490
|
| _ -> false
|
491
|
|
492
|
let expr_list_of_expr expr =
|
493
|
match expr.expr_desc with
|
494
|
| Expr_tuple elist -> elist
|
495
|
| _ -> [expr]
|
496
|
|
497
|
let expr_of_expr_list loc elist =
|
498
|
match elist with
|
499
|
| [t] -> { t with expr_loc = loc }
|
500
|
| t::_ ->
|
501
|
let tlist = List.map (fun e -> e.expr_type) elist in
|
502
|
let clist = List.map (fun e -> e.expr_clock) elist in
|
503
|
{ t with expr_desc = Expr_tuple elist;
|
504
|
expr_type = Type_predef.type_tuple tlist;
|
505
|
expr_clock = Clock_predef.ck_tuple clist;
|
506
|
expr_tag = Utils.new_tag ();
|
507
|
expr_loc = loc }
|
508
|
| _ -> assert false
|
509
|
|
510
|
let call_of_expr expr =
|
511
|
match expr.expr_desc with
|
512
|
| Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
|
513
|
| _ -> assert false
|
514
|
|
515
|
|
516
|
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
|
517
|
let rec expr_of_dimension dim =
|
518
|
let open Dimension in
|
519
|
match dim.dim_desc with
|
520
|
| Dbool b ->
|
521
|
mkexpr dim.dim_loc (Expr_const (const_of_bool b))
|
522
|
| Dint i ->
|
523
|
mkexpr dim.dim_loc (Expr_const (Const_int i))
|
524
|
| Dident id ->
|
525
|
mkexpr dim.dim_loc (Expr_ident id)
|
526
|
| Dite (c, t, e) ->
|
527
|
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
|
528
|
| Dappl (id, args) ->
|
529
|
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
|
530
|
| Dlink dim' -> expr_of_dimension dim'
|
531
|
| Dvar
|
532
|
| Dunivar -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
|
533
|
assert false)
|
534
|
|
535
|
let dimension_of_const loc const =
|
536
|
let open Dimension in
|
537
|
match const with
|
538
|
| Const_int i -> mkdim_int loc i
|
539
|
| Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
|
540
|
| _ -> raise InvalidDimension
|
541
|
|
542
|
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments
|
543
|
into dimension expressions *)
|
544
|
let rec dimension_of_expr expr =
|
545
|
let open Dimension in
|
546
|
match expr.expr_desc with
|
547
|
| Expr_const c -> dimension_of_const expr.expr_loc c
|
548
|
| Expr_ident id -> mkdim_ident expr.expr_loc id
|
549
|
| Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
|
550
|
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
|
551
|
if k = None then raise InvalidDimension;
|
552
|
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
|
553
|
| Expr_ite (i, t, e) ->
|
554
|
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
|
555
|
| _ -> raise InvalidDimension (* not a simple dimension expression *)
|
556
|
|
557
|
|
558
|
let sort_handlers hl =
|
559
|
List.sort (fun (t, _) (t', _) -> compare t t') hl
|
560
|
|
561
|
let num_10 = Num.num_of_int 10
|
562
|
|
563
|
let rec is_eq_const c1 c2 =
|
564
|
match c1, c2 with
|
565
|
| Const_real (n1, i1, _), Const_real (n2, i2, _)
|
566
|
-> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in
|
567
|
let n2 = n2 // (num_10 **/ (num_of_int i2)) in
|
568
|
eq_num n1 n2)
|
569
|
| Const_struct lcl1, Const_struct lcl2
|
570
|
-> List.length lcl1 = List.length lcl2
|
571
|
&& List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
|
572
|
| _ -> c1 = c2
|
573
|
|
574
|
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
|
575
|
| Expr_const c1, Expr_const c2 -> is_eq_const c1 c2
|
576
|
| Expr_ident i1, Expr_ident i2 -> i1 = i2
|
577
|
| Expr_array el1, Expr_array el2
|
578
|
| Expr_tuple el1, Expr_tuple el2 ->
|
579
|
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2
|
580
|
| Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
|
581
|
| Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
|
582
|
| Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2
|
583
|
(* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
|
584
|
(* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
|
585
|
| Expr_pre e, Expr_pre e' -> is_eq_expr e e'
|
586
|
| Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
|
587
|
| Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl')
|
588
|
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
|
589
|
| Expr_power (e1, i1), Expr_power (e2, i2)
|
590
|
| Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
|
591
|
| _ -> false
|
592
|
|
593
|
let get_node_vars nd =
|
594
|
nd.node_inputs @ nd.node_locals @ nd.node_outputs
|
595
|
|
596
|
let mk_new_node_name nd id =
|
597
|
let used_vars = get_node_vars nd in
|
598
|
let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
|
599
|
mk_new_name used id
|
600
|
|
601
|
let get_var id var_list =
|
602
|
List.find (fun v -> v.var_id = id) var_list
|
603
|
|
604
|
let get_node_var id node =
|
605
|
try
|
606
|
get_var id (get_node_vars node)
|
607
|
with Not_found -> begin
|
608
|
(* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
|
609
|
raise Not_found
|
610
|
end
|
611
|
|
612
|
|
613
|
let get_node_eqs =
|
614
|
let get_eqs stmts =
|
615
|
List.fold_right
|
616
|
(fun stmt (res_eq, res_aut) ->
|
617
|
match stmt with
|
618
|
| Eq eq -> eq :: res_eq, res_aut
|
619
|
| Aut aut -> res_eq, aut::res_aut)
|
620
|
stmts
|
621
|
([], []) in
|
622
|
let table_eqs = Hashtbl.create 23 in
|
623
|
(fun nd ->
|
624
|
try
|
625
|
let (old, res) = Hashtbl.find table_eqs nd.node_id
|
626
|
in if old == nd.node_stmts then res else raise Not_found
|
627
|
with Not_found ->
|
628
|
let res = get_eqs nd.node_stmts in
|
629
|
begin
|
630
|
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
|
631
|
res
|
632
|
end)
|
633
|
|
634
|
let get_node_eq id node =
|
635
|
let eqs, auts = get_node_eqs node in
|
636
|
try
|
637
|
List.find (fun eq -> List.mem id eq.eq_lhs) eqs
|
638
|
with
|
639
|
Not_found -> (* Shall be defined in automata auts *) raise Not_found
|
640
|
|
641
|
let get_nodes prog =
|
642
|
List.fold_left (
|
643
|
fun nodes decl ->
|
644
|
match decl.top_decl_desc with
|
645
|
| Node _ -> decl::nodes
|
646
|
| Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes
|
647
|
) [] prog
|
648
|
|
649
|
let get_imported_nodes prog =
|
650
|
List.fold_left (
|
651
|
fun nodes decl ->
|
652
|
match decl.top_decl_desc with
|
653
|
| ImportedNode _ -> decl::nodes
|
654
|
| Const _ | Node _ | Include _ | Open _ | TypeDef _-> nodes
|
655
|
) [] prog
|
656
|
|
657
|
let get_consts prog =
|
658
|
List.fold_right (
|
659
|
fun decl consts ->
|
660
|
match decl.top_decl_desc with
|
661
|
| Const _ -> decl::consts
|
662
|
| Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> consts
|
663
|
) prog []
|
664
|
|
665
|
let get_typedefs prog =
|
666
|
List.fold_right (
|
667
|
fun decl types ->
|
668
|
match decl.top_decl_desc with
|
669
|
| TypeDef _ -> decl::types
|
670
|
| Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> types
|
671
|
) prog []
|
672
|
|
673
|
let get_dependencies prog =
|
674
|
List.fold_right (
|
675
|
fun decl deps ->
|
676
|
match decl.top_decl_desc with
|
677
|
| Open _ -> decl::deps
|
678
|
| Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> deps
|
679
|
) prog []
|
680
|
|
681
|
let get_node_interface nd =
|
682
|
{nodei_id = nd.node_id;
|
683
|
nodei_type = nd.node_type;
|
684
|
nodei_clock = nd.node_clock;
|
685
|
nodei_inputs = nd.node_inputs;
|
686
|
nodei_outputs = nd.node_outputs;
|
687
|
nodei_stateless = nd.node_dec_stateless;
|
688
|
nodei_spec = nd.node_spec;
|
689
|
(* nodei_annot = nd.node_annot; *)
|
690
|
nodei_prototype = None;
|
691
|
nodei_in_lib = [];
|
692
|
}
|
693
|
|
694
|
(************************************************************************)
|
695
|
(* Renaming *)
|
696
|
|
697
|
let rec rename_static rename cty =
|
698
|
match cty with
|
699
|
| Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
|
700
|
| Tydec_clock cty -> Tydec_clock (rename_static rename cty)
|
701
|
| Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
|
702
|
| _ -> cty
|
703
|
|
704
|
let rec rename_carrier rename cck =
|
705
|
match cck with
|
706
|
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
|
707
|
| _ -> cck
|
708
|
|
709
|
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
|
710
|
|
711
|
(* applies the renaming function [fvar] to all variables of expression [expr] *)
|
712
|
(* let rec expr_replace_var fvar expr = *)
|
713
|
(* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
|
714
|
|
715
|
(* and expr_desc_replace_var fvar expr_desc = *)
|
716
|
(* match expr_desc with *)
|
717
|
(* | Expr_const _ -> expr_desc *)
|
718
|
(* | Expr_ident i -> Expr_ident (fvar i) *)
|
719
|
(* | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
|
720
|
(* | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
|
721
|
(* | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
|
722
|
(* | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
|
723
|
(* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *)
|
724
|
(* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
|
725
|
(* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
|
726
|
(* | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
|
727
|
(* | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
|
728
|
(* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *)
|
729
|
(* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *)
|
730
|
|
731
|
|
732
|
|
733
|
let rec rename_expr f_node f_var expr =
|
734
|
{ expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
|
735
|
and rename_expr_desc f_node f_var expr_desc =
|
736
|
let re = rename_expr f_node f_var in
|
737
|
match expr_desc with
|
738
|
| Expr_const _ -> expr_desc
|
739
|
| Expr_ident i -> Expr_ident (f_var i)
|
740
|
| Expr_array el -> Expr_array (List.map re el)
|
741
|
| Expr_access (e1, d) -> Expr_access (re e1, d)
|
742
|
| Expr_power (e1, d) -> Expr_power (re e1, d)
|
743
|
| Expr_tuple el -> Expr_tuple (List.map re el)
|
744
|
| Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
|
745
|
| Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2)
|
746
|
| Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
|
747
|
| Expr_pre e' -> Expr_pre (re e')
|
748
|
| Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
|
749
|
| Expr_merge (i, hl) ->
|
750
|
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
|
751
|
| Expr_appl (i, e', i') ->
|
752
|
Expr_appl (f_node i, re e', Utils.option_map re i')
|
753
|
|
754
|
let rename_dec_type f_node f_var t = assert false (*
|
755
|
Types.rename_dim_type (Dimension.rename f_node f_var) t*)
|
756
|
|
757
|
let rename_dec_clock f_node f_var c = assert false (*
|
758
|
Clocks.rename_clock_expr f_var c*)
|
759
|
|
760
|
let rename_var f_node f_var v = {
|
761
|
v with
|
762
|
var_id = f_var v.var_id;
|
763
|
var_dec_type = rename_dec_type f_node f_var v.var_type;
|
764
|
var_dec_clock = rename_dec_clock f_node f_var v.var_clock
|
765
|
}
|
766
|
|
767
|
let rename_vars f_node f_var = List.map (rename_var f_node f_var)
|
768
|
|
769
|
let rec rename_eq f_node f_var eq = { eq with
|
770
|
eq_lhs = List.map f_var eq.eq_lhs;
|
771
|
eq_rhs = rename_expr f_node f_var eq.eq_rhs
|
772
|
}
|
773
|
and rename_handler f_node f_var h = {h with
|
774
|
hand_state = f_var h.hand_state;
|
775
|
hand_unless = List.map (
|
776
|
fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
|
777
|
) h.hand_unless;
|
778
|
hand_until = List.map (
|
779
|
fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
|
780
|
) h.hand_until;
|
781
|
hand_locals = rename_vars f_node f_var h.hand_locals;
|
782
|
hand_stmts = rename_stmts f_node f_var h.hand_stmts;
|
783
|
hand_annots = rename_annots f_node f_var h.hand_annots;
|
784
|
|
785
|
}
|
786
|
and rename_aut f_node f_var aut = { aut with
|
787
|
aut_id = f_var aut.aut_id;
|
788
|
aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
|
789
|
}
|
790
|
and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with
|
791
|
| Eq eq -> Eq (rename_eq f_node f_var eq)
|
792
|
| Aut at -> Aut (rename_aut f_node f_var at))
|
793
|
stmts
|
794
|
and rename_annotl f_node f_var annots =
|
795
|
List.map
|
796
|
(fun (key, value) -> key, rename_eexpr f_node f_var value)
|
797
|
annots
|
798
|
and rename_annot f_node f_var annot =
|
799
|
{ annot with annots = rename_annotl f_node f_var annot.annots }
|
800
|
and rename_annots f_node f_var annots =
|
801
|
List.map (rename_annot f_node f_var) annots
|
802
|
and rename_eexpr f_node f_var ee =
|
803
|
{ ee with
|
804
|
eexpr_tag = Utils.new_tag ();
|
805
|
eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
|
806
|
eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
|
807
|
}
|
808
|
|
809
|
|
810
|
|
811
|
|
812
|
let rename_node f_node f_var nd =
|
813
|
let rename_var = rename_var f_node f_var in
|
814
|
let rename_expr = rename_expr f_node f_var in
|
815
|
let rename_stmts = rename_stmts f_node f_var in
|
816
|
let inputs = List.map rename_var nd.node_inputs in
|
817
|
let outputs = List.map rename_var nd.node_outputs in
|
818
|
let locals = List.map rename_var nd.node_locals in
|
819
|
let gen_calls = List.map rename_expr nd.node_gencalls in
|
820
|
let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in
|
821
|
let node_asserts = List.map
|
822
|
(fun a ->
|
823
|
{a with assert_expr =
|
824
|
let expr = a.assert_expr in
|
825
|
rename_expr expr})
|
826
|
nd.node_asserts
|
827
|
in
|
828
|
let node_stmts = rename_stmts nd.node_stmts
|
829
|
|
830
|
|
831
|
in
|
832
|
let spec =
|
833
|
Utils.option_map
|
834
|
(fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *)
|
835
|
nd.node_spec
|
836
|
in
|
837
|
let annot = rename_annots f_node f_var nd.node_annot in
|
838
|
{
|
839
|
node_id = f_node nd.node_id;
|
840
|
node_type = nd.node_type;
|
841
|
node_clock = nd.node_clock;
|
842
|
node_inputs = inputs;
|
843
|
node_outputs = outputs;
|
844
|
node_locals = locals;
|
845
|
node_gencalls = gen_calls;
|
846
|
node_checks = node_checks;
|
847
|
node_asserts = node_asserts;
|
848
|
node_stmts = node_stmts;
|
849
|
node_dec_stateless = nd.node_dec_stateless;
|
850
|
node_stateless = nd.node_stateless;
|
851
|
node_spec = spec;
|
852
|
node_annot = annot;
|
853
|
}
|
854
|
|
855
|
|
856
|
let rename_const f_const c =
|
857
|
{ c with const_id = f_const c.const_id }
|
858
|
|
859
|
let rename_typedef f_var t =
|
860
|
match t.tydef_desc with
|
861
|
| Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
|
862
|
| _ -> t
|
863
|
|
864
|
let rename_prog f_node f_var f_const prog =
|
865
|
List.rev (
|
866
|
List.fold_left (fun accu top ->
|
867
|
(match top.top_decl_desc with
|
868
|
| Node nd ->
|
869
|
{ top with top_decl_desc = Node (rename_node f_node f_var nd) }
|
870
|
| Const c ->
|
871
|
{ top with top_decl_desc = Const (rename_const f_const c) }
|
872
|
| TypeDef tdef ->
|
873
|
{ top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
|
874
|
| ImportedNode _
|
875
|
| Include _ | Open _ -> top)
|
876
|
::accu
|
877
|
) [] prog
|
878
|
)
|
879
|
|
880
|
(* Applies the renaming function [fvar] to every rhs
|
881
|
only when the corresponding lhs satisfies predicate [pvar] *)
|
882
|
let eq_replace_rhs_var pvar fvar eq =
|
883
|
let pvar l = List.exists pvar l in
|
884
|
let rec replace lhs rhs =
|
885
|
{ rhs with expr_desc =
|
886
|
match lhs with
|
887
|
| [] -> assert false
|
888
|
| [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc
|
889
|
| _ ->
|
890
|
(match rhs.expr_desc with
|
891
|
| Expr_tuple tl ->
|
892
|
Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
|
893
|
| Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
|
894
|
let args = expr_list_of_expr arg in
|
895
|
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
|
896
|
| Expr_array _
|
897
|
| Expr_access _
|
898
|
| Expr_power _
|
899
|
| Expr_const _
|
900
|
| Expr_ident _
|
901
|
| Expr_appl _ ->
|
902
|
if pvar lhs
|
903
|
then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
|
904
|
else rhs.expr_desc
|
905
|
| Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
|
906
|
| Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2)
|
907
|
| Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2)
|
908
|
| Expr_pre e' -> Expr_pre (replace lhs e')
|
909
|
| Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
|
910
|
in Expr_when (replace lhs e', i', l)
|
911
|
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i
|
912
|
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
|
913
|
)
|
914
|
}
|
915
|
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
|
916
|
|
917
|
|
918
|
(**********************************************************************)
|
919
|
(* Pretty printers *)
|
920
|
|
921
|
let pp_decl_type fmt tdecl =
|
922
|
match tdecl.top_decl_desc with
|
923
|
| Node nd ->
|
924
|
fprintf fmt "%s: " nd.node_id;
|
925
|
Utils.reset_names ();
|
926
|
fprintf fmt "%a@ " Types.print_ty nd.node_type
|
927
|
| ImportedNode ind ->
|
928
|
fprintf fmt "%s: " ind.nodei_id;
|
929
|
Utils.reset_names ();
|
930
|
fprintf fmt "%a@ " Types.print_ty ind.nodei_type
|
931
|
| Const _ | Include _ | Open _ | TypeDef _ -> ()
|
932
|
|
933
|
let pp_prog_type fmt tdecl_list =
|
934
|
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
|
935
|
|
936
|
let pp_decl_clock fmt cdecl =
|
937
|
match cdecl.top_decl_desc with
|
938
|
| Node nd ->
|
939
|
fprintf fmt "%s: " nd.node_id;
|
940
|
Utils.reset_names ();
|
941
|
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
|
942
|
| ImportedNode ind ->
|
943
|
fprintf fmt "%s: " ind.nodei_id;
|
944
|
Utils.reset_names ();
|
945
|
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
|
946
|
| Const _ | Include _ | Open _ | TypeDef _ -> ()
|
947
|
|
948
|
let pp_prog_clock fmt prog =
|
949
|
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
|
950
|
|
951
|
|
952
|
(* filling node table with internal functions *)
|
953
|
let vdecls_of_typ_ck cpt ty =
|
954
|
let loc = Location.dummy_loc in
|
955
|
List.map
|
956
|
(fun _ -> incr cpt;
|
957
|
let name = sprintf "_var_%d" !cpt in
|
958
|
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
|
959
|
(Types.type_list_of_type ty)
|
960
|
|
961
|
let mk_internal_node id =
|
962
|
let spec = None in
|
963
|
let ty = Env.lookup_value Basic_library.type_env id in
|
964
|
let ck = Env.lookup_value Basic_library.clock_env id in
|
965
|
let (tin, tout) = Types.split_arrow ty in
|
966
|
(*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
|
967
|
let cpt = ref (-1) in
|
968
|
mktop
|
969
|
(ImportedNode
|
970
|
{nodei_id = id;
|
971
|
nodei_type = ty;
|
972
|
nodei_clock = ck;
|
973
|
nodei_inputs = vdecls_of_typ_ck cpt tin;
|
974
|
nodei_outputs = vdecls_of_typ_ck cpt tout;
|
975
|
nodei_stateless = Types.get_static_value ty <> None;
|
976
|
nodei_spec = spec;
|
977
|
(* nodei_annot = []; *)
|
978
|
nodei_prototype = None;
|
979
|
nodei_in_lib = [];
|
980
|
})
|
981
|
|
982
|
let add_internal_funs () =
|
983
|
List.iter
|
984
|
(fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
|
985
|
Basic_library.internal_funs
|
986
|
|
987
|
|
988
|
|
989
|
(* Replace any occurence of a var in vars_to_replace by its associated
|
990
|
expression in defs until e does not contain any such variables *)
|
991
|
let rec substitute_expr vars_to_replace defs e =
|
992
|
let se = substitute_expr vars_to_replace defs in
|
993
|
{ e with expr_desc =
|
994
|
let ed = e.expr_desc in
|
995
|
match ed with
|
996
|
| Expr_const _ -> ed
|
997
|
| Expr_array el -> Expr_array (List.map se el)
|
998
|
| Expr_access (e1, d) -> Expr_access (se e1, d)
|
999
|
| Expr_power (e1, d) -> Expr_power (se e1, d)
|
1000
|
| Expr_tuple el -> Expr_tuple (List.map se el)
|
1001
|
| Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
|
1002
|
| Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2)
|
1003
|
| Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
|
1004
|
| Expr_pre e' -> Expr_pre (se e')
|
1005
|
| Expr_when (e', i, l)-> Expr_when (se e', i, l)
|
1006
|
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
|
1007
|
| Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
|
1008
|
| Expr_ident i ->
|
1009
|
if List.exists (fun v -> v.var_id = i) vars_to_replace then (
|
1010
|
let eq_i eq = eq.eq_lhs = [i] in
|
1011
|
if List.exists eq_i defs then
|
1012
|
let sub = List.find eq_i defs in
|
1013
|
let sub' = se sub.eq_rhs in
|
1014
|
sub'.expr_desc
|
1015
|
else
|
1016
|
assert false
|
1017
|
)
|
1018
|
else
|
1019
|
ed
|
1020
|
|
1021
|
}
|
1022
|
|
1023
|
let rec expr_to_eexpr expr =
|
1024
|
{ eexpr_tag = expr.expr_tag;
|
1025
|
eexpr_qfexpr = expr;
|
1026
|
eexpr_quantifiers = [];
|
1027
|
eexpr_type = expr.expr_type;
|
1028
|
eexpr_clock = expr.expr_clock;
|
1029
|
eexpr_loc = expr.expr_loc;
|
1030
|
}
|
1031
|
(* and expr_desc_to_eexpr_desc expr_desc = *)
|
1032
|
(* let conv = expr_to_eexpr in *)
|
1033
|
(* match expr_desc with *)
|
1034
|
(* | Expr_const c -> EExpr_const (match c with *)
|
1035
|
(* | Const_int x -> EConst_int x *)
|
1036
|
(* | Const_real x -> EConst_real x *)
|
1037
|
(* | Const_float x -> EConst_float x *)
|
1038
|
(* | Const_tag x -> EConst_tag x *)
|
1039
|
(* | _ -> assert false *)
|
1040
|
|
1041
|
(* ) *)
|
1042
|
(* | Expr_ident i -> EExpr_ident i *)
|
1043
|
(* | Expr_tuple el -> EExpr_tuple (List.map conv el) *)
|
1044
|
|
1045
|
(* | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) *)
|
1046
|
(* | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *)
|
1047
|
(* | Expr_pre e' -> EExpr_pre (conv e') *)
|
1048
|
(* | Expr_appl (i, e', i') -> *)
|
1049
|
(* EExpr_appl *)
|
1050
|
(* (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *)
|
1051
|
|
1052
|
(* | Expr_when _ *)
|
1053
|
(* | Expr_merge _ -> assert false *)
|
1054
|
(* | Expr_array _ *)
|
1055
|
(* | Expr_access _ *)
|
1056
|
(* | Expr_power _ -> assert false *)
|
1057
|
(* | Expr_ite (c, t, e) -> assert false *)
|
1058
|
(* | _ -> assert false *)
|
1059
|
|
1060
|
|
1061
|
let rec get_expr_calls nodes e =
|
1062
|
let get_calls = get_expr_calls nodes in
|
1063
|
match e.expr_desc with
|
1064
|
| Expr_const _
|
1065
|
| Expr_ident _ -> Utils.ISet.empty
|
1066
|
| Expr_tuple el
|
1067
|
| Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
|
1068
|
| Expr_pre e1
|
1069
|
| Expr_when (e1, _, _)
|
1070
|
| Expr_access (e1, _)
|
1071
|
| Expr_power (e1, _) -> get_calls e1
|
1072
|
| Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e)
|
1073
|
| Expr_arrow (e1, e2)
|
1074
|
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
|
1075
|
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl
|
1076
|
| Expr_appl (i, e', i') ->
|
1077
|
if Basic_library.is_expr_internal_fun e then
|
1078
|
(get_calls e')
|
1079
|
else
|
1080
|
let calls = Utils.ISet.add i (get_calls e') in
|
1081
|
let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
|
1082
|
if List.exists test nodes then
|
1083
|
match (List.find test nodes).top_decl_desc with
|
1084
|
| Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
|
1085
|
| _ -> assert false
|
1086
|
else
|
1087
|
calls
|
1088
|
|
1089
|
and get_eq_calls nodes eq =
|
1090
|
get_expr_calls nodes eq.eq_rhs
|
1091
|
and get_aut_handler_calls nodes h =
|
1092
|
List.fold_left (fun accu stmt -> match stmt with
|
1093
|
| Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu
|
1094
|
| Aut aut' -> Utils.ISet.union (get_aut_calls nodes aut') accu
|
1095
|
) Utils.ISet.empty h.hand_stmts
|
1096
|
and get_aut_calls nodes aut =
|
1097
|
List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)
|
1098
|
Utils.ISet.empty aut.aut_handlers
|
1099
|
and get_node_calls nodes node =
|
1100
|
let eqs, auts = get_node_eqs node in
|
1101
|
let aut_calls =
|
1102
|
List.fold_left
|
1103
|
(fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)
|
1104
|
Utils.ISet.empty auts
|
1105
|
in
|
1106
|
List.fold_left
|
1107
|
(fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)
|
1108
|
aut_calls eqs
|
1109
|
|
1110
|
let get_expr_vars e =
|
1111
|
let rec get_expr_vars vars e =
|
1112
|
get_expr_desc_vars vars e.expr_desc
|
1113
|
and get_expr_desc_vars vars expr_desc =
|
1114
|
(*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);*)
|
1115
|
match expr_desc with
|
1116
|
| Expr_const _ -> vars
|
1117
|
| Expr_ident x -> Utils.ISet.add x vars
|
1118
|
| Expr_tuple el
|
1119
|
| Expr_array el -> List.fold_left get_expr_vars vars el
|
1120
|
| Expr_pre e1 -> get_expr_vars vars e1
|
1121
|
| Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1
|
1122
|
| Expr_access (e1, d)
|
1123
|
| Expr_power (e1, d) -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
|
1124
|
| Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
|
1125
|
| Expr_arrow (e1, e2)
|
1126
|
| Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
|
1127
|
| Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
|
1128
|
| Expr_appl (_, arg, None) -> get_expr_vars vars arg
|
1129
|
| Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
|
1130
|
in
|
1131
|
get_expr_vars Utils.ISet.empty e
|
1132
|
|
1133
|
let rec expr_has_arrows e =
|
1134
|
expr_desc_has_arrows e.expr_desc
|
1135
|
and expr_desc_has_arrows expr_desc =
|
1136
|
match expr_desc with
|
1137
|
| Expr_const _
|
1138
|
| Expr_ident _ -> false
|
1139
|
| Expr_tuple el
|
1140
|
| Expr_array el -> List.exists expr_has_arrows el
|
1141
|
| Expr_pre e1
|
1142
|
| Expr_when (e1, _, _)
|
1143
|
| Expr_access (e1, _)
|
1144
|
| Expr_power (e1, _) -> expr_has_arrows e1
|
1145
|
| Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
|
1146
|
| Expr_arrow (e1, e2)
|
1147
|
| Expr_fby (e1, e2) -> true
|
1148
|
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
|
1149
|
| Expr_appl (i, e', i') -> expr_has_arrows e'
|
1150
|
|
1151
|
and eq_has_arrows eq =
|
1152
|
expr_has_arrows eq.eq_rhs
|
1153
|
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
|
1154
|
and node_has_arrows node =
|
1155
|
let eqs, auts = get_node_eqs node in
|
1156
|
List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts
|
1157
|
|
1158
|
|
1159
|
|
1160
|
let copy_var_decl vdecl =
|
1161
|
mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid)
|
1162
|
|
1163
|
let copy_const cdecl =
|
1164
|
{ cdecl with const_type = Types.new_var () }
|
1165
|
|
1166
|
let copy_node nd =
|
1167
|
{ nd with
|
1168
|
node_type = Types.new_var ();
|
1169
|
node_clock = Clocks.new_var true;
|
1170
|
node_inputs = List.map copy_var_decl nd.node_inputs;
|
1171
|
node_outputs = List.map copy_var_decl nd.node_outputs;
|
1172
|
node_locals = List.map copy_var_decl nd.node_locals;
|
1173
|
node_gencalls = [];
|
1174
|
node_checks = [];
|
1175
|
node_stateless = None;
|
1176
|
}
|
1177
|
|
1178
|
let copy_top top =
|
1179
|
match top.top_decl_desc with
|
1180
|
| Node nd -> { top with top_decl_desc = Node (copy_node nd) }
|
1181
|
| Const c -> { top with top_decl_desc = Const (copy_const c) }
|
1182
|
| _ -> top
|
1183
|
|
1184
|
let copy_prog top_list =
|
1185
|
List.map copy_top top_list
|
1186
|
|
1187
|
|
1188
|
let rec expr_contains_expr expr_tag expr =
|
1189
|
let search = expr_contains_expr expr_tag in
|
1190
|
expr.expr_tag = expr_tag ||
|
1191
|
(
|
1192
|
match expr.expr_desc with
|
1193
|
| Expr_const _ -> false
|
1194
|
| Expr_array el -> List.exists search el
|
1195
|
| Expr_access (e1, _)
|
1196
|
| Expr_power (e1, _) -> search e1
|
1197
|
| Expr_tuple el -> List.exists search el
|
1198
|
| Expr_ite (c, t, e) -> List.exists search [c;t;e]
|
1199
|
| Expr_arrow (e1, e2)
|
1200
|
| Expr_fby (e1, e2) -> List.exists search [e1; e2]
|
1201
|
| Expr_pre e'
|
1202
|
| Expr_when (e', _, _) -> search e'
|
1203
|
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> search h) hl
|
1204
|
| Expr_appl (_, e', None) -> search e'
|
1205
|
| Expr_appl (_, e', Some e'') -> List.exists search [e'; e'']
|
1206
|
| Expr_ident _ -> false
|
1207
|
)
|
1208
|
|
1209
|
|
1210
|
|
1211
|
(* Generate a new local [node] variable *)
|
1212
|
let cpt_fresh = ref 0
|
1213
|
|
1214
|
let reset_cpt_fresh () =
|
1215
|
cpt_fresh := 0
|
1216
|
|
1217
|
let mk_fresh_var (parentid, ctx_env) loc ty ck =
|
1218
|
let rec aux () =
|
1219
|
incr cpt_fresh;
|
1220
|
let s = Printf.sprintf "__%s_%d" parentid !cpt_fresh in
|
1221
|
if List.exists (fun v -> v.var_id = s) ctx_env then aux () else
|
1222
|
{
|
1223
|
var_id = s;
|
1224
|
var_orig = false;
|
1225
|
var_dec_type = dummy_type_dec;
|
1226
|
var_dec_clock = dummy_clock_dec;
|
1227
|
var_dec_const = false;
|
1228
|
var_dec_value = None;
|
1229
|
var_parent_nodeid = Some parentid;
|
1230
|
var_type = ty;
|
1231
|
var_clock = ck;
|
1232
|
var_loc = loc
|
1233
|
}
|
1234
|
in aux ()
|
1235
|
|
1236
|
|
1237
|
let find_eq xl eqs =
|
1238
|
let rec aux accu eqs =
|
1239
|
match eqs with
|
1240
|
| [] ->
|
1241
|
begin
|
1242
|
Format.eprintf "Looking for variables %a in the following equations@.%a@."
|
1243
|
(Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl
|
1244
|
Printers.pp_node_eqs eqs;
|
1245
|
assert false
|
1246
|
end
|
1247
|
| hd::tl ->
|
1248
|
if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl
|
1249
|
in
|
1250
|
aux [] eqs
|
1251
|
|
1252
|
(* Local Variables: *)
|
1253
|
(* compile-command:"make -C .." *)
|
1254
|
(* End: *)
|