From 0bbc2ca88478f5eb15cc914e4a6a85ec0ff8b65b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2020 09:05:03 -0800 Subject: [PATCH] feat: elaborate `optDeriving` --- src/Lean/Elab/Declaration.lean | 20 +++++----- src/Lean/Elab/Deriving/Basic.lean | 17 ++++++++ src/Lean/Elab/Inductive.lean | 34 +++++++++++----- src/Lean/Elab/Structure.lean | 56 ++++++++++++++------------- tests/lean/run/derivingInhabited.lean | 32 +++++++++++++++ 5 files changed, 115 insertions(+), 44 deletions(-) diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index ad576592af..7304133217 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -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 := diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index e9b6616abb..81d6e97f21 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -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 diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index d230629865..ebb7ad971d 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -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 diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 5652e709c5..7fe36fe371 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -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 diff --git a/tests/lean/run/derivingInhabited.lean b/tests/lean/run/derivingInhabited.lean index bfa452d582..ab71f0f3ef 100644 --- a/tests/lean/run/derivingInhabited.lean +++ b/tests/lean/run/derivingInhabited.lean @@ -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