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.
102 lines
3.3 KiB
Text
102 lines
3.3 KiB
Text
/-!
|
||
# Add explicit mode projections
|
||
|
||
This is to fix a bug where structure instance notation was not working when there were opt params.
|
||
-/
|
||
|
||
/-!
|
||
Motivating issue from https://github.com/leanprover/lean4/issues/5406
|
||
The `example` had an elaboration error because the structure instance was expanding to `{b := m.b, x := 1}`.
|
||
Now it expands to `{b := @m.b, x := 1}`.
|
||
-/
|
||
structure Methods where
|
||
b : Nat → (opt : Nat := 42) → Nat
|
||
x : Nat
|
||
|
||
example (m : Methods) : Methods := { m with x := 1 }
|
||
|
||
/-- info: fun m => { b := @Methods.b m, x := 1 } : Methods → Methods -/
|
||
#guard_msgs in #check fun (m : Methods) => { m with x := 1 }
|
||
|
||
|
||
/-!
|
||
Tests of explicit mode, with and without arguments.
|
||
-/
|
||
|
||
/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @m.b
|
||
|
||
/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @(m).b
|
||
|
||
/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @m.1
|
||
|
||
/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @(m).1
|
||
|
||
/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @m.b 1
|
||
|
||
/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @(m).b 1
|
||
|
||
/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @m.1 1
|
||
|
||
/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
|
||
#guard_msgs in #check fun (m : Methods) => @(m).1 1
|
||
|
||
|
||
/-!
|
||
Tests of explicit mode with class instances. The type parameter remains implicit.
|
||
We need this so that structure instances work properly.
|
||
-/
|
||
|
||
class C (α : Type) [Inhabited α] where
|
||
f (x : α := default) : α
|
||
x : Nat
|
||
|
||
/-- info: fun inst => C.f : C Nat → Nat -/
|
||
#guard_msgs in #check fun (inst : C Nat) => inst.f
|
||
|
||
/-- info: fun inst => @C.f Nat instInhabitedNat inst : C Nat → optParam Nat default → Nat -/
|
||
#guard_msgs in #check fun (inst : C Nat) => @inst.f
|
||
|
||
/-- info: fun inst => @C.f Nat instInhabitedNat inst : C Nat → optParam Nat default → Nat -/
|
||
#guard_msgs in #check fun (inst : C Nat) => @C.f _ _ inst
|
||
|
||
/-- info: fun inst => { f := @C.f Nat instInhabitedNat inst, x := 1 } : C Nat → C Nat -/
|
||
#guard_msgs in #check fun (inst : C Nat) => { inst with x := 1 }
|
||
|
||
|
||
/-!
|
||
Tests of deeper updates and accesses.
|
||
-/
|
||
|
||
structure A (α : Type) where
|
||
x : α
|
||
structure B (α β : Type) extends A α where
|
||
y : β
|
||
|
||
/-- info: fun α β x' b => { x := x', y := b.y } : (α β : Type) → α → B α β → B α β -/
|
||
#guard_msgs in #check fun (α β) (x' : α) (b : B α β) => {b with x := x'}
|
||
|
||
/-- info: fun α β b => b.x : (α β : Type) → B α β → α -/
|
||
#guard_msgs in #check fun (α β) (b : B α β) => @b.toA.x
|
||
|
||
/-- info: fun α β b => b.x : (α β : Type) → B α β → α -/
|
||
#guard_msgs in #check fun (α β) (b : B α β) => @b.x
|
||
|
||
|
||
/-!
|
||
Tests of implicit arguments in updates.
|
||
-/
|
||
|
||
structure I where
|
||
f : {_ : Nat} → Nat
|
||
x := 1
|
||
|
||
-- used to give `fun i ↦ ?m.369 i : I → I`
|
||
/-- info: fun i => { f := @I.f i } : I → I -/
|
||
#guard_msgs in #check fun (i : I) => {i with x := 1 }
|