Implement map_frame_concrete

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