From ecf30e93a3b58b3c8a3a1670cc1eef7e50713674 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 29 Oct 2018 13:18:33 -0700
Subject: [PATCH] chore(library/vm): remove `Destruct` instruction

---
 src/library/vm/optimize.cpp |  3 +--
 src/library/vm/vm.cpp       | 25 ++-----------------------
 src/library/vm/vm.h         |  6 ++----
 3 files changed, 5 insertions(+), 29 deletions(-)

diff --git a/src/library/vm/optimize.cpp b/src/library/vm/optimize.cpp
index edd72d22d8..ef5c579333 100644
--- a/src/library/vm/optimize.cpp
+++ b/src/library/vm/optimize.cpp
@@ -99,8 +99,7 @@ class live_vars_fn {
             break;
         case opcode::Drop: case opcode::SConstructor:
         case opcode::Constructor: case opcode::Num: case opcode::String:
-        case opcode::Destruct: case opcode::Proj:
-        case opcode::Apply: case opcode::InvokeGlobal:
+        case opcode::Proj: case opcode::Apply: case opcode::InvokeGlobal:
         case opcode::InvokeBuiltin: case opcode::InvokeCFun:
         case opcode::Closure: case opcode::Expr: case opcode::LocalInfo:
             s = collect(pc+1);
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 60efa0d4be..9a23ad7996 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -533,7 +533,6 @@ void vm_instr::display(std::ostream & out) const {
     case opcode::Num:           out << "num " << *m_mpz; break;
     case opcode::String:        out << "str_lit \"" << *m_str << "\""; break;
     case opcode::Unreachable:   out << "unreachable"; break;
-    case opcode::Destruct:      out << "destruct"; break;
     case opcode::Cases2:        out << "cases2 " << m_pc[1]; break;
     case opcode::CasesN:
         out << "cases";
@@ -683,8 +682,6 @@ vm_instr mk_local_info_instr(unsigned idx, name const & n, optional<expr> const
 
 vm_instr mk_ret_instr() { return vm_instr(opcode::Ret); }
 
-vm_instr mk_destruct_instr() { return vm_instr(opcode::Destruct); }
-
 vm_instr mk_unreachable_instr() { return vm_instr(opcode::Unreachable); }
 
 vm_instr mk_apply_instr() { return vm_instr(opcode::Apply); }
@@ -800,7 +797,7 @@ void vm_instr::copy_args(vm_instr const & i) {
         m_local_idx  = i.m_local_idx;
         m_local_info = new vm_local_info(*i.m_local_info);
         break;
-    case opcode::Ret:         case opcode::Destruct:
+    case opcode::Ret:
     case opcode::Unreachable: case opcode::Apply:
         break;
     }
@@ -911,7 +908,7 @@ void vm_instr::serialize(serializer & s, std::function<name(unsigned)> const & i
     case opcode::LocalInfo:
         s << m_local_idx << m_local_info->first << m_local_info->second;
         break;
-    case opcode::Ret:         case opcode::Destruct:
+    case opcode::Ret:
     case opcode::Unreachable: case opcode::Apply:
         break;
     }
@@ -979,8 +976,6 @@ static vm_instr read_vm_instr(deserializer & d) {
     }
     case opcode::Ret:
         return mk_ret_instr();
-    case opcode::Destruct:
-        return mk_destruct_instr();
     case opcode::Unreachable:
         return mk_unreachable_instr();
     case opcode::Apply:
@@ -2935,22 +2930,6 @@ void vm_state::run() {
                 push_local_info(instr.get_local_idx(), instr.get_local_info());
             m_pc++;
             goto main_loop;
-        case opcode::Destruct: {
-            /** Instruction: destruct
-
-                stack before,              after
-                ...                        ...
-                v                 ==>      v
-                (#i a_1 ... a_n)           a_1
-                ...
-                a_n
-            */
-            vm_obj top = m_stack.back();
-            stack_pop_back();
-            push_fields(top);
-            m_pc++;
-            goto main_loop;
-        }
         case opcode::Cases2: {
             /** Instruction: cases2 pc1 pc2
 
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index f89ca9c4a6..9767b2ba07 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -311,7 +311,7 @@ typedef pair<name, optional<expr>> vm_local_info;
 enum class opcode {
     Push, Move, Ret, Drop, Goto,
     SConstructor, Constructor, Num, String,
-    Destruct, Cases2, CasesN, Proj,
+    Cases2, CasesN, Proj,
     Apply, InvokeGlobal, InvokeBuiltin, InvokeCFun,
     Closure, Unreachable, Expr, LocalInfo
 };
@@ -353,7 +353,7 @@ class vm_instr {
             vm_local_info * m_local_info;
         };
     };
-    /* Apply, Ret, Destruct and Unreachable do not have arguments */
+    /* Apply, Ret and Unreachable do not have arguments */
     friend vm_instr mk_push_instr(unsigned idx);
     friend vm_instr mk_move_instr(unsigned idx);
     friend vm_instr mk_drop_instr(unsigned n);
@@ -364,7 +364,6 @@ class vm_instr {
     friend vm_instr mk_num_instr(mpz const & v);
     friend vm_instr mk_string_instr(std::string const & v);
     friend vm_instr mk_ret_instr();
-    friend vm_instr mk_destruct_instr();
     friend vm_instr mk_unreachable_instr();
     friend vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2);
     friend vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);
@@ -504,7 +503,6 @@ vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
 vm_instr mk_num_instr(mpz const & v);
 vm_instr mk_string_instr(std::string const & v);
 vm_instr mk_ret_instr();
-vm_instr mk_destruct_instr();
 vm_instr mk_unreachable_instr();
 vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2);
 vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);