Revision d75eb6f1 src/tools/seal/seal_extract.ml
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 774 | 774 |
prefix |
| 775 | 775 |
: |
| 776 | 776 |
((expr * bool) list * (ident * expr) list ) list = |
| 777 |
Format.eprintf "Build_switch with %a@." |
|
| 778 |
(Utils.fprintf_list ~sep:",@ " |
|
| 779 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a@ ]@]" |
|
| 780 |
id |
|
| 781 |
pp_mdefs gel)) |
|
| 782 |
mem_defs; |
|
| 777 | 783 |
(* if all mem_defs have empty guards, we are done, return prefix, |
| 778 | 784 |
mem_defs expr. |
| 779 | 785 |
|
| ... | ... | |
| 884 | 890 |
Each assign is stored in a hash tbl as list of guarded |
| 885 | 891 |
expressions. The memory definition is also "rewritten" as such a |
| 886 | 892 |
list of guarded assigns. *) |
| 887 |
let mem_defs = |
|
| 888 |
List.fold_left (fun accu eq ->
|
|
| 893 |
let mem_defs, output_defs =
|
|
| 894 |
List.fold_left (fun (accu_mems, accu_outputs) eq ->
|
|
| 889 | 895 |
match eq.eq_lhs with |
| 890 | 896 |
| [vid] -> |
| 891 |
(* Only focus on non memory definitions *) |
|
| 892 |
if not (List.exists (fun v -> v.var_id = vid) mems) then ( |
|
| 893 |
report ~level:3 (fun fmt -> |
|
| 894 |
Format.fprintf fmt "Registering variable %s@." vid); |
|
| 895 |
add_def vid eq.eq_rhs; |
|
| 896 |
accu |
|
| 897 |
) |
|
| 898 |
else |
|
| 897 |
(* Only focus on memory definitions *) |
|
| 898 |
if List.exists (fun v -> v.var_id = vid) mems then |
|
| 899 | 899 |
( |
| 900 | 900 |
match eq.eq_rhs.expr_desc with |
| 901 | 901 |
| Expr_pre def_m -> |
| 902 | 902 |
report ~level:3 (fun fmt -> |
| 903 | 903 |
Format.fprintf fmt "Preparing mem %s@." vid); |
| 904 |
(vid, rewrite defs def_m)::accu |
|
| 904 |
(vid, rewrite defs def_m)::accu_mems, accu_outputs
|
|
| 905 | 905 |
| _ -> assert false |
| 906 |
) |
|
| 906 |
) |
|
| 907 |
else if List.exists (fun v -> v.var_id = vid) nd.node_outputs then ( |
|
| 908 |
report ~level:3 (fun fmt -> |
|
| 909 |
Format.fprintf fmt "Output variable %s@." vid); |
|
| 910 |
add_def vid eq.eq_rhs; |
|
| 911 |
accu_mems, (vid, rewrite defs eq.eq_rhs)::accu_outputs |
|
| 912 |
|
|
| 913 |
) |
|
| 914 |
else |
|
| 915 |
( |
|
| 916 |
report ~level:3 (fun fmt -> |
|
| 917 |
Format.fprintf fmt "Registering variable %s@." vid); |
|
| 918 |
add_def vid eq.eq_rhs; |
|
| 919 |
accu_mems, accu_outputs |
|
| 920 |
) |
|
| 907 | 921 |
| _ -> assert false (* should have been removed by normalization *) |
| 908 |
) [] sorted_eqs
|
|
| 922 |
) ([], []) sorted_eqs
|
|
| 909 | 923 |
in |
| 910 | 924 |
|
| 911 | 925 |
|
| ... | ... | |
| 928 | 942 |
let init_defs, update_defs = |
| 929 | 943 |
split_init mem_defs |
| 930 | 944 |
in |
| 945 |
let init_out, update_out = |
|
| 946 |
split_init output_defs |
|
| 947 |
in |
|
| 931 | 948 |
report ~level:3 |
| 932 | 949 |
(fun fmt -> |
| 933 | 950 |
Format.fprintf fmt |
| ... | ... | |
| 959 | 976 |
let sw_sys = |
| 960 | 977 |
build_switch_sys update_defs [] |
| 961 | 978 |
in |
| 962 |
let sw_init, sw_sys = clean_sys sw_init, clean_sys sw_sys in |
|
| 963 | 979 |
|
| 980 |
let init_out = |
|
| 981 |
build_switch_sys init_out [] |
|
| 982 |
in |
|
| 983 |
let update_out = |
|
| 984 |
build_switch_sys update_out [] |
|
| 985 |
in |
|
| 986 |
|
|
| 987 |
let sw_init = clean_sys sw_init in |
|
| 988 |
let sw_sys = clean_sys sw_sys in |
|
| 989 |
let init_out = clean_sys init_out in |
|
| 990 |
let update_out = clean_sys update_out in |
|
| 964 | 991 |
|
| 965 | 992 |
(* Some additional checks *) |
| 966 | 993 |
let pp_gl pp_expr = |
| ... | ... | |
| 1146 | 1173 |
) map [] |
| 1147 | 1174 |
|
| 1148 | 1175 |
in |
| 1149 |
process sw_init, process sw_sys |
|
| 1176 |
process sw_init, process sw_sys, process init_out, process update_out |
|
Also available in: Unified diff