From 5ae71e75bd80e1b5de6985c94f364b2b881233ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Dec 2013 16:31:33 -0800
Subject: [PATCH] perf(library/elaborator): avoid exception

Lean was spending 17% on the runtime "throwing exceptions" in the test tests/lean/implicit7.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/elaborator/elaborator.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 3d5a60558..4b13a5b7a 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -224,6 +224,11 @@ class elaborator::imp {
 
     /** \brief Return true iff \c a is a proposition */
     bool is_proposition(expr const & a, context const & ctx) {
+        if (is_metavar(a)) {
+            // Avoid exception at m_type_inferer.
+            // Throw is expensive in C++.
+            return false;
+        }
         try {
             return m_type_inferer.is_proposition(a, ctx);
         } catch (...) {