diff options
| author | Aymeric Fromherz | 2024-05-27 16:03:36 +0200 |
|---|---|---|
| committer | Aymeric Fromherz | 2024-05-27 16:03:36 +0200 |
| commit | 506e9dc3f8f2759769c3293e9cbeba5d6fe79a31 (patch) | |
| tree | 08fa383fbdf726f2e25f7662602b5f765fc5ae8e /compiler/Invariants.ml | |
| parent | 51c43721beb1f4af1e903360c0fbc5c1790f1ab5 (diff) | |
Add markers everywhere, do not use them yet
Diffstat (limited to '')
| -rw-r--r-- | compiler/Invariants.ml | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index bcf92b25..fc882423 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -150,8 +150,8 @@ let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) : method! visit_aloan_content inside_abs lc = let _ = match lc with - | AMutLoan (bid, _) -> register_mut_loan inside_abs bid - | ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids + | AMutLoan (_, bid, _) -> register_mut_loan inside_abs bid + | ASharedLoan (_, bids, _, _) -> register_shared_loan inside_abs bids | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan RMut bid | AIgnoredMutLoan (None, _) | AIgnoredSharedLoan _ @@ -522,7 +522,8 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = match glc with | Concrete (VMutBorrow (_, bv)) -> sanity_check __FILE__ __LINE__ (bv.ty = ty) span - | Abstract (AMutBorrow (_, sv)) -> + | Abstract (AMutBorrow (pm, _, sv)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = ty) span @@ -612,15 +613,17 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | ABottom, _ -> (* Nothing to check *) () | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with - | AMutBorrow (_, av), RMut -> + | AMutBorrow (pm, _, av), RMut -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Check that the child value has the proper type *) sanity_check __FILE__ __LINE__ (av.ty = ref_ty) span - | ASharedBorrow bid, RShared -> ( + | ASharedBorrow (pm, bid), RShared -> ( + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan span ek_all bid ctx in match glc with | Concrete (VSharedLoan (_, sv)) - | Abstract (ASharedLoan (_, sv, _)) -> + | Abstract (ASharedLoan (_, _, sv, _)) -> sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions ref_ty) span @@ -635,8 +638,8 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | _ -> craise __FILE__ __LINE__ span "Inconsistent context") | ALoan lc, aty -> ( match lc with - | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) - -> ( + | AMutLoan (PNone, bid, child_av) + | AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span; (* Lookup the borrowed value to check it has the proper type *) @@ -646,22 +649,25 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = sanity_check __FILE__ __LINE__ (bv.ty = Substitute.erase_regions borrowed_aty) span - | Abstract (AMutBorrow (_, sv)) -> + | Abstract (AMutBorrow (_, _, sv)) -> sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = Substitute.erase_regions borrowed_aty) span | _ -> craise __FILE__ __LINE__ span "Inconsistent context") + | AMutLoan (_, _, _) -> internal_error __FILE__ __LINE__ span | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span - | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> + | ASharedLoan (PNone, _, sv, child_av) + | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions borrowed_aty) span; (* TODO: the type of aloans doesn't make sense, see above *) sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span + | ASharedLoan (_, _, _, _) -> internal_error __FILE__ __LINE__ span | AEndedMutLoan { given_back; child; given_back_span = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_span = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in |