summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml177
1 files changed, 88 insertions, 89 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 59e58721..367f931c 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,4 +1,4 @@
-open Types
+module T = Types
module V = Values
open Scalars
module E = Expressions
@@ -29,8 +29,8 @@ let rec check_borrows_in_value (check : V.borrow_content -> bool)
(v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> true
- | V.Adt av -> FieldId.for_all (check_borrows_in_value check) av.field_values
- | V.Tuple values -> FieldId.for_all (check_borrows_in_value check) values
+ | V.Adt av -> T.FieldId.for_all (check_borrows_in_value check) av.field_values
+ | V.Tuple values -> T.FieldId.for_all (check_borrows_in_value check) values
| V.Assumed (Box bv) -> check_borrows_in_value check bv
| V.Borrow bc -> (
check bc
@@ -48,8 +48,8 @@ let rec check_loans_in_value (check : V.loan_content -> bool)
(v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> true
- | V.Adt av -> FieldId.for_all (check_loans_in_value check) av.field_values
- | V.Tuple values -> FieldId.for_all (check_loans_in_value check) values
+ | V.Adt av -> T.FieldId.for_all (check_loans_in_value check) av.field_values
+ | V.Tuple values -> T.FieldId.for_all (check_loans_in_value check) values
| V.Assumed (Box bv) -> check_loans_in_value check bv
| V.Borrow bc -> (
match bc with
@@ -68,10 +68,10 @@ let rec lookup_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> None
| V.Adt av ->
- let values = FieldId.vector_to_list av.field_values in
+ let values = T.FieldId.vector_to_list av.field_values in
List.find_map (lookup_loan_in_value ek l) values
| V.Tuple values ->
- let values = FieldId.vector_to_list values in
+ let values = T.FieldId.vector_to_list values in
List.find_map (lookup_loan_in_value ek l) values
| V.Assumed (Box bv) -> lookup_loan_in_value ek l bv
| V.Borrow bc -> (
@@ -115,12 +115,12 @@ let rec update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
| V.Concrete _ | V.Bottom | V.Symbolic _ -> v
| V.Adt av ->
let values =
- FieldId.map (update_loan_in_value ek l nlc) av.field_values
+ T.FieldId.map (update_loan_in_value ek l nlc) av.field_values
in
let av = { av with field_values = values } in
{ v with value = Adt av }
| V.Tuple values ->
- let values = FieldId.map (update_loan_in_value ek l nlc) values in
+ let values = T.FieldId.map (update_loan_in_value ek l nlc) values in
{ v with value = Tuple values }
| V.Assumed (Box bv) ->
{ v with value = Assumed (Box (update_loan_in_value ek l nlc bv)) }
@@ -168,10 +168,10 @@ let rec lookup_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id)
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> None
| V.Adt av ->
- let values = FieldId.vector_to_list av.field_values in
+ let values = T.FieldId.vector_to_list av.field_values in
List.find_map (lookup_borrow_in_value ek l) values
| V.Tuple values ->
- let values = FieldId.vector_to_list values in
+ let values = T.FieldId.vector_to_list values in
List.find_map (lookup_borrow_in_value ek l) values
| V.Assumed (Box bv) -> lookup_borrow_in_value ek l bv
| V.Borrow bc -> (
@@ -213,12 +213,12 @@ let rec update_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id)
| V.Concrete _ | V.Bottom | V.Symbolic _ -> v
| V.Adt av ->
let values =
- FieldId.map (update_borrow_in_value ek l nbc) av.field_values
+ T.FieldId.map (update_borrow_in_value ek l nbc) av.field_values
in
let av = { av with field_values = values } in
{ v with value = Adt av }
| V.Tuple values ->
- let values = FieldId.map (update_borrow_in_value ek l nbc) values in
+ let values = T.FieldId.map (update_borrow_in_value ek l nbc) values in
{ v with value = Tuple values }
| V.Assumed (Box bv) ->
{ v with value = Assumed (Box (update_borrow_in_value ek l nbc bv)) }
@@ -297,10 +297,10 @@ let rec loans_in_value (v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ -> false
| V.Adt av ->
- let fields = FieldId.vector_to_list av.field_values in
+ let fields = T.FieldId.vector_to_list av.field_values in
List.exists loans_in_value fields
| V.Tuple fields ->
- let fields = FieldId.vector_to_list fields in
+ let fields = T.FieldId.vector_to_list fields in
List.exists loans_in_value fields
| V.Assumed (Box bv) -> loans_in_value bv
| V.Borrow bc -> (
@@ -315,10 +315,10 @@ let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
match v.V.value with
| V.Concrete _ -> None
| V.Adt av ->
- let fields = FieldId.vector_to_list av.field_values in
+ let fields = T.FieldId.vector_to_list av.field_values in
get_first_loan_in_values fields
| V.Tuple fields ->
- let fields = FieldId.vector_to_list fields in
+ let fields = T.FieldId.vector_to_list fields in
get_first_loan_in_values fields
| V.Assumed (Box bv) -> get_first_loan_in_value bv
| V.Borrow bc -> (
@@ -341,10 +341,10 @@ let rec bottom_in_value (v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ -> false
| V.Adt av ->
- let fields = FieldId.vector_to_list av.field_values in
+ let fields = T.FieldId.vector_to_list av.field_values in
List.exists bottom_in_value fields
| V.Tuple fields ->
- let fields = FieldId.vector_to_list fields in
+ let fields = T.FieldId.vector_to_list fields in
List.exists bottom_in_value fields
| V.Assumed (Box bv) -> bottom_in_value bv
| V.Borrow bc -> (
@@ -376,18 +376,18 @@ let rec end_borrow_get_borrow_in_value config io l outer_borrows v0 :
* boxes upon ending inner borrows *)
({ v0 with value = Assumed (Box bv') }, res)
| V.Adt adt ->
- let values = FieldId.vector_to_list adt.field_values in
+ let values = T.FieldId.vector_to_list adt.field_values in
let values', res =
end_borrow_get_borrow_in_values config io l outer_borrows values
in
- let values' = FieldId.vector_of_list values' in
+ let values' = T.FieldId.vector_of_list values' in
({ v0 with value = Adt { adt with field_values = values' } }, res)
| V.Tuple values ->
- let values = FieldId.vector_to_list values in
+ let values = T.FieldId.vector_to_list values in
let values', res =
end_borrow_get_borrow_in_values config io l outer_borrows values
in
- let values' = FieldId.vector_of_list values' in
+ let values' = T.FieldId.vector_of_list values' in
({ v0 with value = Tuple values' }, res)
| V.Loan (V.MutLoan _) -> (v0, NotFound)
| V.Loan (V.SharedLoan (borrows, v)) ->
@@ -469,17 +469,17 @@ let rec give_back_value_to_value config bid (v : V.typed_value)
let field_values =
List.map
(give_back_value_to_value config bid v)
- (FieldId.vector_to_list av.field_values)
+ (T.FieldId.vector_to_list av.field_values)
in
- let field_values = FieldId.vector_of_list field_values in
+ let field_values = T.FieldId.vector_of_list field_values in
{ destv with value = Adt { av with field_values } }
| V.Tuple values ->
let values =
List.map
(give_back_value_to_value config bid v)
- (FieldId.vector_to_list values)
+ (T.FieldId.vector_to_list values)
in
- let values = FieldId.vector_of_list values in
+ let values = T.FieldId.vector_of_list values in
{ destv with value = Tuple values }
| V.Assumed (Box destv') ->
{
@@ -516,17 +516,17 @@ let rec give_back_shared_to_value (config : C.config) bid
let field_values =
List.map
(give_back_shared_to_value config bid)
- (FieldId.vector_to_list av.field_values)
+ (T.FieldId.vector_to_list av.field_values)
in
- let field_values = FieldId.vector_of_list field_values in
+ let field_values = T.FieldId.vector_of_list field_values in
{ destv with value = Adt { av with field_values } }
| V.Tuple values ->
let values =
List.map
(give_back_shared_to_value config bid)
- (FieldId.vector_to_list values)
+ (T.FieldId.vector_to_list values)
in
- let values = FieldId.vector_of_list values in
+ let values = T.FieldId.vector_of_list values in
{ destv with value = Tuple values }
| V.Assumed (Box destv') ->
{
@@ -613,14 +613,14 @@ let reborrow_shared (config : C.config) (original_bid : V.BorrowId.id)
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> v
| V.Adt av ->
- let fields = FieldId.vector_to_list av.field_values in
+ let fields = T.FieldId.vector_to_list av.field_values in
let fields = List.map reborrow_in_value fields in
- let fields = FieldId.vector_of_list fields in
+ let fields = T.FieldId.vector_of_list fields in
{ v with value = Adt { av with field_values = fields } }
| V.Tuple fields ->
- let fields = FieldId.vector_to_list fields in
+ let fields = T.FieldId.vector_to_list fields in
let fields = List.map reborrow_in_value fields in
- let fields = FieldId.vector_of_list fields in
+ let fields = T.FieldId.vector_of_list fields in
{ v with value = Tuple fields }
| V.Assumed (Box bv) ->
{ v with value = Assumed (Box (reborrow_in_value bv)) }
@@ -813,7 +813,7 @@ type path_fail_kind =
(which should get activated) *)
| FailSymbolic of (E.projection_elem * V.symbolic_proj_comp)
(** Failure because we need to enter a symbolic value (and thus need to expand it) *)
- | FailBottom of (int * E.projection_elem * ety)
+ | FailBottom of (int * E.projection_elem * T.ety)
(** Failure because we need to enter an any value - we can expand Bottom
values if they are left values. We return the number of elements which
were remaining in the path when we reached the error - this allows to
@@ -868,27 +868,27 @@ let rec access_projection (access : projection_access) (env : C.env)
| Some vid, Some vid' -> if vid <> vid' then failwith "Unreachable"
| _ -> failwith "Unreachable");
(* Actually project *)
- let fv = FieldId.nth adt.field_values field_id in
+ let fv = T.FieldId.nth adt.field_values field_id in
match access_projection access env update p fv with
| Error err -> Error err
| Ok (env1, res) ->
(* Update the field value *)
let nvalues =
- FieldId.update_nth adt.field_values field_id res.updated
+ T.FieldId.update_nth adt.field_values field_id res.updated
in
let nadt = V.Adt { adt with V.field_values = nvalues } in
let updated = { v with value = nadt } in
Ok (env1, { res with updated }))
(* Tuples *)
| Field (ProjTuple arity, field_id), V.Tuple values -> (
- assert (arity = FieldId.length values);
- let fv = FieldId.nth values field_id in
+ assert (arity = T.FieldId.length values);
+ let fv = T.FieldId.nth values field_id in
(* Project *)
match access_projection access env update p fv with
| Error err -> Error err
| Ok (env1, res) ->
(* Update the field value *)
- let nvalues = FieldId.update_nth values field_id res.updated in
+ let nvalues = T.FieldId.update_nth values field_id res.updated in
let ntuple = V.Tuple nvalues in
let updated = { v with value = ntuple } in
Ok (env1, { res with updated })
@@ -1078,8 +1078,8 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
variant index when writing one of its fields).
*)
let expand_bottom_value (config : C.config) (access : access_kind)
- (tyctx : type_def TypeDefId.vector) (p : E.place) (remaining_pes : int)
- (pe : E.projection_elem) (ty : ety) (env : C.env) : C.env =
+ (tyctx : T.type_def T.TypeDefId.vector) (p : E.place) (remaining_pes : int)
+ (pe : E.projection_elem) (ty : T.ety) (env : C.env) : C.env =
(* Prepare the update: we need to take the proper prefix of the place
during whose evaluation we got stuck *)
let projection' =
@@ -1099,30 +1099,30 @@ let expand_bottom_value (config : C.config) (access : access_kind)
let nv =
match (pe, ty) with
| ( Field (ProjAdt (def_id, opt_variant_id), _),
- Types.Adt (def_id', regions, types) ) ->
+ T.Adt (def_id', regions, types) ) ->
(* Lookup the definition and check if it is an enumeration - it
should be an enumeration if and only if the projection element
is a field projection with *some* variant id. Retrieve the list
of fields at the same time. *)
assert (def_id = def_id');
- let def = TypeDefId.nth tyctx def_id in
+ let def = T.TypeDefId.nth tyctx def_id in
let fields =
match (def.kind, opt_variant_id) with
| Struct fields, None -> fields
| Enum variants, Some variant_id ->
(* Retrieve the proper variant *)
- let variant = VariantId.nth variants variant_id in
+ let variant = T.VariantId.nth variants variant_id in
variant.fields
| _ -> failwith "Unreachable"
in
(* Initialize the expanded value *)
- let fields = FieldId.vector_to_list fields in
+ let fields = T.FieldId.vector_to_list fields in
let fields =
List.map
- (fun f -> { V.value = Bottom; ty = erase_regions f.field_ty })
+ (fun f -> { V.value = Bottom; ty = T.erase_regions f.T.field_ty })
fields
in
- let fields = FieldId.vector_of_list fields in
+ let fields = T.FieldId.vector_of_list fields in
V.Adt
{
def_id;
@@ -1131,11 +1131,11 @@ let expand_bottom_value (config : C.config) (access : access_kind)
types;
field_values = fields;
}
- | Field (ProjTuple arity, _), Types.Tuple tys ->
+ | Field (ProjTuple arity, _), T.Tuple tys ->
assert (arity = List.length tys);
(* Generate the field values *)
let fields = List.map (fun ty -> { V.value = Bottom; ty }) tys in
- let fields = FieldId.vector_of_list fields in
+ let fields = T.FieldId.vector_of_list fields in
V.Tuple fields
| _ -> failwith "Unreachable"
in
@@ -1180,7 +1180,7 @@ let rec update_env_along_read_place (config : C.config) (access : access_kind)
See [update_env_alond_read_place].
*)
let rec update_env_along_write_place (config : C.config) (access : access_kind)
- (tyctx : type_def TypeDefId.vector) (p : E.place) (nv : V.typed_value)
+ (tyctx : T.type_def T.TypeDefId.vector) (p : E.place) (nv : V.typed_value)
(env : C.env) : C.env =
(* Attempt to write the place: if it fails, update the environment and retry *)
match write_place config access p nv env with
@@ -1234,8 +1234,8 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind)
(* Nothing to do for symbolic values - note that if the value needs
to be copied, etc. we perform additional checks later *)
()
- | V.Adt adt -> FieldId.iter inspect_update adt.field_values
- | V.Tuple values -> FieldId.iter inspect_update values
+ | V.Adt adt -> T.FieldId.iter inspect_update adt.field_values
+ | V.Tuple values -> T.FieldId.iter inspect_update values
| V.Assumed (Box v) -> inspect_update v
| V.Borrow bc -> (
match bc with
@@ -1319,8 +1319,9 @@ let rec drop_borrows_at_place (config : C.config) (p : E.place) (env : C.env) :
| V.Symbolic _ ->
(* Nothing to do for symbolic values - TODO: not sure *)
raise Unimplemented
- | V.Adt adt -> FieldId.iter (inspect_update end_loans) adt.field_values
- | V.Tuple values -> FieldId.iter (inspect_update end_loans) values
+ | V.Adt adt ->
+ T.FieldId.iter (inspect_update end_loans) adt.field_values
+ | V.Tuple values -> T.FieldId.iter (inspect_update end_loans) values
| V.Assumed (Box v) -> inspect_update end_loans v
| V.Borrow bc -> (
assert (not end_loans);
@@ -1382,14 +1383,14 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
match v.V.value with
| V.Concrete _ -> (ctx, v)
| V.Adt av ->
- let fields = FieldId.vector_to_list av.field_values in
+ let fields = T.FieldId.vector_to_list av.field_values in
let ctx', fields = List.fold_left_map (copy_value config) ctx fields in
- let fields = FieldId.vector_of_list fields in
+ let fields = T.FieldId.vector_of_list fields in
(ctx', { v with V.value = V.Adt { av with field_values = fields } })
| V.Tuple fields ->
- let fields = FieldId.vector_to_list fields in
+ let fields = T.FieldId.vector_to_list fields in
let ctx', fields = List.fold_left_map (copy_value config) ctx fields in
- let fields = FieldId.vector_of_list fields in
+ let fields = T.FieldId.vector_of_list fields in
(ctx', { v with V.value = V.Tuple fields })
| V.Bottom -> failwith "Can't copy ⊥"
| V.Assumed _ -> failwith "Can't copy an assumed value"
@@ -1414,31 +1415,30 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
raise Unimplemented
(** Convert a constant operand value to a typed value *)
-let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : ety)
+let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
(cv : E.operand_constant_value) : V.typed_value =
(* Check the type while converting *)
match (ty, cv) with
(* Unit *)
- | Types.Tuple [], Unit ->
- { V.value = V.Tuple (FieldId.vector_of_list []); ty }
+ | T.Tuple [], Unit -> { V.value = V.Tuple (T.FieldId.vector_of_list []); ty }
(* Adt with one variant and no fields *)
- | Types.Adt (def_id, [], []), ConstantAdt def_id' ->
+ | T.Adt (def_id, [], []), ConstantAdt def_id' ->
assert (def_id = def_id');
(* Check that the adt definition only has one variant with no fields,
compute the variant id at the same time. *)
- let def = TypeDefId.nth ctx.type_context def_id in
- assert (RegionVarId.length def.region_params = 0);
- assert (TypeVarId.length def.type_params = 0);
+ let def = T.TypeDefId.nth ctx.type_context def_id in
+ assert (T.RegionVarId.length def.region_params = 0);
+ assert (T.TypeVarId.length def.type_params = 0);
let variant_id =
match def.kind with
| Struct fields ->
- assert (FieldId.length fields = 0);
+ assert (T.FieldId.length fields = 0);
None
| Enum variants ->
- assert (VariantId.length variants = 1);
- let variant_id = VariantId.zero in
- let variant = VariantId.nth variants variant_id in
- assert (FieldId.length variant.fields = 0);
+ assert (T.VariantId.length variants = 1);
+ let variant_id = T.VariantId.zero in
+ let variant = T.VariantId.nth variants variant_id in
+ assert (T.FieldId.length variant.fields = 0);
Some variant_id
in
let value =
@@ -1448,16 +1448,15 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : ety)
variant_id;
regions = [];
types = [];
- field_values = FieldId.vector_of_list [];
+ field_values = T.FieldId.vector_of_list [];
}
in
{ value; ty }
(* Scalar, boolean... *)
- | Types.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty }
- | Types.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty }
- | Types.Str, ConstantValue (String v) ->
- { V.value = V.Concrete (String v); ty }
- | Types.Integer int_ty, ConstantValue (V.Scalar v) ->
+ | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty }
+ | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty }
+ | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty }
+ | T.Integer int_ty, ConstantValue (V.Scalar v) ->
(* Check the type and the ranges *)
assert (int_ty == v.int_ty);
assert (check_scalar_value_in_range v);
@@ -1586,7 +1585,7 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
(* Equality/inequality check is primitive only on primitive types *)
assert (v1.ty = v2.ty);
let b = v1 = v2 in
- Ok (ctx2, { V.value = V.Concrete (Bool b); ty = Types.Bool }))
+ Ok (ctx2, { V.value = V.Concrete (Bool b); ty = T.Bool }))
else
match (v1.V.value, v2.V.value) with
| V.Concrete (V.Scalar sv1), V.Concrete (V.Scalar sv2) -> (
@@ -1610,7 +1609,7 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
| E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
failwith "Unreachable"
in
- Ok { V.value = V.Concrete (Bool b); ty = Types.Bool }
+ Ok { V.value = V.Concrete (Bool b); ty = T.Bool }
| E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
| E.BitOr -> (
(* The two operands must have the same type and the result is an integer *)
@@ -1661,7 +1660,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
let ctx2, v = prepare_rplace config access p ctx in
(* Compute the rvalue - simply a shared borrow with a fresh id *)
let ctx3, bid = C.fresh_borrow_id ctx2 in
- let rv_ty = Types.Ref (Erased, v.ty, Shared) in
+ let rv_ty = T.Ref (T.Erased, v.ty, Shared) in
let bc =
if bkind = E.Shared then V.SharedBorrow bid
else V.InactivatedMutBorrow bid
@@ -1691,7 +1690,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
let ctx2, v = prepare_rplace config access p ctx in
(* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
let ctx3, bid = C.fresh_borrow_id ctx2 in
- let rv_ty = Types.Ref (Erased, v.ty, Mut) in
+ let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
let rv = { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } in
(* Compute the value with which to replace the value at place p *)
let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
@@ -1713,7 +1712,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
failwith
"Invalid input for `discriminant`: structure instead of enum"
| Some variant_id -> (
- let id = Z.of_int (VariantId.to_int variant_id) in
+ let id = Z.of_int (T.VariantId.to_int variant_id) in
match mk_scalar Isize id with
| Error _ ->
failwith "Disciminant id out of range"
@@ -1727,24 +1726,24 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
| E.Aggregate (aggregate_kind, ops) -> (
(* Evaluate the operands *)
let ctx1, values = eval_operands config ctx ops in
- let values = FieldId.vector_of_list values in
+ let values = T.FieldId.vector_of_list values in
(* Match on the aggregate kind *)
match aggregate_kind with
| E.AggregatedTuple ->
let tys =
- List.map (fun v -> v.V.ty) (FieldId.vector_to_list values)
+ List.map (fun v -> v.V.ty) (T.FieldId.vector_to_list values)
in
- Ok (ctx1, { V.value = Tuple values; ty = Types.Tuple tys })
+ Ok (ctx1, { V.value = Tuple values; ty = T.Tuple tys })
| E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
(* Sanity checks *)
let type_def = C.ctx_lookup_type_def ctx def_id in
assert (
- RegionVarId.length type_def.region_params = List.length regions);
+ T.RegionVarId.length type_def.region_params = List.length regions);
let expected_field_types =
Subst.ctx_adt_get_instantiated_field_types ctx1 def_id
opt_variant_id types
in
- assert (expected_field_types = FieldId.map (fun v -> v.V.ty) values);
+ assert (expected_field_types = T.FieldId.map (fun v -> v.V.ty) values);
(* Construct the value *)
let av =
{
@@ -1755,7 +1754,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
V.field_values = values;
}
in
- let aty = Types.Adt (def_id, regions, types) in
+ let aty = T.Adt (def_id, regions, types) in
Ok (ctx1, { V.value = Adt av; ty = aty }))
(** Result of evaluating a statement *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 16:24:37 +0000