Revision a38c681e src/normalization.ml
src/normalization.ml  

65  65 
match expr.expr_desc with 
66  66 
 Expr_arrow (e1, e2) > 
67  67 
let loc = expr.expr_loc in 
68 
let ck = expr.expr_clock in


68 
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in


69  69 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 
70  70 
 _ > assert false 
71  71  
...  ...  
129  129  
130  130 
(* Create an alias for [expr], if none exists yet *) 
131  131 
let mk_expr_alias node (defs, vars) expr = 
132 
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) 

132  133 
match get_expr_alias defs expr with 
133  134 
 Some eq > 
134  135 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
...  ...  
387  388 
*) 
388  389 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) new_locals in 
389  390 
let norm_traceability = { 
390 
annots =


391 
annots = 

391  392 
List.map 
392  393 
(fun v > 
393  394 
let expr = substitute_expr diff_vars defs ( 
394 
let eq = List.find (fun eq > eq.eq_lhs = [v.var_id]) defs in 

395 
let eq = try 

396 
List.find (fun eq > eq.eq_lhs = [v.var_id]) defs 

397 
with Not_found > (Format.eprintf "var not found %s@." v.var_id; assert false) in 

395  398 
eq.eq_rhs) in 
396  399 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
397  400 
["horn_backend";"trace"], pair 
398 
)


401 
)


399  402 
diff_vars ; 
400  403 
annot_loc = Location.dummy_loc 
401  404 
} 
Also available in: Unified diff