diff options
| author | Son HO | 2024-06-04 14:05:44 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-04 14:05:44 +0200 |
| commit | afc4e62ce7a584da0bb0a7350533e321388be545 (patch) | |
| tree | 89f3b6999e1697595f1c3fbb2d9c4d8c60a69e49 /compiler/InterpreterPaths.ml | |
| parent | 4a31acdff7a5dfdc26bf25ad25bb8266b790f891 (diff) | |
| parent | 3ad6c4712fd41efec55f29af5ccc31f68a0e12cf (diff) | |
Merge pull request #228 from AeneasVerif/son/loops2
Add support for projection markers when joining environments
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterPaths.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index faba1088..b2de3b22 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -187,7 +187,7 @@ let rec access_projection (span : Meta.span) (access : projection_access) Ok (ctx, { res with updated = v })) | ( _, Abstract - ( AMutLoan (_, _) + ( AMutLoan (_, _, _) | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) @@ -197,7 +197,9 @@ let rec access_projection (span : Meta.span) (access : projection_access) | AIgnoredSharedLoan _ ) ) -> craise __FILE__ __LINE__ span "Expected a shared (abstraction) loan" - | _, Abstract (ASharedLoan (bids, sv, _av)) -> ( + | _, Abstract (ASharedLoan (pm, bids, sv, _av)) -> ( + (* 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 | Error err -> Error err @@ -205,14 +207,14 @@ let rec access_projection (span : Meta.span) (access : projection_access) (* Relookup the child avalue *) let av = match lookup_loan span ek bid ctx with - | _, Abstract (ASharedLoan (_, _, av)) -> av + | _, Abstract (ASharedLoan (_, _, _, av)) -> av | _ -> craise __FILE__ __LINE__ span "Unexpected" in (* Update the shared loan with the new value returned by {!access_projection} *) let ctx = update_aloan span ek bid - (ASharedLoan (bids, res.updated, av)) + (ASharedLoan (pm, bids, res.updated, av)) ctx in (* Return - note that we don't need to update the borrow itself *) |