Revision 66359a5e src/normalization.ml
src/normalization.ml  

90  90 
var_dec_clock = dummy_clock_dec; 
91  91 
var_dec_const = false; 
92  92 
var_dec_value = None; 
93 
var_parent_nodeid = Some node.node_id; 

93  94 
var_type = ty; 
94  95 
var_clock = ck; 
95  96 
var_loc = loc 
...  ...  
167  168 
(Clocks.clock_list_of_clock expr.expr_clock) in 
168  169 
let new_def = 
169  170 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
170 
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr 

171 
in 

172 
(* Typing and Registering machine type *) 

173 
let _ = Machine_types.type_def node new_aliases expr in 

174 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 

171  175 
else 
172  176 
(defs, vars), expr 
173  177  
...  ...  
420  424 
) (vars, [], []) node.node_asserts in 
421  425 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
422  426 
vars and initial locals ones *) 
423 
let new_locals = node.node_locals @ new_locals in (* we add again, at the 

427 


428 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 

424  429 
beginning of the list the 
425  430 
local declared ones *) 
426  431 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
427  432  
433  
434 
(* Updating annotations: traceability and machine types for fresh variables *) 

435 


436 
(* Compute traceability info: 

437 
 gather newly bound variables 

438 
 compute the associated expression without aliases 

439 
*) 

428  440 
let new_annots = 
429  441 
if !Options.traces then 
430  442 
begin 
431 
(* Compute traceability info: 

432 
 gather newly bound variables 

433 
 compute the associated expression without aliases 

434 
*) 

435 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) new_locals in 

443 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 

436  444 
let norm_traceability = { 
437  445 
annots = List.map (fun v > 
438  446 
let eq = 
...  ...  
446  454 
in 
447  455 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 
448  456 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
457 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 

449  458 
(["traceability"], pair) 
450  459 
) diff_vars; 
451  460 
annot_loc = Location.dummy_loc 
...  ...  
457  466 
node.node_annot 
458  467 
in 
459  468  
469 
let new_annots = 

470 
List.fold_left (fun annots v > 

471 
if Machine_types.is_exportable v then 

472 
let typ = Machine_types.get_specified_type v in 

473 
let typ_name = Machine_types.type_name typ in 

474  
475 
let loc = v.var_loc in 

476 
let typ_as_string = 

477 
mkexpr 

478 
loc 

479 
(Expr_const 

480 
(Const_string typ_name)) 

481 
in 

482 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 

483 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 

484 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 

485 
else 

486 
annots 

487 
) new_annots new_locals 

488 
in 

460  489 
let node = 
461  490 
{ node with 
462 
node_locals = new_locals;


491 
node_locals = all_locals;


463  492 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
464  493 
node_asserts = asserts; 
465  494 
node_annot = new_annots; 
Also available in: Unified diff