From 41697dcf6cab7ec82723ba404f2bda7a4526bb2b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 24 Apr 2024 13:56:16 +1000
Subject: [PATCH] feat: improvements to test_extern command (#3075)

Two improvements
[suggested](https://github.com/leanprover/lean4/pull/2970#issuecomment-1853436906)
by @digama0 after the initial PR was merged.

* Allow testing `implemented_by` attributes as well.
* Use `DecidableEq` rather than `BEq` for stricter testing.
---
 src/Lean/Util/TestExtern.lean            | 10 ++++++----
 tests/lean/run/utf8英語.lean             |  3 +--
 tests/lean/test_extern.lean              | 10 ++++++++--
 tests/lean/test_extern.lean.expected.out |  4 +++-
 4 files changed, 18 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Util/TestExtern.lean b/src/Lean/Util/TestExtern.lean
index 51d91d6b5b..7e21e50635 100644
--- a/src/Lean/Util/TestExtern.lean
+++ b/src/Lean/Util/TestExtern.lean
@@ -8,8 +8,9 @@ import Lean.Elab.SyntheticMVars
 import Lean.Elab.Command
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Eval
+import Lean.Compiler.ImplementedByAttr
 
-open Lean Elab Meta Command Term
+open Lean Elab Meta Command Term Compiler
 
 syntax (name := testExternCmd) "test_extern " term : command
 
@@ -18,14 +19,15 @@ syntax (name := testExternCmd) "test_extern " term : command
     let t ← elabTermAndSynthesize t none
     match t.getAppFn with
     | .const f _ =>
-      if isExtern (← getEnv) f then
+      let env ← getEnv
+      if isExtern env f || (getImplementedBy? env f).isSome then
         let t' := (← unfold t f).expr
-        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
+        let r := mkApp (.const ``reduceBool []) (← mkDecide (← mkEq t t'))
         if ! (← evalExpr Bool (.const ``Bool []) r) then
           throwError
             ("native implementation did not agree with reference implementation!\n" ++
             m!"Compare the outputs of:\n#eval {t}\n and\n#eval {t'}")
       else
-        throwError "test_extern: {f} does not have an @[extern] attribute"
+        throwError "test_extern: {f} does not have an @[extern] attribute or @[implemented_by] attribute"
     | _ => throwError "test_extern: expects a function application"
   | _ => throwUnsupportedSyntax
diff --git a/tests/lean/run/utf8英語.lean b/tests/lean/run/utf8英語.lean
index 9c2e56571b..39800afd2a 100644
--- a/tests/lean/run/utf8英語.lean
+++ b/tests/lean/run/utf8英語.lean
@@ -1,7 +1,6 @@
 import Lean.Util.TestExtern
 
-instance : BEq ByteArray where
-  beq x y := x.data == y.data
+deriving instance DecidableEq for ByteArray
 
 test_extern String.toUTF8 ""
 test_extern String.toUTF8 "\x00"
diff --git a/tests/lean/test_extern.lean b/tests/lean/test_extern.lean
index ff0522fcdd..bc63ddd9b4 100644
--- a/tests/lean/test_extern.lean
+++ b/tests/lean/test_extern.lean
@@ -1,9 +1,15 @@
 import Lean.Util.TestExtern
 
-instance : BEq ByteArray where
-  beq x y := x.data == y.data
+deriving instance DecidableEq for ByteArray
 
 test_extern Nat.add 12 37
 test_extern 4 + 5
 
 test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6
+
+def f := 3
+
+@[implemented_by f]
+def g := 4
+
+test_extern g
diff --git a/tests/lean/test_extern.lean.expected.out b/tests/lean/test_extern.lean.expected.out
index e9459f3b7a..25c3a995a9 100644
--- a/tests/lean/test_extern.lean.expected.out
+++ b/tests/lean/test_extern.lean.expected.out
@@ -1 +1,3 @@
-test_extern.lean:7:0-7:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute
+test_extern.lean:6:0-6:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute or @[implemented_by] attribute
+test_extern.lean:15:0-15:13: error: native implementation did not agree with reference implementation!
+Compare the outputs of: #eval g  and #eval 4