summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml62
1 files changed, 28 insertions, 34 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ad0a70e2..97763abe 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -63,8 +63,10 @@ type exploration_kind = {
*)
exception Found
-(** When looking for something, it can be easier to just throw an exception to
- signal we found what we were looking for.
+(** Utility exception
+
+ When looking for something while exploring a term, it can be easier to
+ just throw an exception to signal we found what we were looking for.
*)
exception FoundBorrowContent of V.borrow_content
@@ -351,41 +353,33 @@ let unwrap_res_to_outer_or opt default =
(** Return the first loan we find in a value *)
let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
- match v.V.value with
- | V.Concrete _ -> None
- | V.Adt av -> get_first_loan_in_values av.field_values
- | V.Borrow bc -> (
- match bc with
- | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None
- | V.MutBorrow (_, bv) -> get_first_loan_in_value bv)
- | V.Loan lc -> Some lc
- | V.Bottom | V.Symbolic _ -> None
-
-and get_first_loan_in_values (vl : V.typed_value list) : V.loan_content option =
- match vl with
- | [] -> None
- | v :: vl' -> (
- match get_first_loan_in_value v with
- | Some lc -> Some lc
- | None -> get_first_loan_in_values vl')
+ let obj =
+ object
+ inherit [_] V.iter_typed_value
+
+ method! visit_loan_content _ lc = raise (FoundLoanContent lc)
+ end
+ in
+ (* We use exceptions *)
+ try
+ obj#visit_typed_value () v;
+ None
+ with FoundLoanContent lc -> Some lc
(** Check if a value contains ⊥ *)
let rec bottom_in_value (v : V.typed_value) : bool =
- match v.V.value with
- | V.Concrete _ -> false
- | V.Adt av -> List.exists bottom_in_value av.field_values
- | V.Borrow bc -> (
- match bc with
- | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> false
- | V.MutBorrow (_, bv) -> bottom_in_value bv)
- | V.Loan lc -> (
- match lc with
- | V.SharedLoan (_, sv) -> bottom_in_value sv
- | V.MutLoan _ -> false)
- | V.Bottom -> true
- | V.Symbolic _ ->
- (* This depends on the regions which have ended *)
- raise Unimplemented
+ let obj =
+ object
+ inherit [_] V.iter_typed_value
+
+ method! visit_Bottom _ = raise Found
+ end
+ in
+ (* We use exceptions *)
+ try
+ obj#visit_typed_value () v;
+ false
+ with Found -> true
(** See [end_borrow_get_borrow_in_env] *)
let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer)