max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/vm/vm): rename cases1 to destruct

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-13 12:30:47 -07:00
parent 4f53cfe5e8
commit f75caddc35
3 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/vm_compiler.cpp
View file

@ -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

10
src/library/vm/vm.cpp
View file

@ -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
... ...

8
src/library/vm/vm.h
View file

@ -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);