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

chore(library/tactic): add missing lean_vm_check's

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-15 15:40:16 -08:00
parent c5287237ee
commit e0d57aa8a3
8 changed files with 9 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/tactic/backward/backward_lemmas.cpp
View file

@ -140,8 +140,7 @@ struct vm_backward_lemmas : public vm_external {
};
backward_lemma_index const & to_backward_lemmas(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_backward_lemmas*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_backward_lemmas*>(to_external(o)));
return static_cast<vm_backward_lemmas*>(to_external(o))->m_val;
}

3
src/library/tactic/simp_lemmas.cpp
View file

@ -1249,8 +1249,7 @@ bool is_simp_lemmas(vm_obj const & o) {
}
simp_lemmas const & to_simp_lemmas(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_simp_lemmas*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_simp_lemmas*>(to_external(o)));
return static_cast<vm_simp_lemmas*>(to_external(o))->m_val;
}

3
src/library/tactic/smt/congruence_tactics.cpp
View file

@ -37,8 +37,7 @@ bool is_cc_state(vm_obj const & o) {
}
congruence_closure::state const & to_cc_state(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_cc_state*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_cc_state*>(to_external(o)));
return static_cast<vm_cc_state*>(to_external(o))->m_val;
}

3
src/library/tactic/smt/ematch.cpp
View file

@ -1055,8 +1055,7 @@ struct vm_ematch_state : public vm_external {
};
ematch_state const & to_ematch_state(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_ematch_state*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_ematch_state*>(to_external(o)));
return static_cast<vm_ematch_state*>(to_external(o))->m_val;
}

6
src/library/tactic/smt/hinst_lemmas.cpp
View file

@ -692,8 +692,7 @@ struct vm_hinst_lemma : public vm_external {
};
hinst_lemma const & to_hinst_lemma(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_hinst_lemma*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_hinst_lemma*>(to_external(o)));
return static_cast<vm_hinst_lemma*>(to_external(o))->m_val;
}
@ -738,8 +737,7 @@ struct vm_hinst_lemmas : public vm_external {
};
hinst_lemmas const & to_hinst_lemmas(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_hinst_lemmas*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_hinst_lemmas*>(to_external(o)));
return static_cast<vm_hinst_lemmas*>(to_external(o))->m_val;
}

3
src/library/tactic/smt/smt_state.cpp
View file

@ -129,8 +129,7 @@ bool is_smt_goal(vm_obj const & o) {
}
smt_goal const & to_smt_goal(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_smt_goal*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_smt_goal*>(to_external(o)));
return static_cast<vm_smt_goal*>(to_external(o))->m_val;
}

3
src/library/tactic/tactic_state.cpp
View file

@ -215,8 +215,7 @@ bool is_tactic_state(vm_obj const & o) {
}
tactic_state const & to_tactic_state(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_tactic_state*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_tactic_state*>(to_external(o)));
return static_cast<vm_tactic_state*>(to_external(o))->m_val;
}

3
src/library/tactic/vm_monitor.cpp
View file

@ -181,8 +181,7 @@ struct vm_vm_decl : public vm_external {
};
vm_decl const & to_vm_decl(vm_obj const & o) {
lean_assert(is_external(o));
lean_assert(dynamic_cast<vm_vm_decl*>(to_external(o)));
lean_vm_check(dynamic_cast<vm_vm_decl*>(to_external(o)));
return static_cast<vm_vm_decl*>(to_external(o))->m_val;
}