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