From f75caddc355b1d8e6de158a4790d0bcdcf53db2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 May 2016 12:30:47 -0700
Subject: [PATCH] feat(library/vm/vm): rename cases1 to destruct

---
 src/library/compiler/vm_compiler.cpp |  2 +-
 src/library/vm/vm.cpp                | 10 +++++-----
 src/library/vm/vm.h                  |  8 ++++----
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 60ce7977fb..4b55396569 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -111,7 +111,7 @@ class vm_compiler_fn {
         if (fn_name == get_nat_cases_on_name())
             emit(mk_nat_cases_instr(0, 0));
         else if (num == 1)
-            emit(mk_cases1_instr());
+            emit(mk_destruct_instr());
         else if (num == 2)
             emit(mk_cases2_instr(0, 0));
         else
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index c795890a1c..357da4d6cd 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -179,7 +179,7 @@ void vm_instr::display(std::ostream & out, std::function<optional<name>(unsigned
     case opcode::Constructor:   out << "cnstr " << m_cidx << " " << m_nfields; break;
     case opcode::Num:           out << "num " << *m_mpz; break;
     case opcode::Unreachable:   out << "unreachable"; break;
-    case opcode::Cases1:        out << "cases1"; break;
+    case opcode::Destruct:      out << "destruct"; break;
     case opcode::Cases2:        out << "cases2 " << m_pc[0] << " " << m_pc[1]; break;
     case opcode::CasesN:
         out << "cases";
@@ -301,7 +301,7 @@ vm_instr mk_num_instr(mpz const & v) {
 
 vm_instr mk_ret_instr() { return vm_instr(opcode::Ret); }
 
-vm_instr mk_cases1_instr() { return vm_instr(opcode::Cases1); }
+vm_instr mk_destruct_instr() { return vm_instr(opcode::Destruct); }
 
 vm_instr mk_unreachable_instr() { return vm_instr(opcode::Unreachable); }
 
@@ -394,7 +394,7 @@ void vm_instr::copy_args(vm_instr const & i) {
     case opcode::Num:
         m_mpz = new mpz(*i.m_mpz);
         break;
-    case opcode::Ret: case opcode::Cases1: case opcode::Unreachable:
+    case opcode::Ret: case opcode::Destruct: case opcode::Unreachable:
         break;
     }
 }
@@ -763,8 +763,8 @@ void vm_state::run() {
             m_stack.push_back(mk_vm_mpz(instr.get_mpz()));
             m_pc++;
             goto main_loop;
-        case opcode::Cases1: {
-            /** Instruction: cases1
+        case opcode::Destruct: {
+            /** Instruction: destruct
 
                stack before,              after
                ...                        ...
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index b7f85dea74..56b993a1cf 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -179,7 +179,7 @@ inline vm_obj const & cfield(vm_obj const & o, unsigned i) { lean_assert(i < csi
 enum class opcode {
     Push, Ret, Drop, Goto,
     SConstructor, Constructor, Num,
-    Cases1, Cases2, CasesN, NatCases, Proj,
+    Destruct, Cases2, CasesN, NatCases, Proj,
     Invoke, InvokeGlobal, InvokeBuiltin, Closure, Unreachable
 };
 
@@ -209,7 +209,7 @@ class vm_instr {
         /* Num */
         mpz * m_mpz;
     };
-    /* Ret, Cases1 and Unreachable do not have arguments */
+    /* Ret, Destruct and Unreachable do not have arguments */
     friend vm_instr mk_push_instr(unsigned idx);
     friend vm_instr mk_drop_instr(unsigned n);
     friend vm_instr mk_proj_instr(unsigned n);
@@ -218,7 +218,7 @@ class vm_instr {
     friend vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
     friend vm_instr mk_num_instr(mpz const & v);
     friend vm_instr mk_ret_instr();
-    friend vm_instr mk_cases1_instr();
+    friend vm_instr mk_destruct_instr();
     friend vm_instr mk_unreachable_instr();
     friend vm_instr mk_nat_cases_instr(unsigned pc);
     friend vm_instr mk_cases2_instr(unsigned pc);
@@ -331,7 +331,7 @@ vm_instr mk_sconstructor_instr(unsigned cidx);
 vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
 vm_instr mk_num_instr(mpz const & v);
 vm_instr mk_ret_instr();
-vm_instr mk_cases1_instr();
+vm_instr mk_destruct_instr();
 vm_instr mk_unreachable_instr();
 vm_instr mk_nat_cases_instr(unsigned pc1, unsigned pc2);
 vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2);