From f5a7a0ceccfeec0dd8801d5a874cb66c1a356f8f Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 31 May 2024 15:00:23 +0200
Subject: format

---
 compiler/InterpreterLoopsJoinCtxs.ml | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 930bffac..b58d1b3e 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -294,30 +294,30 @@ let reduce_ctx = reduce_ctx_with_markers None
 
 (* 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.
+   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).
+   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
+   For instance, if we have the abstractions
 
-  abs@0 { | MB l0 _ |, ML l1 }
-  abs@1 { ︙MB l0 _ ︙, ML l2 }
+   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
+   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 }
+   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.
+   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)
-- 
cgit v1.2.3