1
|
open Lustre_types
|
2
|
open Machine_code_types
|
3
|
open Spec_types
|
4
|
open Corelang
|
5
|
open Utils.Format
|
6
|
|
7
|
let print_statelocaltag = true
|
8
|
|
9
|
let is_memory m id = List.exists (fun o -> o.var_id = id.var_id) m.mmemory
|
10
|
|
11
|
let is_reset_flag id = id.var_id = "_reset"
|
12
|
|
13
|
let pp_vdecl fmt v = pp_print_string fmt v.var_id
|
14
|
|
15
|
let rec pp_val m fmt v =
|
16
|
let pp_val = pp_val m in
|
17
|
match v.value_desc with
|
18
|
| Cst c ->
|
19
|
Printers.pp_const fmt c
|
20
|
| Var v ->
|
21
|
if is_memory m v then
|
22
|
if print_statelocaltag then fprintf fmt "{%s}" v.var_id
|
23
|
else pp_print_string fmt v.var_id
|
24
|
else if print_statelocaltag then fprintf fmt "%s" v.var_id
|
25
|
else pp_vdecl fmt v
|
26
|
| Array vl ->
|
27
|
pp_print_bracketed pp_val fmt vl
|
28
|
| Access (t, i) ->
|
29
|
fprintf fmt "%a[%a]" pp_val t pp_val i
|
30
|
| Power (v, n) ->
|
31
|
fprintf fmt "(%a^%a)" pp_val v pp_val n
|
32
|
| Fun (n, vl) ->
|
33
|
fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
|
34
|
| ResetFlag ->
|
35
|
fprintf fmt "RESET"
|
36
|
|
37
|
module PrintSpec = struct
|
38
|
let pp_reg fmt = function
|
39
|
| ResetFlag ->
|
40
|
pp_print_string fmt "{RESET}"
|
41
|
| StateVar v ->
|
42
|
fprintf fmt "{OUT:%a}" pp_vdecl v
|
43
|
|
44
|
let pp_expr :
|
45
|
type a. machine_t -> formatter -> (value_t, a) expression_t -> unit =
|
46
|
fun m fmt -> function
|
47
|
| Val v ->
|
48
|
pp_val m fmt v
|
49
|
| Tag t ->
|
50
|
pp_print_string fmt t
|
51
|
| Var v ->
|
52
|
pp_vdecl fmt v
|
53
|
| Memory r ->
|
54
|
pp_reg fmt r
|
55
|
|
56
|
let pp_predicate m fmt p =
|
57
|
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
58
|
fun fmt e -> pp_expr m fmt e
|
59
|
in
|
60
|
match p with
|
61
|
| Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
|
62
|
fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f
|
63
|
(pp_print_option
|
64
|
~none:(fun fmt () -> pp_print_string fmt "SELF")
|
65
|
pp_print_string)
|
66
|
inst
|
67
|
(pp_print_option pp_print_int)
|
68
|
i
|
69
|
(pp_print_parenthesized pp_expr)
|
70
|
(inputs @ locals @ outputs)
|
71
|
| Reset (f, inst, r) ->
|
72
|
fprintf fmt "Reset_%a<%a> on %a" pp_print_string f pp_print_string inst
|
73
|
(pp_val m) r
|
74
|
| MemoryPack (f, inst, i) ->
|
75
|
fprintf fmt "MemoryPack_%a<%a>%a" pp_print_string f
|
76
|
(pp_print_option
|
77
|
~none:(fun fmt () -> pp_print_string fmt "SELF")
|
78
|
pp_print_string)
|
79
|
inst
|
80
|
(pp_print_option pp_print_int)
|
81
|
i
|
82
|
| ResetCleared f ->
|
83
|
fprintf fmt "ResetCleared_%a" pp_print_string f
|
84
|
| Initialization ->
|
85
|
()
|
86
|
|
87
|
let pp_spec m =
|
88
|
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
89
|
fun fmt e -> pp_expr m fmt e
|
90
|
in
|
91
|
let rec pp_spec fmt f =
|
92
|
match f with
|
93
|
| True ->
|
94
|
pp_print_string fmt "true"
|
95
|
| False ->
|
96
|
pp_print_string fmt "false"
|
97
|
| Equal (a, b) ->
|
98
|
fprintf fmt "%a == %a" pp_expr a pp_expr b
|
99
|
| And fs ->
|
100
|
pp_print_list
|
101
|
~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
|
102
|
(fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)
|
103
|
fmt fs
|
104
|
| Or fs ->
|
105
|
pp_print_list
|
106
|
~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
|
107
|
(fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)
|
108
|
fmt fs
|
109
|
| Imply (a, b) ->
|
110
|
fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
|
111
|
| Exists (xs, a) ->
|
112
|
fprintf fmt "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
|
113
|
(pp_comma_list Printers.pp_var)
|
114
|
xs pp_spec a
|
115
|
| Forall (xs, a) ->
|
116
|
fprintf fmt "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
|
117
|
(pp_comma_list Printers.pp_var)
|
118
|
xs pp_spec a
|
119
|
| Ternary (e, a, b) ->
|
120
|
fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])" pp_expr e
|
121
|
pp_spec a pp_spec b
|
122
|
| Predicate p ->
|
123
|
pp_predicate m fmt p
|
124
|
| StateVarPack r ->
|
125
|
fprintf fmt "StateVarPack<%a>" pp_reg r
|
126
|
| ExistsMem (_f, a, b) ->
|
127
|
fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
|
128
|
in
|
129
|
pp_spec
|
130
|
end
|
131
|
|
132
|
let pp_spec m =
|
133
|
if !Options.spec <> "no" then
|
134
|
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
|
135
|
(fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
|
136
|
else pp_print_nothing
|
137
|
|
138
|
let rec pp_instr m fmt i =
|
139
|
let pp_val = pp_val m in
|
140
|
let pp_branch = pp_branch m in
|
141
|
(match i.instr_desc with
|
142
|
| MLocalAssign (i, v) ->
|
143
|
fprintf fmt "%s := %a" i.var_id pp_val v
|
144
|
| MStateAssign (i, v) ->
|
145
|
fprintf fmt "{%s} := %a" i.var_id pp_val v
|
146
|
| MResetAssign b ->
|
147
|
fprintf fmt "RESET := %a" pp_print_bool b
|
148
|
| MSetReset i ->
|
149
|
fprintf fmt "set_reset %s" i
|
150
|
| MClearReset ->
|
151
|
fprintf fmt "clear_reset %s" m.mname.node_id
|
152
|
| MNoReset i ->
|
153
|
fprintf fmt "noreset %s" i
|
154
|
| MStep (il, i, vl) ->
|
155
|
fprintf fmt "%a := %s%a" (pp_comma_list pp_vdecl) il i
|
156
|
(pp_print_parenthesized pp_val)
|
157
|
vl
|
158
|
| MBranch (g, hl) ->
|
159
|
fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}" pp_val g
|
160
|
(pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch)
|
161
|
hl
|
162
|
| MComment s ->
|
163
|
pp_print_string fmt s
|
164
|
| MSpec s ->
|
165
|
pp_print_string fmt ("@" ^ s));
|
166
|
(* Annotation *)
|
167
|
(* let _ = *)
|
168
|
(* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original
|
169
|
expr: %a" Printers.pp_expr e *)
|
170
|
(* in *)
|
171
|
(match i.lustre_eq with
|
172
|
| None ->
|
173
|
()
|
174
|
| Some eq ->
|
175
|
fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq);
|
176
|
pp_spec m fmt i.instr_spec
|
177
|
|
178
|
and pp_branch m fmt (t, h) =
|
179
|
fprintf fmt "@[<v 2>%s:@,%a@]" t
|
180
|
(pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m))
|
181
|
h
|
182
|
|
183
|
let pp_instrs m = pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
|
184
|
|
185
|
(* merge log: get_node_def was in c0f8 *)
|
186
|
(* Returns the node/machine associated to id in m calls *)
|
187
|
let get_node_def id m =
|
188
|
try
|
189
|
let decl, _ = List.assoc id m.mcalls in
|
190
|
Corelang.node_of_top decl
|
191
|
with Not_found ->
|
192
|
(* eprintf "Unable to find node %s in list [%a]@.@?" *)
|
193
|
(* id *)
|
194
|
(* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n))
|
195
|
m.mcalls *)
|
196
|
(* ; *)
|
197
|
raise Not_found
|
198
|
|
199
|
(* merge log: machine_vars was in 44686 *)
|
200
|
let machine_vars m =
|
201
|
m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
|
202
|
|
203
|
let pp_step m fmt s =
|
204
|
fprintf fmt
|
205
|
"@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ \
|
206
|
asserts : @[%a@]@]@ "
|
207
|
(pp_comma_list Printers.pp_var)
|
208
|
s.step_inputs
|
209
|
(pp_comma_list Printers.pp_var)
|
210
|
s.step_outputs
|
211
|
(pp_comma_list Printers.pp_var)
|
212
|
s.step_locals
|
213
|
(pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
|
214
|
s.step_checks (pp_instrs m) s.step_instrs
|
215
|
(pp_comma_list (pp_val m))
|
216
|
s.step_asserts
|
217
|
|
218
|
let pp_static_call fmt (node, args) =
|
219
|
fprintf fmt "%s<%a>" (node_name node)
|
220
|
(pp_comma_list Dimension.pp_dimension)
|
221
|
args
|
222
|
|
223
|
let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2
|
224
|
|
225
|
let pp_memory_pack m fmt mp =
|
226
|
fprintf fmt "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]" pp_print_string
|
227
|
mp.mpname.node_id
|
228
|
(pp_print_option pp_print_int)
|
229
|
mp.mpindex (PrintSpec.pp_spec m) mp.mpformula
|
230
|
|
231
|
let pp_memory_packs m fmt =
|
232
|
if !Options.spec <> "no" then
|
233
|
fprintf fmt "@[<v 2>memory_packs:@ %a@]" (pp_print_list (pp_memory_pack m))
|
234
|
else pp_print_nothing fmt
|
235
|
|
236
|
let pp_transition m fmt t =
|
237
|
fprintf fmt "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]" pp_print_string
|
238
|
t.tname.node_id
|
239
|
(pp_print_option pp_print_int)
|
240
|
t.tindex
|
241
|
(pp_print_parenthesized pp_vdecl)
|
242
|
(t.tinputs @ t.tlocals @ t.toutputs)
|
243
|
(PrintSpec.pp_spec m) t.tformula
|
244
|
|
245
|
let pp_transitions m fmt =
|
246
|
if !Options.spec <> "no" then
|
247
|
fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m))
|
248
|
else pp_print_nothing fmt
|
249
|
|
250
|
let pp_machine fmt m =
|
251
|
fprintf fmt
|
252
|
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const \
|
253
|
: %a@ step :@ @[<v 2>%a@]@ spec : @[<v>%t@ %a@ @ %a@]@ annot \
|
254
|
: @[%a@]@]@ "
|
255
|
m.mname.node_id
|
256
|
(pp_comma_list Printers.pp_var)
|
257
|
m.mmemory
|
258
|
(pp_comma_list pp_instance)
|
259
|
m.minstances (pp_instrs m) m.minit (pp_instrs m) m.mconst (pp_step m)
|
260
|
m.mstep
|
261
|
(fun fmt ->
|
262
|
match m.mspec.mnode_spec with
|
263
|
| None ->
|
264
|
()
|
265
|
| Some (NodeSpec id) ->
|
266
|
fprintf fmt "cocospec: %s" id
|
267
|
| Some (Contract spec) ->
|
268
|
Printers.pp_spec fmt spec)
|
269
|
(pp_memory_packs m) m.mspec.mmemory_packs (pp_transitions m)
|
270
|
m.mspec.mtransitions
|
271
|
(pp_print_list Printers.pp_expr_annot)
|
272
|
m.mannot
|
273
|
|
274
|
let pp_machines = pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
|
275
|
|
276
|
let rec is_const_value v =
|
277
|
match v.value_desc with
|
278
|
| Cst _ ->
|
279
|
true
|
280
|
| Fun (_, args) ->
|
281
|
Basic_library.is_value_internal_fun v && List.for_all is_const_value args
|
282
|
| _ ->
|
283
|
false
|
284
|
|
285
|
(* Returns the declared stateless status and the computed one. *)
|
286
|
let get_stateless_status_node n =
|
287
|
( n.node_dec_stateless,
|
288
|
try Utils.desome n.node_stateless
|
289
|
with _ ->
|
290
|
failwith ("stateless status of machine " ^ n.node_id ^ " not computed") )
|
291
|
|
292
|
let get_stateless_status_top_decl td =
|
293
|
match td.top_decl_desc with
|
294
|
| Node n ->
|
295
|
get_stateless_status_node n
|
296
|
| ImportedNode n ->
|
297
|
n.nodei_stateless, false
|
298
|
| _ ->
|
299
|
true, false
|
300
|
|
301
|
let get_stateless_status m = get_stateless_status_node m.mname
|
302
|
|
303
|
let is_stateless m = m.minstances = [] && m.mmemory = []
|
304
|
|
305
|
(* let is_input m id =
|
306
|
* List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
|
307
|
|
308
|
let is_output m id =
|
309
|
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
|
310
|
|
311
|
let get_instr_spec i = i.instr_spec
|
312
|
|
313
|
let mk_val v t = { value_desc = v; value_type = t; value_annot = None }
|
314
|
|
315
|
let vdecl_to_val vd = mk_val (Var vd) vd.var_type
|
316
|
|
317
|
let vdecls_to_vals = List.map vdecl_to_val
|
318
|
|
319
|
let id_to_tag id =
|
320
|
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
|
321
|
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
|
322
|
|
323
|
let mk_conditional ?lustre_eq c t e =
|
324
|
mkinstr ?lustre_eq
|
325
|
(* (Ternary (Val c,
|
326
|
* And (List.map get_instr_spec t),
|
327
|
* And (List.map get_instr_spec e))) *)
|
328
|
(MBranch (c, [ tag_true, t; tag_false, e ]))
|
329
|
|
330
|
let mk_branch ?lustre_eq c br =
|
331
|
mkinstr ?lustre_eq
|
332
|
(* (And (List.map (fun (l, instrs) ->
|
333
|
* Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
|
334
|
* br)) *)
|
335
|
(MBranch (c, br))
|
336
|
|
337
|
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
|
338
|
|
339
|
let mk_assign ?lustre_eq x v =
|
340
|
mkinstr ?lustre_eq (* (Equal (Var x, Val v)) *) (MLocalAssign (x, v))
|
341
|
|
342
|
let arrow_machine =
|
343
|
let state = "_first" in
|
344
|
let var_state =
|
345
|
dummy_var_decl state Type_predef.type_bool
|
346
|
(* (Types.new_ty Types.Tbool) *)
|
347
|
in
|
348
|
let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
|
349
|
let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
|
350
|
let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
|
351
|
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
|
352
|
assert (var_input1.var_type = var_input2.var_type);
|
353
|
let t_arg = var_input1.var_type in
|
354
|
(* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de
|
355
|
reprendre le type des variables non ? *)
|
356
|
{
|
357
|
mname = Arrow.arrow_desc;
|
358
|
mmemory = [ var_state ];
|
359
|
mcalls = [];
|
360
|
minstances = [];
|
361
|
minit = [ mkinstr (MStateAssign (var_state, cst true)) ];
|
362
|
mstatic = [];
|
363
|
mconst = [];
|
364
|
mstep =
|
365
|
{
|
366
|
step_inputs = Arrow.arrow_desc.node_inputs;
|
367
|
step_outputs = Arrow.arrow_desc.node_outputs;
|
368
|
step_locals = [];
|
369
|
step_checks = [];
|
370
|
step_instrs =
|
371
|
[
|
372
|
mk_conditional
|
373
|
(mk_val (Var var_state) Type_predef.type_bool)
|
374
|
(List.map mkinstr
|
375
|
[
|
376
|
MStateAssign (var_state, cst false);
|
377
|
MLocalAssign (var_output, mk_val (Var var_input1) t_arg);
|
378
|
])
|
379
|
(List.map mkinstr
|
380
|
[ MLocalAssign (var_output, mk_val (Var var_input2) t_arg) ]);
|
381
|
];
|
382
|
step_asserts = [];
|
383
|
};
|
384
|
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
|
385
|
mannot = [];
|
386
|
msch = None;
|
387
|
}
|
388
|
|
389
|
let empty_desc =
|
390
|
{
|
391
|
node_id = Arrow.arrow_id;
|
392
|
node_type = Types.bottom;
|
393
|
node_clock = Clocks.bottom;
|
394
|
node_inputs = [];
|
395
|
node_outputs = [];
|
396
|
node_locals = [];
|
397
|
node_gencalls = [];
|
398
|
node_checks = [];
|
399
|
node_asserts = [];
|
400
|
node_stmts = [];
|
401
|
node_dec_stateless = true;
|
402
|
node_stateless = Some true;
|
403
|
node_spec = None;
|
404
|
node_annot = [];
|
405
|
node_iscontract = false;
|
406
|
}
|
407
|
|
408
|
let empty_machine =
|
409
|
{
|
410
|
mname = empty_desc;
|
411
|
mmemory = [];
|
412
|
mcalls = [];
|
413
|
minstances = [];
|
414
|
minit = [];
|
415
|
mstatic = [];
|
416
|
mconst = [];
|
417
|
mstep =
|
418
|
{
|
419
|
step_inputs = [];
|
420
|
step_outputs = [];
|
421
|
step_locals = [];
|
422
|
step_checks = [];
|
423
|
step_instrs = [];
|
424
|
step_asserts = [];
|
425
|
};
|
426
|
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
|
427
|
mannot = [];
|
428
|
msch = None;
|
429
|
}
|
430
|
|
431
|
let new_instance =
|
432
|
let cpt = ref (-1) in
|
433
|
fun callee tag ->
|
434
|
let o =
|
435
|
if Stateless.check_node callee then node_name callee
|
436
|
else
|
437
|
Printf.sprintf "ni_%d"
|
438
|
(incr cpt;
|
439
|
!cpt)
|
440
|
in
|
441
|
let o =
|
442
|
if !Options.ansi && is_generic_node callee then
|
443
|
Printf.sprintf "%s_inst_%d" o
|
444
|
(incr cpt;
|
445
|
!cpt)
|
446
|
else o
|
447
|
in
|
448
|
o
|
449
|
|
450
|
let get_machine_opt machines name =
|
451
|
List.fold_left
|
452
|
(fun res m ->
|
453
|
match res with
|
454
|
| Some _ ->
|
455
|
res
|
456
|
| None ->
|
457
|
if m.mname.node_id = name then Some m else None)
|
458
|
None machines
|
459
|
|
460
|
let get_machine machines node_name =
|
461
|
try Utils.desome (get_machine_opt machines node_name)
|
462
|
with Utils.DeSome ->
|
463
|
eprintf "Unable to find machine %s in machines %a@.@?" node_name
|
464
|
(Utils.fprintf_list ~sep:", " (fun fmt m ->
|
465
|
pp_print_string fmt m.mname.node_id))
|
466
|
machines;
|
467
|
assert false
|
468
|
|
469
|
let get_const_assign m id =
|
470
|
try
|
471
|
match
|
472
|
get_instr_desc
|
473
|
(List.find
|
474
|
(fun instr ->
|
475
|
match get_instr_desc instr with
|
476
|
| MLocalAssign (v, _) ->
|
477
|
v == id
|
478
|
| _ ->
|
479
|
false)
|
480
|
m.mconst)
|
481
|
with
|
482
|
| MLocalAssign (_, e) ->
|
483
|
e
|
484
|
| _ ->
|
485
|
assert false
|
486
|
with Not_found -> assert false
|
487
|
|
488
|
let value_of_ident loc m id =
|
489
|
(* is is a state var *)
|
490
|
try
|
491
|
let v = List.find (fun v -> v.var_id = id) m.mmemory in
|
492
|
mk_val (Var v) v.var_type
|
493
|
with Not_found -> (
|
494
|
try
|
495
|
(* id is a node var *)
|
496
|
let v = get_node_var id m.mname in
|
497
|
mk_val (Var v) v.var_type
|
498
|
with Not_found -> (
|
499
|
try
|
500
|
(* id is a constant *)
|
501
|
let c =
|
502
|
Corelang.var_decl_of_const
|
503
|
(const_of_top (Hashtbl.find Corelang.consts_table id))
|
504
|
in
|
505
|
mk_val (Var c) c.var_type
|
506
|
with Not_found ->
|
507
|
(* id is a tag *)
|
508
|
let t = Const_tag id in
|
509
|
mk_val (Cst t) (Typing.type_const loc t)))
|
510
|
|
511
|
(* type of internal fun used in dimension expression *)
|
512
|
let type_of_value_appl f args =
|
513
|
if List.mem f Basic_library.arith_funs then (List.hd args).value_type
|
514
|
else Type_predef.type_bool
|
515
|
|
516
|
let rec value_of_dimension m dim =
|
517
|
match dim.Dimension.dim_desc with
|
518
|
| Dimension.Dbool b ->
|
519
|
mk_val
|
520
|
(Cst (Const_tag (if b then tag_true else tag_false)))
|
521
|
Type_predef.type_bool
|
522
|
| Dimension.Dint i ->
|
523
|
mk_val (Cst (Const_int i)) Type_predef.type_int
|
524
|
| Dimension.Dident v ->
|
525
|
value_of_ident dim.Dimension.dim_loc m v
|
526
|
| Dimension.Dappl (f, args) ->
|
527
|
let vargs = List.map (value_of_dimension m) args in
|
528
|
mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)
|
529
|
| Dimension.Dite (i, t, e) -> (
|
530
|
match List.map (value_of_dimension m) [ i; t; e ] with
|
531
|
| [ vi; vt; ve ] ->
|
532
|
mk_val (Fun ("ite", [ vi; vt; ve ])) vt.value_type
|
533
|
| _ ->
|
534
|
assert false)
|
535
|
| Dimension.Dlink dim' ->
|
536
|
value_of_dimension m dim'
|
537
|
| _ ->
|
538
|
assert false
|
539
|
|
540
|
let rec dimension_of_value value =
|
541
|
match value.value_desc with
|
542
|
| Cst (Const_tag t) when t = tag_true ->
|
543
|
Dimension.mkdim_bool Location.dummy_loc true
|
544
|
| Cst (Const_tag t) when t = tag_false ->
|
545
|
Dimension.mkdim_bool Location.dummy_loc false
|
546
|
| Cst (Const_int i) ->
|
547
|
Dimension.mkdim_int Location.dummy_loc i
|
548
|
| Var v ->
|
549
|
Dimension.mkdim_ident Location.dummy_loc v.var_id
|
550
|
| Fun (f, args) ->
|
551
|
Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
|
552
|
| _ ->
|
553
|
assert false
|
554
|
|
555
|
let rec join_branches hl1 hl2 =
|
556
|
match hl1, hl2 with
|
557
|
| [], _ ->
|
558
|
hl2
|
559
|
| _, [] ->
|
560
|
hl1
|
561
|
| (t1, h1) :: q1, (t2, h2) :: q2 ->
|
562
|
if t1 < t2 then (t1, h1) :: join_branches q1 hl2
|
563
|
else if t1 > t2 then (t2, h2) :: join_branches hl1 q2
|
564
|
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
|
565
|
|
566
|
and join_guards inst1 insts2 =
|
567
|
match get_instr_desc inst1, insts2 with
|
568
|
| ( MBranch (x1, hl1),
|
569
|
({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 )
|
570
|
when x1 = x2 ->
|
571
|
mkinstr
|
572
|
~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
|
573
|
(* TODO on pourrait uniquement concatener les lustres de inst1 et
|
574
|
hd(inst2) *)
|
575
|
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
|
576
|
:: insts2
|
577
|
| _ ->
|
578
|
inst1 :: insts2
|
579
|
|
580
|
let join_guards_list insts = List.fold_right join_guards insts []
|