Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

1 files changed, 18 insertions, 13 deletions

diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index e47ba82d..30b75790 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -8,37 +8,40 @@ open Cps
     applies this change to an environment [ctx] by inserting a new borrow id in
     the set of borrows tracked by a shared value, referenced by the
     [original_bid] argument.  *)
-val reborrow_shared : BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx
+val reborrow_shared :
+  Meta.meta -> BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx
 
 (** End a borrow identified by its id, while preserving the invariants.
 
     If the borrow is inside another borrow/an abstraction or contains loans,
     [end_borrow] will end those borrows/abstractions/loans first.
   *)
-val end_borrow : config -> BorrowId.id -> cm_fun
+val end_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun
 
 (** End a set of borrows identified by their ids, while preserving the invariants. *)
-val end_borrows : config -> BorrowId.Set.t -> cm_fun
+val end_borrows : config -> Meta.meta -> BorrowId.Set.t -> cm_fun
 
 (** End an abstraction while preserving the invariants. *)
-val end_abstraction : config -> AbstractionId.id -> cm_fun
+val end_abstraction : config -> Meta.meta -> AbstractionId.id -> cm_fun
 
 (** End a set of abstractions while preserving the invariants. *)
-val end_abstractions : config -> AbstractionId.Set.t -> cm_fun
+val end_abstractions : config -> Meta.meta -> AbstractionId.Set.t -> cm_fun
 
 (** End a borrow and return the resulting environment, ignoring synthesis *)
-val end_borrow_no_synth : config -> BorrowId.id -> eval_ctx -> eval_ctx
+val end_borrow_no_synth :
+  config -> Meta.meta -> BorrowId.id -> eval_ctx -> eval_ctx
 
 (** End a set of borrows and return the resulting environment, ignoring synthesis *)
-val end_borrows_no_synth : config -> BorrowId.Set.t -> eval_ctx -> eval_ctx
+val end_borrows_no_synth :
+  config -> Meta.meta -> BorrowId.Set.t -> eval_ctx -> eval_ctx
 
 (** End an abstraction and return the resulting environment, ignoring synthesis *)
 val end_abstraction_no_synth :
-  config -> AbstractionId.id -> eval_ctx -> eval_ctx
+  config -> Meta.meta -> AbstractionId.id -> eval_ctx -> eval_ctx
 
 (** End a set of abstractions and return the resulting environment, ignoring synthesis *)
 val end_abstractions_no_synth :
-  config -> AbstractionId.Set.t -> eval_ctx -> eval_ctx
+  config -> Meta.meta -> AbstractionId.Set.t -> eval_ctx -> eval_ctx
 
 (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants.
 
@@ -49,7 +52,7 @@ val end_abstractions_no_synth :
     the corresponding shared loan with a mutable loan (after having ended the
     other shared borrows which point to this loan).
  *)
-val promote_reserved_mut_borrow : config -> BorrowId.id -> cm_fun
+val promote_reserved_mut_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun
 
 (** Transform an abstraction to an abstraction where the values are not
     structured.
@@ -91,7 +94,8 @@ val promote_reserved_mut_borrow : config -> BorrowId.id -> cm_fun
     - [ctx]
     - [abs]
  *)
-val destructure_abs : abs_kind -> bool -> bool -> eval_ctx -> abs -> abs
+val destructure_abs :
+  Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> abs -> abs
 
 (** Return [true] if the values in an abstraction are destructured.
 
@@ -99,7 +103,7 @@ val destructure_abs : abs_kind -> bool -> bool -> eval_ctx -> abs -> abs
 
     The input boolean is [destructure_shared_value]. See {!destructure_abs}.
  *)
-val abs_is_destructured : bool -> eval_ctx -> abs -> bool
+val abs_is_destructured : Meta.meta -> bool -> eval_ctx -> abs -> bool
 
 (** Turn a value into a abstractions.
 
@@ -125,7 +129,7 @@ val abs_is_destructured : bool -> eval_ctx -> abs -> bool
     - [v]
  *)
 val convert_value_to_abstractions :
-  abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list
+  Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list
 
 (** See {!merge_into_abstraction}.
 
@@ -232,6 +236,7 @@ type merge_duplicates_funcs = {
     results from the merge.
  *)
 val merge_into_abstraction :
+  Meta.meta ->
   abs_kind ->
   bool ->
   merge_duplicates_funcs option ->