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