Revision 1eda3e78
Added by Xavier Thirioux almost 8 years ago
| 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 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
- work in progress for automata...