diff options
| -rw-r--r-- | src/Interpreter.ml | 62 |
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) |