From 378dca293efeb99d262cc926824ed969be9d6cab Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Feb 2020 19:49:13 -0800
Subject: [PATCH] test: add `Expr.find?` test

---
 src/Init/Lean/Util/FindExpr.lean | 18 +++++++++---------
 tests/lean/run/replace.lean      | 10 ++++++++++
 2 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/Init/Lean/Util/FindExpr.lean b/src/Init/Lean/Util/FindExpr.lean
index 88d4db3650..1b143f8505 100644
--- a/src/Init/Lean/Util/FindExpr.lean
+++ b/src/Init/Lean/Util/FindExpr.lean
@@ -44,23 +44,23 @@ else do
 unsafe def initCache : State :=
 { keys    := mkArray cacheSize.toNat (cast lcProof ()) }
 
-@[inline] unsafe def findExprUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
+@[inline] unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
 (findM? p cacheSize e).run' initCache
 
 end FindImpl
 
-@[implementedBy FindImpl.findExprUnsafe?]
-partial def findExpr? (p : Expr → Bool) : Expr → Option Expr
+@[implementedBy FindImpl.findUnsafe?]
+partial def find? (p : Expr → Bool) : Expr → Option Expr
 | e =>
   /- This is a reference implementation for the unsafe one above -/
   if p e then some e
   else match e with
-    | Expr.forallE _ d b _   => findExpr? d <|> findExpr? b
-    | Expr.lam _ d b _       => findExpr? d <|> findExpr? b
-    | Expr.mdata _ b _       => findExpr? b
-    | Expr.letE _ t v b _    => findExpr? t <|> findExpr? v <|> findExpr? b
-    | Expr.app f a _         => findExpr? f <|> findExpr? a
-    | Expr.proj _ _ b _      => findExpr? b
+    | Expr.forallE _ d b _   => find? d <|> find? b
+    | Expr.lam _ d b _       => find? d <|> find? b
+    | Expr.mdata _ b _       => find? b
+    | Expr.letE _ t v b _    => find? t <|> find? v <|> find? b
+    | Expr.app f a _         => find? f <|> find? a
+    | Expr.proj _ _ b _      => find? b
     | e                      => none
 
 end Expr
diff --git a/tests/lean/run/replace.lean b/tests/lean/run/replace.lean
index 2fa50cd9be..0e88b620cf 100644
--- a/tests/lean/run/replace.lean
+++ b/tests/lean/run/replace.lean
@@ -14,3 +14,13 @@ e.replace $ fun e => match e with
 #eval replaceTest $ mkBig 4
 
 #eval (replaceTest $ mkBig 128).getAppFn
+
+def findTest (e : Expr) : Option Expr :=
+e.find? $ fun e => match e with
+  | Expr.const c _ _ => c == `g
+  | _ => false
+
+#eval findTest $ mkBig 4
+#eval findTest $ replaceTest $ mkBig 4
+#eval findTest $ mkBig 128
+#eval findTest $ (replaceTest $ mkBig 128)