Revision 01c7d5e1 src/machine_code.ml
src/machine_code.ml | ||
---|---|---|
99 | 99 |
mstatic: var_decl list; (* static inputs only *) |
100 | 100 |
mstep: step_t; |
101 | 101 |
mspec: node_annot option; |
102 |
mannot: expr_annot option;
|
|
102 |
mannot: expr_annot list;
|
|
103 | 103 |
} |
104 | 104 |
|
105 | 105 |
let pp_step fmt s = |
... | ... | |
170 | 170 |
node_dec_stateless = false; |
171 | 171 |
node_stateless = Some false; |
172 | 172 |
node_spec = None; |
173 |
node_annot = None; }
|
|
173 |
node_annot = []; }
|
|
174 | 174 |
|
175 | 175 |
let arrow_top_decl = |
176 | 176 |
{ |
... | ... | |
202 | 202 |
[MLocalAssign(var_output, LocalVar var_input2)] ] |
203 | 203 |
}; |
204 | 204 |
mspec = None; |
205 |
mannot = None;
|
|
205 |
mannot = [];
|
|
206 | 206 |
} |
207 | 207 |
|
208 | 208 |
let new_instance = |
... | ... | |
229 | 229 |
(* s : step instructions *) |
230 | 230 |
let translate_ident node (m, si, j, d, s) id = |
231 | 231 |
try (* id is a node var *) |
232 |
let var_id = node_var id node in |
|
232 |
let var_id = get_node_var id node in
|
|
233 | 233 |
if ISet.exists (fun v -> v.var_id = id) m |
234 | 234 |
then StateVar var_id |
235 | 235 |
else LocalVar var_id |
... | ... | |
351 | 351 |
(*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*) |
352 | 352 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
353 | 353 |
| [x], Expr_arrow (e1, e2) -> |
354 |
let var_x = node_var x node in |
|
354 |
let var_x = get_node_var x node in
|
|
355 | 355 |
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in |
356 | 356 |
let c1 = translate_expr node args e1 in |
357 | 357 |
let c2 = translate_expr node args e2 in |
... | ... | |
360 | 360 |
Utils.IMap.add o (arrow_top_decl, []) j, |
361 | 361 |
d, |
362 | 362 |
(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s) |
363 |
| [x], Expr_pre e1 when ISet.mem (node_var x node) d -> |
|
364 |
let var_x = node_var x node in |
|
363 |
| [x], Expr_pre e1 when ISet.mem (get_node_var x node) d ->
|
|
364 |
let var_x = get_node_var x node in
|
|
365 | 365 |
(ISet.add var_x m, |
366 | 366 |
si, |
367 | 367 |
j, |
368 | 368 |
d, |
369 | 369 |
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s) |
370 |
| [x], Expr_fby (e1, e2) when ISet.mem (node_var x node) d -> |
|
371 |
let var_x = node_var x node in |
|
370 |
| [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
|
|
371 |
let var_x = get_node_var x node in
|
|
372 | 372 |
(ISet.add var_x m, |
373 | 373 |
MStateAssign (var_x, translate_expr node args e1) :: si, |
374 | 374 |
j, |
... | ... | |
376 | 376 |
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s) |
377 | 377 |
|
378 | 378 |
| p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) -> |
379 |
let var_p = List.map (fun v -> node_var v node) p in |
|
379 |
let var_p = List.map (fun v -> get_node_var v node) p in
|
|
380 | 380 |
let el = |
381 | 381 |
match arg.expr_desc with |
382 | 382 |
| Expr_tuple el -> el |
... | ... | |
402 | 402 |
| [x], Expr_ite (c, t, e) |
403 | 403 |
when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) |
404 | 404 |
-> |
405 |
let var_x = node_var x node in |
|
405 |
let var_x = get_node_var x node in
|
|
406 | 406 |
(m, |
407 | 407 |
si, |
408 | 408 |
j, |
... | ... | |
412 | 412 |
) |
413 | 413 |
|
414 | 414 |
| [x], _ -> ( |
415 |
let var_x = node_var x node in |
|
415 |
let var_x = get_node_var x node in
|
|
416 | 416 |
(m, si, j, d, |
417 | 417 |
control_on_clock |
418 | 418 |
node |
Also available in: Unified diff