diff options
author | Son Ho | 2022-01-13 21:32:06 +0100 |
---|---|---|
committer | Son Ho | 2022-01-13 21:32:06 +0100 |
commit | 19783cea9664e5ac0b14419b4aa961716010aafb (patch) | |
tree | 47d22bf2a18d70d180129c2b41fe19c4bb836438 /src/Invariants.ml | |
parent | e9c3dfc34d7cac0d2449b4d11db5adf7218b25db (diff) |
Introduce "AIgnore" for the avalues
Diffstat (limited to '')
-rw-r--r-- | src/Invariants.ml | 13 |
1 files changed, 6 insertions, 7 deletions
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 |