Add type and set/map for marker and borrow id

4 files changed, 22 insertions, 10 deletions

diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 675dc544..9aee361d 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -26,6 +26,20 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result
 (** Union Find *)
 module UF = UnionFind.Make (UnionFind.StoreMap)
 
+type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord]
+
+module MarkerBorrowIdOrd = struct
+  type t = marker_borrow_id
+
+  let compare = compare_marker_borrow_id
+  let to_string = show_marker_borrow_id
+  let pp_t = pp_marker_borrow_id
+  let show_t = show_marker_borrow_id
+end
+
+module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd)
+module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd)
+
 (** A small utility -
 
     Rem.: some environments may be ill-formed (they may contain several times
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 81e5004f..5c3ce66d 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -280,8 +280,8 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets)
 
 (* TODO Adapt and comment *)
 let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
-    (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets)
-    (ctx0 : eval_ctx) : eval_ctx =
+    (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx)
+    : eval_ctx =
   (* Debug *)
   log#ldebug
     (lazy
@@ -336,9 +336,7 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
 
   (* 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 span false explore env
-  in
+  let ids_maps = compute_abs_borrows_loans_maps span false explore env in
   let {
     abs_ids;
     abs_to_borrows;
@@ -353,7 +351,7 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
 
   (* Change the merging behaviour depending on the input parameters *)
   let abs_to_borrows, loan_to_abs =
- (abs_to_borrows_loans, borrow_loan_to_abs)
+    (abs_to_borrows_loans, borrow_loan_to_abs)
   in
 
   (* Merge the abstractions together *)
@@ -411,8 +409,8 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
                     (* Update the environment - pay attention to the order: we
                        we merge [abs_id1] *into* [abs_id0] *)
                     let nctx, abs_id =
-                      merge_into_abstraction span abs_kind can_end (Some merge_funs)
-                        !ctx abs_id1 abs_id0
+                      merge_into_abstraction span abs_kind can_end
+                        (Some merge_funs) !ctx abs_id1 abs_id0
                     in
                     ctx := nctx;
 
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 729b248f..9fe4638d 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -32,7 +32,7 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
 
   let module R (Id0 : Identifiers.Id) (Id1 : Identifiers.Id) = struct
     (*
-       [check_singleton_sets]: check that the mapping maps to a singletong.
+       [check_singleton_sets]: check that the mapping maps to a singleton.
        [check_not_already_registered]: check if the mapping was not already registered.
     *)
     let register_mapping (check_singleton_sets : bool)
diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam
index b57cc9f6..1539c521 100644
--- a/tests/test_runner/aeneas_test_runner.opam
+++ b/tests/test_runner/aeneas_test_runner.opam
@@ -7,7 +7,7 @@ homepage: "https://github.com/AeneasVerif/aeneas"
 bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
 depends: [
   "ocaml"
-  "dune" {>= "3.12"}
+  "dune" {>= "3.7"}
   "odoc" {with-doc}
 ]
 build: [