From 3598da14b7de6452b03e98e701996a8b6d4d5d38 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 31 May 2024 14:46:12 +0200
Subject: Add documentation to collapse

---
 compiler/InterpreterLoopsJoinCtxs.ml | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 4b5cfb82..930bffac 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -292,7 +292,33 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
 (* Reduce_ctx can only be called in a context with no markers *)
 let reduce_ctx = reduce_ctx_with_markers None
 
-(* TODO Adapt and comment *)
+(* Collapse an environment
+
+  This is the second part of a join, where we attempt to simplify and remove all projection markers.
+  This function is called after reducing the environments, and attempting to simplify all the pairs
+  of borrows and loans.
+
+  We traverse all abstractions, and merge abstractions when they contain the same element,
+  but with dual markers (i.e., PLeft and PRight).
+
+  For instance, if we have the abstractions
+
+  abs@0 { | MB l0 _ |, ML l1 }
+  abs@1 { ︙MB l0 _ ︙, ML l2 }
+
+  we will merge abs@0 and abs@1 into a new abstraction abs@2, removing the marker for duplicated elements,
+  and taking the join of the remaining elements
+
+  abs@2 { MB l0 _, ML l1, ML l2 }
+
+  Rem.: Doing this might introduce new pairs of borrow/loans to be merged in different abstractions: in the example above,
+  this could occur if there was another abstraction in the context containing ML l0, which would need to be simplified through
+  a further reduce.
+  It is unclear whether this can happen in practice. If so, a solution would be to preprocess the environments when doing
+  a join: while not in the current formalism, it is sound to split an element with no markers into a duplicated pair of the
+  same element with left and right markers. Doing this before reduce would allow to reduce all possible pairs of borrow/loans,
+  before finally collapsing and removing all markers.
+*)
 let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id)
     (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx)
     : eval_ctx =
-- 
cgit v1.2.3