diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Values.ml | 315 |
1 files changed, 0 insertions, 315 deletions
diff --git a/src/Values.ml b/src/Values.ml index 764612af..aabd41c2 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -275,318 +275,3 @@ type abs = { In order to model the relations between the borrows, we use "abstraction values", which are a special kind of value. *) - -(* -(** Polymorphic version of the map visitor for [g_typed_value]. - - The polymorphic visitor generated by the visitors macro caused some - trouble, especially because the map functions allowed to change the - type parameters (for instance the typed of `visit_'ty` was: - `'env 'r_0 'r_1. 'env -> 'r_0 ty -> 'r_1 ty`, which prevented from - initializing it as `fun ty -> ty`). - - TODO: this is now useless... -*) -class virtual ['self] map_g_typed_value = - object (self : 'self) - inherit [_] VisitorsRuntime.map - - method visit_Concrete - : 'env 'r 'sv 'bc 'lc. - 'env -> constant_value -> ('r, 'sv, 'bc, 'lc) g_value = - fun _env cv -> Concrete cv - - method visit_Bottom - : 'env 'r 'sv 'bc 'lc. 'env -> ('r, 'sv, 'bc, 'lc) g_value = - fun _env -> Bottom - - method visit_Borrow - : 'env 'r 'sv 'bc 'lc. - ('env -> 'bc -> 'bc) -> 'env -> 'bc -> ('r, 'sv, 'bc, 'lc) g_value = - fun visit_'bc env bc -> Borrow (visit_'bc env bc) - - method visit_Loan - : 'env 'r 'sv 'bc 'lc. - ('env -> 'lc -> 'lc) -> 'env -> 'lc -> ('r, 'sv, 'bc, 'lc) g_value = - fun visit_'lc env lc -> Loan (visit_'lc env lc) - - method visit_Symbolic - : 'env 'r 'sv 'bc 'lc. - ('env -> 'sv -> 'sv) -> 'env -> 'sv -> ('r, 'sv, 'bc, 'lc) g_value = - fun visit_'sv env sv -> Symbolic (visit_'sv env sv) - - method visit_g_value - : 'env 'r 'sv 'bc 'lc. - ('env -> 'sv -> 'sv) -> - ('env -> 'bc -> 'bc) -> - ('env -> 'lc -> 'lc) -> - 'env -> - ('r, 'sv, 'bc, 'lc) g_value -> - ('r, 'sv, 'bc, 'lc) g_value = - fun visit_'sv visit_'bc visit_'lc env v -> - match v with - | Concrete cv -> self#visit_Concrete env cv - | Adt av -> - Adt (self#visit_g_adt_value visit_'sv visit_'bc visit_'lc env av) - | Bottom -> self#visit_Bottom env - | Borrow bc -> self#visit_Borrow visit_'bc env bc - | Loan lc -> self#visit_Loan visit_'lc env lc - | Symbolic sv -> self#visit_Symbolic visit_'sv env sv - - method visit_g_adt_value - : 'env 'r 'sv 'bc 'lc. - ('env -> 'sv -> 'sv) -> - ('env -> 'bc -> 'bc) -> - ('env -> 'lc -> 'lc) -> - 'env -> - ('r, 'sv, 'bc, 'lc) g_adt_value -> - ('r, 'sv, 'bc, 'lc) g_adt_value = - fun visit_'sv visit_'bc visit_'lc env av -> - let variant_id = av.variant_id in - let field_values = - self#visit_list - (self#visit_g_typed_value visit_'sv visit_'bc visit_'lc) - env av.field_values - in - { variant_id; field_values } - - method visit_g_typed_value - : 'env 'r 'sv 'bc 'lc. - ('env -> 'sv -> 'sv) -> - ('env -> 'bc -> 'bc) -> - ('env -> 'lc -> 'lc) -> - 'env -> - ('r, 'sv, 'bc, 'lc) g_typed_value -> - ('r, 'sv, 'bc, 'lc) g_typed_value = - fun visit_'sv visit_'bc visit_'lc env v -> - let value = - self#visit_g_value visit_'sv visit_'bc visit_'lc env v.value - in - let ty = self#visit_ty env v.ty in - { value; ty } - - method visit_ty : 'env 'r. 'env -> 'r ty -> 'r ty = fun _env ty -> ty - end - -(** Map iterator for typed values. - - Unfortunately, we can't rely on [map_g_typed_value]: polymorphic visitors - don't work in our case, because we sometimes have to reimplement methods - like `visit_Loan`. For instance, when implementing `update_borrow`, we - can't simply reimplement `visit_Borrow` because we need a method which - returns a value or a typed value. - *) -class ['self] map_typed_value = - object (self : 'self) - inherit [_] VisitorsRuntime.map - - method visit_Concrete : 'env -> constant_value -> value = - fun _env cv -> Concrete cv - - method visit_Bottom : 'env -> value = fun _env -> Bottom - - method visit_Borrow : 'env -> borrow_content -> value = - fun env bc -> Borrow (self#visit_borrow_content env bc) - - method visit_Loan : 'env -> loan_content -> value = - fun env lc -> Loan (self#visit_loan_content env lc) - - method visit_Symbolic : 'env -> symbolic_proj_comp -> value = - fun env sv -> Symbolic (self#visit_symbolic_proj_comp env sv) - - method visit_value : 'env -> value -> value = - fun env v -> - match v with - | Concrete cv -> self#visit_Concrete env cv - | Adt av -> Adt (self#visit_adt_value env av) - | Bottom -> self#visit_Bottom env - | Borrow bc -> self#visit_Borrow env bc - | Loan lc -> self#visit_Loan env lc - | Symbolic sv -> self#visit_Symbolic env sv - - method visit_adt_value : 'env -> adt_value -> adt_value = - fun env av -> - let variant_id = av.variant_id in - let field_values = - self#visit_list self#visit_typed_value env av.field_values - in - { variant_id; field_values } - - method visit_typed_value : 'env -> typed_value -> typed_value = - fun env v -> - let value = self#visit_value env v.value in - let ty = self#visit_ety env v.ty in - { value; ty } - - method visit_ety : 'env -> ety -> ety = fun _env ty -> ty - - method visit_symbolic_proj_comp - : 'env -> symbolic_proj_comp -> symbolic_proj_comp = - fun _env sv -> sv - - method visit_borrow_content : 'env -> borrow_content -> borrow_content = - fun env bc -> - match bc with - | SharedBorrow bid -> self#visit_SharedBorrow env bid - | MutBorrow (bid, v) -> self#visit_MutBorrow env bid v - | InactivatedMutBorrow bid -> self#visit_InactivatedMutBorrow env bid - - method visit_SharedBorrow : 'env -> BorrowId.id -> borrow_content = - fun _env bid -> SharedBorrow bid - - method visit_MutBorrow - : 'env -> BorrowId.id -> typed_value -> borrow_content = - fun env bid v -> - let v = self#visit_typed_value env v in - MutBorrow (bid, v) - - method visit_InactivatedMutBorrow : 'env -> BorrowId.id -> borrow_content = - fun _env bid -> InactivatedMutBorrow bid - - method visit_loan_content : 'env -> loan_content -> loan_content = - fun env lc -> - match lc with - | SharedLoan (bids, v) -> self#visit_SharedLoan env bids v - | MutLoan bid -> self#visit_MutLoan env bid - - method visit_SharedLoan - : 'env -> BorrowId.set_t -> typed_value -> loan_content = - fun env bids v -> - let v = self#visit_typed_value env v in - SharedLoan (bids, v) - - method visit_MutLoan : 'env -> BorrowId.id -> loan_content = - fun _env bid -> MutLoan bid - end - -class ['self] map_typed_avalue = - object (self : 'self) - inherit [_] map_typed_value - - method visit_a_Concrete : 'env -> constant_value -> avalue = - fun _env cv -> Concrete cv - - method visit_a_Bottom : 'env -> avalue = fun _env -> Bottom - - method visit_a_Borrow : 'env -> aborrow_content -> avalue = - fun env bc -> Borrow (self#visit_aborrow_content env bc) - - method visit_a_Loan : 'env -> aloan_content -> avalue = - fun env lc -> Loan (self#visit_aloan_content env lc) - - method visit_a_Symbolic : 'env -> aproj -> avalue = - fun env sv -> Symbolic (self#visit_aproj env sv) - - method visit_avalue : 'env -> avalue -> avalue = - fun env v -> - match v with - | Concrete cv -> self#visit_a_Concrete env cv - | Adt av -> Adt (self#visit_aadt_value env av) - | Bottom -> self#visit_a_Bottom env - | Borrow bc -> self#visit_a_Borrow env bc - | Loan lc -> self#visit_a_Loan env lc - | Symbolic sv -> self#visit_a_Symbolic env sv - - method visit_aadt_value : 'env -> aadt_value -> aadt_value = - fun env av -> - let variant_id = av.variant_id in - let field_values = - self#visit_list self#visit_typed_avalue env av.field_values - in - { variant_id; field_values } - - method visit_typed_avalue : 'env -> typed_avalue -> typed_avalue = - fun env v -> - let value = self#visit_avalue env v.value in - let ty = self#visit_rty env v.ty in - { value; ty } - - method visit_rty : 'env -> rty -> rty = fun _env ty -> ty - - method visit_aproj : 'env -> aproj -> aproj = fun _env sv -> sv - - method visit_aborrow_content : 'env -> aborrow_content -> aborrow_content = - fun env bc -> - match bc with - | AMutBorrow (bid, v) -> self#visit_AMutBorrow env bid v - | ASharedBorrow bid -> self#visit_ASharedBorrow env bid - | AIgnoredMutBorrow v -> self#visit_AIgnoredMutBorrow env v - | AIgnoredSharedBorrow asb -> self#visit_AIgnoredSharedBorrow env asb - - method visit_AMutBorrow - : 'env -> BorrowId.id -> typed_avalue -> aborrow_content = - fun env bid av -> - let av = self#visit_typed_avalue env av in - AMutBorrow (bid, av) - - method visit_ASharedBorrow : 'env -> BorrowId.id -> aborrow_content = - fun _env bid -> ASharedBorrow bid - - method visit_AIgnoredMutBorrow : 'env -> typed_avalue -> aborrow_content = - fun env av -> - let av = self#visit_typed_avalue env av in - AIgnoredMutBorrow av - - method visit_AIgnoredSharedBorrow - : 'env -> abstract_shared_borrows -> aborrow_content = - fun _env asb -> AIgnoredSharedBorrow asb - - method visit_aloan_content : 'env -> aloan_content -> aloan_content = - fun env lc -> - match lc with - | AMutLoan (bid, av) -> self#visit_AMutLoan env bid av - | ASharedLoan (bids, v, av) -> self#visit_ASharedLoan env bids v av - | AEndedMutLoan { given_back; child } -> - self#visit_AEndedMutLoan env given_back child - | AEndedSharedLoan (v, av) -> self#visit_AEndedSharedLoan env v av - | AIgnoredMutLoan (bids, v) -> self#visit_AIgnoredMutLoan env bids v - | AEndedIgnoredMutLoan { given_back; child } -> - self#visit_AEndedIgnoredMutLoan env given_back child - | AIgnoredSharedLoan asb -> self#visit_AIgnoredSharedLoan env asb - - method visit_AMutLoan : 'env -> BorrowId.id -> typed_avalue -> aloan_content - = - fun env bid av -> - let av = self#visit_typed_avalue env av in - AMutLoan (bid, av) - - method visit_ASharedLoan - : 'env -> BorrowId.set_t -> typed_value -> typed_avalue -> aloan_content - = - fun env bids v av -> - let v = self#visit_typed_value env v in - let av = self#visit_typed_avalue env av in - ASharedLoan (bids, v, av) - - method visit_AEndedMutLoan - : 'env -> typed_value -> typed_avalue -> aloan_content = - fun env given_back child -> - let given_back = self#visit_typed_value env given_back in - let child = self#visit_typed_avalue env child in - AEndedMutLoan { given_back; child } - - method visit_AEndedSharedLoan - : 'env -> typed_value -> typed_avalue -> aloan_content = - fun env v av -> - let v = self#visit_typed_value env v in - let av = self#visit_typed_avalue env av in - AEndedSharedLoan (v, av) - - method visit_AIgnoredMutLoan - : 'env -> BorrowId.id -> typed_avalue -> aloan_content = - fun env id av -> - let av = self#visit_typed_avalue env av in - AIgnoredMutLoan (id, av) - - method visit_AEndedIgnoredMutLoan - : 'env -> typed_avalue -> typed_avalue -> aloan_content = - fun env given_back child -> - let given_back = self#visit_typed_avalue env given_back in - let child = self#visit_typed_avalue env child in - AEndedIgnoredMutLoan { given_back; child } - - method visit_AIgnoredSharedLoan - : 'env -> abstract_shared_borrows -> aloan_content = - fun _env asb -> AIgnoredSharedLoan asb - end - *) |