From ab2637af8b82f13be8ac38a800368bce6bbd10e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jan 2022 23:10:06 +0100
Subject: Finish implementing visit_typed_avalue for check_typing_invariant

---
 src/Invariants.ml | 36 ++++++++++++++++++++++++------------
 1 file changed, 24 insertions(+), 12 deletions(-)

(limited to 'src/Invariants.ml')

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 2cbae606..9390436c 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -492,18 +492,30 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | V.AIgnoredMutBorrow av, T.Mut -> assert (av.V.ty = ref_ty)
             | V.AProjSharedBorrow _, T.Shared -> ()
             | _ -> failwith "Inconsistent context")
-        | V.ALoan lc, ty -> raise Unimplemented
-        (* (
-             match lc with
-             | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
-             | V.MutLoan 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)
-                 | _ -> failwith "Inconsistent context"))*)
+        | V.ALoan lc, aty -> (
+            match lc with
+            | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av)
+              -> (
+                assert (child_av.V.ty = 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 aty)
+                | Abstract (V.AMutBorrow (_, sv)) ->
+                    assert (
+                      Subst.erase_regions sv.V.ty = Subst.erase_regions aty)
+                | _ -> failwith "Inconsistent context")
+            | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
+              ->
+                let ty = Subst.erase_regions aty in
+                assert (sv.V.ty = ty);
+                assert (child_av.V.ty = aty)
+            | V.AEndedMutLoan { given_back; child }
+            | V.AEndedIgnoredMutLoan { given_back; child } ->
+                assert (given_back.V.ty = aty);
+                assert (child.V.ty = aty)
+            | V.AIgnoredSharedLoan child_av -> assert (child_av.V.ty = aty))
         | V.ASymbolic aproj, ty ->
             let ty1 = Subst.erase_regions ty in
             let ty2 =
-- 
cgit v1.2.3