From b951d7e571a24729303169733062154c4639f73a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 1 Dec 2021 13:49:32 +0100
Subject: Move some definitions to new files

---
 src/Interpreter.ml | 13 +++----------
 src/Print.ml       |  7 ++++---
 src/Substitute.ml  |  3 ++-
 src/Types.ml       | 44 --------------------------------------------
 src/TypesUtils.ml  | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 src/ValuesUtils.ml |  7 +++++++
 6 files changed, 64 insertions(+), 58 deletions(-)
 create mode 100644 src/TypesUtils.ml
 create mode 100644 src/ValuesUtils.ml

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 21124c48..fefbb00b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -7,6 +7,8 @@ module C = Contexts
 module Subst = Substitute
 module A = CfimAst
 module L = Logging
+open TypesUtils
+open ValuesUtils
 
 (* TODO: Change state-passing style to : st -> ... -> (st, v) *)
 (* TODO: check that the value types are correct when evaluating *)
@@ -21,7 +23,7 @@ module L = Logging
    where invariants might be broken, etc.
  *)
 
-(* TODO: test with PLT-redex *)
+(* TODO: intensively test with PLT-redex *)
 
 (** Some utilities *)
 
@@ -38,15 +40,6 @@ let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
 let statement_to_string ctx =
   Print.EvalCtxCfimAst.statement_to_string ctx "" "  "
 
-(* TODO: move *)
-let mk_unit_ty : T.ety = T.Tuple []
-
-(* TODO: move *)
-let mk_unit_value : V.typed_value = { V.value = V.Tuple []; V.ty = mk_unit_ty }
-
-let mk_typed_value (ty : T.ety) (value : V.value) : V.typed_value =
-  { V.value; ty }
-
 (* TODO: move *)
 let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
     =
diff --git a/src/Print.ml b/src/Print.ml
index 9c1aaa94..b4c9a73a 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -2,6 +2,7 @@
 
 open Identifiers
 module T = Types
+module TU = TypesUtils
 module V = Values
 module E = Expressions
 module A = CfimAst
@@ -438,7 +439,7 @@ module Contexts = struct
       T.TypeDefId.id -> T.VariantId.id option -> string list option =
    fun def_id opt_variant_id ->
     let def = T.TypeDefId.nth ctx def_id in
-    let fields = T.type_def_get_fields def opt_variant_id in
+    let fields = TU.type_def_get_fields def opt_variant_id in
     (* TODO: the field name should be optional?? *)
     let fields = List.map (fun f -> f.T.field_name) fields in
     Some fields
@@ -546,7 +547,7 @@ module CfimAst = struct
       T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
    fun def_id opt_variant_id field_id ->
     let def = T.TypeDefId.nth ctx def_id in
-    let fields = T.type_def_get_fields def opt_variant_id in
+    let fields = TU.type_def_get_fields def opt_variant_id in
     let field = T.FieldId.nth fields field_id in
     field.T.field_name
 
@@ -801,7 +802,7 @@ module CfimAst = struct
     (* Return type *)
     let ret_ty = sg.output in
     let ret_ty =
-      if T.ty_is_unit ret_ty then "" else " -> " ^ rty_to_string ret_ty
+      if TU.ty_is_unit ret_ty then "" else " -> " ^ rty_to_string ret_ty
     in
 
     (* All the locals (with erased regions) *)
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 3a2358f8..ad896c41 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -3,6 +3,7 @@
  *)
 
 module T = Types
+module TU = TypesUtils
 module V = Values
 module E = Expressions
 module A = CfimAst
@@ -58,7 +59,7 @@ let type_def_get_instantiated_field_type (def : T.type_def)
   let ty_subst =
     make_type_subst (List.map (fun x -> x.T.tv_index) def.T.type_params) types
   in
-  let fields = T.type_def_get_fields def opt_variant_id in
+  let fields = TU.type_def_get_fields def opt_variant_id in
   List.map
     (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty)
     fields
diff --git a/src/Types.ml b/src/Types.ml
index 7b4da265..ba179ef8 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -105,47 +105,3 @@ type type_def = {
   kind : type_def_kind;
 }
 [@@deriving show]
-
-(** Convert an [rty] to an [ety] by erasing the region variables
-    
-    TODO: this can be done through a substitution
-*)
-let rec erase_regions (ty : rty) : ety =
-  match ty with
-  | Adt (def_id, regions, tys) ->
-      let regions = List.map (fun _ -> Erased) regions in
-      let tys = List.map erase_regions tys in
-      Adt (def_id, regions, tys)
-  | Tuple tys -> Tuple (List.map erase_regions tys)
-  | TypeVar vid -> TypeVar vid
-  | Bool -> Bool
-  | Char -> Char
-  | Never -> Never
-  | Integer int_ty -> Integer int_ty
-  | Str -> Str
-  | Array ty -> Array (erase_regions ty)
-  | Slice ty -> Slice (erase_regions ty)
-  | Ref (_, ty, ref_kind) -> Ref (Erased, erase_regions ty, ref_kind)
-  | Assumed (aty, regions, tys) ->
-      let regions = List.map (fun _ -> Erased) regions in
-      let tys = List.map erase_regions tys in
-      Assumed (aty, regions, tys)
-
-(** Retrieve the list of fields for the given variant of a [type_def].
-
-    Raises [Invalid_argument] if the arguments are incorrect.
- *)
-let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
-    : field list =
-  match (def.kind, opt_variant_id) with
-  | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
-  | Struct fields, None -> fields
-  | _ ->
-      raise
-        (Invalid_argument
-           "The variant id should be [Some] if and only if the definition is \
-            an enumeration")
-
-(** Return [true] if a [ty] is actually `unit` *)
-let ty_is_unit (ty : 'r ty) : bool =
-  match ty with Tuple tys -> List.length tys = 0 | _ -> false
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
new file mode 100644
index 00000000..0e6040b2
--- /dev/null
+++ b/src/TypesUtils.ml
@@ -0,0 +1,48 @@
+open Types
+
+(** Convert an [rty] to an [ety] by erasing the region variables
+    
+    TODO: this can be done through a substitution
+*)
+let rec erase_regions (ty : rty) : ety =
+  match ty with
+  | Adt (def_id, regions, tys) ->
+      let regions = List.map (fun _ -> Erased) regions in
+      let tys = List.map erase_regions tys in
+      Adt (def_id, regions, tys)
+  | Tuple tys -> Tuple (List.map erase_regions tys)
+  | TypeVar vid -> TypeVar vid
+  | Bool -> Bool
+  | Char -> Char
+  | Never -> Never
+  | Integer int_ty -> Integer int_ty
+  | Str -> Str
+  | Array ty -> Array (erase_regions ty)
+  | Slice ty -> Slice (erase_regions ty)
+  | Ref (_, ty, ref_kind) -> Ref (Erased, erase_regions ty, ref_kind)
+  | Assumed (aty, regions, tys) ->
+      let regions = List.map (fun _ -> Erased) regions in
+      let tys = List.map erase_regions tys in
+      Assumed (aty, regions, tys)
+
+(** Retrieve the list of fields for the given variant of a [type_def].
+
+    Raises [Invalid_argument] if the arguments are incorrect.
+ *)
+let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
+    : field list =
+  match (def.kind, opt_variant_id) with
+  | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
+  | Struct fields, None -> fields
+  | _ ->
+      raise
+        (Invalid_argument
+           "The variant id should be [Some] if and only if the definition is \
+            an enumeration")
+
+(** Return [true] if a [ty] is actually `unit` *)
+let ty_is_unit (ty : 'r ty) : bool =
+  match ty with Tuple tys -> List.length tys = 0 | _ -> false
+
+(** The unit type *)
+let mk_unit_ty : ety = Tuple []
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
new file mode 100644
index 00000000..3fd04b56
--- /dev/null
+++ b/src/ValuesUtils.ml
@@ -0,0 +1,7 @@
+module T = Types
+open TypesUtils
+open Values
+
+let mk_unit_value : typed_value = { value = Tuple []; ty = mk_unit_ty }
+
+let mk_typed_value (ty : T.ety) (value : value) : typed_value = { value; ty }
-- 
cgit v1.2.3