feat: improvements to test_extern command (leanprover#3075)

Two improvements
[suggested](leanprover#2970 (comment))
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

@@ -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

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"

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

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