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

feat: allow constants to be type classes

Browse source 
There no reason against constants to be type classes so it is just the check in `addClass` that is needed to be modified.

Closes #1054
This commit is contained in:
Jakob von Raumer 2022-03-19 13:43:48 +01:00 • committed by Leonardo de Moura
parent 6e94801c00
commit a91f92c11e
2 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/Class.lean
View file

@ -65,7 +65,7 @@ def hasOutParams (env : Environment) (n : Name) : Bool :=
private partial def checkOutParam : Nat → Array FVarId → Expr → Except String Bool
| i, outParams, Expr.forallE _ d b _ =>
if d.isOutParam then
let fvarId := { name := Name.mkNum `_fvar outParams.size }
let fvarId := { name := Name.mkNum `_fvar outParams.size }
let outParams := outParams.push fvarId
let fvar := mkFVar fvarId
let b := b.instantiate1 fvar
@ -76,15 +76,15 @@ private partial def checkOutParam : Nat → Array FVarId → Expr → Except Str
checkOutParam (i+1) outParams b
| i, outParams, e => pure (outParams.size > 0)
def addClass (env : Environment) (clsName : Name) : Except String Environment :=
def addClass (env : Environment) (clsName : Name) : Except String Environment := do
if isClass env clsName then
Except.error s!"class has already been declared '{clsName}'"
else match env.find? clsName with
| none => Except.error ("unknown declaration '" ++ toString clsName ++ "'")
| some decl@(ConstantInfo.inductInfo _) => do
let b ← checkOutParam 1 #[] decl.type
Except.ok (classExtension.addEntry env { name := clsName, hasOutParam := b })
| some _ => Except.error ("invalid 'class', declaration '" ++ toString clsName ++ "' must be inductive datatype or structure")
throw s!"class has already been declared '{clsName}'"
let some decl := env.find? clsName
| throw s!"unknown declaration '{clsName}'"
unless decl matches .inductInfo .. || decl matches .axiomInfo .. do
throw s!"invalid 'class', declaration '{clsName}' must be inductive datatype, structure, or constant"
let b ← checkOutParam 1 #[] decl.type
return classExtension.addEntry env { name := clsName, hasOutParam := b }
private def consumeNLambdas : Nat → Expr → Option Expr
| 0, e => some e

4
tests/lean/class_def_must_fail.lean.expected.out
View file

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