Update the env frame iterators to prepare support for abstractions

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