Do more cleanup

1 files changed, 37 insertions, 42 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5440dc3c..b7794946 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -951,11 +951,6 @@ let rec access_projection (access : projection_access) (env : C.env)
     (* Function to (eventually) update the value we find *)
       (update : V.typed_value -> V.typed_value) (p : E.projection)
     (v : V.typed_value) : (C.env * updated_read_value) path_access_result =
-  (* (* Debug *)
-     L.log#ldebug
-       (lazy
-         ("access_projection:\n" ^ "- p: " ^ E.show_projection p ^ "\n- v: "
-        ^ V.show_typed_value v));*)
   (* For looking up/updating shared loans *)
   let ek : exploration_kind =
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -987,14 +982,14 @@ let rec access_projection (access : projection_access) (env : C.env)
           let fv = T.FieldId.nth adt.field_values field_id in
           match access_projection access env update p' fv with
           | Error err -> Error err
-          | Ok (env1, res) ->
+          | Ok (env, res) ->
               (* Update the field value *)
               let nvalues =
                 T.FieldId.update_nth adt.field_values field_id res.updated
               in
               let nadt = V.Adt { adt with V.field_values = nvalues } in
               let updated = { v with value = nadt } in
-              Ok (env1, { res with updated }))
+              Ok (env, { res with updated }))
       (* Tuples *)
       | Field (ProjTuple arity, field_id), V.Tuple values -> (
           assert (arity = List.length values);
@@ -1002,12 +997,12 @@ let rec access_projection (access : projection_access) (env : C.env)
           (* Project *)
           match access_projection access env update p' fv with
           | Error err -> Error err
-          | Ok (env1, res) ->
+          | Ok (env, res) ->
               (* Update the field value *)
               let nvalues = T.FieldId.update_nth values field_id res.updated in
               let ntuple = V.Tuple nvalues in
               let updated = { v with value = ntuple } in
-              Ok (env1, { res with updated })
+              Ok (env, { res with updated })
           (* If we reach Bottom, it may mean we need to expand an uninitialized
            * enumeration value *))
       | Field (ProjAdt (_, _), _), V.Bottom ->
@@ -1027,9 +1022,9 @@ let rec access_projection (access : projection_access) (env : C.env)
            * interpreter *)
           match access_projection access env update p' bv with
           | Error err -> Error err
-          | Ok (env1, res) ->
+          | Ok (env, res) ->
               let nv = { v with value = V.Assumed (V.Box res.updated) } in
-              Ok (env1, { res with updated = nv }))
+              Ok (env, { res with updated = nv }))
       (* Borrows *)
       | Deref, V.Borrow bc -> (
           match bc with
@@ -1042,30 +1037,30 @@ let rec access_projection (access : projection_access) (env : C.env)
                     (* Explore the shared value *)
                     match access_projection access env update p' sv with
                     | Error err -> Error err
-                    | Ok (env1, res) ->
+                    | Ok (env, res) ->
                         (* Update the shared loan with the new value returned
                            by [access_projection] *)
-                        let env2 =
+                        let env =
                           update_loan ek bid
                             (V.SharedLoan (bids, res.updated))
-                            env1
+                            env
                         in
                         (* Return - note that we don't need to update the borrow itself *)
-                        Ok (env2, { res with updated = v }))
+                        Ok (env, { res with updated = v }))
               else Error (FailBorrow bc)
           | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid)
           | V.MutBorrow (bid, bv) ->
               if access.enter_mut_borrows then
                 match access_projection access env update p' bv with
                 | Error err -> Error err
-                | Ok (env1, res) ->
+                | Ok (env, res) ->
                     let nv =
                       {
                         v with
                         value = V.Borrow (V.MutBorrow (bid, res.updated));
                       }
                     in
-                    Ok (env1, { res with updated = nv })
+                    Ok (env, { res with updated = nv })
               else Error (FailBorrow bc))
       | _, V.Loan lc -> (
           match lc with
@@ -1077,14 +1072,14 @@ let rec access_projection (access : projection_access) (env : C.env)
               if access.enter_shared_loans then
                 match access_projection access env update (pe :: p') sv with
                 | Error err -> Error err
-                | Ok (env1, res) ->
+                | Ok (env, res) ->
                     let nv =
                       {
                         v with
                         value = V.Loan (V.SharedLoan (bids, res.updated));
                       }
                     in
-                    Ok (env1, { res with updated = nv })
+                    Ok (env, { res with updated = nv })
               else Error (FailSharedLoan bids))
       | ( _,
           ( V.Concrete _ | V.Adt _ | V.Tuple _ | V.Bottom | V.Assumed _
@@ -1110,11 +1105,11 @@ let access_place (access : projection_access)
   (* Apply the projection *)
   match access_projection access env update p.projection value with
   | Error err -> Error err
-  | Ok (env1, res) ->
+  | Ok (env, res) ->
       (* Update the value *)
-      let env2 = C.env_update_var_value env1 p.var_id res.updated in
+      let env = C.env_update_var_value env p.var_id res.updated in
       (* Return *)
-      Ok (env2, res.read)
+      Ok (env, res.read)
 
 type access_kind =
   | Read  (** We can go inside borrows and loans *)
@@ -2012,9 +2007,9 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
   let rec list_locals env =
     match env with
     | [] -> failwith "Inconsistent environment"
-    | C.Abs _ :: env' -> list_locals env'
-    | C.Var (var, _) :: env' ->
-        let locals = list_locals env' in
+    | C.Abs _ :: env -> list_locals env
+    | C.Var (var, _) :: env ->
+        let locals = list_locals env in
         if var.index <> ret_vid then var.index :: locals else locals
     | C.Frame :: _ -> []
   in
@@ -2026,7 +2021,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
       ^ String.concat "," (List.map V.VarId.to_string locals)
       ^ "]"));
   (* Drop the local variables *)
-  let ctx1 =
+  let ctx =
     List.fold_left
       (fun ctx lid -> drop_value config ctx (mk_place_from_var_id lid))
       ctx locals
@@ -2035,22 +2030,22 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
   L.log#ldebug
     (lazy
       ("ctx_pop_frame: after dropping local variables:\n"
-     ^ eval_ctx_to_string ctx1));
+     ^ eval_ctx_to_string ctx));
   (* Move the return value out of the return variable *)
-  let ctx2, ret_value =
-    eval_operand config ctx1 (E.Move (mk_place_from_var_id ret_vid))
+  let ctx, ret_value =
+    eval_operand config ctx (E.Move (mk_place_from_var_id ret_vid))
   in
   (* Pop the frame *)
   let rec pop env =
     match env with
     | [] -> failwith "Inconsistent environment"
-    | C.Abs abs :: env' -> C.Abs abs :: pop env'
-    | C.Var (_, _) :: env' -> pop env'
-    | C.Frame :: env' -> env'
+    | C.Abs abs :: env -> C.Abs abs :: pop env
+    | C.Var (_, _) :: env -> pop env
+    | C.Frame :: env -> env
   in
-  let env3 = pop ctx2.env in
-  let ctx3 = { ctx2 with env = env3 } in
-  (ctx3, ret_value)
+  let env = pop ctx.env in
+  let ctx = { ctx with env } in
+  (ctx, ret_value)
 
 (** Assign a value to a given place *)
 let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value)
@@ -2289,22 +2284,22 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
       (* Evaluate the rvalue *)
       match eval_rvalue config ctx rvalue with
       | Error err -> Error err
-      | Ok (ctx1, rvalue) ->
+      | Ok (ctx, rvalue) ->
           (* Assign *)
-          let ctx2 = assign_to_place config ctx1 rvalue p in
-          Ok (ctx2, Unit))
+          let ctx = assign_to_place config ctx rvalue p in
+          Ok (ctx, Unit))
   | A.FakeRead p ->
-      let ctx1, _ = prepare_rplace config Read p ctx in
-      Ok (ctx1, Unit)
+      let ctx, _ = prepare_rplace config Read p ctx in
+      Ok (ctx, Unit)
   | A.SetDiscriminant (p, variant_id) ->
       set_discriminant config ctx p variant_id
   | A.Drop p -> Ok (drop_value config ctx p, Unit)
   | A.Assert assertion -> (
-      let ctx1, v = eval_operand config ctx assertion.cond in
+      let ctx, v = eval_operand config ctx assertion.cond in
       assert (v.ty = T.Bool);
       match v.value with
       | Concrete (Bool b) ->
-          if b = assertion.expected then Ok (ctx1, Unit) else Error Panic
+          if b = assertion.expected then Ok (ctx, Unit) else Error Panic
       | _ -> failwith "Expected a boolean")
   | A.Call call -> eval_function_call config ctx call
   | A.Panic -> Error Panic