summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Contexts.ml26
1 files changed, 24 insertions, 2 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 9bcaaa43..295b5164 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -148,7 +148,7 @@ 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 a frame. *)
+(** Visitor to iterate over the values in the current frame *)
class ['self] iter_frame_concrete =
object (self : 'self)
inherit [_] V.iter_typed_value
@@ -163,6 +163,28 @@ class ['self] iter_frame_concrete =
| Var (vid, v) :: env ->
self#visit_env_value_Var acc vid v;
self#visit_env acc env
- | Abs _ :: _ -> raise Errors.Unimplemented (* TODO *)
+ | Abs _ :: _ -> failwith "Unexpected abstraction"
| Frame :: _ -> (* We stop here *) ()
end
+
+(** Visitor to iterate over the values in the current frame *)
+class ['self] map_frame_concrete =
+ object (self : 'self)
+ inherit [_] V.map_typed_value
+
+ method visit_env_value_Var : 'acc -> binder -> typed_value -> env_value =
+ 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_value_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