diff options
author | Son Ho | 2022-01-04 22:40:55 +0100 |
---|---|---|
committer | Son Ho | 2022-01-04 22:40:55 +0100 |
commit | 02a1cd57fe3a36f042579a2d0e8c194e4d9a599a (patch) | |
tree | 368d53ed7ad7bfa8139fb124ccfbb6a8a20c1c67 | |
parent | 84bd12c6d832f20529bbfa763ac1a2de3909d382 (diff) |
Finish implementing visit_typed_value for check_typing_invariant
-rw-r--r-- | src/Invariants.ml | 9 |
1 files changed, 6 insertions, 3 deletions
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) |