From fdd1cb575160d6b995bc44255c31372ef64d15de Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Apr 2022 11:28:17 -0700 Subject: [PATCH] chore: remove workarounds for #1090 --- src/Init/Meta.lean | 14 +------------- src/Init/Prelude.lean | 25 +++---------------------- src/Lean/Elab/Level.lean | 2 +- src/Lean/Elab/PatternVar.lean | 6 +++--- src/Lean/Elab/Syntax.lean | 16 +--------------- src/Lean/Parser/Basic.lean | 9 +-------- src/Lean/Parser/Extension.lean | 6 ------ src/Lean/Syntax.lean | 3 --- 8 files changed, 10 insertions(+), 71 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index c057fbeff0..37a109a83b 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -524,7 +524,7 @@ def decodeNatLitVal? (s : String) : Option Nat := else if c.isDigit then decodeDecimalLitAux s 0 0 else none -def isLitCore? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String := +def isLit? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String := match stx with | Syntax.node _ k args => if k == litKind && args.size == 1 then @@ -535,18 +535,6 @@ def isLitCore? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String := none | _ => none -def isLit? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String := -- TODO remove staging hack - if litKind == `num || litKind == `numLit then - isLitCore? `num stx <|> isLitCore? `numLit stx - else if litKind == `str || litKind == `strLit then - isLitCore? `str stx <|> isLitCore? `strLit stx - else if litKind == `char || litKind == `charLit then - isLitCore? `char stx <|> isLitCore? `charLit stx - else if litKind == `name || litKind == `nameLit then - isLitCore? `name stx <|> isLitCore? `nameLit stx - else - isLitCore? litKind stx - private def isNatLitAux (litKind : SyntaxNodeKind) (stx : Syntax) : Option Nat := match isLit? litKind stx with | some val => decodeNatLitVal? val diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 2f7a24a18b..b1d1fb57f9 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1873,16 +1873,8 @@ def setKind (stx : Syntax) (k : SyntaxNodeKind) : Syntax := | Syntax.node info _ args => Syntax.node info k args | _ => stx -def isOfKind (stx : Syntax) (k : SyntaxNodeKind) : Bool := -- TODO remove staging hack - cond (or (beq k `num) (beq k `numLit)) - (or (beq stx.getKind `num) (beq stx.getKind `numLit)) - (cond (or (beq k `str) (beq k `strLit)) - (or (beq stx.getKind `str) (beq stx.getKind `strLit)) - (cond (or (beq k `char) (beq k `charLit)) - (or (beq stx.getKind `char) (beq stx.getKind `charLit)) - (cond (or (beq k `name) (beq k `nameLit)) - (or (beq stx.getKind `name) (beq stx.getKind `nameLit)) - (beq stx.getKind k)))) +def isOfKind (stx : Syntax) (k : SyntaxNodeKind) : Bool := + beq stx.getKind k def getArg (stx : Syntax) (i : Nat) : Syntax := match stx with @@ -1924,24 +1916,13 @@ def matchesNull (stx : Syntax) (n : Nat) : Bool := def matchesIdent (stx : Syntax) (id : Name) : Bool := and stx.isIdent (beq stx.getId id) -def matchesLitCore (stx : Syntax) (k : SyntaxNodeKind) (val : String) : Bool := +def matchesLit (stx : Syntax) (k : SyntaxNodeKind) (val : String) : Bool := match stx with | Syntax.node _ k' args => and (beq k k') (match args.getD 0 Syntax.missing with | Syntax.atom _ val' => beq val val' | _ => false) | _ => false -def matchesLit (stx : Syntax) (k : SyntaxNodeKind) (val : String) : Bool := -- TODO remove staging hack - cond (or (beq k `num) (beq k `numLit)) - (or (matchesLitCore stx `num val) (matchesLitCore stx `numLit val)) - (cond (or (beq k `str) (beq k `strLit)) - (or (matchesLitCore stx `str val) (matchesLitCore stx `strLit val)) - (cond (or (beq k `char) (beq k `charLit)) - (or (matchesLitCore stx `char val) (matchesLitCore stx `charLit val)) - (cond (or (beq k `name) (beq k `nameLit)) - (or (matchesLitCore stx `name val) (matchesLitCore stx `nameLit val)) - (matchesLitCore stx k val)))) - def setArgs (stx : Syntax) (args : Array Syntax) : Syntax := match stx with | node info k _ => node info k args diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index e88bfb17b9..23bb7ca3b0 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -65,7 +65,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do return mkLevelIMax' (← elabLevel stx) lvl else if kind == ``Lean.Parser.Level.hole then mkFreshLevelMVar - else if kind == numLitKind || kind == `num || kind == `numLit then -- TODO remove staging hack + else if kind == numLitKind then 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 366c9b78ab..2aa5b7cf61 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 || k == `str || k == `strLit then -- TODO remove staging hack + else if k == strLitKind then return stx - else if k == numLitKind || k == `num || k == `numLit then -- TODO remove staging hack + else if k == numLitKind then return stx else if k == scientificLitKind then return stx - else if k == charLitKind || k == `char || k == `charLit then -- TODO remove staging hack + else if k == charLitKind then 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/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 59946a1248..b674830304 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -339,22 +339,8 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do let stx' ← `($[$doc?:docComment]? def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val) withMacroExpansion stx stx' <| elabCommand stx' --- TODO remove staging hack -def normKindCore (k : SyntaxNodeKind) : SyntaxNodeKind := - if k == `num || k == `numLit then numLitKind - else if k == `char || k == `charLit then charLitKind - else if k == `str || k == `strLit then strLitKind - else if k == `name || k == `nameLit then nameLitKind - else k - --- TODO remove staging hack -def normKind (k : SyntaxNodeKind) : SyntaxNodeKind := - match k with - | Name.str s "antiquot" .. => normKindCore s ++ `antiquot - | _ => k - def checkRuleKind (given expected : SyntaxNodeKind) : Bool := - normKind given == normKind expected || normKind given == normKind (expected ++ `antiquot) + given == expected || given == expected ++ `antiquot def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind | `(matchAltExpr| | $pat:term => $rhs) => do diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 8e98c850c4..14d65dc4a7 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1725,14 +1725,7 @@ instance : Coe String Parser := ⟨fun s => symbol s ⟩ produces the syntax tree for `$e`. -/ def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser := let kind := (kind.getD Name.anonymous) ++ `antiquot - -- TODO remove staging hack - let kindP := - if name == "strLit" then nonReservedSymbol "strLit" <|> nonReservedSymbol "str" - else if name == "numLit" then nonReservedSymbol "numLit" <|> nonReservedSymbol "num" - else if name == "nameLit" then nonReservedSymbol "nameLit" <|> nonReservedSymbol "name" - else if name == "charLit" then nonReservedSymbol "charLit" <|> nonReservedSymbol "char" - else nonReservedSymbol name - let nameP := node `antiquotName $ checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> kindP + let nameP := node `antiquotName $ checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name -- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different -- antiquotation kind via `noImmediateColon` let nameP := if anonymous then nameP <|> checkNoImmediateColon >> pushNone else nameP diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 4eb75c72da..defb470b9e 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -32,12 +32,6 @@ 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 3d5f8ff322..fcfc39934b 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -25,9 +25,6 @@ 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 - || k == `strLit || k == `numLit || k == `charLit || k == `nameLit || k == `scientificLit namespace SyntaxNode