From 2c8fd7fb95331aa5e1c1e1155cfc23e84eafff3a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Mar 2024 20:09:15 -0700 Subject: [PATCH] chore: avoid reserved name TODO: update state0 and cleanup --- src/Lean/Elab/Declaration.lean | 3 ++- src/Lean/Elab/DefView.lean | 7 +++++-- src/Lean/Linter/MissingDocs.lean | 2 +- src/Lean/Parser/Command.lean | 6 ++++-- stage0/src/stdlib_flags.h | 2 +- 5 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index c8af67d77a..90e2cf682b 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -42,7 +42,8 @@ private def isNamedDef (stx : Syntax) : Bool := let decl := stx[1] let k := decl.getKind k == ``Lean.Parser.Command.abbrev || - k == ``Lean.Parser.Command.def || + k == ``Lean.Parser.Command.definition || + k == ``Lean.Parser.Command.def || -- TODO: delete k == ``Lean.Parser.Command.theorem || k == ``Lean.Parser.Command.opaque || k == ``Lean.Parser.Command.axiom || diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 246b9987f7..71c1f92429 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -142,7 +142,8 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView := def isDefLike (stx : Syntax) : Bool := let declKind := stx.getKind declKind == ``Parser.Command.abbrev || - declKind == ``Parser.Command.def || + declKind == ``Parser.Command.definition || + declKind == ``Parser.Command.def || -- TODO: delete declKind == ``Parser.Command.theorem || declKind == ``Parser.Command.opaque || declKind == ``Parser.Command.instance || @@ -152,7 +153,9 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := let declKind := stx.getKind if declKind == ``Parser.Command.«abbrev» then return mkDefViewOfAbbrev modifiers stx - else if declKind == ``Parser.Command.def then + else if declKind == ``Parser.Command.definition then + return mkDefViewOfDef modifiers stx + else if declKind == ``Parser.Command.def then -- TODO: delete return mkDefViewOfDef modifiers stx else if declKind == ``Parser.Command.theorem then return mkDefViewOfTheorem modifiers stx diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index e9c6e97882..81930a1a7c 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -123,7 +123,7 @@ def declModifiersPubNoDoc (mods : Syntax) : Bool := def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do if k == ``«abbrev» then lintNamed id "public abbrev" - else if k == ``«def» then lintNamed id "public def" + else if k == ``definition then lintNamed id "public def" else if k == ``«opaque» then lintNamed id "public opaque" else if k == ``«axiom» then lintNamed id "public axiom" else if k == ``«inductive» then lintNamed id "public inductive" diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 1558d097d8..995d55d43f 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -114,7 +114,9 @@ def «abbrev» := leading_parser "abbrev " >> declId >> ppIndent optDeclSig >> declVal def optDefDeriving := optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") -def «def» := leading_parser +def definition := leading_parser + "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving +def «def» := leading_parser -- TODO: delete "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving def «theorem» := leading_parser "theorem " >> recover declId skipUntilWsOrDelim >> ppIndent declSig >> declVal @@ -198,7 +200,7 @@ def «structure» := leading_parser optDeriving @[builtin_command_parser] def declaration := leading_parser declModifiers false >> - («abbrev» <|> «def» <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|> + («abbrev» <|> definition <|> «def» <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure») @[builtin_command_parser] def «deriving» := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", " diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba4..658ab0874e 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -8,7 +8,7 @@ options get_default_options() { // switch to `true` for ABI-breaking changes affecting meta code opts = opts.update({"interpreter", "prefer_native"}, false); // switch to `true` for changing built-in parsers used in quotations - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax // with custom precheck hooks were affected opts = opts.update({"quotPrecheck"}, true);