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.
151 lines
3.5 KiB
Lean4
151 lines
3.5 KiB
Lean4
/-!
|
|
# Testing named parent projections for `structure`s
|
|
-/
|
|
|
|
structure S where
|
|
x : Nat
|
|
structure T where
|
|
y : Nat
|
|
structure U where
|
|
x : Nat
|
|
|
|
/-!
|
|
Non-atomic parent projections are not allowed.
|
|
-/
|
|
/-- error: Invalid parent projection name `non.atomic`: Name must be atomic -/
|
|
#guard_msgs in structure S' extends non.atomic : S
|
|
|
|
/-!
|
|
Shadowing other fields is not allowed.
|
|
-/
|
|
/--
|
|
error: Field `x` has already been declared
|
|
|
|
Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection
|
|
-/
|
|
#guard_msgs in structure S' extends x : S
|
|
|
|
/-!
|
|
Duplicate parent projections
|
|
-/
|
|
/--
|
|
error: Field `toP` has already been declared
|
|
|
|
Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection
|
|
-/
|
|
#guard_msgs in structure S' extends toP : S, toP : T
|
|
|
|
/-!
|
|
Duplicate parent projections because from different namespaces
|
|
-/
|
|
structure NS1.S
|
|
structure NS2.S
|
|
/--
|
|
error: Field `toS` has already been declared
|
|
|
|
Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection
|
|
-/
|
|
#guard_msgs in structure S' extends NS1.S, NS2.S
|
|
|
|
/-!
|
|
Duplicate parent projections, when there are overlapping fields
|
|
-/
|
|
/--
|
|
error: Field `toS` has already been declared
|
|
|
|
Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection
|
|
-/
|
|
#guard_msgs in structure S' extends S, toS : U
|
|
/--
|
|
error: Field `toP` has already been declared
|
|
|
|
Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection
|
|
-/
|
|
#guard_msgs in structure S' extends toP : S, toP : T
|
|
|
|
/-!
|
|
Duplicate parent projections because from different namespaces, when there are duplicate fields
|
|
-/
|
|
structure NS1.S' where x : Nat
|
|
structure NS2.S' where x : Nat
|
|
/--
|
|
error: Field `toS'` has already been declared
|
|
|
|
Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection
|
|
-/
|
|
#guard_msgs in structure S' extends NS1.S', NS2.S'
|
|
|
|
/-!
|
|
Field conflicts with projection
|
|
-/
|
|
/-- error: Field `toS` has already been declared as a projection for parent `S` -/
|
|
#guard_msgs in structure S' extends S where
|
|
toS : Nat
|
|
|
|
/-!
|
|
Field conflicts with indirect parent projection
|
|
-/
|
|
structure GP where
|
|
structure P extends toGP : GP where
|
|
/--
|
|
error: Field `toGP` has already been declared as a projection for an indirect parent structure `GP`
|
|
|
|
Note: This projection was inherited from this structure's immediate parent `P`
|
|
-/
|
|
#guard_msgs in
|
|
structure C extends P where
|
|
toGP : Unit
|
|
|
|
/-!
|
|
Checking that the projection name is honored.
|
|
-/
|
|
structure S2 extends toTheS : S where
|
|
y : Nat
|
|
/--
|
|
info: structure S2 : Type
|
|
number of parameters: 0
|
|
parents:
|
|
S2.toTheS : S
|
|
fields:
|
|
S.x : Nat
|
|
S2.y : Nat
|
|
constructor:
|
|
S2.mk (toTheS : S) (y : Nat) : S2
|
|
field notation resolution order:
|
|
S2, S
|
|
-/
|
|
#guard_msgs in #print S2
|
|
|
|
/-!
|
|
Checking that the projection name is honored.
|
|
-/
|
|
structure S2' extends toTheS : S, toTheU : U where
|
|
y : Nat
|
|
/--
|
|
info: structure S2' : Type
|
|
number of parameters: 0
|
|
parents:
|
|
S2'.toTheS : S
|
|
S2'.toTheU : U
|
|
fields:
|
|
S.x : Nat
|
|
S2'.y : Nat
|
|
constructor:
|
|
S2'.mk (toTheS : S) (y : Nat) : S2'
|
|
field notation resolution order:
|
|
S2', S, U
|
|
-/
|
|
#guard_msgs in #print S2'
|
|
|
|
/-!
|
|
Structure instances, setting a parent
|
|
-/
|
|
/-- info: { toTheS := s, y := 1 } : S2' -/
|
|
#guard_msgs in variable (s : S) in #check { toTheS := s, y := 1 : S2' }
|
|
/-- info: { x := s.x, y := 1 } : S2' -/
|
|
#guard_msgs in variable (s : U) in #check { toTheU := s, y := 1 : S2' }
|
|
/-- info: { x := 2, y := 1 } : S2' -/
|
|
#guard_msgs in #check { toTheS.x := 2, y := 1 : S2' }
|
|
/-- info: { x := 2, y := 1 } : S2' -/
|
|
#guard_msgs in #check { toTheU.x := 2, y := 1 : S2' }
|