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