Introduce "AIgnore" for the avalues

5 files changed, 11 insertions, 8 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 067b867e..ebfd87c7 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -978,7 +978,7 @@ and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id)
 
       method! visit_ASymbolic _ sproj =
         match sproj with
-        | V.AProjBorrows (_, _) -> ()
+        | V.AProjBorrows (_, _) | V.AEndedProjLoans | V.AEndedProjBorrows -> ()
         | V.AProjLoans sv -> raise (FoundSymbolicValue sv)
     end
   in
@@ -1064,6 +1064,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
         | V.AProjLoans _ -> failwith "Unexpected"
         | V.AProjBorrows (sv, proj_ty) ->
             raise (FoundAProjBorrows (sv, proj_ty))
+        | V.AEndedProjLoans | V.AEndedProjBorrows -> ()
     end
   in
   (* Lookup the abstraction *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 9b272db8..65502126 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -226,6 +226,7 @@ let bottom_in_avalue (ended_regions : T.RegionId.set_t) (v : V.typed_avalue) :
         match ap with
         | V.AProjLoans _sv -> ()
         | V.AProjBorrows (_sv, _rty) -> ()
+        | V.AEndedProjLoans | V.AEndedProjBorrows -> ()
     end
   in
   (* We use exceptions *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 3fc390b5..23f7d456 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -593,14 +593,13 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 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 ->
+        | V.ASymbolic aproj, ty -> (
             let ty1 = Subst.erase_regions ty in
-            let ty2 =
-              match aproj with
-              | V.AProjLoans sv | V.AProjBorrows (sv, _) ->
-                  Subst.erase_regions sv.V.sv_ty
-            in
-            assert (ty1 = ty2)
+            match aproj with
+            | V.AProjLoans sv | V.AProjBorrows (sv, _) ->
+                let ty2 = Subst.erase_regions sv.V.sv_ty in
+                assert (ty1 = ty2)
+            | V.AEndedProjLoans | V.AEndedProjBorrows -> ())
         | _ -> failwith "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
diff --git a/src/Print.ml b/src/Print.ml
index 3869012a..d7830549 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -363,6 +363,7 @@ module Values = struct
     | ABorrow bc -> aborrow_content_to_string fmt bc
     | ALoan lc -> aloan_content_to_string fmt lc
     | ASymbolic s -> aproj_to_string fmt s
+    | AIgnored -> "_"
 
   and aloan_content_to_string (fmt : value_formatter) (lc : V.aloan_content) :
       string =
diff --git a/src/Values.ml b/src/Values.ml
index 41d8bd85..707986f8 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -250,6 +250,7 @@ type avalue =
   | ALoan of aloan_content
   | ABorrow of aborrow_content
   | ASymbolic of aproj
+  | AIgnored  (** A value we don't own and thus ignore *)
 
 and adt_avalue = {
   variant_id : (VariantId.id option[@opaque]);