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

feat: add antiquotation support for strLit, numLit and charLit

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-22 12:57:28 -08:00
parent 0be31c14ec
commit a5bcebb07f
1 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Lean/Parser/Parser.lean
View file

@ -1070,7 +1070,7 @@ fun _ c s =>
let s := tokenFn c s;
if s.hasError || !(s.stxStack.back.isOfKind numLitKind) then s.mkErrorAt "numeral" iniPos else s
@[inline] def numLit {k : ParserKind} : Parser k :=
@[inline] def numLitNoAntiquot {k : ParserKind} : Parser k :=
{ fn := numLitFn,
info := mkAtomicInfo "numLit" }
@ -1080,7 +1080,7 @@ fun _ c s =>
let s := tokenFn c s;
if s.hasError || !(s.stxStack.back.isOfKind strLitKind) then s.mkErrorAt "string literal" iniPos else s
@[inline] def strLit {k : ParserKind} : Parser k :=
@[inline] def strLitNoAntiquot {k : ParserKind} : Parser k :=
{ fn := strLitFn,
info := mkAtomicInfo "strLit" }
@ -1090,7 +1090,7 @@ fun _ c s =>
let s := tokenFn c s;
if s.hasError || !(s.stxStack.back.isOfKind charLitKind) then s.mkErrorAt "character literal" iniPos else s
@[inline] def charLit {k : ParserKind} : Parser k :=
@[inline] def charLitNoAntiquot {k : ParserKind} : Parser k :=
{ fn := charLitFn,
info := mkAtomicInfo "charLit" }
@ -1476,6 +1476,15 @@ mkAntiquot "ident" `ident <|> identNoAntiquot
def rawIdent {k : ParserKind} : Parser k :=
mkAntiquot "ident" `ident <|> rawIdentNoAntiquot
def numLit {k : ParserKind} : Parser k :=
mkAntiquot "numLit" numLitKind <|> numLitNoAntiquot
def strLit {k : ParserKind} : Parser k :=
mkAntiquot "strLit" strLitKind <|> strLitNoAntiquot
def charLit {k : ParserKind} : Parser k :=
mkAntiquot "charLit" charLitKind <|> charLitNoAntiquot
def categoryParserOfStackFn (offset : Nat) : ParserFn leading :=
fun rbp ctx s =>
let stack := s.stxStack;