Add the "V" prefix to most variants related to values

1 files changed, 134 insertions, 143 deletions

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 8895bd8e..7830099f 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -150,8 +150,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
         (* Register the loan *)
         let _ =
           match lc with
-          | V.SharedLoan (bids, _) -> register_shared_loan inside_abs bids
-          | V.MutLoan bid -> register_mut_loan inside_abs bid
+          | VSharedLoan (bids, _) -> register_shared_loan inside_abs bids
+          | VMutLoan bid -> register_mut_loan inside_abs bid
         in
         (* Continue exploring *)
         super#visit_loan_content inside_abs lc
@@ -159,14 +159,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
       method! visit_aloan_content inside_abs lc =
         let _ =
           match lc with
-          | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid
-          | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
-          | V.AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid
-          | V.AIgnoredMutLoan (None, _)
-          | V.AIgnoredSharedLoan _
-          | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
-          | V.AEndedSharedLoan (_, _)
-          | V.AEndedIgnoredMutLoan
+          | AMutLoan (bid, _) -> register_mut_loan inside_abs bid
+          | ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
+          | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid
+          | AIgnoredMutLoan (None, _)
+          | AIgnoredSharedLoan _
+          | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+          | AEndedSharedLoan (_, _)
+          | AEndedIgnoredMutLoan
               { given_back = _; child = _; given_back_meta = _ } ->
               (* Do nothing *)
               ()
@@ -244,9 +244,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
         (* Register the loan *)
         let _ =
           match bc with
-          | V.SharedBorrow bid -> register_borrow Shared bid
-          | V.MutBorrow (bid, _) -> register_borrow Mut bid
-          | V.ReservedMutBorrow bid -> register_borrow Reserved bid
+          | VSharedBorrow bid -> register_borrow Shared bid
+          | VMutBorrow (bid, _) -> register_borrow Mut bid
+          | VReservedMutBorrow bid -> register_borrow Reserved bid
         in
         (* Continue exploring *)
         super#visit_borrow_content env bc
@@ -254,12 +254,12 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
       method! visit_aborrow_content env bc =
         let _ =
           match bc with
-          | V.AMutBorrow (bid, _) -> register_borrow Mut bid
-          | V.ASharedBorrow bid -> register_borrow Shared bid
-          | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
-          | V.AIgnoredMutBorrow (None, _)
-          | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _
-          | V.AEndedSharedBorrow | V.AProjSharedBorrow _ ->
+          | AMutBorrow (bid, _) -> register_borrow Mut bid
+          | ASharedBorrow bid -> register_borrow Shared bid
+          | AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
+          | AIgnoredMutBorrow (None, _)
+          | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow
+          | AProjSharedBorrow _ ->
               (* Do nothing *)
               ()
         in
@@ -305,7 +305,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
     object
       inherit [_] C.iter_eval_ctx as super
 
-      method! visit_Bottom info =
+      method! visit_VBottom info =
         (* No ⊥ inside borrowed values *)
         assert (Config.allow_bottom_below_borrow || not info.outer_borrow)
 
@@ -317,8 +317,8 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         (* Update the info *)
         let info =
           match lc with
-          | V.SharedLoan (_, _) -> set_outer_shared info
-          | V.MutLoan _ ->
+          | VSharedLoan (_, _) -> set_outer_shared info
+          | VMutLoan _ ->
               (* No mutable loan inside a shared loan *)
               assert (not info.outer_shared);
               set_outer_mut info
@@ -330,11 +330,11 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         (* Update the info *)
         let info =
           match bc with
-          | V.SharedBorrow _ -> set_outer_shared info
-          | V.ReservedMutBorrow _ ->
+          | VSharedBorrow _ -> set_outer_shared info
+          | VReservedMutBorrow _ ->
               assert (not info.outer_borrow);
               set_outer_shared info
-          | V.MutBorrow (_, _) -> set_outer_mut info
+          | VMutBorrow (_, _) -> set_outer_mut info
         in
         (* Continue exploring *)
         super#visit_borrow_content info bc
@@ -343,17 +343,16 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         (* Update the info *)
         let info =
           match lc with
-          | V.AMutLoan (_, _) -> set_outer_mut info
-          | V.ASharedLoan (_, _, _) -> set_outer_shared info
-          | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
-            ->
+          | AMutLoan (_, _) -> set_outer_mut info
+          | ASharedLoan (_, _, _) -> set_outer_shared info
+          | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } ->
               set_outer_mut info
-          | V.AEndedSharedLoan (_, _) -> set_outer_shared info
-          | V.AIgnoredMutLoan (_, _) -> set_outer_mut info
-          | V.AEndedIgnoredMutLoan
+          | AEndedSharedLoan (_, _) -> set_outer_shared info
+          | AIgnoredMutLoan (_, _) -> set_outer_mut info
+          | AEndedIgnoredMutLoan
               { given_back = _; child = _; given_back_meta = _ } ->
               set_outer_mut info
-          | V.AIgnoredSharedLoan _ -> set_outer_shared info
+          | AIgnoredSharedLoan _ -> set_outer_shared info
         in
         (* Continue exploring *)
         super#visit_aloan_content info lc
@@ -362,12 +361,12 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         (* Update the info *)
         let info =
           match bc with
-          | V.AMutBorrow (_, _) -> set_outer_mut info
-          | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info
-          | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
-          | V.AEndedIgnoredMutBorrow _ ->
+          | AMutBorrow (_, _) -> set_outer_mut info
+          | ASharedBorrow _ | AEndedSharedBorrow -> set_outer_shared info
+          | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _
+            ->
               set_outer_mut info
-          | V.AProjSharedBorrow _ -> set_outer_shared info
+          | AProjSharedBorrow _ -> set_outer_shared info
         in
         (* Continue exploring *)
         super#visit_aborrow_content info bc
@@ -416,10 +415,10 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         (* Check that the types have erased regions *)
         assert (ty_is_ety tv.ty);
         (* Check the current pair (value, type) *)
-        (match (tv.V.value, tv.V.ty) with
-        | V.VLiteral cv, T.TLiteral ty -> check_literal_type cv ty
+        (match (tv.value, tv.ty) with
+        | VLiteral cv, TLiteral ty -> check_literal_type cv ty
         (* ADT case *)
-        | V.VAdt av, T.TAdt (T.TAdtId def_id, generics) ->
+        | VAdt av, TAdt (TAdtId def_id, generics) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
             let def = C.ctx_lookup_type_decl ctx def_id in
@@ -428,53 +427,51 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               List.length generics.regions = List.length def.generics.regions);
             assert (List.length generics.types = List.length def.generics.types);
             (* Check that the variant id is consistent *)
-            (match (av.V.variant_id, def.T.kind) with
-            | Some variant_id, T.Enum variants ->
+            (match (av.variant_id, def.kind) with
+            | Some variant_id, Enum variants ->
                 assert (T.VariantId.to_int variant_id < List.length variants)
-            | None, T.Struct _ -> ()
+            | None, Struct _ -> ()
             | _ -> raise (Failure "Erroneous typing"));
             (* Check that the field types are correct *)
             let field_types =
-              Assoc.type_decl_get_inst_norm_field_etypes ctx def av.V.variant_id
+              Assoc.type_decl_get_inst_norm_field_etypes ctx def av.variant_id
                 generics
             in
-            let fields_with_types =
-              List.combine av.V.field_values field_types
-            in
+            let fields_with_types = List.combine av.field_values field_types in
             List.iter
-              (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty))
+              (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.ty = ty))
               fields_with_types
         (* Tuple case *)
-        | V.VAdt av, T.TAdt (T.TTuple, generics) ->
+        | VAdt av, TAdt (TTuple, generics) ->
             assert (generics.regions = []);
             assert (generics.const_generics = []);
-            assert (av.V.variant_id = None);
+            assert (av.variant_id = None);
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
             let fields_with_types =
-              List.combine av.V.field_values generics.types
+              List.combine av.field_values generics.types
             in
             List.iter
-              (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty))
+              (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.ty = ty))
               fields_with_types
         (* Assumed type case *)
-        | V.VAdt av, T.TAdt (T.TAssumed aty_id, generics) -> (
-            assert (av.V.variant_id = None);
+        | VAdt av, TAdt (TAssumed aty_id, generics) -> (
+            assert (av.variant_id = None);
             match
               ( aty_id,
-                av.V.field_values,
+                av.field_values,
                 generics.regions,
                 generics.types,
                 generics.const_generics )
             with
             (* Box *)
-            | T.TBox, [ inner_value ], [], [ inner_ty ], [] ->
-                assert (inner_value.V.ty = inner_ty)
-            | T.TArray, inner_values, _, [ inner_ty ], [ cg ] ->
+            | TBox, [ inner_value ], [], [ inner_ty ], [] ->
+                assert (inner_value.ty = inner_ty)
+            | TArray, inner_values, _, [ inner_ty ], [ cg ] ->
                 (* *)
                 assert (
                   List.for_all
-                    (fun (v : V.typed_value) -> v.V.ty = inner_ty)
+                    (fun (v : V.typed_value) -> v.ty = inner_ty)
                     inner_values);
                 (* The length is necessarily concrete *)
                 let len =
@@ -483,37 +480,37 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                     .value
                 in
                 assert (Z.of_int (List.length inner_values) = len)
-            | (T.TSlice | T.TStr), _, _, _, _ -> raise (Failure "Unexpected")
+            | (TSlice | TStr), _, _, _, _ -> raise (Failure "Unexpected")
             | _ -> raise (Failure "Erroneous type"))
-        | V.Bottom, _ -> (* Nothing to check *) ()
-        | V.Borrow bc, T.TRef (_, ref_ty, rkind) -> (
+        | VBottom, _ -> (* Nothing to check *) ()
+        | VBorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
-            | V.SharedBorrow bid, T.Shared | V.ReservedMutBorrow bid, T.Mut -> (
+            | VSharedBorrow bid, Shared | VReservedMutBorrow bid, Mut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan ek_all bid ctx in
                 match glc with
-                | Concrete (V.SharedLoan (_, sv))
-                | Abstract (V.ASharedLoan (_, sv, _)) ->
-                    assert (sv.V.ty = ref_ty)
+                | Concrete (VSharedLoan (_, sv))
+                | Abstract (ASharedLoan (_, sv, _)) ->
+                    assert (sv.ty = ref_ty)
                 | _ -> raise (Failure "Inconsistent context"))
-            | V.MutBorrow (_, bv), T.Mut ->
+            | VMutBorrow (_, bv), Mut ->
                 assert (
                   (* Check that the borrowed value has the proper type *)
-                  bv.V.ty = ref_ty)
+                  bv.ty = ref_ty)
             | _ -> raise (Failure "Erroneous typing"))
-        | V.Loan lc, ty -> (
+        | VLoan lc, ty -> (
             match lc with
-            | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
-            | V.MutLoan bid -> (
+            | VSharedLoan (_, sv) -> assert (sv.ty = ty)
+            | VMutLoan bid -> (
                 (* Lookup the borrowed value to check it has the proper type *)
                 let glc = lookup_borrow ek_all bid ctx in
                 match glc with
-                | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
-                | Abstract (V.AMutBorrow (_, sv)) ->
-                    assert (Subst.erase_regions sv.V.ty = ty)
+                | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = ty)
+                | Abstract (AMutBorrow (_, sv)) ->
+                    assert (Subst.erase_regions sv.ty = ty)
                 | _ -> raise (Failure "Inconsistent context")))
-        | V.Symbolic sv, ty ->
-            let ty' = Subst.erase_regions sv.V.sv_ty in
+        | VSymbolic sv, ty ->
+            let ty' = Subst.erase_regions sv.sv_ty in
             assert (ty' = ty)
         | _ -> raise (Failure "Erroneous typing"));
         (* Continue exploring to inspect the subterms *)
@@ -531,9 +528,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         (* Check that the types have regions *)
         assert (ty_is_rty atv.ty);
         (* Check the current pair (value, type) *)
-        (match (atv.V.value, atv.V.ty) with
+        (match (atv.value, atv.ty) with
         (* ADT case *)
-        | V.AAdt av, T.TAdt (T.TAdtId def_id, generics) ->
+        | AAdt av, TAdt (TAdtId def_id, generics) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
             let def = C.ctx_lookup_type_decl ctx def_id in
@@ -545,132 +542,126 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               List.length generics.const_generics
               = List.length def.generics.const_generics);
             (* Check that the variant id is consistent *)
-            (match (av.V.variant_id, def.T.kind) with
-            | Some variant_id, T.Enum variants ->
+            (match (av.variant_id, def.kind) with
+            | Some variant_id, Enum variants ->
                 assert (T.VariantId.to_int variant_id < List.length variants)
-            | None, T.Struct _ -> ()
+            | None, Struct _ -> ()
             | _ -> raise (Failure "Erroneous typing"));
             (* Check that the field types are correct *)
             let field_types =
-              Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.V.variant_id
+              Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.variant_id
                 generics
             in
-            let fields_with_types =
-              List.combine av.V.field_values field_types
-            in
+            let fields_with_types = List.combine av.field_values field_types in
             List.iter
-              (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty))
+              (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.ty = ty))
               fields_with_types
         (* Tuple case *)
-        | V.AAdt av, T.TAdt (T.TTuple, generics) ->
+        | AAdt av, TAdt (TTuple, generics) ->
             assert (generics.regions = []);
             assert (generics.const_generics = []);
-            assert (av.V.variant_id = None);
+            assert (av.variant_id = None);
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
             let fields_with_types =
-              List.combine av.V.field_values generics.types
+              List.combine av.field_values generics.types
             in
             List.iter
-              (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty))
+              (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.ty = ty))
               fields_with_types
         (* Assumed type case *)
-        | V.AAdt av, T.TAdt (T.TAssumed aty_id, generics) -> (
-            assert (av.V.variant_id = None);
+        | AAdt av, TAdt (TAssumed aty_id, generics) -> (
+            assert (av.variant_id = None);
             match
               ( aty_id,
-                av.V.field_values,
+                av.field_values,
                 generics.regions,
                 generics.types,
                 generics.const_generics )
             with
             (* Box *)
-            | T.TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
-                assert (boxed_value.V.ty = boxed_ty)
+            | TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
+                assert (boxed_value.ty = boxed_ty)
             | _ -> raise (Failure "Erroneous type"))
-        | V.ABottom, _ -> (* Nothing to check *) ()
-        | V.ABorrow bc, T.TRef (_, ref_ty, rkind) -> (
+        | ABottom, _ -> (* Nothing to check *) ()
+        | ABorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
-            | V.AMutBorrow (_, av), T.Mut ->
+            | AMutBorrow (_, av), Mut ->
                 (* Check that the child value has the proper type *)
-                assert (av.V.ty = ref_ty)
-            | V.ASharedBorrow bid, T.Shared -> (
+                assert (av.ty = ref_ty)
+            | ASharedBorrow bid, Shared -> (
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan ek_all bid ctx in
                 match glc with
-                | Concrete (V.SharedLoan (_, sv))
-                | Abstract (V.ASharedLoan (_, sv, _)) ->
-                    assert (sv.V.ty = Subst.erase_regions ref_ty)
+                | Concrete (VSharedLoan (_, sv))
+                | Abstract (ASharedLoan (_, sv, _)) ->
+                    assert (sv.ty = Subst.erase_regions ref_ty)
                 | _ -> raise (Failure "Inconsistent context"))
-            | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
-                assert (av.V.ty = ref_ty)
-            | ( V.AEndedIgnoredMutBorrow
-                  { given_back; child; given_back_meta = _ },
-                T.Mut ) ->
-                assert (given_back.V.ty = ref_ty);
-                assert (child.V.ty = ref_ty)
-            | V.AProjSharedBorrow _, T.Shared -> ()
+            | AIgnoredMutBorrow (_opt_bid, av), Mut -> assert (av.ty = ref_ty)
+            | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ },
+                Mut ) ->
+                assert (given_back.ty = ref_ty);
+                assert (child.ty = ref_ty)
+            | AProjSharedBorrow _, Shared -> ()
             | _ -> raise (Failure "Inconsistent context"))
-        | V.ALoan lc, aty -> (
+        | ALoan lc, aty -> (
             match lc with
-            | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (Some bid, child_av)
+            | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
               -> (
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (child_av.V.ty = borrowed_aty);
+                assert (child_av.ty = borrowed_aty);
                 (* Lookup the borrowed value to check it has the proper type *)
                 let glc = lookup_borrow ek_all bid ctx in
                 match glc with
-                | Concrete (V.MutBorrow (_, bv)) ->
-                    assert (bv.V.ty = Subst.erase_regions borrowed_aty)
-                | Abstract (V.AMutBorrow (_, sv)) ->
+                | Concrete (VMutBorrow (_, bv)) ->
+                    assert (bv.ty = Subst.erase_regions borrowed_aty)
+                | Abstract (AMutBorrow (_, sv)) ->
                     assert (
-                      Subst.erase_regions sv.V.ty
+                      Subst.erase_regions sv.ty
                       = Subst.erase_regions borrowed_aty)
                 | _ -> raise (Failure "Inconsistent context"))
-            | V.AIgnoredMutLoan (None, child_av) ->
+            | AIgnoredMutLoan (None, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (child_av.V.ty = borrowed_aty)
-            | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
-              ->
+                assert (child_av.ty = borrowed_aty)
+            | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (sv.V.ty = Subst.erase_regions borrowed_aty);
+                assert (sv.ty = Subst.erase_regions borrowed_aty);
                 (* TODO: the type of aloans doesn't make sense, see above *)
-                assert (child_av.V.ty = borrowed_aty)
-            | V.AEndedMutLoan { given_back; child; given_back_meta = _ }
-            | V.AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ }
-              ->
+                assert (child_av.ty = borrowed_aty)
+            | AEndedMutLoan { given_back; child; given_back_meta = _ }
+            | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (given_back.V.ty = borrowed_aty);
-                assert (child.V.ty = borrowed_aty)
-            | V.AIgnoredSharedLoan child_av ->
-                assert (child_av.V.ty = aloan_get_expected_child_type aty))
-        | V.ASymbolic aproj, ty -> (
+                assert (given_back.ty = borrowed_aty);
+                assert (child.ty = borrowed_aty)
+            | AIgnoredSharedLoan child_av ->
+                assert (child_av.ty = aloan_get_expected_child_type aty))
+        | ASymbolic aproj, ty -> (
             let ty1 = Subst.erase_regions ty in
             match aproj with
-            | V.AProjLoans (sv, _) ->
-                let ty2 = Subst.erase_regions sv.V.sv_ty in
+            | AProjLoans (sv, _) ->
+                let ty2 = Subst.erase_regions sv.sv_ty in
                 assert (ty1 = ty2);
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
-                assert (ty_has_regions_in_set abs.regions sv.V.sv_ty)
-            | V.AProjBorrows (sv, proj_ty) ->
-                let ty2 = Subst.erase_regions sv.V.sv_ty in
+                assert (ty_has_regions_in_set abs.regions sv.sv_ty)
+            | AProjBorrows (sv, proj_ty) ->
+                let ty2 = Subst.erase_regions sv.sv_ty in
                 assert (ty1 = ty2);
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
                 assert (ty_has_regions_in_set abs.regions proj_ty)
-            | V.AEndedProjLoans (_msv, given_back_ls) ->
+            | AEndedProjLoans (_msv, given_back_ls) ->
                 List.iter
                   (fun (_, proj) ->
                     match proj with
                     | V.AProjBorrows (_sv, ty') -> assert (ty' = ty)
-                    | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ()
+                    | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()
                     | _ -> raise (Failure "Unexpected"))
                   given_back_ls
-            | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ())
-        | V.AIgnored, _ -> ()
+            | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
+        | AIgnored, _ -> ()
         | _ ->
             log#lerror
               (lazy
@@ -757,7 +748,7 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
     object
       inherit [_] C.iter_eval_ctx as super
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
-      method! visit_Symbolic _ sv = add_env_sv sv
+      method! visit_VSymbolic _ sv = add_env_sv sv
 
       method! visit_abstract_shared_borrow abs asb =
         let abs = Option.get abs in