From 52bcaf0cdd1c08ece0f9f09bdc0d32b753a2a00f Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 31 May 2024 11:55:51 +0200
Subject: Add markers when creating new abstractions because of a join with
 bottom

---
 compiler/InterpreterLoopsJoinCtxs.ml | 51 +++---------------------------------
 1 file changed, 4 insertions(+), 47 deletions(-)

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 1e099d96..2f2dba41 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -664,58 +664,15 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
           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 }
+            {
+              abs with
+              avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues;
+            }
       | x -> x
     in
 
-- 
cgit v1.2.3