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.
113 lines
2.5 KiB
Text
113 lines
2.5 KiB
Text
import Lean
|
||
/-!
|
||
# Testing features of the app delaborator, including overapplication
|
||
-/
|
||
|
||
/-!
|
||
Check that the optional value equality check is specialized to the supplied arguments
|
||
(rather than, formerly, the locally-defined fvars from a telescope).
|
||
-/
|
||
def foo (α : Type) [Inhabited α] (x : α := default) : α := x
|
||
|
||
/-- info: foo Nat : Nat -/
|
||
#guard_msgs in #check foo Nat
|
||
/-- info: foo Nat 1 : Nat -/
|
||
#guard_msgs in #check foo Nat 1
|
||
|
||
/-!
|
||
Check that optional value omission is aware of unfolding.
|
||
-/
|
||
def Ty := (x : Nat := 1) → Fin (x + 1)
|
||
|
||
def f (y : Nat := 2) : Ty := fun x => 0
|
||
|
||
/-- info: f 3 4 : Fin (4 + 1) -/
|
||
#guard_msgs in #check f 3 4
|
||
/-- info: f 3 : Fin (1 + 1) -/
|
||
#guard_msgs in #check f 3
|
||
/-- info: f : Fin (1 + 1) -/
|
||
#guard_msgs in #check (f)
|
||
|
||
|
||
/-!
|
||
Check that overapplied projections pretty print using projection notation.
|
||
-/
|
||
|
||
structure Foo where
|
||
f : Nat → Nat
|
||
|
||
/-- info: ∀ (x : Foo), x.f 1 = 0 : Prop -/
|
||
#guard_msgs in #check ∀ (x : Foo), x.f 1 = 0
|
||
|
||
/-!
|
||
`have` in function position
|
||
-/
|
||
/--
|
||
info: (have f := id;
|
||
f)
|
||
1 : Nat
|
||
-/
|
||
#guard_msgs in #check (have f := id; f) 1
|
||
|
||
/-!
|
||
Overapplied `OfNat.ofNat`
|
||
-/
|
||
instance : OfNat (Nat → Nat) 1 where
|
||
ofNat := id
|
||
|
||
/-- info: 1 2 : Nat -/
|
||
#guard_msgs in #check (1 : Nat → Nat) 2
|
||
|
||
/-!
|
||
Overapplied `dite`
|
||
-/
|
||
|
||
/-- info: (if _h : True then id else id) 1 : Nat -/
|
||
#guard_msgs in #check (if _h : True then id else id) 1
|
||
|
||
|
||
/-!
|
||
Testing that multiple optional arguments are omitted rather than just the last (issue #4812)
|
||
-/
|
||
|
||
def g (a : Nat) (b := 1) (c := 2) (d := 3) := a + b + c + d
|
||
|
||
/-- info: g 0 : Nat -/
|
||
#guard_msgs in #check g 0
|
||
|
||
-- Both the `start` and `stop` arguments are omitted.
|
||
/-- info: fun a => Array.foldl (fun x y => x + y) 0 a : Array Nat → Nat -/
|
||
#guard_msgs in #check fun (a : Array Nat) => a.foldl (fun x y => x + y) 0
|
||
|
||
|
||
/-!
|
||
Testing overriding the app delaborator with an `@[app_delab]`
|
||
-/
|
||
|
||
def myFun (x : Nat) : Nat := x
|
||
|
||
/-- info: myFun 2 : Nat -/
|
||
#guard_msgs in #check myFun 2
|
||
|
||
open Lean PrettyPrinter Delaborator in
|
||
@[app_delab myFun] def delabMyFun : Delab := withOverApp 0 `(id)
|
||
|
||
/-- info: id✝ 2 : Nat -/
|
||
#guard_msgs in #check myFun 2
|
||
|
||
/-!
|
||
Testing `@[app_delab]` error conditions.
|
||
-/
|
||
|
||
/-- error: unknown declaration `noSuchFunction` -/
|
||
#guard_msgs in
|
||
open Lean PrettyPrinter Delaborator in
|
||
@[app_delab noSuchFunction] def delabErr1 : Delab := withOverApp 0 `(id)
|
||
|
||
def A.f := 0
|
||
def B.f := 0
|
||
open A B
|
||
/-- error: ambiguous declaration `f` -/
|
||
#guard_msgs in
|
||
open Lean PrettyPrinter Delaborator in
|
||
@[app_delab f] def delabErr2 : Delab := withOverApp 0 `(id)
|