From dbe4aa447eb636bde3a5f2641f6c60ce4b60a968 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 May 2020 16:12:53 -0700 Subject: [PATCH] chore: explicit `lbp` at `ParserDescr.symbol` --- src/Init/LeanInit.lean | 4 ++-- src/Lean/Elab/Syntax.lean | 1 + src/Lean/Parser/Parser.lean | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index e9766bf9f7..6895bd8890 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -148,7 +148,7 @@ inductive ParserDescr | sepBy1 : ParserDescr → ParserDescr → ParserDescr | node : Name → ParserDescr → ParserDescr | trailingNode : Name → ParserDescr → ParserDescr -| symbol : String → Option Nat → ParserDescr +| symbol : String → Nat → ParserDescr | nonReservedSymbol : String → Bool → ParserDescr | numLit : ParserDescr | strLit : ParserDescr @@ -157,7 +157,7 @@ inductive ParserDescr | ident : ParserDescr | parser : Name → Nat → ParserDescr -instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol "" none⟩ +instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol "" 0⟩ abbrev TrailingParserDescr := ParserDescr /- Syntax -/ diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index dba38bf277..5de5d9c38d 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -102,6 +102,7 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax if ctx.leadingIdentAsSymbol && rbp?.isNone then `(ParserDescr.nonReservedSymbol $(quote atom) false) else + -- TODO: fix (quote rbp?) `(ParserDescr.symbol $(quote atom) $(quote rbp?)) | none => liftM throwUnsupportedSyntax else if kind == `Lean.Parser.Syntax.num then diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index 17a01d28c2..1730f0eac3 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -1725,7 +1725,7 @@ def compileParserDescr (categories : ParserCategories) : ParserDescr → Except | ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂ | ParserDescr.node k d => node k <$> compileParserDescr d | ParserDescr.trailingNode k d => trailingNode k <$> compileParserDescr d -| ParserDescr.symbol tk lbp => pure $ symbolAux tk lbp +| ParserDescr.symbol tk lbp => pure $ symbol tk lbp | ParserDescr.numLit => pure $ numLit | ParserDescr.strLit => pure $ strLit | ParserDescr.charLit => pure $ charLit