From a64fdc8b1be70de43afe35ff788ba3240318daac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 15:02:17 +0100
Subject: WIP Beginning working on better errors: began replacing raise
 (Failure) and assert by craise and cassert. Does not compile yet, still need
 to propagate the meta variable where it's relevant

---
 compiler/InterpreterLoopsJoinCtxs.ml | 78 ++++++++++++++++++------------------
 1 file changed, 40 insertions(+), 38 deletions(-)

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 88f290c4..fc2a97e5 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -7,6 +7,7 @@ open InterpreterUtils
 open InterpreterBorrows
 open InterpreterLoopsCore
 open InterpreterLoopsMatchCtxs
+open Errors
 
 (** The local logger *)
 let log = Logging.loops_join_ctxs_log
@@ -18,7 +19,7 @@ let log = Logging.loops_join_ctxs_log
     called typically after we merge abstractions together (see {!collapse_ctx}
     for instance).
  *)
-let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
+let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (old_abs_ids : AbstractionId.Set.t)
     (ctx : eval_ctx) : eval_ctx =
   let reorder_in_fresh_abs (abs : abs) : abs =
     (* Split between the loans and borrows *)
@@ -26,7 +27,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow abs.avalues in
 
@@ -39,13 +40,13 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
     let get_borrow_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     in
     let get_loan_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ALoan (AMutLoan (lid, _)) -> lid
       | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     in
     (* We use ordered maps to reorder the borrows and loans *)
     let reorder (get_bid : typed_avalue -> BorrowId.id)
@@ -128,7 +129,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
     This can happen when merging environments (note that such environments are not well-formed -
     they become well formed again after collapsing).
  *)
-let collapse_ctx (loop_id : LoopId.id)
+let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
     (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets)
     (ctx0 : eval_ctx) : eval_ctx =
   (* Debug *)
@@ -274,7 +275,7 @@ let collapse_ctx (loop_id : LoopId.id)
      ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string !ctx ^ "\n\n"));
 
   (* Reorder the loans and borrows in the fresh abstractions *)
-  let ctx = reorder_loans_borrows_in_fresh_abs old_ids.aids !ctx in
+  let ctx = reorder_loans_borrows_in_fresh_abs meta old_ids.aids !ctx in
 
   log#ldebug
     (lazy
@@ -285,7 +286,7 @@ let collapse_ctx (loop_id : LoopId.id)
   (* Return the new context *)
   ctx
 
-let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
+let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx)
     : merge_duplicates_funcs =
   (* Rem.: the merge functions raise exceptions (that we catch). *)
   let module S : MatchJoinState = struct
@@ -306,8 +307,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
   *)
   let merge_amut_borrows id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    assert (is_aignored child0.value);
-    assert (is_aignored child1.value);
+    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
+    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
 
     (* We need to pick a type for the avalue. The types on the left and on the
        right may use different regions: it doesn't really matter (here, we pick
@@ -325,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
       let _, ty1, _ = ty_as_ref ty1 in
-      assert (not (ty_has_borrows ctx.type_ctx.type_infos ty0));
-      assert (not (ty_has_borrows ctx.type_ctx.type_infos ty1))
+      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta "";
+      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta ""
     in
 
     (* Same remarks as for [merge_amut_borrows] *)
@@ -337,8 +338,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
 
   let merge_amut_loans id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    assert (is_aignored child0.value);
-    assert (is_aignored child1.value);
+    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
+    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
     (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let child = child0 in
@@ -348,15 +349,15 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
   let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1
       (sv1 : typed_value) child1 =
     (* Sanity checks *)
-    assert (is_aignored child0.value);
-    assert (is_aignored child1.value);
+    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
+    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
     (* Same remarks as for [merge_amut_borrows].
 
        This time we need to also merge the shared values. We rely on the
        join matcher [JM] to do so.
     *)
-    assert (not (value_has_loans_or_borrows ctx sv0.value));
-    assert (not (value_has_loans_or_borrows ctx sv1.value));
+    cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "";
+    cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta "";
     let ty = ty0 in
     let child = child0 in
     let sv = M.match_typed_values ctx ctx sv0 sv1 in
@@ -370,10 +371,10 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
     merge_ashared_loans;
   }
 
-let merge_into_abstraction (loop_id : LoopId.id) (abs_kind : abs_kind)
+let merge_into_abstraction (meta : Meta.meta) (loop_id : LoopId.id) (abs_kind : abs_kind)
     (can_end : bool) (ctx : eval_ctx) (aid0 : AbstractionId.id)
     (aid1 : AbstractionId.id) : eval_ctx * AbstractionId.id =
-  let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in
+  let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in
   merge_into_abstraction abs_kind can_end (Some merge_funs) ctx aid0 aid1
 
 (** Collapse an environment, merging the duplicated borrows/loans.
@@ -383,13 +384,13 @@ let merge_into_abstraction (loop_id : LoopId.id) (abs_kind : abs_kind)
     We do this because when we join environments, we may introduce duplicated
     loans and borrows. See the explanations for {!join_ctxs}.
  *)
-let collapse_ctx_with_merge (loop_id : LoopId.id) (old_ids : ids_sets)
+let collapse_ctx_with_merge (meta : Meta.meta) (loop_id : LoopId.id) (old_ids : ids_sets)
     (ctx : eval_ctx) : eval_ctx =
-  let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in
-  try collapse_ctx loop_id (Some merge_funs) old_ids ctx
-  with ValueMatchFailure _ -> raise (Failure "Unexpected")
+  let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in
+  try collapse_ctx meta loop_id (Some merge_funs) old_ids ctx
+  with ValueMatchFailure _ -> craise meta "Unexpected"
 
-let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
+let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     (ctx1 : eval_ctx) : ctx_or_update =
   (* Debug *)
   log#ldebug
@@ -422,14 +423,14 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
       match ee with
       | EBinding (BVar _, _) ->
           (* Variables are necessarily in the prefix *)
-          raise (Failure "Unreachable")
+          craise meta "Unreachable"
       | EBinding (BDummy did, _) ->
-          assert (not (DummyVarId.Set.mem did fixed_ids.dids))
+          cassert (not (DummyVarId.Set.mem did fixed_ids.dids)) meta ""
       | EAbs abs ->
-          assert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids))
+          cassert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta ""
       | EFrame ->
           (* This should have been eliminated *)
-          raise (Failure "Unreachable")
+          craise meta "Unreachable"
     in
     List.iter check_valid env0;
     List.iter check_valid env1;
@@ -465,7 +466,7 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
            are not in the prefix anymore *)
         if DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Still in the prefix: match the values *)
-          assert (b0 = b1);
+          cassert (b0 = b1) meta "Bindings are not the same. We are not in the prefix anymore";
           let b = b0 in
           let v = M.match_typed_values ctx0 ctx1 v0 v1 in
           let var = EBinding (BDummy b, v) in
@@ -487,7 +488,8 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
 
         (* Variable bindings *must* be in the prefix and consequently their
            ids must be the same *)
-        assert (b0 = b1);
+        cassert (b0 = b1) meta "Variable bindings *must* be in the prefix and consequently their
+        ids must be the same";
         (* Match the values *)
         let b = b0 in
         let v = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -505,7 +507,7 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
           (* Still in the prefix: the abstractions must be the same *)
-          assert (abs0 = abs1);
+          cassert (abs0 = abs1) meta "The abstractions are not the same";
           (* Continue *)
           abs :: join_prefixes env0' env1')
         else (* Not in the prefix anymore *)
@@ -520,7 +522,7 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     let env0, env1 =
       match (env0, env1) with
       | EFrame :: env0, EFrame :: env1 -> (env0, env1)
-      | _ -> raise (Failure "Unreachable")
+      | _ -> craise meta "Unreachable"
     in
 
     log#ldebug
@@ -634,7 +636,7 @@ let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   in
   { ctx with env }
 
-let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
+let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
     (fixed_ids : ids_sets) (old_ctx : eval_ctx) (ctxl : eval_ctx list) :
     (eval_ctx * eval_ctx list) * eval_ctx =
   (* # Join with the new contexts, one by one
@@ -647,7 +649,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
   *)
   let joined_ctx = ref old_ctx in
   let rec join_one_aux (ctx : eval_ctx) : eval_ctx =
-    match join_ctxs loop_id fixed_ids !joined_ctx ctx with
+    match join_ctxs meta loop_id fixed_ids !joined_ctx ctx with
     | Ok nctx ->
         joined_ctx := nctx;
         ctx
@@ -659,7 +661,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
           | LoansInRight bids ->
               InterpreterBorrows.end_borrows_no_synth config bids ctx
           | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
-              raise (Failure "Unexpected")
+              craise meta "Unexpected"
         in
         join_one_aux ctx
   in
@@ -677,7 +679,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
        ^ eval_ctx_to_string ctx));
 
     (* Collapse the context we want to add to the join *)
-    let ctx = collapse_ctx loop_id None fixed_ids ctx in
+    let ctx = collapse_ctx meta loop_id None fixed_ids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
@@ -696,14 +698,14 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
     (* Collapse again - the join might have introduce abstractions we want
        to merge with the others (note that those abstractions may actually
        lead to borrows/loans duplications) *)
-    joined_ctx := collapse_ctx_with_merge loop_id fixed_ids !joined_ctx;
+    joined_ctx := collapse_ctx_with_merge meta loop_id fixed_ids !joined_ctx;
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n"
         ^ eval_ctx_to_string !joined_ctx));
 
     (* Sanity check *)
-    if !Config.sanity_checks then Invariants.check_invariants !joined_ctx;
+    if !Config.sanity_checks then Invariants.check_invariants meta !joined_ctx;
     (* Return *)
     ctx1
   in
-- 
cgit v1.2.3


From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 21 Mar 2024 12:34:40 +0100
Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to
 do and we need to see how translate_crate can give meta to the functions it
 calls

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

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index fc2a97e5..ef4807e4 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -136,7 +136,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
-     ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n"));
+     ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string meta ctx0 ^ "\n\n"));
 
   let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in
   let can_end = true in
@@ -160,7 +160,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
            | EBinding (BDummy id, v) ->
                if is_fresh_did id then
                  let absl =
-                   convert_value_to_abstractions abs_kind can_end
+                   convert_value_to_abstractions meta abs_kind can_end
                      destructure_shared_values ctx0 v
                  in
                  List.map (fun abs -> EAbs abs) absl
@@ -171,19 +171,19 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx: after converting values to abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n"
+     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n"
       ));
 
   log#ldebug
     (lazy
       ("collapse_ctx: after decomposing the shared values in the abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n"
+     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n"
       ));
 
   (* Explore all the *new* abstractions, and compute various maps *)
   let explore (abs : abs) = is_fresh_abs_id abs.abs_id in
   let ids_maps =
-    compute_abs_borrows_loans_maps (merge_funs = None) explore env
+    compute_abs_borrows_loans_maps meta (merge_funs = None) explore env
   in
   let {
     abs_ids;
@@ -252,12 +252,12 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
                         ^ AbstractionId.to_string abs_id1
                         ^ " into "
                         ^ AbstractionId.to_string abs_id0
-                        ^ ":\n\n" ^ eval_ctx_to_string !ctx));
+                        ^ ":\n\n" ^ eval_ctx_to_string meta !ctx));
 
                     (* Update the environment - pay attention to the order: we
                        we merge [abs_id1] *into* [abs_id0] *)
                     let nctx, abs_id =
-                      merge_into_abstraction abs_kind can_end merge_funs !ctx
+                      merge_into_abstraction meta abs_kind can_end merge_funs !ctx
                         abs_id1 abs_id0
                     in
                     ctx := nctx;
@@ -272,7 +272,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
-     ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string !ctx ^ "\n\n"));
+     ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string meta !ctx ^ "\n\n"));
 
   (* Reorder the loans and borrows in the fresh abstractions *)
   let ctx = reorder_loans_borrows_in_fresh_abs meta old_ids.aids !ctx in
@@ -281,7 +281,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
      ^ "\n\n- after collapse and reorder borrows/loans:\n"
-     ^ eval_ctx_to_string ctx ^ "\n\n"));
+     ^ eval_ctx_to_string meta ctx ^ "\n\n"));
 
   (* Return the new context *)
   ctx
@@ -360,7 +360,7 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
     cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta "";
     let ty = ty0 in
     let child = child0 in
-    let sv = M.match_typed_values ctx ctx sv0 sv1 in
+    let sv = M.match_typed_values meta ctx ctx sv0 sv1 in
     let value = ALoan (ASharedLoan (ids, sv, child)) in
     { value; ty }
   in
@@ -375,7 +375,7 @@ let merge_into_abstraction (meta : Meta.meta) (loop_id : LoopId.id) (abs_kind :
     (can_end : bool) (ctx : eval_ctx) (aid0 : AbstractionId.id)
     (aid1 : AbstractionId.id) : eval_ctx * AbstractionId.id =
   let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in
-  merge_into_abstraction abs_kind can_end (Some merge_funs) ctx aid0 aid1
+  merge_into_abstraction meta abs_kind can_end (Some merge_funs) ctx aid0 aid1
 
 (** Collapse an environment, merging the duplicated borrows/loans.
 
@@ -397,9 +397,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
     (lazy
       ("join_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
      ^ "\n\n- ctx0:\n"
-      ^ eval_ctx_to_string_no_filter ctx0
+      ^ eval_ctx_to_string_no_filter meta ctx0
       ^ "\n\n- ctx1:\n"
-      ^ eval_ctx_to_string_no_filter ctx1
+      ^ eval_ctx_to_string_no_filter meta ctx1
       ^ "\n\n"));
 
   let env0 = List.rev ctx0.env in
@@ -413,9 +413,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
       (lazy
         ("join_suffixes:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
        ^ "\n\n- ctx0:\n"
-        ^ eval_ctx_to_string_no_filter { ctx0 with env = List.rev env0 }
+        ^ eval_ctx_to_string_no_filter meta { ctx0 with env = List.rev env0 }
         ^ "\n\n- ctx1:\n"
-        ^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 }
+        ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 }
         ^ "\n\n"));
 
     (* Sanity check: there are no values/abstractions which should be in the prefix *)
@@ -456,9 +456,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
           (lazy
             ("join_prefixes: BDummys:\n\n- fixed_ids:\n" ^ "\n"
            ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n"
-            ^ env_elem_to_string ctx0 var0
+            ^ env_elem_to_string meta ctx0 var0
             ^ "\n\n- value1:\n"
-            ^ env_elem_to_string ctx1 var1
+            ^ env_elem_to_string meta ctx1 var1
             ^ "\n\n"));
 
         (* Two cases: the dummy value is an old value, in which case the bindings
@@ -468,7 +468,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
           (* Still in the prefix: match the values *)
           cassert (b0 = b1) meta "Bindings are not the same. We are not in the prefix anymore";
           let b = b0 in
-          let v = M.match_typed_values ctx0 ctx1 v0 v1 in
+          let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in
           let var = EBinding (BDummy b, v) in
           (* Continue *)
           var :: join_prefixes env0' env1')
@@ -481,9 +481,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
           (lazy
             ("join_prefixes: BVars:\n\n- fixed_ids:\n" ^ "\n"
            ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n"
-            ^ env_elem_to_string ctx0 var0
+            ^ env_elem_to_string meta ctx0 var0
             ^ "\n\n- value1:\n"
-            ^ env_elem_to_string ctx1 var1
+            ^ env_elem_to_string meta ctx1 var1
             ^ "\n\n"));
 
         (* Variable bindings *must* be in the prefix and consequently their
@@ -492,7 +492,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
         ids must be the same";
         (* Match the values *)
         let b = b0 in
-        let v = M.match_typed_values ctx0 ctx1 v0 v1 in
+        let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in
         let var = EBinding (BVar b, v) in
         (* Continue *)
         var :: join_prefixes env0' env1'
@@ -501,8 +501,8 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
         log#ldebug
           (lazy
             ("join_prefixes: Abs:\n\n- fixed_ids:\n" ^ "\n"
-           ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n" ^ abs_to_string ctx0 abs0
-           ^ "\n\n- abs1:\n" ^ abs_to_string ctx1 abs1 ^ "\n\n"));
+           ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n" ^ abs_to_string meta ctx0 abs0
+           ^ "\n\n- abs1:\n" ^ abs_to_string meta ctx1 abs1 ^ "\n\n"));
 
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
@@ -584,7 +584,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
   with ValueMatchFailure e -> Error e
 
 (** Destructure all the new abstractions *)
-let destructure_new_abs (loop_id : LoopId.id)
+let destructure_new_abs (meta : Meta.meta) (loop_id : LoopId.id)
     (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in
   let can_end = true in
@@ -597,7 +597,7 @@ let destructure_new_abs (loop_id : LoopId.id)
       (fun abs ->
         if is_fresh_abs_id abs.abs_id then
           let abs =
-            destructure_abs abs_kind can_end destructure_shared_values ctx abs
+            destructure_abs meta abs_kind can_end destructure_shared_values ctx abs
           in
           abs
         else abs)
@@ -657,9 +657,9 @@ let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (lo
         let ctx =
           match err with
           | LoanInRight bid ->
-              InterpreterBorrows.end_borrow_no_synth config bid ctx
+              InterpreterBorrows.end_borrow_no_synth meta config bid ctx
           | LoansInRight bids ->
-              InterpreterBorrows.end_borrows_no_synth config bids ctx
+              InterpreterBorrows.end_borrows_no_synth meta config bids ctx
           | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
               craise meta "Unexpected"
         in
@@ -669,21 +669,21 @@ let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
-       ^ eval_ctx_to_string ctx));
+       ^ eval_ctx_to_string meta ctx));
 
     (* Destructure the abstractions introduced in the new context *)
-    let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in
+    let ctx = destructure_new_abs meta loop_id fixed_ids.aids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n"
-       ^ eval_ctx_to_string ctx));
+       ^ eval_ctx_to_string meta ctx));
 
     (* Collapse the context we want to add to the join *)
     let ctx = collapse_ctx meta loop_id None fixed_ids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
-       ^ eval_ctx_to_string ctx));
+       ^ eval_ctx_to_string meta ctx));
 
     (* Refresh the fresh abstractions *)
     let ctx = refresh_abs fixed_ids.aids ctx in
@@ -693,7 +693,7 @@ let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after join:\n"
-       ^ eval_ctx_to_string ctx1));
+       ^ eval_ctx_to_string meta ctx1));
 
     (* Collapse again - the join might have introduce abstractions we want
        to merge with the others (note that those abstractions may actually
@@ -702,7 +702,7 @@ let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n"
-        ^ eval_ctx_to_string !joined_ctx));
+        ^ eval_ctx_to_string meta !joined_ctx));
 
     (* Sanity check *)
     if !Config.sanity_checks then Invariants.check_invariants meta !joined_ctx;
-- 
cgit v1.2.3


From 9b1a0d82c19375619904efe7e18e064701fb947b Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Mon, 25 Mar 2024 10:16:15 +0100
Subject: Replaced some unclear TODOs error message placeholder by clearer
 TODOs, they were forgotten before last push

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

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index ef4807e4..b8d5094b 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -326,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
       let _, ty1, _ = ty_as_ref ty1 in
-      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta "";
-      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta ""
+      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta "TODO: error message";
+      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta "TODO: error message"
     in
 
     (* Same remarks as for [merge_amut_borrows] *)
@@ -356,8 +356,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
        This time we need to also merge the shared values. We rely on the
        join matcher [JM] to do so.
     *)
-    cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "";
-    cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta "";
+    cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
+    cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta "TODO: error message";
     let ty = ty0 in
     let child = child0 in
     let sv = M.match_typed_values meta ctx ctx sv0 sv1 in
@@ -425,9 +425,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
           (* Variables are necessarily in the prefix *)
           craise meta "Unreachable"
       | EBinding (BDummy did, _) ->
-          cassert (not (DummyVarId.Set.mem did fixed_ids.dids)) meta ""
+          cassert (not (DummyVarId.Set.mem did fixed_ids.dids)) meta "TODO: error message"
       | EAbs abs ->
-          cassert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta ""
+          cassert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta "TODO: error message"
       | EFrame ->
           (* This should have been eliminated *)
           craise meta "Unreachable"
-- 
cgit v1.2.3


From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Mon, 25 Mar 2024 12:06:05 +0100
Subject: Inverted meta and config argument orders (from meta -> config to
 config -> meta)

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

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index b8d5094b..c4709b7e 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -636,7 +636,7 @@ let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   in
   { ctx with env }
 
-let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
+let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
     (fixed_ids : ids_sets) (old_ctx : eval_ctx) (ctxl : eval_ctx list) :
     (eval_ctx * eval_ctx list) * eval_ctx =
   (* # Join with the new contexts, one by one
@@ -657,9 +657,9 @@ let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (lo
         let ctx =
           match err with
           | LoanInRight bid ->
-              InterpreterBorrows.end_borrow_no_synth meta config bid ctx
+              InterpreterBorrows.end_borrow_no_synth config meta bid ctx
           | LoansInRight bids ->
-              InterpreterBorrows.end_borrows_no_synth meta config bids ctx
+              InterpreterBorrows.end_borrows_no_synth config meta bids ctx
           | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
               craise meta "Unexpected"
         in
-- 
cgit v1.2.3


From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 27 Mar 2024 10:22:06 +0100
Subject: Added sanity_check and sanity_check_opt_meta helpers and changed
 sanity checks related cassert to these helpers to have a proper error message

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

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index c4709b7e..74d31975 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -307,8 +307,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
   *)
   let merge_amut_borrows id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
-    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
+    sanity_check (is_aignored child0.value) meta;
+    sanity_check (is_aignored child1.value) meta;
 
     (* We need to pick a type for the avalue. The types on the left and on the
        right may use different regions: it doesn't really matter (here, we pick
@@ -326,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
       let _, ty1, _ = ty_as_ref ty1 in
-      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta "TODO: error message";
-      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta "TODO: error message"
+      sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta;
+      sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta
     in
 
     (* Same remarks as for [merge_amut_borrows] *)
@@ -338,8 +338,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
 
   let merge_amut_loans id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
-    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
+    sanity_check (is_aignored child0.value) meta;
+    sanity_check (is_aignored child1.value) meta;
     (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let child = child0 in
@@ -349,8 +349,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
   let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1
       (sv1 : typed_value) child1 =
     (* Sanity checks *)
-    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
-    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
+    sanity_check (is_aignored child0.value) meta;
+    sanity_check (is_aignored child1.value) meta;
     (* Same remarks as for [merge_amut_borrows].
 
        This time we need to also merge the shared values. We rely on the
@@ -425,9 +425,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
           (* Variables are necessarily in the prefix *)
           craise meta "Unreachable"
       | EBinding (BDummy did, _) ->
-          cassert (not (DummyVarId.Set.mem did fixed_ids.dids)) meta "TODO: error message"
+          sanity_check (not (DummyVarId.Set.mem did fixed_ids.dids)) meta
       | EAbs abs ->
-          cassert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta "TODO: error message"
+          sanity_check (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta
       | EFrame ->
           (* This should have been eliminated *)
           craise meta "Unreachable"
-- 
cgit v1.2.3


From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 13:56:31 +0100
Subject: Should answer all comments, there are still some TODO: error message
 left

---
 compiler/InterpreterLoopsJoinCtxs.ml | 42 +++++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 20 deletions(-)

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 74d31975..8153ef08 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -136,7 +136,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
-     ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string meta ctx0 ^ "\n\n"));
+     ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n"));
 
   let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in
   let can_end = true in
@@ -171,13 +171,13 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx: after converting values to abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n"
+     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"
       ));
 
   log#ldebug
     (lazy
       ("collapse_ctx: after decomposing the shared values in the abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n"
+     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"
       ));
 
   (* Explore all the *new* abstractions, and compute various maps *)
@@ -252,7 +252,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
                         ^ AbstractionId.to_string abs_id1
                         ^ " into "
                         ^ AbstractionId.to_string abs_id0
-                        ^ ":\n\n" ^ eval_ctx_to_string meta !ctx));
+                        ^ ":\n\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx));
 
                     (* Update the environment - pay attention to the order: we
                        we merge [abs_id1] *into* [abs_id0] *)
@@ -272,7 +272,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
-     ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string meta !ctx ^ "\n\n"));
+     ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx ^ "\n\n"));
 
   (* Reorder the loans and borrows in the fresh abstractions *)
   let ctx = reorder_loans_borrows_in_fresh_abs meta old_ids.aids !ctx in
@@ -281,7 +281,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
      ^ "\n\n- after collapse and reorder borrows/loans:\n"
-     ^ eval_ctx_to_string meta ctx ^ "\n\n"));
+     ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"));
 
   (* Return the new context *)
   ctx
@@ -290,6 +290,7 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
     : merge_duplicates_funcs =
   (* Rem.: the merge functions raise exceptions (that we catch). *)
   let module S : MatchJoinState = struct
+    let meta = meta
     let loop_id = loop_id
     let nabs = ref []
   end in
@@ -356,11 +357,11 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
        This time we need to also merge the shared values. We rely on the
        join matcher [JM] to do so.
     *)
-    cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
-    cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta "TODO: error message";
+    sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+    sanity_check (not (value_has_loans_or_borrows ctx sv1.value)) meta;
     let ty = ty0 in
     let child = child0 in
-    let sv = M.match_typed_values meta ctx ctx sv0 sv1 in
+    let sv = M.match_typed_values ctx ctx sv0 sv1 in
     let value = ALoan (ASharedLoan (ids, sv, child)) in
     { value; ty }
   in
@@ -397,9 +398,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
     (lazy
       ("join_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
      ^ "\n\n- ctx0:\n"
-      ^ eval_ctx_to_string_no_filter meta ctx0
+      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0
       ^ "\n\n- ctx1:\n"
-      ^ eval_ctx_to_string_no_filter meta ctx1
+      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1
       ^ "\n\n"));
 
   let env0 = List.rev ctx0.env in
@@ -413,9 +414,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
       (lazy
         ("join_suffixes:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
        ^ "\n\n- ctx0:\n"
-        ^ eval_ctx_to_string_no_filter meta { ctx0 with env = List.rev env0 }
+        ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx0 with env = List.rev env0 }
         ^ "\n\n- ctx1:\n"
-        ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 }
+        ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 }
         ^ "\n\n"));
 
     (* Sanity check: there are no values/abstractions which should be in the prefix *)
@@ -441,6 +442,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
   in
 
   let module S : MatchJoinState = struct
+    let meta = meta
     let loop_id = loop_id
     let nabs = nabs
   end in
@@ -468,7 +470,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
           (* Still in the prefix: match the values *)
           cassert (b0 = b1) meta "Bindings are not the same. We are not in the prefix anymore";
           let b = b0 in
-          let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in
+          let v = M.match_typed_values ctx0 ctx1 v0 v1 in
           let var = EBinding (BDummy b, v) in
           (* Continue *)
           var :: join_prefixes env0' env1')
@@ -492,7 +494,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
         ids must be the same";
         (* Match the values *)
         let b = b0 in
-        let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in
+        let v = M.match_typed_values ctx0 ctx1 v0 v1 in
         let var = EBinding (BVar b, v) in
         (* Continue *)
         var :: join_prefixes env0' env1'
@@ -669,21 +671,21 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
-       ^ eval_ctx_to_string meta ctx));
+       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
     (* Destructure the abstractions introduced in the new context *)
     let ctx = destructure_new_abs meta loop_id fixed_ids.aids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n"
-       ^ eval_ctx_to_string meta ctx));
+       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
     (* Collapse the context we want to add to the join *)
     let ctx = collapse_ctx meta loop_id None fixed_ids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
-       ^ eval_ctx_to_string meta ctx));
+       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
     (* Refresh the fresh abstractions *)
     let ctx = refresh_abs fixed_ids.aids ctx in
@@ -693,7 +695,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after join:\n"
-       ^ eval_ctx_to_string meta ctx1));
+       ^ eval_ctx_to_string ~meta:(Some meta) ctx1));
 
     (* Collapse again - the join might have introduce abstractions we want
        to merge with the others (note that those abstractions may actually
@@ -702,7 +704,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n"
-        ^ eval_ctx_to_string meta !joined_ctx));
+        ^ eval_ctx_to_string ~meta:(Some meta) !joined_ctx));
 
     (* Sanity check *)
     if !Config.sanity_checks then Invariants.check_invariants meta !joined_ctx;
-- 
cgit v1.2.3


From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 17:14:27 +0100
Subject: formatting

---
 compiler/InterpreterLoopsJoinCtxs.ml | 93 ++++++++++++++++++++++--------------
 1 file changed, 56 insertions(+), 37 deletions(-)

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 8153ef08..020e812a 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -19,8 +19,8 @@ let log = Logging.loops_join_ctxs_log
     called typically after we merge abstractions together (see {!collapse_ctx}
     for instance).
  *)
-let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (old_abs_ids : AbstractionId.Set.t)
-    (ctx : eval_ctx) : eval_ctx =
+let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
+    (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   let reorder_in_fresh_abs (abs : abs) : abs =
     (* Split between the loans and borrows *)
     let is_borrow (av : typed_avalue) : bool =
@@ -136,7 +136,9 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
-     ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n"));
+     ^ "\n\n- ctx0:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+      ^ "\n\n"));
 
   let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in
   let can_end = true in
@@ -171,14 +173,16 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx: after converting values to abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"
-      ));
+     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ "\n\n"));
 
   log#ldebug
     (lazy
       ("collapse_ctx: after decomposing the shared values in the abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"
-      ));
+     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ "\n\n"));
 
   (* Explore all the *new* abstractions, and compute various maps *)
   let explore (abs : abs) = is_fresh_abs_id abs.abs_id in
@@ -252,13 +256,14 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
                         ^ AbstractionId.to_string abs_id1
                         ^ " into "
                         ^ AbstractionId.to_string abs_id0
-                        ^ ":\n\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx));
+                        ^ ":\n\n"
+                        ^ eval_ctx_to_string ~meta:(Some meta) !ctx));
 
                     (* Update the environment - pay attention to the order: we
                        we merge [abs_id1] *into* [abs_id0] *)
                     let nctx, abs_id =
-                      merge_into_abstraction meta abs_kind can_end merge_funs !ctx
-                        abs_id1 abs_id0
+                      merge_into_abstraction meta abs_kind can_end merge_funs
+                        !ctx abs_id1 abs_id0
                     in
                     ctx := nctx;
 
@@ -272,7 +277,9 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
-     ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx ^ "\n\n"));
+     ^ "\n\n- after collapse:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) !ctx
+      ^ "\n\n"));
 
   (* Reorder the loans and borrows in the fresh abstractions *)
   let ctx = reorder_loans_borrows_in_fresh_abs meta old_ids.aids !ctx in
@@ -281,13 +288,14 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
      ^ "\n\n- after collapse and reorder borrows/loans:\n"
-     ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"));
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ "\n\n"));
 
   (* Return the new context *)
   ctx
 
-let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx)
-    : merge_duplicates_funcs =
+let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta)
+    (loop_id : LoopId.id) (ctx : eval_ctx) : merge_duplicates_funcs =
   (* Rem.: the merge functions raise exceptions (that we catch). *)
   let module S : MatchJoinState = struct
     let meta = meta
@@ -372,9 +380,10 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
     merge_ashared_loans;
   }
 
-let merge_into_abstraction (meta : Meta.meta) (loop_id : LoopId.id) (abs_kind : abs_kind)
-    (can_end : bool) (ctx : eval_ctx) (aid0 : AbstractionId.id)
-    (aid1 : AbstractionId.id) : eval_ctx * AbstractionId.id =
+let merge_into_abstraction (meta : Meta.meta) (loop_id : LoopId.id)
+    (abs_kind : abs_kind) (can_end : bool) (ctx : eval_ctx)
+    (aid0 : AbstractionId.id) (aid1 : AbstractionId.id) :
+    eval_ctx * AbstractionId.id =
   let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in
   merge_into_abstraction meta abs_kind can_end (Some merge_funs) ctx aid0 aid1
 
@@ -385,14 +394,14 @@ let merge_into_abstraction (meta : Meta.meta) (loop_id : LoopId.id) (abs_kind :
     We do this because when we join environments, we may introduce duplicated
     loans and borrows. See the explanations for {!join_ctxs}.
  *)
-let collapse_ctx_with_merge (meta : Meta.meta) (loop_id : LoopId.id) (old_ids : ids_sets)
-    (ctx : eval_ctx) : eval_ctx =
+let collapse_ctx_with_merge (meta : Meta.meta) (loop_id : LoopId.id)
+    (old_ids : ids_sets) (ctx : eval_ctx) : eval_ctx =
   let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in
   try collapse_ctx meta loop_id (Some merge_funs) old_ids ctx
   with ValueMatchFailure _ -> craise meta "Unexpected"
 
-let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
-    (ctx1 : eval_ctx) : ctx_or_update =
+let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
+    (ctx0 : eval_ctx) (ctx1 : eval_ctx) : ctx_or_update =
   (* Debug *)
   log#ldebug
     (lazy
@@ -414,9 +423,11 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
       (lazy
         ("join_suffixes:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
        ^ "\n\n- ctx0:\n"
-        ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx0 with env = List.rev env0 }
+        ^ eval_ctx_to_string_no_filter ~meta:(Some meta)
+            { ctx0 with env = List.rev env0 }
         ^ "\n\n- ctx1:\n"
-        ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 }
+        ^ eval_ctx_to_string_no_filter ~meta:(Some meta)
+            { ctx1 with env = List.rev env1 }
         ^ "\n\n"));
 
     (* Sanity check: there are no values/abstractions which should be in the prefix *)
@@ -428,7 +439,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
       | EBinding (BDummy did, _) ->
           sanity_check (not (DummyVarId.Set.mem did fixed_ids.dids)) meta
       | EAbs abs ->
-          sanity_check (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta
+          sanity_check
+            (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids))
+            meta
       | EFrame ->
           (* This should have been eliminated *)
           craise meta "Unreachable"
@@ -468,7 +481,8 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
            are not in the prefix anymore *)
         if DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Still in the prefix: match the values *)
-          cassert (b0 = b1) meta "Bindings are not the same. We are not in the prefix anymore";
+          cassert (b0 = b1) meta
+            "Bindings are not the same. We are not in the prefix anymore";
           let b = b0 in
           let v = M.match_typed_values ctx0 ctx1 v0 v1 in
           let var = EBinding (BDummy b, v) in
@@ -490,8 +504,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
 
         (* Variable bindings *must* be in the prefix and consequently their
            ids must be the same *)
-        cassert (b0 = b1) meta "Variable bindings *must* be in the prefix and consequently their
-        ids must be the same";
+        cassert (b0 = b1) meta
+          "Variable bindings *must* be in the prefix and consequently their\n\
+          \        ids must be the same";
         (* Match the values *)
         let b = b0 in
         let v = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -503,8 +518,11 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
         log#ldebug
           (lazy
             ("join_prefixes: Abs:\n\n- fixed_ids:\n" ^ "\n"
-           ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n" ^ abs_to_string meta ctx0 abs0
-           ^ "\n\n- abs1:\n" ^ abs_to_string meta ctx1 abs1 ^ "\n\n"));
+           ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n"
+            ^ abs_to_string meta ctx0 abs0
+            ^ "\n\n- abs1:\n"
+            ^ abs_to_string meta ctx1 abs1
+            ^ "\n\n"));
 
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
@@ -599,7 +617,8 @@ let destructure_new_abs (meta : Meta.meta) (loop_id : LoopId.id)
       (fun abs ->
         if is_fresh_abs_id abs.abs_id then
           let abs =
-            destructure_abs meta abs_kind can_end destructure_shared_values ctx abs
+            destructure_abs meta abs_kind can_end destructure_shared_values ctx
+              abs
           in
           abs
         else abs)
@@ -638,9 +657,9 @@ let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   in
   { ctx with env }
 
-let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
-    (fixed_ids : ids_sets) (old_ctx : eval_ctx) (ctxl : eval_ctx list) :
-    (eval_ctx * eval_ctx list) * eval_ctx =
+let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta)
+    (loop_id : LoopId.id) (fixed_ids : ids_sets) (old_ctx : eval_ctx)
+    (ctxl : eval_ctx list) : (eval_ctx * eval_ctx list) * eval_ctx =
   (* # Join with the new contexts, one by one
 
      For every context, we repeteadly attempt to join it with the current
@@ -671,21 +690,21 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
-       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+        ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
     (* Destructure the abstractions introduced in the new context *)
     let ctx = destructure_new_abs meta loop_id fixed_ids.aids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n"
-       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+        ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
     (* Collapse the context we want to add to the join *)
     let ctx = collapse_ctx meta loop_id None fixed_ids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
-       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+        ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
     (* Refresh the fresh abstractions *)
     let ctx = refresh_abs fixed_ids.aids ctx in
@@ -695,7 +714,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after join:\n"
-       ^ eval_ctx_to_string ~meta:(Some meta) ctx1));
+        ^ eval_ctx_to_string ~meta:(Some meta) ctx1));
 
     (* Collapse again - the join might have introduce abstractions we want
        to merge with the others (note that those abstractions may actually
-- 
cgit v1.2.3


From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

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

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 020e812a..3b1767e8 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -27,7 +27,7 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow abs.avalues in
 
@@ -40,13 +40,13 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
     let get_borrow_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     in
     let get_loan_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ALoan (AMutLoan (lid, _)) -> lid
       | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     in
     (* We use ordered maps to reorder the borrows and loans *)
     let reorder (get_bid : typed_avalue -> BorrowId.id)
@@ -316,8 +316,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta)
   *)
   let merge_amut_borrows id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    sanity_check (is_aignored child0.value) meta;
-    sanity_check (is_aignored child1.value) meta;
+    sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta;
+    sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta;
 
     (* We need to pick a type for the avalue. The types on the left and on the
        right may use different regions: it doesn't really matter (here, we pick
@@ -335,8 +335,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta)
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
       let _, ty1, _ = ty_as_ref ty1 in
-      sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta;
-      sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta
+      sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta;
+      sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta
     in
 
     (* Same remarks as for [merge_amut_borrows] *)
@@ -347,8 +347,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta)
 
   let merge_amut_loans id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    sanity_check (is_aignored child0.value) meta;
-    sanity_check (is_aignored child1.value) meta;
+    sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta;
+    sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta;
     (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let child = child0 in
@@ -358,15 +358,15 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta)
   let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1
       (sv1 : typed_value) child1 =
     (* Sanity checks *)
-    sanity_check (is_aignored child0.value) meta;
-    sanity_check (is_aignored child1.value) meta;
+    sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta;
+    sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta;
     (* Same remarks as for [merge_amut_borrows].
 
        This time we need to also merge the shared values. We rely on the
        join matcher [JM] to do so.
     *)
-    sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
-    sanity_check (not (value_has_loans_or_borrows ctx sv1.value)) meta;
+    sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+    sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv1.value)) meta;
     let ty = ty0 in
     let child = child0 in
     let sv = M.match_typed_values ctx ctx sv0 sv1 in
@@ -398,7 +398,7 @@ let collapse_ctx_with_merge (meta : Meta.meta) (loop_id : LoopId.id)
     (old_ids : ids_sets) (ctx : eval_ctx) : eval_ctx =
   let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in
   try collapse_ctx meta loop_id (Some merge_funs) old_ids ctx
-  with ValueMatchFailure _ -> craise meta "Unexpected"
+  with ValueMatchFailure _ -> craise __FILE__ __LINE__ meta "Unexpected"
 
 let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
     (ctx0 : eval_ctx) (ctx1 : eval_ctx) : ctx_or_update =
@@ -435,16 +435,16 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
       match ee with
       | EBinding (BVar _, _) ->
           (* Variables are necessarily in the prefix *)
-          craise meta "Unreachable"
+          craise __FILE__ __LINE__ meta "Unreachable"
       | EBinding (BDummy did, _) ->
-          sanity_check (not (DummyVarId.Set.mem did fixed_ids.dids)) meta
+          sanity_check __FILE__ __LINE__ (not (DummyVarId.Set.mem did fixed_ids.dids)) meta
       | EAbs abs ->
-          sanity_check
+          sanity_check __FILE__ __LINE__
             (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids))
             meta
       | EFrame ->
           (* This should have been eliminated *)
-          craise meta "Unreachable"
+          craise __FILE__ __LINE__ meta "Unreachable"
     in
     List.iter check_valid env0;
     List.iter check_valid env1;
@@ -481,7 +481,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
            are not in the prefix anymore *)
         if DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Still in the prefix: match the values *)
-          cassert (b0 = b1) meta
+          cassert __FILE__ __LINE__ (b0 = b1) meta
             "Bindings are not the same. We are not in the prefix anymore";
           let b = b0 in
           let v = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -504,7 +504,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
 
         (* Variable bindings *must* be in the prefix and consequently their
            ids must be the same *)
-        cassert (b0 = b1) meta
+        cassert __FILE__ __LINE__ (b0 = b1) meta
           "Variable bindings *must* be in the prefix and consequently their\n\
           \        ids must be the same";
         (* Match the values *)
@@ -527,7 +527,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
           (* Still in the prefix: the abstractions must be the same *)
-          cassert (abs0 = abs1) meta "The abstractions are not the same";
+          cassert __FILE__ __LINE__ (abs0 = abs1) meta "The abstractions are not the same";
           (* Continue *)
           abs :: join_prefixes env0' env1')
         else (* Not in the prefix anymore *)
@@ -542,7 +542,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
     let env0, env1 =
       match (env0, env1) with
       | EFrame :: env0, EFrame :: env1 -> (env0, env1)
-      | _ -> craise meta "Unreachable"
+      | _ -> craise __FILE__ __LINE__ meta "Unreachable"
     in
 
     log#ldebug
@@ -682,7 +682,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta)
           | LoansInRight bids ->
               InterpreterBorrows.end_borrows_no_synth config meta bids ctx
           | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
-              craise meta "Unexpected"
+              craise __FILE__ __LINE__ meta "Unexpected"
         in
         join_one_aux ctx
   in
-- 
cgit v1.2.3


From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 14:07:36 +0100
Subject: formatting and changed save_error condition for failing from b to not
 b

---
 compiler/InterpreterLoopsJoinCtxs.ml | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 3b1767e8..d97b05d0 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -335,8 +335,12 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta)
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
       let _, ty1, _ = ty_as_ref ty1 in
-      sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta;
-      sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta
+      sanity_check __FILE__ __LINE__
+        (not (ty_has_borrows ctx.type_ctx.type_infos ty0))
+        meta;
+      sanity_check __FILE__ __LINE__
+        (not (ty_has_borrows ctx.type_ctx.type_infos ty1))
+        meta
     in
 
     (* Same remarks as for [merge_amut_borrows] *)
@@ -365,8 +369,12 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta)
        This time we need to also merge the shared values. We rely on the
        join matcher [JM] to do so.
     *)
-    sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta;
-    sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv1.value)) meta;
+    sanity_check __FILE__ __LINE__
+      (not (value_has_loans_or_borrows ctx sv0.value))
+      meta;
+    sanity_check __FILE__ __LINE__
+      (not (value_has_loans_or_borrows ctx sv1.value))
+      meta;
     let ty = ty0 in
     let child = child0 in
     let sv = M.match_typed_values ctx ctx sv0 sv1 in
@@ -437,7 +445,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
           (* Variables are necessarily in the prefix *)
           craise __FILE__ __LINE__ meta "Unreachable"
       | EBinding (BDummy did, _) ->
-          sanity_check __FILE__ __LINE__ (not (DummyVarId.Set.mem did fixed_ids.dids)) meta
+          sanity_check __FILE__ __LINE__
+            (not (DummyVarId.Set.mem did fixed_ids.dids))
+            meta
       | EAbs abs ->
           sanity_check __FILE__ __LINE__
             (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids))
@@ -527,7 +537,8 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
           (* Still in the prefix: the abstractions must be the same *)
-          cassert __FILE__ __LINE__ (abs0 = abs1) meta "The abstractions are not the same";
+          cassert __FILE__ __LINE__ (abs0 = abs1) meta
+            "The abstractions are not the same";
           (* Continue *)
           abs :: join_prefixes env0' env1')
         else (* Not in the prefix anymore *)
-- 
cgit v1.2.3


From 1a86cac476c1f5c0d64d5a12db267d3ac651561b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 29 Mar 2024 17:49:46 +0100
Subject: Cleanup and fix a mistake

---
 compiler/InterpreterLoopsJoinCtxs.ml | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'compiler/InterpreterLoopsJoinCtxs.ml')

diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index d97b05d0..de00cb93 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -491,8 +491,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
            are not in the prefix anymore *)
         if DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Still in the prefix: match the values *)
-          cassert __FILE__ __LINE__ (b0 = b1) meta
-            "Bindings are not the same. We are not in the prefix anymore";
+          sanity_check __FILE__ __LINE__ (b0 = b1) meta;
           let b = b0 in
           let v = M.match_typed_values ctx0 ctx1 v0 v1 in
           let var = EBinding (BDummy b, v) in
@@ -514,9 +513,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
 
         (* Variable bindings *must* be in the prefix and consequently their
            ids must be the same *)
-        cassert __FILE__ __LINE__ (b0 = b1) meta
-          "Variable bindings *must* be in the prefix and consequently their\n\
-          \        ids must be the same";
+        sanity_check __FILE__ __LINE__ (b0 = b1) meta;
         (* Match the values *)
         let b = b0 in
         let v = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -537,8 +534,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
           (* Still in the prefix: the abstractions must be the same *)
-          cassert __FILE__ __LINE__ (abs0 = abs1) meta
-            "The abstractions are not the same";
+          sanity_check __FILE__ __LINE__ (abs0 = abs1) meta;
           (* Continue *)
           abs :: join_prefixes env0' env1')
         else (* Not in the prefix anymore *)
-- 
cgit v1.2.3