max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improvements to test_extern command (#3075)

Browse source 
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.
This commit is contained in:
Kim Morrison 2024-04-24 13:56:16 +10:00 • committed by GitHub
parent 3990a9b3be
commit 41697dcf6c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 18 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Util/TestExtern.lean
View file

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

3
tests/lean/run/utf8英語.lean
View file

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

10
tests/lean/test_extern.lean
View file

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

4
tests/lean/test_extern.lean.expected.out
View file

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