summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Interpreter.ml13
-rw-r--r--src/Print.ml7
-rw-r--r--src/Substitute.ml3
-rw-r--r--src/Types.ml44
-rw-r--r--src/TypesUtils.ml48
-rw-r--r--src/ValuesUtils.ml7
6 files changed, 64 insertions, 58 deletions
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 *)
@@ -39,15 +41,6 @@ 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
=
{ A.index; name; var_ty }
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 }
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 18:21:30 +0000