feat: elaborate optDeriving
This commit is contained in:
Leonardo de Moura
parent
2a653743a1
commit
0bbc2ca884
5 changed files with 115 additions and 44 deletions
|
|
@ -84,7 +84,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
|||
|
||||
/-
|
||||
parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
|
||||
parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor
|
||||
parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor >> optDeriving
|
||||
-/
|
||||
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
|
||||
checkValidInductiveModifier modifiers
|
||||
|
|
@ -105,15 +105,17 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
|
|||
let inferMod := !ctor[3].isNone
|
||||
let (binders, type?) := expandOptDeclSig ctor[4]
|
||||
pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
|
||||
let classes ← getOptDerivingClasses decl[5]
|
||||
pure {
|
||||
ref := decl,
|
||||
modifiers := modifiers,
|
||||
shortDeclName := name,
|
||||
declName := declName,
|
||||
levelNames := levelNames,
|
||||
binders := binders,
|
||||
type? := type?,
|
||||
ctors := ctors
|
||||
ref := decl
|
||||
modifiers := modifiers
|
||||
shortDeclName := name
|
||||
declName := declName
|
||||
levelNames := levelNames
|
||||
binders := binders
|
||||
type? := type?
|
||||
ctors := ctors
|
||||
derivingClasses := classes
|
||||
}
|
||||
|
||||
private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
|
||||
|
|
|
|||
|
|
@ -41,6 +41,23 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandE
|
|||
logException ex
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
structure DerivingClassView where
|
||||
ref : Syntax
|
||||
className : Name
|
||||
|
||||
/- parser! optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") -/
|
||||
def getOptDerivingClasses [Monad m] [MonadRef m] [MonadEnv m] [MonadExceptOf Exception m] [MonadResolveName m] [AddErrorMessageContext m]
|
||||
(optDeriving : Syntax) : m (Array DerivingClassView) := do
|
||||
if optDeriving.isNone then
|
||||
return #[]
|
||||
else
|
||||
optDeriving[0][1].getSepArgs.mapM fun ident => do
|
||||
let className ← resolveGlobalConstNoOverload ident.getId
|
||||
return { ref := ident, className := className }
|
||||
|
||||
def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit :=
|
||||
withRef view.ref do applyDerivingHandlers view.className declNames
|
||||
|
||||
builtin_initialize
|
||||
registerTraceClass `Elab.Deriving
|
||||
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ import Lean.Elab.Command
|
|||
import Lean.Elab.CollectFVars
|
||||
import Lean.Elab.DefView
|
||||
import Lean.Elab.DeclUtil
|
||||
import Lean.Elab.Deriving.Basic
|
||||
|
||||
namespace Lean.Elab.Command
|
||||
open Meta
|
||||
|
|
@ -53,18 +54,19 @@ instance : Inhabited CtorView :=
|
|||
⟨{ ref := arbitrary, modifiers := {}, inferMod := false, declName := arbitrary, binders := arbitrary, type? := none }⟩
|
||||
|
||||
structure InductiveView where
|
||||
ref : Syntax
|
||||
modifiers : Modifiers
|
||||
shortDeclName : Name
|
||||
declName : Name
|
||||
levelNames : List Name
|
||||
binders : Syntax
|
||||
type? : Option Syntax
|
||||
ctors : Array CtorView
|
||||
ref : Syntax
|
||||
modifiers : Modifiers
|
||||
shortDeclName : Name
|
||||
declName : Name
|
||||
levelNames : List Name
|
||||
binders : Syntax
|
||||
type? : Option Syntax
|
||||
ctors : Array CtorView
|
||||
derivingClasses : Array DerivingClassView
|
||||
|
||||
instance : Inhabited InductiveView :=
|
||||
⟨{ ref := arbitrary, modifiers := {}, shortDeclName := arbitrary, declName := arbitrary,
|
||||
levelNames := [], binders := arbitrary, type? := none, ctors := #[] }⟩
|
||||
levelNames := [], binders := arbitrary, type? := none, ctors := #[], derivingClasses := #[] }⟩
|
||||
|
||||
structure ElabHeaderResult where
|
||||
view : InductiveView
|
||||
|
|
@ -488,10 +490,24 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
|
|||
for view in views do
|
||||
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
|
||||
|
||||
private def applyDerivingHandlers (views : Array InductiveView) : CommandElabM Unit := do
|
||||
let mut processed : NameSet := {}
|
||||
for view in views do
|
||||
for classView in view.derivingClasses do
|
||||
let className := classView.className
|
||||
unless processed.contains className do
|
||||
processed := processed.insert className
|
||||
let mut declNames := #[]
|
||||
for view in views do
|
||||
if view.derivingClasses.any fun classView => classView.className == className then
|
||||
declNames := declNames.push view.declName
|
||||
classView.applyHandlers declNames
|
||||
|
||||
def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
|
||||
let view0 := views[0]
|
||||
let ref := view0.ref
|
||||
runTermElabM view0.declName fun vars => withRef ref do
|
||||
mkInductiveDecl vars views
|
||||
applyDerivingHandlers views
|
||||
|
||||
end Lean.Elab.Command
|
||||
|
|
|
|||
|
|
@ -507,7 +507,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
|
|||
addDefaults lctx defaultAuxDecls
|
||||
|
||||
/-
|
||||
parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields
|
||||
parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields >> optDeriving
|
||||
|
||||
where
|
||||
def «extends» := parser! " extends " >> sepBy1 termParser ", "
|
||||
|
|
@ -527,32 +527,36 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
|
|||
let exts := stx[3]
|
||||
let parents := if exts.isNone then #[] else exts[0][1].getSepArgs
|
||||
let optType := stx[4]
|
||||
let derivingClassViews ← getOptDerivingClasses stx[6]
|
||||
let type ← if optType.isNone then `(Sort _) else pure optType[0][1]
|
||||
runTermElabM none fun scopeVars => do
|
||||
let scopeLevelNames ← Term.getLevelNames
|
||||
let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
|
||||
Term.withDeclName declName do
|
||||
let ctor ← expandCtor stx modifiers declName
|
||||
let fields ← expandFields stx modifiers declName
|
||||
Term.withLevelNames allUserLevelNames <| Term.withAutoBoundImplicitLocal <|
|
||||
Term.elabBinders params (catchAutoBoundImplicit := true) fun params => do
|
||||
let params ← Term.addAutoBoundImplicits params
|
||||
let allUserLevelNames ← Term.getLevelNames
|
||||
Term.withAutoBoundImplicitLocal (flag := false) do
|
||||
elabStructureView {
|
||||
ref := stx,
|
||||
modifiers := modifiers,
|
||||
scopeLevelNames := scopeLevelNames,
|
||||
allUserLevelNames := allUserLevelNames,
|
||||
declName := declName,
|
||||
isClass := isClass,
|
||||
scopeVars := scopeVars,
|
||||
params := params,
|
||||
parents := parents,
|
||||
type := type,
|
||||
ctor := ctor,
|
||||
fields := fields
|
||||
}
|
||||
let declName ←
|
||||
runTermElabM none fun scopeVars => do
|
||||
let scopeLevelNames ← Term.getLevelNames
|
||||
let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
|
||||
Term.withDeclName declName do
|
||||
let ctor ← expandCtor stx modifiers declName
|
||||
let fields ← expandFields stx modifiers declName
|
||||
Term.withLevelNames allUserLevelNames <| Term.withAutoBoundImplicitLocal <|
|
||||
Term.elabBinders params (catchAutoBoundImplicit := true) fun params => do
|
||||
let params ← Term.addAutoBoundImplicits params
|
||||
let allUserLevelNames ← Term.getLevelNames
|
||||
Term.withAutoBoundImplicitLocal (flag := false) do
|
||||
elabStructureView {
|
||||
ref := stx
|
||||
modifiers := modifiers
|
||||
scopeLevelNames := scopeLevelNames
|
||||
allUserLevelNames := allUserLevelNames
|
||||
declName := declName
|
||||
isClass := isClass
|
||||
scopeVars := scopeVars
|
||||
params := params
|
||||
parents := parents
|
||||
type := type
|
||||
ctor := ctor
|
||||
fields := fields
|
||||
}
|
||||
return declName
|
||||
derivingClassViews.forM fun view => view.applyHandlers #[declName]
|
||||
|
||||
builtin_initialize registerTraceClass `Elab.structure
|
||||
|
||||
|
|
|
|||
|
|
@ -15,3 +15,35 @@ deriving instance Inhabited for Bla
|
|||
|
||||
def ex2 [Inhabited α] : Inhabited (Foo α β) :=
|
||||
inferInstance
|
||||
|
||||
structure Point (α : Type) where
|
||||
x : α
|
||||
y : α
|
||||
deriving Inhabited
|
||||
|
||||
def ex3 [Inhabited α] : Inhabited (Point α) :=
|
||||
inferInstance
|
||||
|
||||
inductive Lst (α : Type) where
|
||||
| nil
|
||||
| cons : α → Lst α → Lst α
|
||||
deriving Inhabited
|
||||
|
||||
def ex4 : Inhabited (Lst α) :=
|
||||
inferInstance
|
||||
|
||||
mutual
|
||||
|
||||
inductive FooLst (α : Type) where
|
||||
| nil
|
||||
| cons : Boo α → FooLst α → FooLst α
|
||||
deriving Inhabited
|
||||
|
||||
inductive Boo (α : Type) where
|
||||
| node : FooLst α → Boo α
|
||||
deriving Inhabited
|
||||
|
||||
end
|
||||
|
||||
def ex5 : Inhabited (Boo α) :=
|
||||
inferInstance
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue