diff options
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 2 | ||||
| -rw-r--r-- | tests/test_runner/aeneas_test_runner.opam | 2 |
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: [ |