Lean.Data.Parsec

source

inductive Lean.Parsec.ParseResult (α : Type) :

Type

success: {α : Type} → String.Iterator → α → Lean.Parsec.ParseResult α
error: {α : Type} → String.Iterator → String → Lean.Parsec.ParseResult α

source

instance Lean.Parsec.instReprParseResult:

{α : Type} → [inst : Repr α] → Repr (Lean.Parsec.ParseResult α)

Equations

Lean.Parsec.instReprParseResult = { reprPrec := [anonymous] }

source

def Lean.Parsec (α : Type) :

Type

Equations

Lean.Parsec α = (String.Iterator → Lean.Parsec.ParseResult α)

source

instance Lean.Parsec.instInhabitedParsec (α : Type) :

Inhabited (Lean.Parsec α)

Equations

Lean.Parsec.instInhabitedParsec α = { default := fun it => Lean.Parsec.ParseResult.error it "" }

source

@[inline]

def Lean.Parsec.pure {α : Type} (a : α) :

Lean.Parsec α

Equations

Lean.Parsec.pure a it = Lean.Parsec.ParseResult.success it a

source

@[inline]

def Lean.Parsec.bind {α : Type} {β : Type} (f : Lean.Parsec α) (g : α → Lean.Parsec β) :

Lean.Parsec β

Equations

Lean.Parsec.bind f g it = match f it with | Lean.Parsec.ParseResult.success rem a => g a rem | Lean.Parsec.ParseResult.error pos msg => Lean.Parsec.ParseResult.error pos msg

source

instance Lean.Parsec.instMonadParsec:

Monad Lean.Parsec

Equations

Lean.Parsec.instMonadParsec = Monad.mk

source

@[inline]

def Lean.Parsec.fail {α : Type} (msg : String) :

Lean.Parsec α

Equations

Lean.Parsec.fail msg it = Lean.Parsec.ParseResult.error it msg

source

@[inline]

def Lean.Parsec.orElse {α : Type} (p : Lean.Parsec α) (q : Unit → Lean.Parsec α) :

Lean.Parsec α

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def Lean.Parsec.attempt {α : Type} (p : Lean.Parsec α) :

Lean.Parsec α

Equations

One or more equations did not get rendered due to their size.

source

instance Lean.Parsec.instAlternativeParsec:

Alternative Lean.Parsec

Equations

Lean.Parsec.instAlternativeParsec = Alternative.mk (fun {α} => Lean.Parsec.fail "") fun {α} => Lean.Parsec.orElse

source

def Lean.Parsec.expectedEndOfInput:

String

Equations

Lean.Parsec.expectedEndOfInput = "expected end of input"

source

@[inline]

def Lean.Parsec.eof:

Lean.Parsec Unit

Equations

Lean.Parsec.eof it = if String.Iterator.hasNext it = true then Lean.Parsec.ParseResult.error it Lean.Parsec.expectedEndOfInput else Lean.Parsec.ParseResult.success it ()

source

@[inline]

partial def Lean.Parsec.manyCore {α : Type} (p : Lean.Parsec α) (acc : Array α) :

Lean.Parsec (Array α)

source

@[inline]

def Lean.Parsec.many {α : Type} (p : Lean.Parsec α) :

Lean.Parsec (Array α)

Equations

Lean.Parsec.many p = Lean.Parsec.manyCore p #[]

source

@[inline]

def Lean.Parsec.many1 {α : Type} (p : Lean.Parsec α) :

Lean.Parsec (Array α)

Equations

Lean.Parsec.many1 p = do let a ← p Lean.Parsec.manyCore p #[a]

source

@[inline]

partial def Lean.Parsec.manyCharsCore (p : Lean.Parsec Char) (acc : String) :

Lean.Parsec String

source

@[inline]

def Lean.Parsec.manyChars (p : Lean.Parsec Char) :

Lean.Parsec String

Equations

Lean.Parsec.manyChars p = Lean.Parsec.manyCharsCore p ""

source

@[inline]

def Lean.Parsec.many1Chars (p : Lean.Parsec Char) :

Lean.Parsec String

Equations

Lean.Parsec.many1Chars p = do let a ← p Lean.Parsec.manyCharsCore p (Char.toString a)

source

def Lean.Parsec.pstring (s : String) :

Lean.Parsec String

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def Lean.Parsec.skipString (s : String) :

Lean.Parsec Unit

Equations

Lean.Parsec.skipString s = SeqRight.seqRight (Lean.Parsec.pstring s) fun x => pure ()

source

def Lean.Parsec.unexpectedEndOfInput:

String

Equations

Lean.Parsec.unexpectedEndOfInput = "unexpected end of input"

source

@[inline]

def Lean.Parsec.anyChar:

Lean.Parsec Char

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def Lean.Parsec.pchar (c : Char) :

Lean.Parsec Char

Equations

Lean.Parsec.pchar c = Lean.Parsec.attempt do let a ← Lean.Parsec.anyChar if a = c then pure c else Lean.Parsec.fail (toString "expected: '" ++ toString c ++ toString "'")

source

@[inline]

def Lean.Parsec.skipChar (c : Char) :

Lean.Parsec Unit

Equations

Lean.Parsec.skipChar c = SeqRight.seqRight (Lean.Parsec.pchar c) fun x => pure ()

source

@[inline]

def Lean.Parsec.digit:

Lean.Parsec Char

Equations

Lean.Parsec.digit = Lean.Parsec.attempt do let c ← Lean.Parsec.anyChar if Char.ofNat 48 ≤ c ∧ c ≤ Char.ofNat 57 then pure c else Lean.Parsec.fail (toString "digit expected")

source

@[inline]

def Lean.Parsec.hexDigit:

Lean.Parsec Char

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def Lean.Parsec.asciiLetter:

Lean.Parsec Char

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def Lean.Parsec.satisfy (p : Char → Bool) :

Lean.Parsec Char

Equations

Lean.Parsec.satisfy p = Lean.Parsec.attempt do let c ← Lean.Parsec.anyChar if p c = true then pure c else Lean.Parsec.fail "condition not satisfied"

source

@[inline]

def Lean.Parsec.notFollowedBy {α : Type} (p : Lean.Parsec α) :

Lean.Parsec Unit

Equations

One or more equations did not get rendered due to their size.

source

partial def Lean.Parsec.skipWs (it : String.Iterator) :

String.Iterator

source

@[inline]

def Lean.Parsec.peek?:

Lean.Parsec (Option Char)

Equations

Lean.Parsec.peek? it = if String.Iterator.hasNext it = true then Lean.Parsec.ParseResult.success it (some (String.Iterator.curr it)) else Lean.Parsec.ParseResult.success it none

source

@[inline]

def Lean.Parsec.peek!:

Lean.Parsec Char

Equations

Lean.Parsec.peek! = do let discr ← Lean.Parsec.peek? match discr with | some c => pure c | x => Lean.Parsec.fail Lean.Parsec.unexpectedEndOfInput

source

@[inline]

def Lean.Parsec.skip:

Lean.Parsec Unit

Equations

Lean.Parsec.skip it = Lean.Parsec.ParseResult.success (String.Iterator.next it) ()

source

@[inline]

def Lean.Parsec.ws:

Lean.Parsec Unit

Equations

Lean.Parsec.ws it = Lean.Parsec.ParseResult.success (Lean.Parsec.skipWs it) ()