Documentation

Lean.Data.Parsec

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

Type

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

instance Lean.Parsec.instReprParseResult :

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

Equations

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

noncomputable def Lean.Parsec (α : Type) :

Type

Equations

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

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

Inhabited (Lean.Parsec α)

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lean.Parsec.bind {α : Type} {β : Type} (f : Lean.Parsec α) (g : α → 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

instance Lean.Parsec.instMonadParsec :

Monad Lean.Parsec

Equations

Lean.Parsec.instMonadParsec = Monad.mk

@[inline]

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

Equations

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

@[inline]

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

Equations

Lean.Parsec.orElse p q it = match p it with | Lean.Parsec.ParseResult.success rem a => Lean.Parsec.ParseResult.success rem a | Lean.Parsec.ParseResult.error rem err => if it = rem then q () it else Lean.Parsec.ParseResult.error rem err

@[inline]

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

Equations

Lean.Parsec.attempt p it = match p it with | Lean.Parsec.ParseResult.success rem res => Lean.Parsec.ParseResult.success rem res | Lean.Parsec.ParseResult.error x err => Lean.Parsec.ParseResult.error it err

instance Lean.Parsec.instAlternativeParsec :

Alternative Lean.Parsec

Equations

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

def Lean.Parsec.expectedEndOfInput :

Equations

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

@[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 ()

@[inline]

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

Lean.Parsec (Array α)

@[inline]

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

Lean.Parsec (Array α)

Equations

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

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

@[inline]

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

Lean.Parsec String

@[inline]

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

Lean.Parsec String

Equations

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

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

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

Lean.Parsec String

Equations

Lean.Parsec.pstring s it = let substr := String.Iterator.extract it (String.Iterator.forward it (String.length s)); if substr = s then Lean.Parsec.ParseResult.success (String.Iterator.forward it (String.length s)) substr else Lean.Parsec.ParseResult.error it (toString "expected: " ++ toString s ++ toString "")

@[inline]

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

Lean.Parsec Unit

Equations

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

def Lean.Parsec.unexpectedEndOfInput :

Equations

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

@[inline]

def Lean.Parsec.anyChar :

Lean.Parsec Char

Equations

Lean.Parsec.anyChar it = if String.Iterator.hasNext it = true then Lean.Parsec.ParseResult.success (String.Iterator.next it) (String.Iterator.curr it) else Lean.Parsec.ParseResult.error it Lean.Parsec.unexpectedEndOfInput

@[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 "'")

@[inline]

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

Lean.Parsec Unit

Equations

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

@[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")

@[inline]

def Lean.Parsec.hexDigit :

Lean.Parsec Char

Equations

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

@[inline]

def Lean.Parsec.asciiLetter :

Lean.Parsec Char

Equations

Lean.Parsec.asciiLetter = Lean.Parsec.attempt do let c ← Lean.Parsec.anyChar if Char.ofNat 65 ≤ c ∧ c ≤ Char.ofNat 90 ∨ Char.ofNat 97 ≤ c ∧ c ≤ Char.ofNat 122 then pure c else Lean.Parsec.fail (toString "ASCII letter expected")

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

@[inline]

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

Lean.Parsec Unit

Equations

Lean.Parsec.notFollowedBy p it = match p it with | Lean.Parsec.ParseResult.success x x_1 => Lean.Parsec.ParseResult.error it "" | Lean.Parsec.ParseResult.error x x_1 => Lean.Parsec.ParseResult.success it ()

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

String.Iterator

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

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

@[inline]

def Lean.Parsec.skip :

Lean.Parsec Unit

Equations

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

@[inline]

def Lean.Parsec.ws :

Lean.Parsec Unit

Equations

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