From 5aaade47d85eefd9b623f3715329949c70214288 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 28 Jan 2015 16:42:42 -0800
Subject: [PATCH] feat(library/match): add new API

---
 src/library/match.cpp | 13 +++++++++++++
 src/library/match.h   |  1 +
 2 files changed, 14 insertions(+)

diff --git a/src/library/match.cpp b/src/library/match.cpp
index e69e144f20..2bb99d4aff 100644
--- a/src/library/match.cpp
+++ b/src/library/match.cpp
@@ -352,6 +352,19 @@ bool match(expr const & p, expr const & t, buffer<optional<expr>> & esubst, buff
         return match_fn(esubst, lsubst, name_generator(*g_tmp_prefix), name_subst, plugin).match(p, t);
 }
 
+match_plugin mk_whnf_match_plugin(type_checker & tc) {
+    return [&](expr const & p, expr const & t, match_context & ctx) { // NOLINT
+        try {
+            constraint_seq cs;
+            expr p1 = tc.whnf(p, cs);
+            expr t1 = tc.whnf(t, cs);
+            return !cs && (p1 != p || t1 != t) && ctx.match(p1, t1);
+        } catch (exception&) {
+            return false;
+        }
+    };
+}
+
 match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> tc) {
     return [=](expr const & p, expr const & t, match_context & ctx) { // NOLINT
         try {
diff --git a/src/library/match.h b/src/library/match.h
index 511b5eaf36..ec1a552f56 100644
--- a/src/library/match.h
+++ b/src/library/match.h
@@ -50,6 +50,7 @@ typedef std::function<bool(expr const &, expr const &, match_context &)> match_p
 
 /** \brief Create a match_plugin that puts terms in weak-head-normal-form before failing */
 match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> tc);
+match_plugin mk_whnf_match_plugin(type_checker & tc);
 
 /**
    \brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p.