diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 6 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 4 |
2 files changed, 8 insertions, 2 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index b85f6692..28caf6e6 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1417,6 +1417,9 @@ let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx = let end_borrow_no_synth config id ctx = get_cf_ctx_no_synth (end_borrow config id) ctx +let end_borrows_no_synth config ids ctx = + get_cf_ctx_no_synth (end_borrows config ids) ctx + let end_abstraction_no_synth config id ctx = get_cf_ctx_no_synth (end_abstraction config id) ctx @@ -1770,8 +1773,7 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool) [ { V.value; ty } ]) | V.Symbolic _ -> (* For now, we force all the symbolic values containing borrows to - be eagerly expanded *) - (* We don't support nested borrows for now *) + be eagerly expanded, and we don't support nested borrows *) assert (not (value_has_borrows ctx v.V.value)); (* Return nothing *) [] diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index a1a8fb0c..0d1be9c2 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -33,6 +33,10 @@ val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun (** End a borrow and return the resulting environment, ignoring synthesis *) val end_borrow_no_synth : C.config -> V.BorrowId.id -> C.eval_ctx -> C.eval_ctx +(** End a set of borrows and return the resulting environment, ignoring synthesis *) +val end_borrows_no_synth : + C.config -> V.BorrowId.Set.t -> C.eval_ctx -> C.eval_ctx + (** End an abstraction and return the resulting environment, ignoring synthesis *) val end_abstraction_no_synth : C.config -> V.AbstractionId.id -> C.eval_ctx -> C.eval_ctx |