Move some definitions to a new PureUtils.ml file

4 files changed, 104 insertions, 111 deletions

diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index efe26bc4..b3e65055 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -2,6 +2,7 @@
 
 open Errors
 open Pure
+open PureUtils
 open TranslateCore
 
 (** The local logger *)
@@ -299,7 +300,7 @@ let to_monadic (def : fun_def) : fun_def =
       method! visit_call env call =
         (* If no arguments, introduce unit *)
         if call.args = [] then
-          let args = [ Value (SymbolicToPure.unit_rvalue, None) ] in
+          let args = [ Value (unit_rvalue, None) ] in
           { call with args } (* Otherwise: nothing to do *)
         else super#visit_call env call
     end
@@ -311,12 +312,10 @@ let to_monadic (def : fun_def) : fun_def =
   let def =
     if def.inputs = [] then (
       assert (def.signature.inputs = []);
-      let signature =
-        { def.signature with inputs = [ SymbolicToPure.unit_ty ] }
-      in
+      let signature = { def.signature with inputs = [ unit_ty ] } in
       let var_cnt = get_expression_min_var_counter def.body in
       let id, _ = VarId.fresh var_cnt in
-      let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in
+      let var = { id; basename = None; ty = unit_ty } in
       let inputs = [ var ] in
       { def with signature; inputs })
     else def
@@ -326,10 +325,10 @@ let to_monadic (def : fun_def) : fun_def =
     match (def.back_id, def.signature.outputs) with
     | None, [ out_ty ] ->
         (* Forward function: there is always exactly one output *)
-        SymbolicToPure.mk_result_ty out_ty
+        mk_result_ty out_ty
     | Some _, outputs ->
         (* Backward function: we have to group them *)
-        SymbolicToPure.mk_result_ty (SymbolicToPure.mk_tuple_ty outputs)
+        mk_result_ty (mk_tuple_ty outputs)
     | _ -> failwith "Unreachable"
   in
   let outputs = [ output_ty ] in
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
new file mode 100644
index 00000000..e5ce94a0
--- /dev/null
+++ b/src/PureUtils.ml
@@ -0,0 +1,90 @@
+open Identifiers
+open Pure
+
+(* TODO : move *)
+let binop_can_fail (binop : E.binop) : bool =
+  match binop with
+  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
+  | Div | Rem | Add | Sub | Mul -> true
+  | Shl | Shr -> raise Errors.Unimplemented
+
+let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
+
+let mk_tuple_ty (tys : ty list) : ty = Adt (Tuple, tys)
+
+let unit_ty : ty = Adt (Tuple, [])
+
+let unit_rvalue : typed_rvalue =
+  let value = RvAdt { variant_id = None; field_values = [] } in
+  let ty = unit_ty in
+  { value; ty }
+
+let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
+  let value = RvPlace (mk_place_from_var v) in
+  let ty = v.ty in
+  { value; ty }
+
+let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
+  let value = LvVar (Var (v, mp)) in
+  let ty = v.ty in
+  { value; ty }
+
+let mk_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue =
+  let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in
+  let ty = Adt (Tuple, tys) in
+  let value = LvAdt { variant_id = None; field_values = vl } in
+  { value; ty }
+
+let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id)
+    (vl : typed_lvalue list) : typed_lvalue =
+  let value = LvAdt { variant_id = Some variant_id; field_values = vl } in
+  { value; ty = adt_ty }
+
+let ty_as_integer (t : ty) : T.integer_type =
+  match t with Integer int_ty -> int_ty | _ -> failwith "Unreachable"
+
+(* TODO: move *)
+let type_def_is_enum (def : T.type_def) : bool =
+  match def.kind with T.Struct _ -> false | Enum _ -> true
+
+let mk_result_fail_rvalue (ty : ty) : typed_rvalue =
+  let ty = Adt (Assumed Result, [ ty ]) in
+  let value = RvAdt { variant_id = Some result_fail_id; field_values = [] } in
+  { value; ty }
+
+let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue =
+  let ty = Adt (Assumed Result, [ v.ty ]) in
+  let value =
+    RvAdt { variant_id = Some result_return_id; field_values = [ v ] }
+  in
+  { value; ty }
+
+let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
+
+(** Type substitution *)
+let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty =
+  let obj =
+    object
+      inherit [_] map_ty
+
+      method! visit_TypeVar _ var_id = tsubst var_id
+    end
+  in
+  obj#visit_ty () ty
+
+let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
+    =
+  let ls = List.combine vars tys in
+  let mp =
+    List.fold_left
+      (fun mp (k, v) -> TypeVarId.Map.add (k : type_var).index v mp)
+      TypeVarId.Map.empty ls
+  in
+  fun id -> TypeVarId.Map.find id mp
+
+let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
+    inst_fun_sig =
+  let subst = ty_substitute tsubst in
+  let inputs = List.map subst sg.inputs in
+  let outputs = List.map subst sg.outputs in
+  { inputs; outputs }
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 345555e7..d7bcadb4 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1,11 +1,8 @@
 open Errors
-open Pure
 open CfimAstUtils
+open Pure
+open PureUtils
 module Id = Identifiers
-module T = Types
-module V = Values
-module E = Expressions
-module A = CfimAst
 module M = Modules
 module S = SymbolicAst
 module TA = TypesAnalysis
@@ -15,96 +12,6 @@ module PP = PrintPure
 (** The local logger *)
 let log = L.symbolic_to_pure_log
 
-(* TODO : move *)
-let binop_can_fail (binop : E.binop) : bool =
-  match binop with
-  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
-  | Div | Rem | Add | Sub | Mul -> true
-  | Shl | Shr -> raise Unimplemented
-
-(* TODO: move *)
-let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
-
-let mk_tuple_ty (tys : ty list) : ty = Adt (Tuple, tys)
-
-let unit_ty : ty = Adt (Tuple, [])
-
-let unit_rvalue : typed_rvalue =
-  let value = RvAdt { variant_id = None; field_values = [] } in
-  let ty = unit_ty in
-  { value; ty }
-
-let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
-  let value = RvPlace (mk_place_from_var v) in
-  let ty = v.ty in
-  { value; ty }
-
-(* TODO: move *)
-let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
-  let value = LvVar (Var (v, mp)) in
-  let ty = v.ty in
-  { value; ty }
-
-let mk_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue =
-  let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in
-  let ty = Adt (Tuple, tys) in
-  let value = LvAdt { variant_id = None; field_values = vl } in
-  { value; ty }
-
-let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id)
-    (vl : typed_lvalue list) : typed_lvalue =
-  let value = LvAdt { variant_id = Some variant_id; field_values = vl } in
-  { value; ty = adt_ty }
-
-let ty_as_integer (t : ty) : T.integer_type =
-  match t with Integer int_ty -> int_ty | _ -> failwith "Unreachable"
-
-(* TODO: move *)
-let type_def_is_enum (def : T.type_def) : bool =
-  match def.kind with T.Struct _ -> false | Enum _ -> true
-
-let mk_result_fail_rvalue (ty : ty) : typed_rvalue =
-  let ty = Adt (Assumed Result, [ ty ]) in
-  let value = RvAdt { variant_id = Some result_fail_id; field_values = [] } in
-  { value; ty }
-
-let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue =
-  let ty = Adt (Assumed Result, [ v.ty ]) in
-  let value =
-    RvAdt { variant_id = Some result_return_id; field_values = [ v ] }
-  in
-  { value; ty }
-
-let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
-
-(** Type substitution *)
-let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty =
-  let obj =
-    object
-      inherit [_] map_ty
-
-      method! visit_TypeVar _ var_id = tsubst var_id
-    end
-  in
-  obj#visit_ty () ty
-
-let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
-    =
-  let ls = List.combine vars tys in
-  let mp =
-    List.fold_left
-      (fun mp (k, v) -> TypeVarId.Map.add (k : type_var).index v mp)
-      TypeVarId.Map.empty ls
-  in
-  fun id -> TypeVarId.Map.find id mp
-
-let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
-    inst_fun_sig =
-  let subst = ty_substitute tsubst in
-  let inputs = List.map subst sg.inputs in
-  let outputs = List.map subst sg.outputs in
-  { inputs; outputs }
-
 type regular_fun_id = A.fun_id * T.RegionGroupId.id option
 [@@deriving show, ord]
 (** We use this type as a key for lookups *)
@@ -183,13 +90,16 @@ type bs_ctx = {
 (** Body synthesis context *)
 
 (* TODO: move *)
+let bs_ctx_to_value_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter =
+  Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs
+    ctx.fun_context.cfim_fun_defs ctx.fun_def
+
 let type_def_to_string (ctx : bs_ctx) (def : type_def) : string =
   let type_params = def.type_params in
   let type_defs = ctx.type_context.cfim_type_defs in
   let fmt = PrintPure.mk_type_formatter type_defs type_params in
   PrintPure.type_def_to_string fmt def
 
-(* TODO: move *)
 let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string =
   let type_params = ctx.fun_def.signature.type_params in
   let type_defs = ctx.type_context.cfim_type_defs in
@@ -197,7 +107,6 @@ let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string =
   let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
   PrintPure.typed_rvalue_to_string fmt v
 
-(* TODO: move *)
 let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
   let type_params = sg.type_params in
   let type_defs = ctx.type_context.cfim_type_defs in
@@ -205,7 +114,6 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
   let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
   PrintPure.fun_sig_to_string fmt sg
 
-(* TODO: move *)
 let fun_def_to_string (ctx : bs_ctx) (def : Pure.fun_def) : string =
   let type_params = def.signature.type_params in
   let type_defs = ctx.type_context.cfim_type_defs in
@@ -214,11 +122,6 @@ let fun_def_to_string (ctx : bs_ctx) (def : Pure.fun_def) : string =
   PrintPure.fun_def_to_string fmt def
 
 (* TODO: move *)
-let bs_ctx_to_value_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter =
-  Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs
-    ctx.fun_context.cfim_fun_defs ctx.fun_def
-
-(* TODO: move *)
 let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   let fmt = bs_ctx_to_value_formatter ctx in
   let fmt = Print.CfimAst.ast_to_value_formatter fmt in
diff --git a/src/Translate.ml b/src/Translate.ml
index 63b6027e..005ace94 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -6,6 +6,7 @@ module A = CfimAst
 module M = Modules
 module SA = SymbolicAst
 module Micro = PureMicroPasses
+open PureUtils
 open TranslateCore
 
 (** The local logger *)
@@ -175,7 +176,7 @@ let translate_function_to_pure (config : C.partial_config)
     let backward_output_tys =
       List.map (fun (v : Pure.var) -> v.ty) backward_outputs
     in
-    let backward_ret_ty = SymbolicToPure.mk_tuple_ty backward_output_tys in
+    let backward_ret_ty = mk_tuple_ty backward_output_tys in
     let backward_inputs =
       T.RegionGroupId.Map.singleton back_id backward_inputs
     in