summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/InterpreterBorrowsCore.ml20
-rw-r--r--compiler/InterpreterPaths.ml2
-rw-r--r--compiler/Invariants.ml21
-rw-r--r--compiler/Print.ml1
4 files changed, 25 insertions, 19 deletions
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 3bef7b30..0469d58e 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -256,12 +256,12 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
method! visit_aloan_content env lc =
match lc with
| AMutLoan (pm, bid, av) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if bid = l then raise (FoundGLoanContent (Abstract lc))
else super#visit_AMutLoan env pm bid av
| ASharedLoan (pm, bids, v, av) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if BorrowId.Set.mem l bids then
raise (FoundGLoanContent (Abstract lc))
@@ -401,11 +401,11 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
method! visit_aloan_content env lc =
match lc with
| AMutLoan (pm, bid, av) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if bid = l then update () else super#visit_AMutLoan env pm bid av
| ASharedLoan (pm, bids, v, av) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if BorrowId.Set.mem l bids then update ()
else super#visit_ASharedLoan env pm bids v av
@@ -462,12 +462,12 @@ let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind)
method! visit_aborrow_content env bc =
match bc with
| AMutBorrow (pm, bid, av) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if bid = l then raise (FoundGBorrowContent (Abstract bc))
else super#visit_AMutBorrow env pm bid av
| ASharedBorrow (pm, bid) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if bid = l then raise (FoundGBorrowContent (Abstract bc))
else super#visit_ASharedBorrow env pm bid
@@ -584,12 +584,12 @@ let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
method! visit_ABorrow env bc =
match bc with
| AMutBorrow (pm, bid, av) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if bid = l then update ()
else ABorrow (super#visit_AMutBorrow env pm bid av)
| ASharedBorrow (pm, bid) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
if bid = l then update ()
else ABorrow (super#visit_ASharedBorrow env pm bid)
@@ -1199,11 +1199,11 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
method! visit_aloan_content env lc =
match lc with
| AMutLoan (pm, bid, _) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
raise (FoundBorrowIds (Borrow bid))
| ASharedLoan (pm, bids, _, _) ->
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
raise (FoundBorrowIds (Borrows bids))
| AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index a74017d1..b2de3b22 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -198,7 +198,7 @@ let rec access_projection (span : Meta.span) (access : projection_access)
craise __FILE__ __LINE__ span
"Expected a shared (abstraction) loan"
| _, Abstract (ASharedLoan (pm, bids, sv, _av)) -> (
- (* Sanity check: markers can only appear when we're doing a join *)
+ (* Sanity check: projection markers can only appear when we're doing a join *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
(* Explore the shared value *)
match access_projection span access ctx update p' sv with
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index fc882423..50e6e87f 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -497,14 +497,14 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
| VBorrow bc, TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
| VSharedBorrow bid, RShared | VReservedMutBorrow bid, RMut -> (
- (* Lookup the borrowed value to check it has the proper type *)
+ (* Lookup the borrowed value to check it has the proper type.
+ Note that we ignore the marker: we will check it when
+ checking the loan itself. *)
let _, glc = lookup_loan span ek_all bid ctx in
match glc with
- | Concrete (VSharedLoan (_, sv)) ->
+ | Concrete (VSharedLoan (_, sv))
+ | Abstract (ASharedLoan (_, _, sv, _)) ->
sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span
- | Abstract (ASharedLoan (pm, _, sv, _)) ->
- sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span;
- sanity_check __FILE__ __LINE__ (pm = PNone) span
| _ -> craise __FILE__ __LINE__ span "Inconsistent context")
| VMutBorrow (_, bv), RMut ->
sanity_check __FILE__ __LINE__
@@ -517,12 +517,13 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
| VSharedLoan (_, sv) ->
sanity_check __FILE__ __LINE__ (sv.ty = ty) span
| VMutLoan bid -> (
- (* Lookup the borrowed value to check it has the proper type *)
+ (* Lookup the borrowed value to check it has the proper type. *)
let glc = lookup_borrow span ek_all bid ctx in
match glc with
| Concrete (VMutBorrow (_, bv)) ->
sanity_check __FILE__ __LINE__ (bv.ty = ty) span
| Abstract (AMutBorrow (pm, _, sv)) ->
+ (* The marker check is redundant, but doesn't cost much *)
sanity_check __FILE__ __LINE__ (pm = PNone) span;
sanity_check __FILE__ __LINE__
(Substitute.erase_regions sv.ty = ty)
@@ -655,7 +656,9 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
= Substitute.erase_regions borrowed_aty)
span
| _ -> craise __FILE__ __LINE__ span "Inconsistent context")
- | AMutLoan (_, _, _) -> internal_error __FILE__ __LINE__ span
+ | AMutLoan (_, _, _) ->
+ (* We get there if the projection marker is not [PNone] *)
+ 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
@@ -667,7 +670,9 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
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
+ | ASharedLoan (_, _, _, _) ->
+ (* We get there if the projection marker is not [PNone] *)
+ 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
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 9a3a7d16..7495d6bf 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -148,6 +148,7 @@ module Values = struct
| AEndedProjBorrows _mv -> "_"
| AIgnoredProjBorrows -> "_"
+ (** Wrap a value inside its marker, if there is one *)
let add_proj_marker (pm : proj_marker) (s : string) : string =
match pm with
| PNone -> s
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 21:30:28 +0000