summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-08 16:10:28 +0100
committerSon Ho2021-12-08 16:10:28 +0100
commit8863b733fa615451cba67646ebeac6b8db2207fc (patch)
treee35138ff66d81793b27a0a0c8622cdfd386d4776 /src
parent83ed1022f9fb4e2042d048d6576898d5d4bef26b (diff)
Update the env frame iterators to prepare support for abstractions
Diffstat (limited to 'src')
-rw-r--r--src/Contexts.ml71
-rw-r--r--src/Interpreter.ml24
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