summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorAymeric Fromherz2024-05-31 14:46:12 +0200
committerAymeric Fromherz2024-05-31 14:46:12 +0200
commit3598da14b7de6452b03e98e701996a8b6d4d5d38 (patch)
tree89a52f0de50718f41cf10ca4a33f88f0480ea04b /compiler
parent2e3d1cdfde3e19af97e0d0fa47f92cfd66c688d9 (diff)
Add documentation to collapse
Diffstat (limited to 'compiler')
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml28
1 files changed, 27 insertions, 1 deletions
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 =