Revision 1eda3e78 src/corelang.ml
src/corelang.ml  

68  68 
var_clock = Clocks.new_var false; 
69  69 
var_loc = c.const_loc } 
70  70  
71 
let mk_new_name vdecl_list id =


71 
let mk_new_name used id =


72  72 
let rec new_name name cpt = 
73 
if List.exists (fun v > v.var_id = name) vdecl_list


73 
if used name


74  74 
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) 
75  75 
else name 
76  76 
in new_name id 1 
...  ...  
475  475  
476  476 
let get_node_var id node = get_var id (get_node_vars node) 
477  477  
478 
let get_node_eqs = 

479 
let get_eqs stmts = 

480 
List.fold_right 

481 
(fun stmt res > 

482 
match stmt with 

483 
 Eq eq > eq :: res 

484 
 Aut _ > assert false) 

485 
stmts 

486 
[] in 

487 
let table_eqs = Hashtbl.create 23 in 

488 
(fun nd > 

489 
try 

490 
let (old, res) = Hashtbl.find table_eqs nd.node_id 

491 
in if old == nd.node_stmts then res else raise Not_found 

492 
with Not_found > 

493 
let res = get_eqs nd.node_stmts in 

494 
begin 

495 
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res); 

496 
res 

497 
end) 

498  
478  499 
let get_node_eq id node = 
479 
List.find (fun eq > List.mem id eq.eq_lhs) node.node_eqs


500 
List.find (fun eq > List.mem id eq.eq_lhs) (get_node_eqs node)


480  501  
481  502 
let get_nodes prog = 
482  503 
List.fold_left ( 
...  ...  
639  660 
rename_expr f_node f_var f_const expr}) 
640  661 
nd.node_asserts 
641  662 
in 
642 
let eqs = List.map rename_eq nd.node_eqs in


663 
let node_stmts = List.map (fun eq > Eq (rename_eq eq)) (get_node_eqs nd) in


643  664 
let spec = 
644  665 
Utils.option_map 
645  666 
(fun s > rename_node_annot f_node f_var f_const s) 
...  ...  
660  681 
node_gencalls = gen_calls; 
661  682 
node_checks = node_checks; 
662  683 
node_asserts = node_asserts; 
663 
node_eqs = eqs;


684 
node_stmts = node_stmts;


664  685 
node_dec_stateless = nd.node_dec_stateless; 
665  686 
node_stateless = nd.node_stateless; 
666  687 
node_spec = spec; 
...  ...  
889  910 
and get_eq_calls nodes eq = 
890  911 
get_expr_calls nodes eq.eq_rhs 
891  912 
and get_node_calls nodes node = 
892 
List.fold_left (fun accu eq > Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs


913 
List.fold_left (fun accu eq > Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)


893  914  
894  915 
let rec get_expr_vars vars e = 
895  916 
get_expr_desc_vars vars e.expr_desc 
...  ...  
932  953 
and eq_has_arrows eq = 
933  954 
expr_has_arrows eq.eq_rhs 
934  955 
and node_has_arrows node = 
935 
List.exists (fun eq > eq_has_arrows eq) node.node_eqs


956 
List.exists (fun eq > eq_has_arrows eq) (get_node_eqs node)


936  957  
937  958 
(* Local Variables: *) 
938  959 
(* compilecommand:"make C .." *) 
Also available in: Unified diff