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

feat(library/init/lean/parser/parser): add symbolNoWs trailing parser

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-05 16:22:36 -07:00
parent fa96fb8deb
commit ee5ec98fa9
1 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
library/init/lean/parser/parser.lean
View file

@ -733,6 +733,35 @@ let sym := sym.trim;
{ info := symbolInfo sym lbp,
fn := symbolFn sym }
partial def strAux (sym : String) (errorMsg : String) : Nat → BasicParserFn
| j c s :=
if sym.atEnd j then s
else
let i := s.pos;
let input := c.input;
if input.atEnd i || sym.get j != input.get i then s.mkError errorMsg
else strAux (sym.next j) c (s.next input i)
@[inline] def symbolNoWsFnAux (sym : String) (errorMsg : String) : ParserFn trailing :=
fun leading c s =>
let stx : Syntax := leading;
match stx.getTailInfo with
| some info =>
if info.trailing.stopPos > info.trailing.startPos then
s.mkError errorMsg
else
strAux sym errorMsg 0 c s
| none => s.mkError errorMsg
@[inline] def symbolNoWsFn (sym : String) : ParserFn trailing :=
symbolNoWsFnAux sym ("expected '" ++ sym ++ "' without whitespaces arount it")
/- Similar to `symbol`, but succeeds only if there is no space whitespace after leading term and after `sym`. -/
@[inline] def symbolNoWs (sym : String) (lbp : Option Nat := none) : TrailingParser :=
let sym := sym.trim;
{ info := symbolInfo sym lbp,
fn := symbolNoWsFn sym }
def unicodeSymbolFnAux (sym asciiSym : String) (errorMsg : String) : BasicParserFn :=
satisfySymbolFn (fun s => s == sym || s == asciiSym) errorMsg