Project

General

Profile

Revision d75eb6f1 src/tools/seal/seal_extract.ml

View differences:

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