feat: test_extern command

src/Lean/Util/TestExtern.lean

@@ -0,0 +1,25 @@
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Command
+import Lean.Meta.Tactic.Unfold
+import Lean.Meta.Eval
+
+open Lean Elab Meta Command Term
+
+syntax (name := testExternCmd) "test_extern " term : command
+
+@[command_elab testExternCmd] unsafe def elabTestExtern : CommandElab
+  | `(test_extern $t:term) => liftTermElabM do
+    let t ← elabTermAndSynthesize t none
+    match t.getAppFn with
+    | .const f _ =>
+      if isExtern (← getEnv) f then
+        let t' := (← unfold t f).expr
+        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[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: expects a function application"
+  | _ => throwUnsupportedSyntax

tests/lean/test_extern.lean

@@ -0,0 +1,16 @@
+import Lean.Util.TestExtern
+
+instance : BEq ByteArray where
+  beq x y := x.data == y.data
+
+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
+
+@[extern "lean_nat_add"]
+protected def Nat.not_add : (@& Nat) → (@& Nat) → Nat
+  | a, Nat.zero   => a
+  | a, Nat.succ b => Nat.succ (Nat.add a b)
+
+test_extern Nat.not_add 0 0