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

fix: reject [class] at declarations that are not inductive datatypes or structures

Browse source 
closes #42
This commit is contained in:
Leonardo de Moura 2019-10-21 22:52:13 -07:00
parent d8a3dfb63d
commit 1418f12248
7 changed files with 45 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/Init/Lean/Class.lean
View file

@ -91,7 +91,8 @@ def addClass (env : Environment) (clsName : Name) : Except String Environment :=
if isClass env clsName then Except.error ("class has already been declared '" ++ toString clsName ++ "'")
else match env.find clsName with
| none => Except.error ("unknown declaration '" ++ toString clsName ++ "'")
| some decl => Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName decl.type.hasOutParam))
| some decl@(ConstantInfo.inductInfo _) => Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName decl.type.hasOutParam))
| some _ => Except.error ("invalid 'class', declaration '" ++ toString clsName ++ "' must be inductive datatype or structure")
private def consumeNLambdas : Nat → Expr → Option Expr
| 0, e => some e

7
tests/lean/class_def_must_fail.lean Normal file
View file

@ -0,0 +1,7 @@
/- The following definition should fail. -/
@[class] def Foo (n : Nat) : Prop := n > 2
def Bla (n : Nat) : Prop := n > 2
attribute [class] Bla

2
tests/lean/class_def_must_fail.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
class_def_must_fail.lean:2:13: error: invalid 'class', declaration 'Foo' must be inductive datatype or structure
class_def_must_fail.lean:7:0: error: invalid 'class', declaration 'Bla' must be inductive datatype or structure

5
tests/lean/fail/typeclass_outparam.lean
View file

@ -1,5 +1,4 @@
@[class] axiom OPClass (α : outParam Type) (β : Type) : Type
@[instance] axiom op₁ : OPClass Nat Nat
class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ())
instance op₁ : OPClass Nat Nat := {}
#synth OPClass Bool Nat

11
tests/lean/run/typeclass_append.lean
View file

@ -6,9 +6,14 @@ Authors: Daniel Selsam
Performance test to ensure quadratic blowup is avoided.
-/
@[class] axiom Append {α : Type} (xs₁ xs₂ : List α) (out : outParam $ List α) : Type
@[instance] axiom AppendBase {α : Type} (xs₂ : List α) : Append [] xs₂ xs₂
@[instance] axiom AppendStep {α : Type} (x : α) (xs₁ xs₂ out : List α) [Append xs₁ xs₂ out] : Append (x::xs₁) xs₂ (x::out)
class Append {α : Type} (xs₁ xs₂ : List α) (out : outParam $ List α) : Type :=
(u : Unit := ())
instance AppendBase {α : Type} (xs₂ : List α) : Append [] xs₂ xs₂ :=
{}
instance AppendStep {α : Type} (x : α) (xs₁ xs₂ out : List α) [Append xs₁ xs₂ out] : Append (x::xs₁) xs₂ (x::out) :=
{}
#synth Append
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199]

44
tests/lean/run/typeclass_diamond.lean
View file

@ -1,30 +1,30 @@
@[class] axiom Top₁ (n : Nat) : Type
@[class] axiom Bot₁ (n : Nat) : Type
@[class] axiom Left₁ (n : Nat) : Type
@[class] axiom Right₁ (n : Nat) : Type
class Top₁ (n : Nat) : Type := (u : Unit := ())
class Bot₁ (n : Nat) : Type := (u : Unit := ())
class Left₁ (n : Nat) : Type := (u : Unit := ())
class Right₁ (n : Nat) : Type := (u : Unit := ())
@[instance] axiom Bot₁Inst : Bot₁ Nat.zero
instance Bot₁Inst : Bot₁ Nat.zero := {}
instance Left₁ToBot₁ (n : Nat) [Left₁ n] : Bot₁ n := {}
@[instance] axiom Left₁ToBot₁ (n : Nat) [Left₁ n] : Bot₁ n
@[instance] axiom Right₁ToBot₁ (n : Nat) [Right₁ n] : Bot₁ n
@[instance] axiom Top₁ToLeft₁ (n : Nat) [Top₁ n] : Left₁ n
@[instance] axiom Top₁ToRight₁ (n : Nat) [Top₁ n] : Right₁ n
@[instance] axiom Bot₁ToTopSucc (n : Nat) [Bot₁ n] : Top₁ n.succ
instance Right₁ToBot₁ (n : Nat) [Right₁ n] : Bot₁ n := {}
instance Top₁ToLeft₁ (n : Nat) [Top₁ n] : Left₁ n := {}
instance Top₁ToRight₁ (n : Nat) [Top₁ n] : Right₁ n := {}
instance Bot₁ToTopSucc (n : Nat) [Bot₁ n] : Top₁ n.succ := {}
@[class] axiom Top₂ (n : Nat) : Type
@[class] axiom Bot₂ (n : Nat) : Type
@[class] axiom Left₂ (n : Nat) : Type
@[class] axiom Right₂ (n : Nat) : Type
class Top₂ (n : Nat) : Type := (u : Unit := ())
class Bot₂ (n : Nat) : Type := (u : Unit := ())
class Left₂ (n : Nat) : Type := (u : Unit := ())
class Right₂ (n : Nat) : Type := (u : Unit := ())
@[instance] axiom Left₂ToBot₂ (n : Nat) [Left₂ n] : Bot₂ n
@[instance] axiom Right₂ToBot₂ (n : Nat) [Right₂ n] : Bot₂ n
@[instance] axiom Top₂ToLeft₂ (n : Nat) [Top₂ n] : Left₂ n
@[instance] axiom Top₂ToRight₂ (n : Nat) [Top₂ n] : Right₂ n
@[instance] axiom Bot₂ToTopSucc (n : Nat) [Bot₂ n] : Top₂ n.succ
instance Left₂ToBot₂ (n : Nat) [Left₂ n] : Bot₂ n := {}
instance Right₂ToBot₂ (n : Nat) [Right₂ n] : Bot₂ n := {}
instance Top₂ToLeft₂ (n : Nat) [Top₂ n] : Left₂ n := {}
instance Top₂ToRight₂ (n : Nat) [Top₂ n] : Right₂ n := {}
instance Bot₂ToTopSucc (n : Nat) [Bot₂ n] : Top₂ n.succ := {}
@[class] axiom Top (n : Nat) : Type
class Top (n : Nat) : Type := (u : Unit := ())
@[instance] axiom Top₁ToTop (n : Nat) [Top₁ n] : Top n
@[instance] axiom Top₂ToTop (n : Nat) [Top₂ n] : Top n
instance Top₁ToTop (n : Nat) [Top₁ n] : Top n := {}
instance Top₂ToTop (n : Nat) [Top₂ n] : Top n := {}
#synth Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ

4
tests/lean/run/typeclass_outparam.lean
View file

@ -1,5 +1,5 @@
@[class] axiom OPClass (α : outParam Type) (β : Type) : Type
class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ())
@[instance] axiom op₁ : OPClass Nat Nat
instance op₁ : OPClass Nat Nat := {}
#synth OPClass Nat Nat