diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 5f41bd5b10..0922aef25a 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -53,19 +53,19 @@ private def checkUniverseOffset [Monad m] [MonadError m] [MonadOptions m] (n : N partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do let kind := stx.getKind - if kind == `Lean.Parser.Level.paren then + if kind == ``Lean.Parser.Level.paren then elabLevel (stx.getArg 1) - else if kind == `Lean.Parser.Level.max then + else if kind == ``Lean.Parser.Level.max then let args := stx.getArg 1 |>.getArgs args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl => return mkLevelMax' (← elabLevel stx) lvl - else if kind == `Lean.Parser.Level.imax then + else if kind == ``Lean.Parser.Level.imax then let args := stx.getArg 1 |>.getArgs args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl => return mkLevelIMax' (← elabLevel stx) lvl - else if kind == `Lean.Parser.Level.hole then + else if kind == ``Lean.Parser.Level.hole then mkFreshLevelMVar - else if kind == numLitKind then + else if kind == numLitKind || kind == `num then -- TODO remove staging hack match stx.isNatLit? with | some val => checkUniverseOffset val; return Level.ofNat val | none => throwIllFormedSyntax diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 2aa5b7cf61..604d051c3a 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -209,13 +209,13 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc return stx.setArg 2 lhs |>.setArg 3 rhs else if k == ``Lean.Parser.Term.inaccessible then return stx - else if k == strLitKind then + else if k == strLitKind || k == `str then -- TODO remove staging hack return stx - else if k == numLitKind then + else if k == numLitKind || k == `num then -- TODO remove staging hack return stx else if k == scientificLitKind then return stx - else if k == charLitKind then + else if k == charLitKind || k == `char then -- TODO remove staging hack return stx else if k == ``Lean.Parser.Term.quotedName then /- Quoted names have an elaboration function associated with them, and they will not be macro expanded. diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index defb470b9e..4eb75c72da 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -32,6 +32,12 @@ builtin_initialize registerBuiltinNodeKind scientificLitKind registerBuiltinNodeKind charLitKind registerBuiltinNodeKind nameLitKind + -- TODO remove staging hack + registerBuiltinNodeKind `str + registerBuiltinNodeKind `num + registerBuiltinNodeKind `scientific + registerBuiltinNodeKind `char + registerBuiltinNodeKind `name builtin_initialize builtinParserCategoriesRef : IO.Ref ParserCategories ← IO.mkRef {} diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index fcfc39934b..f48bf02c2e 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -25,6 +25,8 @@ def unreachIsNodeIdent {β info rawVal val preresolved} (h : IsNode (Syntax.iden def isLitKind (k : SyntaxNodeKind) : Bool := k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == scientificLitKind + -- TODO remove staging hack + || k == `str || k == `num || k == `char || k == `name || k == `scientific namespace SyntaxNode