1 files changed, 89 insertions, 0 deletions
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index f21fdcd5..a1a8fb0c 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -30,6 +30,13 @@ val end_abstraction : C.config -> V.AbstractionId.id -> cm_fun
 (** End a set of abstractions while preserving the invariants. *)
 val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun
 
+(** End a borrow and return the resulting environment, ignoring synthesis *)
+val end_borrow_no_synth : C.config -> V.BorrowId.id -> C.eval_ctx -> C.eval_ctx
+
+(** End an abstraction and return the resulting environment, ignoring synthesis *)
+val end_abstraction_no_synth :
+  C.config -> V.AbstractionId.id -> C.eval_ctx -> C.eval_ctx
+
 (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants.
 
     Reserved borrows are special mutable borrows which are created as shared borrows
@@ -40,3 +47,85 @@ val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun
     other shared borrows which point to this loan).
  *)
 val promote_reserved_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
+
+(** Transform an abstraction to an abstraction where the values are not
+    structured.
+
+    For instance:
+    {[
+      abs {
+        (mut_borrow l0, mut_borrow l1, _)
+      }
+
+          ~~>
+
+      abs {
+        mut_borrow l0
+        mut_borrow l1
+      }
+    ]}
+
+    Rem.: we do this to simplify the merging of abstractions. We can do this
+    because for now, we don't support nested borrows.
+
+    Paramters:
+    - [abs_kind]
+    - [can_end]
+    - [ctx]
+    - [abs]
+ *)
+val destructure_abs : V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs
+
+(** Return [true] if the values in an abstraction are destructured.
+
+    We simply destructure it and check that it gives the identity.
+ *)
+val abs_is_destructured : C.eval_ctx -> V.abs -> bool
+
+(** Turn a value into a abstractions.
+
+    We are conservative, and don't group borrows/loans into the same abstraction
+    unless necessary.
+
+    For instance:
+    {[
+      _ -> (mut_borrow l1 (mut_loan l2), mut_borrow l3)
+
+      ~~>
+
+      abs'0 { mut_borrow l1, mut_loan l2 }
+      abs'1 { mut_borrow l3 }
+    ]}
+
+    Parameters:
+    - [abs_kind]
+    - [can_end]
+    - [ctx]
+    - [v]
+ *)
+val convert_value_to_abstractions :
+  V.abs_kind -> bool -> C.eval_ctx -> V.typed_value -> V.abs list
+
+(** Merge two abstractions together.
+
+    Merging two abstractions together implies removing the loans/borrows
+    which appear in one and whose associated loans/borrows appear in the
+    other. For instance:
+    {[
+      abs'0 { mut_borrow l0, mut_loan l1 }
+      abs'1 { mut_borrow l1, mut_borrow l2 }
+
+          ~~>
+
+      abs'01 { mut_borrow l0, mut_borrow l2 }
+    ]}
+
+    Parameters:
+    - [kind]
+    - [can_end]
+    - [ctx]
+    - [abs0]
+    - [abs1]
+ *)
+val merge_abstractions :
+  V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs -> V.abs