Make progress on the fixed point computation

2 files changed, 86 insertions, 6 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 1b05911b..a8d50720 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1423,6 +1423,9 @@ let end_borrows_no_synth config ids ctx =
 let end_abstraction_no_synth config id ctx =
   get_cf_ctx_no_synth (end_abstraction config id) ctx
 
+let end_abstractions_no_synth config ids ctx =
+  get_cf_ctx_no_synth (end_abstractions config ids) ctx
+
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
     This function updates the shared loan to a mutable loan (we then update
@@ -1923,8 +1926,7 @@ type merge_abstraction_info = {
     - all the borrows are destructured (for instance, shared loans can't
       contain shared loans).
  *)
-let compute_merge_abstractions_info (ctx : C.eval_ctx) (abs : V.abs) :
-    merge_abstraction_info =
+let compute_merge_abstractions_info (abs : V.abs) : merge_abstraction_info =
   let loans : V.loan_id_set ref = ref V.BorrowId.Set.empty in
   let borrows : V.borrow_id_set ref = ref V.BorrowId.Set.empty in
   let borrows_loans : borrow_or_loan_id list ref = ref [] in
@@ -2060,7 +2062,23 @@ type merge_duplicates_funcs = {
     V.mvalue ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [mv0]
+          - [child0]
+          - [ty1]
+          - [mv1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [ty1]
+       *)
   merge_amut_loans :
     V.loan_id ->
     T.rty ->
@@ -2068,13 +2086,33 @@ type merge_duplicates_funcs = {
     T.rty ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [child0]
+          - [ty1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_loans :
     V.loan_id_set ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [ids]
+          - [ty0]
+          - [sv0]
+          - [child0]
+          - [ty1]
+          - [sv1]
+          - [child1]
+       *)
 }
 
 let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
@@ -2094,7 +2132,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
     loan_to_content = loan_to_content0;
     borrow_to_content = borrow_to_content0;
   } =
-    compute_merge_abstractions_info ctx abs0
+    compute_merge_abstractions_info abs0
   in
 
   let {
@@ -2104,7 +2142,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
     loan_to_content = loan_to_content1;
     borrow_to_content = borrow_to_content1;
   } =
-    compute_merge_abstractions_info ctx abs1
+    compute_merge_abstractions_info abs1
   in
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
@@ -2181,7 +2219,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
   let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
       (bc1 : g_borrow_content_with_ty) : V.typed_avalue =
     match (bc0, bc1) with
-    | Concrete (ty0, bc0), Concrete (ty1, bc1) ->
+    | Concrete _, Concrete _ ->
         (* This can happen only in case of nested borrows *)
         raise (Failure "Unreachable")
     | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
@@ -2212,7 +2250,8 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
         (* Register the loan ids *)
         V.BorrowId.Set.iter set_loan_as_merged ids;
         (* Merge *)
-        (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 ty1 sv1
+        (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 child0 ty1 sv1
+          child1
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 8b8b76d9..01ce206a 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -41,6 +41,10 @@ val end_borrows_no_synth :
 val end_abstraction_no_synth :
   C.config -> V.AbstractionId.id -> C.eval_ctx -> C.eval_ctx
 
+(** End a set of abstractions and return the resulting environment, ignoring synthesis *)
+val end_abstractions_no_synth :
+  C.config -> V.AbstractionId.Set.t -> 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
@@ -133,6 +137,7 @@ val convert_value_to_abstractions :
     Rem.: it may be more idiomatic to have a functor, but this seems a bit
     heavyweight, though.
   *)
+
 type merge_duplicates_funcs = {
   merge_amut_borrows :
     V.borrow_id ->
@@ -143,7 +148,23 @@ type merge_duplicates_funcs = {
     V.mvalue ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [mv0]
+          - [child0]
+          - [ty1]
+          - [mv1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [ty1]
+       *)
   merge_amut_loans :
     V.loan_id ->
     T.rty ->
@@ -151,13 +172,33 @@ type merge_duplicates_funcs = {
     T.rty ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [child0]
+          - [ty1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_loans :
     V.loan_id_set ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [ids]
+          - [ty0]
+          - [sv0]
+          - [child0]
+          - [ty1]
+          - [sv1]
+          - [child1]
+       *)
 }
 
 (** Merge two abstractions together.