summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorAymeric Fromherz2024-05-27 16:44:28 +0200
committerAymeric Fromherz2024-05-27 16:44:28 +0200
commitc236ccfb22e64f56f4398d067582ebd570bf1a0b (patch)
treed318095b40de9b7684b90c52773a0de326c799a6 /compiler
parent506e9dc3f8f2759769c3293e9cbeba5d6fe79a31 (diff)
Add projection markers when joining environments
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml59
1 files changed, 59 insertions, 0 deletions
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 7ea442db..0f61f619 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -467,6 +467,65 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
(* This should have been eliminated *)
craise __FILE__ __LINE__ span "Unreachable"
in
+
+ (* Add a projection marker to a typed avalue *)
+ let add_marker_avalue (pm : proj_marker) (av : typed_avalue) : typed_avalue
+ =
+ let obj =
+ object
+ inherit [_] map_typed_avalue as super
+
+ method! visit_borrow_content _ _ =
+ craise __FILE__ __LINE__ span "Unexpected borrow"
+
+ method! visit_loan_content _ _ =
+ craise __FILE__ __LINE__ span "Unexpected loan"
+
+ method! visit_symbolic_value _ sv =
+ (* While ctx0 and ctx1 are different, we assume that the type info context is
+ the same in both. Hence, we can use ctx0's types wlog *)
+ sanity_check __FILE__ __LINE__
+ (not (symbolic_value_has_borrows ctx0 sv))
+ span;
+ sv
+
+ method! visit_aloan_content env lc =
+ match lc with
+ | AMutLoan (pm0, bid, av) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aloan_content env (AMutLoan (pm, bid, av))
+ | ASharedLoan (pm0, bids, av, child) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aloan_content env
+ (ASharedLoan (pm, bids, av, child))
+ | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
+
+ method! visit_aborrow_content env bc =
+ match bc with
+ | AMutBorrow (pm0, bid, av) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aborrow_content env (AMutBorrow (pm, bid, av))
+ | ASharedBorrow (pm0, bid) ->
+ sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+ super#visit_aborrow_content env (ASharedBorrow (pm, bid))
+ | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
+ end
+ in
+ obj#visit_typed_avalue () av
+ in
+
+ (* Add projection marker to all abstractions in the left and right environments *)
+ let add_marker (pm : proj_marker) (ee : env_elem) : env_elem =
+ match ee with
+ | EAbs abs ->
+ EAbs
+ { abs with avalues = List.map (add_marker_avalue pm) abs.avalues }
+ | x -> x
+ in
+
+ let env0 = List.map (add_marker PLeft) env0 in
+ let env1 = List.map (add_marker PRight) env1 in
+
List.iter check_valid env0;
List.iter check_valid env1;
(* Concatenate the suffixes and append the abstractions introduced while