test(tests/playground/parser/parser): add HasAndthen and HasOrelse instances

This commit is contained in:
Leonardo de Moura 2019-04-13 17:07:27 -07:00
parent abaf181495
commit c8a045d69f
2 changed files with 7 additions and 3 deletions

View file

@ -677,12 +677,18 @@ end RecParserFn
@[inline] def andthen {ρ : Type} [ParserFnLift ρ] : AbsParser ρ → AbsParser ρ → AbsParser ρ :=
mapParser₂ andthenInfo andthenFn
instance absParserAndthen {ρ : Type} [ParserFnLift ρ] : HasAndthen (AbsParser ρ) :=
⟨andthen⟩
@[inline] def node {ρ : Type} [ParserFnLift ρ] (k : SyntaxNodeKind) : AbsParser ρ → AbsParser ρ :=
mapParser nodeInfo (nodeFn k)
@[inline] def orelse {ρ : Type} [ParserFnLift ρ] : AbsParser ρ → AbsParser ρ → AbsParser ρ :=
mapParser₂ orelseInfo orelseFn
instance absParserHasOrelse {ρ : Type} [ParserFnLift ρ] : HasOrelse (AbsParser ρ) :=
⟨orelse⟩
@[inline] def try {ρ : Type} [ParserFnLift ρ] : AbsParser ρ → AbsParser ρ :=
mapParser noFirstTokenInfo tryFn

View file

@ -1,7 +1,5 @@
import parser
open Parser
local infix ` ; `:10 := Parser.andthen
local infix ` || `:5 := Parser.orelse
def mkNumPairKind : IO SyntaxNodeKind := nextKind `numPair
@[init mkNumPairKind] constant numPairKind : SyntaxNodeKind := default _
@ -33,7 +31,7 @@ node numSetKind $
"{"; sepBy number ","; "}"
def testParser1 : TermParser :=
many (numPairP || numSetP)
many (numPairP <|> numSetP)
def parenIdentP : TermParser :=
node parenIdentKind $