diff options
| -rw-r--r-- | src/Contexts.ml | 71 | ||||
| -rw-r--r-- | src/Interpreter.ml | 24 |
2 files changed, 39 insertions, 56 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index cc28dd27..8f92ae78 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -12,6 +12,8 @@ type binder = { (** Environment value: mapping from variable to value, abstraction (only used in symbolic mode) or stack frame delimiter. + + TODO: rename Var (-> Binding?) *) type env_elem = Var of (binder[@opaque]) * typed_value | Abs of abs | Frame [@@deriving @@ -184,33 +186,17 @@ let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx = let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in ctx_push_vars ctx vars -(** Visitor to iterate over the values in the current frame *) -class ['self] iter_frame_concrete = +(** Visitor to iterate over the values in the *current* frame *) +class ['self] iter_frame = object (self : 'self) - inherit [_] V.iter_typed_value + inherit [_] V.iter_abs + (* TODO: remove "env_elem" from the name *) method visit_env_elem_Var : 'acc -> binder -> typed_value -> unit = fun acc vid v -> self#visit_typed_value acc v - method visit_env : 'acc -> env -> unit = - fun acc env -> - match env with - | [] -> () - | Var (vid, v) :: env -> - self#visit_env_elem_Var acc vid v; - self#visit_env acc env - | Abs _ :: _ -> failwith "Unexpected abstraction" - | Frame :: _ -> (* We stop here *) () - end - -(** Visitor to iterate over the values in an environment (we explore an - environment until we find the end of the current frame) *) -class ['self] iter_env_concrete = - object (self : 'self) - inherit [_] V.iter_typed_value - - method visit_env_elem_Var : 'acc -> binder -> typed_value -> unit = - fun acc vid v -> self#visit_typed_value acc v + method visit_env_elem_Abs : 'acc -> abs -> unit = + fun acc abs -> self#visit_abs acc abs method visit_env : 'acc -> env -> unit = fun acc env -> @@ -219,42 +205,24 @@ class ['self] iter_env_concrete = | Var (vid, v) :: env -> self#visit_env_elem_Var acc vid v; self#visit_env acc env - | Abs _ :: _ -> failwith "Unexpected abstraction" - | Frame :: env -> self#visit_env acc env + | Abs abs :: env -> + self#visit_env_elem_Abs acc abs; + self#visit_env acc env + | Frame :: _ -> (* We stop here *) () end -(** Visitor to map over the values in the current frame *) +(** Visitor to map over the values in the *current* frame *) class ['self] map_frame_concrete = object (self : 'self) - inherit [_] V.map_typed_value + inherit [_] V.map_abs method visit_env_elem_Var : 'acc -> binder -> typed_value -> env_elem = fun acc vid v -> let v = self#visit_typed_value acc v in Var (vid, v) - method visit_env : 'acc -> env -> env = - fun acc env -> - match env with - | [] -> [] - | Var (vid, v) :: env -> - let v = self#visit_env_elem_Var acc vid v in - let env = self#visit_env acc env in - v :: env - | Abs _ :: _ -> failwith "Unexpected abstraction" - | Frame :: env -> (* We stop here *) Frame :: env - end - -(** Visitor to iterate over the values in an environment (we explore an - environment until we find the end of the current frame) *) -class ['self] map_env_concrete = - object (self : 'self) - inherit [_] V.map_typed_value - - method visit_env_elem_Var : 'acc -> binder -> typed_value -> env_elem = - fun acc vid v -> - let v = self#visit_typed_value acc v in - Var (vid, v) + method visit_env_elem_Abs : 'acc -> abs -> env_elem = + fun acc abs -> Abs (self#visit_abs acc abs) method visit_env : 'acc -> env -> env = fun acc env -> @@ -264,6 +232,9 @@ class ['self] map_env_concrete = let v = self#visit_env_elem_Var acc vid v in let env = self#visit_env acc env in v :: env - | Abs _ :: _ -> failwith "Unexpected abstraction" - | Frame :: env -> Frame :: self#visit_env acc env + | Abs abs :: env -> + let abs = self#visit_env_elem_Abs acc abs in + let env = self#visit_env acc env in + abs :: env + | Frame :: env -> (* We stop here *) Frame :: env end diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 560cf58b..878e8e17 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -127,7 +127,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : V.loan_content option = let obj = object - inherit [_] C.iter_env_concrete as super + inherit [_] C.iter_env as super method! visit_borrow_content env bc = match bc with @@ -160,6 +160,8 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : below, we are more resilient to definition updates (the compiler is our friend). *) + + method! visit_Abs _ _ = raise Unimplemented end in (* We use exceptions *) @@ -198,7 +200,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_env_concrete as super + inherit [_] C.map_env as super method! visit_borrow_content env bc = match bc with @@ -229,6 +231,8 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) else super#visit_MutLoan env bid (** We reimplement [visit_loan_content] (rather than one of the sub- functions) on purpose: exhaustive matches are good for maintenance *) + + method! visit_Abs _ _ = raise Unimplemented end in @@ -242,7 +246,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : V.borrow_content option = let obj = object - inherit [_] C.iter_env_concrete as super + inherit [_] C.iter_env as super method! visit_borrow_content env bc = match bc with @@ -269,6 +273,8 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) (* Control the dive *) if ek.enter_shared_loans then super#visit_SharedLoan env bids sv else () + + method! visit_Abs _ _ = raise Unimplemented end in (* We use exceptions *) @@ -306,7 +312,7 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_env_concrete as super + inherit [_] C.map_env as super method! visit_borrow_content env bc = match bc with @@ -339,6 +345,8 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) | V.MutLoan bid -> (* Nothing specific to do *) super#visit_MutLoan env bid + + method! visit_Abs _ _ = raise Unimplemented end in @@ -429,7 +437,7 @@ let end_borrow_get_borrow_in_env (io : inner_outer) (l : V.BorrowId.id) (* The environment is used to keep track of the outer loans *) let obj = object - inherit [_] C.map_env_concrete as super + inherit [_] C.map_env as super method! visit_Loan outer_borrows lc = match lc with @@ -470,6 +478,8 @@ let end_borrow_get_borrow_in_env (io : inner_outer) (l : V.BorrowId.id) update_outer_borrows io outer_borrows (Borrow l') in V.Borrow (super#visit_MutBorrow outer_borrows l' bv) + + method! visit_Abs _ _ = raise Unimplemented end in (* Catch the exceptions - raised if there are outer borrows *) @@ -614,7 +624,7 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) let obj = object - inherit [_] C.map_env_concrete as super + inherit [_] C.map_env as super method! visit_SharedLoan env bids sv = (* Shared loan: check if the borrow id we are looking for is in the @@ -625,6 +635,8 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) let bids' = V.BorrowId.Set.add new_bid bids in V.SharedLoan (bids', sv)) else super#visit_SharedLoan env bids sv + + method! visit_Abs _ _ = raise Unimplemented end in |