mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
108 lines
2.6 KiB
Lean4
108 lines
2.6 KiB
Lean4
import Lean
|
||
|
||
/-- Foo structure is just a test -/
|
||
structure Foo where
|
||
/-- main name -/ name : String := "hello"
|
||
/-- documentation for the second field -/ val : Nat := 0
|
||
|
||
/-- documenting test axiom -/
|
||
axiom myAxiom : Nat
|
||
|
||
structure Boo (α : Type) where
|
||
/-- Boo constructor has a custom name -/
|
||
makeBoo ::
|
||
/-- Boo.x docString -/ x : Nat
|
||
y : Bool
|
||
|
||
/-- inductive datatype Tree documentation -/
|
||
inductive Tree (α : Type) where
|
||
/-- Tree.node documentation -/ | node : List (Tree α) → Tree α
|
||
/-- Tree.leaf stores the values -/ | leaf : α → Tree α
|
||
|
||
namespace Bla
|
||
|
||
/-- documenting definition in namespace -/
|
||
def test (x : Nat) : Nat :=
|
||
aux x + 1
|
||
where
|
||
/-- We can document 'where' functions too
|
||
|
||
... and indentation is stripped, even after an empty line. -/
|
||
aux x := x + 2
|
||
|
||
end Bla
|
||
|
||
def f (x : Nat) : IO Nat := do
|
||
let rec /-- let rec documentation at f -/ foo
|
||
| 0 => 1
|
||
| x+1 => foo x + 2
|
||
return foo x
|
||
|
||
def g (x : Nat) : Nat :=
|
||
let rec /-- let rec documentation at g -/ foo
|
||
| 0 => 1
|
||
| x+1 => foo x + 2
|
||
foo x
|
||
|
||
open Lean
|
||
|
||
def printDocString (declName : Name) : MetaM Unit := do
|
||
match (← findDocString? (← getEnv) declName) with
|
||
| some docStr => IO.println (repr docStr)
|
||
| none => IO.println s!"doc string for '{declName}' is not available"
|
||
|
||
def printDocStringTest : MetaM Unit := do
|
||
printDocString `Foo
|
||
printDocString `Foo.name
|
||
printDocString `Foo.val
|
||
printDocString `myAxiom
|
||
printDocString `Boo
|
||
printDocString `Boo.makeBoo
|
||
printDocString `Boo.x
|
||
printDocString `Boo.y
|
||
printDocString `Tree
|
||
printDocString `Tree.node
|
||
printDocString `Tree.leaf
|
||
printDocString `Bla.test
|
||
printDocString `Bla.test.aux
|
||
printDocString `f
|
||
printDocString `f.foo
|
||
printDocString `g
|
||
printDocString `g.foo
|
||
printDocString `optParam
|
||
printDocString `namedPattern
|
||
printDocString `Lean.Meta.forallTelescopeReducing
|
||
|
||
#eval printDocStringTest
|
||
|
||
def printRanges (declName : Name) : MetaM Unit := do
|
||
match (← findDeclarationRanges? declName) with
|
||
| some range => IO.println f!"{declName} :={Std.Format.indentD <| repr range}"
|
||
| none => IO.println s!"range for '{declName}' is not available"
|
||
|
||
def printRangesTest : MetaM Unit := do
|
||
printRanges `Foo
|
||
printRanges `Foo.name
|
||
printRanges `Foo.val
|
||
printRanges `myAxiom
|
||
printRanges `Boo
|
||
printRanges `Boo.makeBoo
|
||
printRanges `Boo.x
|
||
printRanges `Boo.y
|
||
printRanges `Tree
|
||
printRanges `Tree.rec
|
||
printRanges `Tree.casesOn
|
||
printRanges `Tree.node
|
||
printRanges `Tree.leaf
|
||
printRanges `Bla.test
|
||
printRanges `Bla.test.aux
|
||
printRanges `f
|
||
printRanges `f.foo
|
||
printRanges `g
|
||
printRanges `g.foo
|
||
|
||
#eval printRangesTest
|
||
|
||
/-- no dice -/
|
||
add_decl_doc Nat.add
|