From 02a1cd57fe3a36f042579a2d0e8c194e4d9a599a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jan 2022 22:40:55 +0100
Subject: Finish implementing visit_typed_value for check_typing_invariant

---
 src/Invariants.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'src/Invariants.ml')

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 03cafd60..457c00ad 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -397,11 +397,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             match (bc, rkind) with
             | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut
               ->
-                (* Lookup the borrowed value to check it has the proper type *)
-                raise Unimplemented
+                (* TODO: lookup the borrowed value to check it has the proper type *)
+                ()
             | V.MutBorrow (_, bv), T.Mut -> assert (bv.V.ty = ref_ty)
             | _ -> failwith "Erroneous typing")
-        | V.Loan lc, _ -> raise Unimplemented
+        | V.Loan lc, ty -> (
+            match lc with
+            | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
+            | V.MutLoan _ -> ())
         | V.Symbolic spc, ty ->
             let ty' = Subst.erase_regions spc.V.svalue.V.sv_ty in
             assert (ty' = ty)
-- 
cgit v1.2.3