From e0d57aa8a36ebc9bc1619bae2c4176dd10592ffc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Feb 2017 15:40:16 -0800
Subject: [PATCH] chore(library/tactic): add missing lean_vm_check's

---
 src/library/tactic/backward/backward_lemmas.cpp | 3 +--
 src/library/tactic/simp_lemmas.cpp              | 3 +--
 src/library/tactic/smt/congruence_tactics.cpp   | 3 +--
 src/library/tactic/smt/ematch.cpp               | 3 +--
 src/library/tactic/smt/hinst_lemmas.cpp         | 6 ++----
 src/library/tactic/smt/smt_state.cpp            | 3 +--
 src/library/tactic/tactic_state.cpp             | 3 +--
 src/library/tactic/vm_monitor.cpp               | 3 +--
 8 files changed, 9 insertions(+), 18 deletions(-)

diff --git a/src/library/tactic/backward/backward_lemmas.cpp b/src/library/tactic/backward/backward_lemmas.cpp
index debfae99f8..35e9a64cf6 100644
--- a/src/library/tactic/backward/backward_lemmas.cpp
+++ b/src/library/tactic/backward/backward_lemmas.cpp
@@ -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;
 }
 
diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index 5492eae0a3..d6a59770cb 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -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;
 }
 
diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp
index 40b3e9ca82..13ab07ba24 100644
--- a/src/library/tactic/smt/congruence_tactics.cpp
+++ b/src/library/tactic/smt/congruence_tactics.cpp
@@ -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;
 }
 
diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp
index 36a3942ff1..d14ee6e890 100644
--- a/src/library/tactic/smt/ematch.cpp
+++ b/src/library/tactic/smt/ematch.cpp
@@ -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;
 }
 
diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp
index af734852ce..1d758352ff 100644
--- a/src/library/tactic/smt/hinst_lemmas.cpp
+++ b/src/library/tactic/smt/hinst_lemmas.cpp
@@ -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;
 }
 
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index 98ebf34502..e9c483dcf1 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -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;
 }
 
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 6d99e194b6..b7ca687906 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -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;
 }
 
diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp
index fa535e3419..719a3602df 100644
--- a/src/library/tactic/vm_monitor.cpp
+++ b/src/library/tactic/vm_monitor.cpp
@@ -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;
 }