max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: explicit lbp at ParserDescr.symbol

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-27 16:12:53 -07:00
parent 6e5cd5fcc0
commit dbe4aa447e
3 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/LeanInit.lean
View file

@ -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 -/

1
src/Lean/Elab/Syntax.lean
View file

@ -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

2
src/Lean/Parser/Parser.lean
View file

@ -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