From 5ced8867b067bbfd153cdbf39146e63e97792d2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Sep 2020 16:53:25 -0700 Subject: [PATCH] feat: anonymous instances and support for all kinds of definition at `mutual` --- src/Lean/Elab/Command.lean | 1 + src/Lean/Elab/DeclModifiers.lean | 5 ++- src/Lean/Elab/DeclUtil.lean | 8 ++++ src/Lean/Elab/Declaration.lean | 68 +++---------------------------- src/Lean/Elab/Definition.lean | 69 ++++++++++++++++++++++++++++++++ src/Lean/Elab/MutualDef.lean | 37 +++++++---------- 6 files changed, 102 insertions(+), 86 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 4ea6996710..7454867a8c 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -32,6 +32,7 @@ structure State := (scopes : List Scope := [{ kind := "root", header := "" }]) (nextMacroScope : Nat := firstFrontendMacroScope + 1) (maxRecDepth : Nat) +(nextInstIdx : Nat := 1) -- for generating anonymous instance names (ngen : NameGenerator := {}) instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _, maxRecDepth := 0 }⟩ diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 5163c34f1e..cce7bd237d 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich import Lean.Modifiers import Lean.Elab.Attributes import Lean.Elab.Exception +import Lean.Elab.DeclUtil namespace Lean namespace Elab @@ -122,9 +123,9 @@ match visibility with checkNotAlreadyDeclared declName; pure declName - def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (atomicName : Name) : m Name := do -unless (extractMacroScopes atomicName).name.isAtomic $ +let name := (extractMacroScopes atomicName).name; +unless (name.isAtomic || isFreshInstanceName name) $ throwError ("atomic identifier expected '" ++ atomicName ++ "'"); let declName := currNamespace ++ atomicName; applyVisibility modifiers.visibility declName diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean index 994e01d137..77a09b9b78 100644 --- a/src/Lean/Elab/DeclUtil.lean +++ b/src/Lean/Elab/DeclUtil.lean @@ -52,5 +52,13 @@ let binders := stx.getArg 0; let typeSpec := stx.getArg 1; (binders, typeSpec.getArg 1) +def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name := +(env.mainModule ++ `_instance).appendIndexAfter nextIdx + +def isFreshInstanceName (name : Name) : Bool := +match name with +| Name.str _ s _ => "_instance".isPrefixOf s +| _ => false + end Elab end Lean diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 9c8a7b0db2..6ae70ae111 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -59,51 +59,6 @@ else else none -def elabAbbrev (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := -elabDefLike $ mkDefViewOfAbbrev modifiers stx - -def elabDef (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := -elabDefLike $ mkDefViewOfDef modifiers stx - -def elabTheorem (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := -elabDefLike $ mkDefViewOfTheorem modifiers stx - -def elabConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do --- parser! "constant " >> declId >> declSig >> optional declValSimple -let (binders, type) := expandDeclSig (stx.getArg 2); -val ← match (stx.getArg 3).getOptional? with - | some val => pure val - | none => do { - val ← `(arbitrary _); - pure $ Syntax.node `Lean.Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ] - }; -elabDefLike { - ref := stx, kind := DefKind.opaque, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := some type, val := val -} - -def elabInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do --- parser! "instance " >> optional declId >> declSig >> declVal -let (binders, type) := expandDeclSig (stx.getArg 2); -let modifiers := modifiers.addAttribute { name := `instance }; -declId ← match (stx.getArg 1).getOptional? with - | some declId => pure declId - | none => throwError "not implemented yet"; -elabDefLike { - ref := stx, kind := DefKind.def, modifiers := modifiers, - declId := declId, binders := binders, type? := type, val := stx.getArg 3 -} - -def elabExample (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := --- parser! "example " >> declSig >> declVal -let (binders, type) := expandDeclSig (stx.getArg 1); -let id := mkIdentFrom stx `_example; -let declId := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode]; -elabDefLike { - ref := stx, kind := DefKind.example, modifiers := modifiers, - declId := declId, binders := binders, type? := some type, val := stx.getArg 2 -} - def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do -- parser! "axiom " >> declId >> declSig let declId := stx.getArg 1; @@ -193,26 +148,17 @@ fun stx => match expandDeclNamespace? stx with modifiers ← elabModifiers (stx.getArg 0); let decl := stx.getArg 1; let declKind := decl.getKind; - if declKind == `Lean.Parser.Command.abbrev then - elabAbbrev modifiers decl - else if declKind == `Lean.Parser.Command.def then - elabDef modifiers decl - else if declKind == `Lean.Parser.Command.theorem then - elabTheorem modifiers decl - else if declKind == `Lean.Parser.Command.constant then - elabConstant modifiers decl - else if declKind == `Lean.Parser.Command.instance then - elabInstance modifiers decl - else if declKind == `Lean.Parser.Command.axiom then + if declKind == `Lean.Parser.Command.axiom then elabAxiom modifiers decl - else if declKind == `Lean.Parser.Command.example then - elabExample modifiers decl else if declKind == `Lean.Parser.Command.inductive then elabInductive modifiers decl else if declKind == `Lean.Parser.Command.classInductive then elabClassInductive modifiers decl else if declKind == `Lean.Parser.Command.structure then elabStructure modifiers decl + else if isDefLike decl then do + view ← mkDefView modifiers decl; + elabDefLike view else throwError "unexpected declaration" @@ -233,10 +179,8 @@ elabInductiveViews views /- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/ private def isMutualDef (stx : Syntax) : Bool := (stx.getArg 1).getArgs.all $ fun elem => - let decl := elem.getArg 1; - let declKind := decl.getKind; - declKind == `Lean.Parser.Command.def || - declKind == `Lean.Parser.Command.abbrev + let decl := elem.getArg 1; + isDefLike decl private def isMutualPreambleCommand (stx : Syntax) : Bool := let k := stx.getKind; diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean index 42a32a0e88..4516c9a717 100644 --- a/src/Lean/Elab/Definition.lean +++ b/src/Lean/Elab/Definition.lean @@ -64,6 +64,75 @@ let (binders, type) := expandDeclSig (stx.getArg 2); { ref := stx, kind := DefKind.theorem, modifiers := modifiers, declId := stx.getArg 1, binders := binders, type? := some type, val := stx.getArg 3 } +def mkFreshInstanceName : CommandElabM Name := do +s ← get; +let idx := s.nextInstIdx; +modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 }; +pure $ Lean.Elab.mkFreshInstanceName s.env idx + +def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do +-- parser! "constant " >> declId >> declSig >> optional declValSimple +let (binders, type) := expandDeclSig (stx.getArg 2); +val ← match (stx.getArg 3).getOptional? with + | some val => pure val + | none => do { + val ← `(arbitrary _); + pure $ Syntax.node `Lean.Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ] + }; +pure { + ref := stx, kind := DefKind.opaque, modifiers := modifiers, + declId := stx.getArg 1, binders := binders, type? := some type, val := val +} + +def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do +-- parser! "instance " >> optional declId >> declSig >> declVal +let (binders, type) := expandDeclSig (stx.getArg 2); +let modifiers := modifiers.addAttribute { name := `instance }; +declId ← match (stx.getArg 1).getOptional? with + | some declId => pure declId + | none => do { + id ← mkFreshInstanceName; + pure $ Syntax.node `Lean.Parser.Command.declId #[mkIdentFrom stx id, mkNullNode] + }; +pure { + ref := stx, kind := DefKind.def, modifiers := modifiers, + declId := declId, binders := binders, type? := type, val := stx.getArg 3 +} + +def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView := +-- parser! "example " >> declSig >> declVal +let (binders, type) := expandDeclSig (stx.getArg 1); +let id := mkIdentFrom stx `_example; +let declId := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode]; +{ ref := stx, kind := DefKind.example, modifiers := modifiers, + declId := declId, binders := binders, type? := some type, val := stx.getArg 2 } + +def isDefLike (stx : Syntax) : Bool := +let declKind := stx.getKind; +declKind == `Lean.Parser.Command.«abbrev» || +declKind == `Lean.Parser.Command.«def» || +declKind == `Lean.Parser.Command.«theorem» || +declKind == `Lean.Parser.Command.«constant» || +declKind == `Lean.Parser.Command.«instance» || +declKind == `Lean.Parser.Command.«example» + +def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := +let declKind := stx.getKind; +if declKind == `Lean.Parser.Command.«abbrev» then + pure $ mkDefViewOfAbbrev modifiers stx +else if declKind == `Lean.Parser.Command.«def» then + pure $ mkDefViewOfDef modifiers stx +else if declKind == `Lean.Parser.Command.«theorem» then + pure $ mkDefViewOfTheorem modifiers stx +else if declKind == `Lean.Parser.Command.«constant» then + mkDefViewOfConstant modifiers stx +else if declKind == `Lean.Parser.Command.«instance» then + mkDefViewOfInstance modifiers stx +else if declKind == `Lean.Parser.Command.«example» then + pure $ mkDefViewOfExample modifiers stx +else + throwError "unexpected kind of definition" + private def removeUnused (vars : Array Expr) (xs : Array Expr) (e : Expr) (eType : Expr) : TermElabM (LocalContext × LocalInstances × Array Expr) := do let used : CollectFVars.State := {}; diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index d316088659..664675a608 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -23,16 +23,7 @@ structure MutualDefView := namespace Term open Meta -open Command (DefView mkDefViewOfAbbrev mkDefViewOfDef mkDefViewOfTheorem) - -private def mkDefView {m} [Monad m] [MonadError m] (modifiers : Modifiers) (decl : Syntax) : m DefView := -let k := decl.getKind; -if k == `Lean.Parser.Command.«abbrev» then - pure (mkDefViewOfAbbrev modifiers decl) -else if k == `Lean.Parser.Command.«def» then - pure (mkDefViewOfDef modifiers decl) -else - throwError "unexpected kind of definition" +open Command (DefView) def checkModifiers (m₁ m₂ : Modifiers) : TermElabM Unit := do unless (m₁.isUnsafe == m₂.isUnsafe) $ @@ -43,11 +34,9 @@ unless (m₁.isPartial == m₂.isPartial) $ throwError "cannot mix partial and non-partial definitions"; pure () -def elabHeaders (ds : Array Syntax) : TermElabM (Array MutualDefView) := -ds.foldlM - (fun (headers : Array MutualDefView) (d : Syntax) => withRef d do - modifiers ← elabModifiers (d.getArg 0); - view ← mkDefView modifiers (d.getArg 1); +def elabHeaders (views : Array DefView) : TermElabM (Array MutualDefView) := +views.foldlM + (fun (headers : Array MutualDefView) (view : DefView) => withRef view.ref do currNamespace ← getCurrNamespace; currLevelNames ← getLevelNames; ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId currNamespace currLevelNames view.declId view.modifiers; @@ -70,7 +59,7 @@ ds.foldlM throwError "number of parameters mismatch"; unless (levelNames == firstHeader.levelNames) $ throwError "universe parameters mismatch in mutual definition"; - checkModifiers modifiers firstHeader.modifiers; + checkModifiers view.modifiers firstHeader.modifiers; forallTelescopeCompatible type firstHeader.type xs.size fun _ _ _ => pure ()) (fun ex => match ex with | Exception.error ref msg => throw (Exception.error ref ("invalid mutually recursive definitions, " ++ msg)) @@ -78,8 +67,8 @@ ds.foldlM else pure (); pure $ headers.push { - ref := d, - modifiers := modifiers, + ref := view.ref, + modifiers := view.modifiers, kind := view.kind, shortDeclName := shortDeclName, declName := declName, @@ -90,16 +79,20 @@ ds.foldlM }) #[] -def elabMutualDef (vars : Array Expr) (ds : Array Syntax) : TermElabM Unit := do -views ← elabHeaders ds; +def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := do +views ← elabHeaders views; throwError "WIP mutual def" end Term namespace Command -def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := -runTermElabM none fun vars => Term.elabMutualDef vars ds +def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do +views ← ds.mapM fun d => do { + modifiers ← elabModifiers (d.getArg 0); + mkDefView modifiers (d.getArg 1) +}; +runTermElabM none fun vars => Term.elabMutualDef vars views end Command end Elab