diff options
Diffstat (limited to 'compiler/InterpreterBorrows.mli')
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 30b75790..56df9344 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -9,39 +9,39 @@ open Cps the set of borrows tracked by a shared value, referenced by the [original_bid] argument. *) val reborrow_shared : - Meta.meta -> BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx + Meta.span -> 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 -> Meta.meta -> BorrowId.id -> cm_fun +val end_borrow : config -> Meta.span -> BorrowId.id -> cm_fun (** End a set of borrows identified by their ids, while preserving the invariants. *) -val end_borrows : config -> Meta.meta -> BorrowId.Set.t -> cm_fun +val end_borrows : config -> Meta.span -> BorrowId.Set.t -> cm_fun (** End an abstraction while preserving the invariants. *) -val end_abstraction : config -> Meta.meta -> AbstractionId.id -> cm_fun +val end_abstraction : config -> Meta.span -> AbstractionId.id -> cm_fun (** End a set of abstractions while preserving the invariants. *) -val end_abstractions : config -> Meta.meta -> AbstractionId.Set.t -> cm_fun +val end_abstractions : config -> Meta.span -> AbstractionId.Set.t -> cm_fun (** End a borrow and return the resulting environment, ignoring synthesis *) val end_borrow_no_synth : - config -> Meta.meta -> BorrowId.id -> eval_ctx -> eval_ctx + config -> Meta.span -> BorrowId.id -> eval_ctx -> eval_ctx (** End a set of borrows and return the resulting environment, ignoring synthesis *) val end_borrows_no_synth : - config -> Meta.meta -> BorrowId.Set.t -> eval_ctx -> eval_ctx + config -> Meta.span -> BorrowId.Set.t -> eval_ctx -> eval_ctx (** End an abstraction and return the resulting environment, ignoring synthesis *) val end_abstraction_no_synth : - config -> Meta.meta -> AbstractionId.id -> eval_ctx -> eval_ctx + config -> Meta.span -> AbstractionId.id -> eval_ctx -> eval_ctx (** End a set of abstractions and return the resulting environment, ignoring synthesis *) val end_abstractions_no_synth : - config -> Meta.meta -> AbstractionId.Set.t -> eval_ctx -> eval_ctx + config -> Meta.span -> AbstractionId.Set.t -> eval_ctx -> eval_ctx (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants. @@ -52,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 -> Meta.meta -> BorrowId.id -> cm_fun +val promote_reserved_mut_borrow : config -> Meta.span -> BorrowId.id -> cm_fun (** Transform an abstraction to an abstraction where the values are not structured. @@ -95,7 +95,7 @@ val promote_reserved_mut_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun - [abs] *) val destructure_abs : - Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> abs -> abs + Meta.span -> abs_kind -> bool -> bool -> eval_ctx -> abs -> abs (** Return [true] if the values in an abstraction are destructured. @@ -103,7 +103,7 @@ val destructure_abs : The input boolean is [destructure_shared_value]. See {!destructure_abs}. *) -val abs_is_destructured : Meta.meta -> bool -> eval_ctx -> abs -> bool +val abs_is_destructured : Meta.span -> bool -> eval_ctx -> abs -> bool (** Turn a value into a abstractions. @@ -129,7 +129,7 @@ val abs_is_destructured : Meta.meta -> bool -> eval_ctx -> abs -> bool - [v] *) val convert_value_to_abstractions : - Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list + Meta.span -> abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list (** See {!merge_into_abstraction}. @@ -236,7 +236,7 @@ type merge_duplicates_funcs = { results from the merge. *) val merge_into_abstraction : - Meta.meta -> + Meta.span -> abs_kind -> bool -> merge_duplicates_funcs option -> |