Lean.Data.Xml.Parser

source

@[inline]

abbrev Lean.Xml.Parser.LeanChar :

Type

Equations

Lean.Xml.Parser.LeanChar = Char

source

def Lean.Xml.Parser.endl :

Lean.Parsec Lean.Xml.Parser.LeanChar

Equations

Lean.Xml.Parser.endl = SeqRight.seqRight (HOrElse.hOrElse (Lean.Parsec.skipString "\x0d\n") fun x => HOrElse.hOrElse (Lean.Parsec.skipChar (Char.ofNat 13)) fun x => Lean.Parsec.skipChar (Char.ofNat 10)) fun x => pure (Char.ofNat 10)

source

def Lean.Xml.Parser.quote {α : Type} (p : Lean.Parsec α) :

Lean.Parsec α

Equations

Lean.Xml.Parser.quote p = HOrElse.hOrElse (SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 39)) fun x => p) fun x => Lean.Parsec.skipChar (Char.ofNat 39)) fun x => SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 34)) fun x => p) fun x => Lean.Parsec.skipChar (Char.ofNat 34)

source

def Lean.Xml.Parser.Char :

Lean.Parsec Lean.Xml.Parser.LeanChar

Equations

Lean.Xml.Parser.Char = HOrElse.hOrElse (Lean.Parsec.attempt do let c ← Lean.Parsec.anyChar let cNat ← pure (Char.toNat c) if 32 ≤ cNat ∧ cNat ≤ 55295 ∨ 57344 ≤ cNat ∧ cNat ≤ 65533 ∨ 65536 ≤ cNat ∧ cNat ≤ 1114111 then pure c else Lean.Parsec.fail "expected xml char") fun x => HOrElse.hOrElse (Lean.Parsec.pchar (Char.ofNat 9)) fun x => Lean.Xml.Parser.endl

source

def Lean.Xml.Parser.S :

Lean.Parsec String

Equations

Lean.Xml.Parser.S = Lean.Parsec.many1Chars (HOrElse.hOrElse (Lean.Parsec.pchar (Char.ofNat 32)) fun x => HOrElse.hOrElse Lean.Xml.Parser.endl fun x => Lean.Parsec.pchar (Char.ofNat 9))

source

def Lean.Xml.Parser.Eq :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.Eq = SeqLeft.seqLeft (SeqRight.seqRight (optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 61)) fun x => optional Lean.Xml.Parser.S

source

def Lean.Xml.Parser.NameStartChar :

Lean.Parsec Lean.Xml.Parser.LeanChar

Equations

Lean.Xml.Parser.NameStartChar = 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 if c = Char.ofNat 58 ∨ c = Char.ofNat 95 then pure c else let cNum := Char.toNat c; if Array.any Lean.Xml.Parser.nameStartCharRanges (fun x => match x with | (lo, hi) => decide (lo ≤ cNum ∧ cNum ≤ hi)) 0 (Array.size Lean.Xml.Parser.nameStartCharRanges) = true then pure c else Lean.Parsec.fail "expected a name character"

source

def Lean.Xml.Parser.NameChar :

Lean.Parsec Lean.Xml.Parser.LeanChar

Equations

Lean.Xml.Parser.NameChar = HOrElse.hOrElse Lean.Xml.Parser.NameStartChar fun x => HOrElse.hOrElse Lean.Parsec.digit fun x => HOrElse.hOrElse (Lean.Parsec.pchar (Char.ofNat 45)) fun x => HOrElse.hOrElse (Lean.Parsec.pchar (Char.ofNat 46)) fun x => HOrElse.hOrElse (Lean.Parsec.pchar (Char.ofNat 183)) fun x => Lean.Parsec.satisfy fun c => decide (Char.ofNat 768 ≤ c ∧ c ≤ Char.ofNat 879 ∨ Char.ofNat 8255 ≤ c ∧ c ≤ Char.ofNat 8256)

source

def Lean.Xml.Parser.Name :

Lean.Parsec String

Equations

Lean.Xml.Parser.Name = do let x ← Lean.Xml.Parser.NameStartChar Lean.Parsec.manyCharsCore Lean.Xml.Parser.NameChar (Char.toString x)

source

def Lean.Xml.Parser.VersionNum :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.VersionNum = SeqLeft.seqLeft (Lean.Parsec.skipString "1.") fun x => Lean.Parsec.many1 Lean.Parsec.digit

source

def Lean.Xml.Parser.VersionInfo :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.VersionInfo = do SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Parsec.skipString "version" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.VersionNum

source

def Lean.Xml.Parser.EncName :

Lean.Parsec String

Equations

Lean.Xml.Parser.EncName = do let x ← Lean.Parsec.asciiLetter Lean.Parsec.manyCharsCore (HOrElse.hOrElse Lean.Parsec.asciiLetter fun x => HOrElse.hOrElse Lean.Parsec.digit fun x => HOrElse.hOrElse (Lean.Parsec.pchar (Char.ofNat 45)) fun x => HOrElse.hOrElse (Lean.Parsec.pchar (Char.ofNat 95)) fun x => Lean.Parsec.pchar (Char.ofNat 46)) (Char.toString x)

source

def Lean.Xml.Parser.EncodingDecl :

Lean.Parsec String

Equations

Lean.Xml.Parser.EncodingDecl = do SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Parsec.skipString "encoding" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.EncName

source

def Lean.Xml.Parser.SDDecl :

Lean.Parsec String

Equations

Lean.Xml.Parser.SDDecl = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Parsec.skipString "standalone") fun x => Lean.Xml.Parser.Eq) fun x => Lean.Xml.Parser.quote (HOrElse.hOrElse (Lean.Parsec.pstring "yes") fun x => Lean.Parsec.pstring "no")

source

def Lean.Xml.Parser.XMLdecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.XMLdecl = do Lean.Parsec.skipString " Lean.Xml.Parser.VersionInfo SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (optional Lean.Xml.Parser.EncodingDecl) fun x => optional Lean.Xml.Parser.SDDecl) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipString "?>"

source

def Lean.Xml.Parser.Comment :

Lean.Parsec String

Equations

Lean.Xml.Parser.Comment = let notDash := Char.toString <$> Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 45); SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.skipString ""

source

def Lean.Xml.Parser.PITarget :

Lean.Parsec String

Equations

Lean.Xml.Parser.PITarget = SeqLeft.seqLeft (SeqLeft.seqLeft (SeqLeft.seqLeft Lean.Xml.Parser.Name fun x => HOrElse.hOrElse (Lean.Parsec.skipChar (Char.ofNat 88)) fun x => Lean.Parsec.skipChar (Char.ofNat 120)) fun x => HOrElse.hOrElse (Lean.Parsec.skipChar (Char.ofNat 77)) fun x => Lean.Parsec.skipChar (Char.ofNat 109)) fun x => HOrElse.hOrElse (Lean.Parsec.skipChar (Char.ofNat 76)) fun x => Lean.Parsec.skipChar (Char.ofNat 108)

source

def Lean.Xml.Parser.PI :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.PI = do SeqLeft.seqLeft (SeqLeft.seqLeft (Lean.Parsec.skipString ") fun x => Lean.Xml.Parser.PITarget) fun x => optional (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Parsec.manyChars (SeqRight.seqRight (Lean.Parsec.notFollowedBy (Lean.Parsec.skipString "?>")) fun x => Lean.Xml.Parser.Char)) Lean.Parsec.skipString "?>"

source

def Lean.Xml.Parser.Misc :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.Misc = HOrElse.hOrElse (SeqRight.seqRight Lean.Xml.Parser.Comment fun x => pure ()) fun x => HOrElse.hOrElse Lean.Xml.Parser.PI fun x => SeqRight.seqRight Lean.Xml.Parser.S fun x => pure ()

source

def Lean.Xml.Parser.SystemLiteral :

Lean.Parsec String

Equations

Lean.Xml.Parser.SystemLiteral = HOrElse.hOrElse (SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.pchar (Char.ofNat 34)) fun x => Lean.Parsec.manyChars (Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 34))) fun x => Lean.Parsec.pchar (Char.ofNat 34)) fun x => SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.pchar (Char.ofNat 39)) fun x => Lean.Parsec.manyChars (Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 39))) fun x => pure (Char.ofNat 39)

source

def Lean.Xml.Parser.PubidChar :

Lean.Parsec Lean.Xml.Parser.LeanChar

Equations

Lean.Xml.Parser.PubidChar = HOrElse.hOrElse Lean.Parsec.asciiLetter fun x => HOrElse.hOrElse Lean.Parsec.digit fun x => HOrElse.hOrElse Lean.Xml.Parser.endl fun x => Lean.Parsec.attempt do let c ← Lean.Parsec.anyChar if String.contains "-'()+,./:=?;!*#@$_%" c = true then pure c else Lean.Parsec.fail "PublidChar expected"

source

def Lean.Xml.Parser.PubidLiteral :

Lean.Parsec String

Equations

Lean.Xml.Parser.PubidLiteral = HOrElse.hOrElse (SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.pchar (Char.ofNat 34)) fun x => Lean.Parsec.manyChars Lean.Xml.Parser.PubidChar) fun x => Lean.Parsec.pchar (Char.ofNat 34)) fun x => SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.pchar (Char.ofNat 39)) fun x => Lean.Parsec.manyChars (Lean.Parsec.attempt do let c ← Lean.Xml.Parser.PubidChar if c = Char.ofNat 39 then Lean.Parsec.fail "'\\'' not expected" else pure c)) fun x => Lean.Parsec.pchar (Char.ofNat 39)

source

def Lean.Xml.Parser.ExternalID :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.ExternalID = HOrElse.hOrElse (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipString "SYSTEM") fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.SystemLiteral) fun x => pure ()) fun x => SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipString "PUBLIC") fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.PubidLiteral) fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.SystemLiteral) fun x => pure ()

source

def Lean.Xml.Parser.Mixed :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.Mixed = HOrElse.hOrElse (do Lean.Parsec.skipChar (Char.ofNat 40) SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipString "#PCDATA") fun x => Lean.Parsec.many (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 124)) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Name)) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipString ")*") fun x => SeqLeft.seqLeft (SeqLeft.seqLeft (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 40)) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipString "#PCDATA") fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 41)

source

partial def Lean.Xml.Parser.cp :

Lean.Parsec Unit

source

partial def Lean.Xml.Parser.choice :

Lean.Parsec Unit

source

partial def Lean.Xml.Parser.seq :

Lean.Parsec Unit

source

def Lean.Xml.Parser.children :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.children = SeqLeft.seqLeft (HOrElse.hOrElse Lean.Xml.Parser.choice fun x => Lean.Xml.Parser.seq) fun x => optional (HOrElse.hOrElse (Lean.Parsec.skipChar (Char.ofNat 63)) fun x => HOrElse.hOrElse (Lean.Parsec.skipChar (Char.ofNat 42)) fun x => Lean.Parsec.skipChar (Char.ofNat 43))

source

def Lean.Xml.Parser.contentspec :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.contentspec = HOrElse.hOrElse (Lean.Parsec.skipString "EMPTY") fun x => HOrElse.hOrElse (Lean.Parsec.skipString "ANY") fun x => HOrElse.hOrElse Lean.Xml.Parser.Mixed fun x => Lean.Xml.Parser.children

source

def Lean.Xml.Parser.elementDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.elementDecl = do Lean.Parsec.skipString " SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Xml.Parser.Name) fun x => Lean.Xml.Parser.contentspec) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 62)

source

def Lean.Xml.Parser.StringType :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.StringType = Lean.Parsec.skipString "CDATA"

source

def Lean.Xml.Parser.TokenizedType :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.TokenizedType = HOrElse.hOrElse (Lean.Parsec.skipString "ID") fun x => HOrElse.hOrElse (Lean.Parsec.skipString "IDREF") fun x => HOrElse.hOrElse (Lean.Parsec.skipString "IDREFS") fun x => HOrElse.hOrElse (Lean.Parsec.skipString "ENTITY") fun x => HOrElse.hOrElse (Lean.Parsec.skipString "ENTITIES") fun x => HOrElse.hOrElse (Lean.Parsec.skipString "NMTOKEN") fun x => Lean.Parsec.skipString "NMTOKENS"

source

def Lean.Xml.Parser.NotationType :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.NotationType = do Lean.Parsec.skipString "NOTATION" SeqLeft.seqLeft (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Parsec.skipChar (Char.ofNat 40)) fun x => optional Lean.Xml.Parser.S SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight Lean.Xml.Parser.Name fun x => Lean.Parsec.many (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 124)) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Name)) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 41)

source

def Lean.Xml.Parser.Nmtoken :

Lean.Parsec String

Equations

Lean.Xml.Parser.Nmtoken = Lean.Parsec.many1Chars Lean.Xml.Parser.NameChar

source

def Lean.Xml.Parser.Enumeration :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.Enumeration = do Lean.Parsec.skipChar (Char.ofNat 40) SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (optional Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Nmtoken) fun x => Lean.Parsec.many (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 124)) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Nmtoken)) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 41)

source

def Lean.Xml.Parser.EnumeratedType :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.EnumeratedType = HOrElse.hOrElse Lean.Xml.Parser.NotationType fun x => Lean.Xml.Parser.Enumeration

source

def Lean.Xml.Parser.AttType :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.AttType = HOrElse.hOrElse Lean.Xml.Parser.StringType fun x => HOrElse.hOrElse Lean.Xml.Parser.TokenizedType fun x => Lean.Xml.Parser.EnumeratedType

source

def Lean.Xml.Parser.predefinedEntityToChar :

String → Option Lean.Xml.Parser.LeanChar

Equations

Lean.Xml.Parser.predefinedEntityToChar x = match x with | "lt" => some (Char.ofNat 60) | "gt" => some (Char.ofNat 62) | "amp" => some (Char.ofNat 38) | "apos" => some (Char.ofNat 39) | "quot" => some (Char.ofNat 34) | x => none

source

def Lean.Xml.Parser.EntityRef :

Lean.Parsec (Option Lean.Xml.Parser.LeanChar)

Equations

Lean.Xml.Parser.EntityRef = Lean.Parsec.attempt (SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 38)) fun x => Lean.Xml.Parser.predefinedEntityToChar <$> Lean.Xml.Parser.Name) fun x => Lean.Parsec.skipChar (Char.ofNat 59))

source

@[inline]

def Lean.Xml.Parser.hexDigitToNat (c : Lean.Xml.Parser.LeanChar) :

Nat

Equations

Lean.Xml.Parser.hexDigitToNat c = if Char.ofNat 48 ≤ c ∧ c ≤ Char.ofNat 57 then Char.toNat c - Char.toNat (Char.ofNat 48) else if Char.ofNat 97 ≤ c ∧ c ≤ Char.ofNat 102 then Char.toNat c - Char.toNat (Char.ofNat 97) + 10 else Char.toNat c - Char.toNat (Char.ofNat 65) + 10

source

def Lean.Xml.Parser.digitsToNat (base : Nat) (digits : Array Nat) :

Nat

Equations

Lean.Xml.Parser.digitsToNat base digits = Array.foldl (fun r d => r * base + d) 0 digits 0 (Array.size digits)

source

def Lean.Xml.Parser.CharRef :

Lean.Parsec Lean.Xml.Parser.LeanChar

Equations

Lean.Xml.Parser.CharRef = do Lean.Parsec.skipString "&#" let charCode ← HOrElse.hOrElse (Lean.Xml.Parser.digitsToNat 10 <$> Lean.Parsec.many1 (Lean.Xml.Parser.hexDigitToNat <$> Lean.Parsec.digit)) fun x => SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 120)) fun x => Lean.Xml.Parser.digitsToNat 16 <$> Lean.Parsec.many1 (Lean.Xml.Parser.hexDigitToNat <$> Lean.Parsec.hexDigit) Lean.Parsec.skipChar (Char.ofNat 59) pure (Char.ofNat charCode)

source

def Lean.Xml.Parser.Reference :

Lean.Parsec (Option Lean.Xml.Parser.LeanChar)

Equations

Lean.Xml.Parser.Reference = HOrElse.hOrElse Lean.Xml.Parser.EntityRef fun x => some <$> Lean.Xml.Parser.CharRef

source

def Lean.Xml.Parser.AttValue :

Lean.Parsec String

Equations

Lean.Xml.Parser.AttValue = do let chars ← HOrElse.hOrElse (do Lean.Parsec.skipChar (Char.ofNat 34) SeqLeft.seqLeft (Lean.Parsec.many (HOrElse.hOrElse (some <$> Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 60 ∧ c ≠ Char.ofNat 38 ∧ c ≠ Char.ofNat 34)) fun x => Lean.Xml.Parser.Reference)) fun x => Lean.Parsec.skipChar (Char.ofNat 34)) fun x => do Lean.Parsec.skipChar (Char.ofNat 39) SeqLeft.seqLeft (Lean.Parsec.many (HOrElse.hOrElse (some <$> Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 60 ∧ c ≠ Char.ofNat 38 ∧ c ≠ Char.ofNat 39)) fun x => Lean.Xml.Parser.Reference)) fun x => Lean.Parsec.skipChar (Char.ofNat 39) pure (Array.foldl (fun s c => match c with | some c => String.push s c | x => s) "" chars 0 (Array.size chars))

source

def Lean.Xml.Parser.DefaultDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.DefaultDecl = HOrElse.hOrElse (Lean.Parsec.skipString "#REQUIRED") fun x => HOrElse.hOrElse (Lean.Parsec.skipString "#IMPLIED") fun x => SeqRight.seqRight (SeqRight.seqRight (optional (SeqLeft.seqLeft (Lean.Parsec.skipString "#FIXED") fun x => Lean.Xml.Parser.S)) fun x => Lean.Xml.Parser.AttValue) fun x => pure ()

source

def Lean.Xml.Parser.AttDef :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.AttDef = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Xml.Parser.Name) fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.AttType) fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.DefaultDecl

source

def Lean.Xml.Parser.AttlistDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.AttlistDecl = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipString ") fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Name) fun x => Lean.Parsec.many Lean.Xml.Parser.AttDef) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 62)

source

def Lean.Xml.Parser.PEReference :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.PEReference = SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 37)) fun x => Lean.Xml.Parser.Name) fun x => Lean.Parsec.skipChar (Char.ofNat 59)

source

def Lean.Xml.Parser.EntityValue :

Lean.Parsec String

Equations

Lean.Xml.Parser.EntityValue = do let chars ← HOrElse.hOrElse (do Lean.Parsec.skipChar (Char.ofNat 34) SeqLeft.seqLeft (Lean.Parsec.many (HOrElse.hOrElse (some <$> Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 37 ∧ c ≠ Char.ofNat 38 ∧ c ≠ Char.ofNat 34)) fun x => HOrElse.hOrElse (SeqRight.seqRight Lean.Xml.Parser.PEReference fun x => pure none) fun x => Lean.Xml.Parser.Reference)) fun x => Lean.Parsec.skipChar (Char.ofNat 34)) fun x => do Lean.Parsec.skipChar (Char.ofNat 39) SeqLeft.seqLeft (Lean.Parsec.many (HOrElse.hOrElse (some <$> Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 37 ∧ c ≠ Char.ofNat 38 ∧ c ≠ Char.ofNat 39)) fun x => HOrElse.hOrElse (SeqRight.seqRight Lean.Xml.Parser.PEReference fun x => pure none) fun x => Lean.Xml.Parser.Reference)) fun x => Lean.Parsec.skipChar (Char.ofNat 39) pure (Array.foldl (fun s c => match c with | some c => String.push s c | x => s) "" chars 0 (Array.size chars))

source

def Lean.Xml.Parser.NDataDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.NDataDecl = SeqLeft.seqLeft (SeqLeft.seqLeft (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Parsec.skipString "NDATA") fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Name

source

def Lean.Xml.Parser.EntityDef :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.EntityDef = HOrElse.hOrElse (SeqRight.seqRight Lean.Xml.Parser.EntityValue fun x => pure ()) fun x => SeqLeft.seqLeft Lean.Xml.Parser.ExternalID fun x => optional Lean.Xml.Parser.NDataDecl

source

def Lean.Xml.Parser.GEDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.GEDecl = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipString ") fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Name) fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.EntityDef) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 62)

source

def Lean.Xml.Parser.PEDef :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.PEDef = HOrElse.hOrElse (SeqRight.seqRight Lean.Xml.Parser.EntityValue fun x => pure ()) fun x => Lean.Xml.Parser.ExternalID

source

def Lean.Xml.Parser.PEDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.PEDecl = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipString ") fun x => Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 37)) fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Name) fun x => Lean.Xml.Parser.PEDef) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 62)

source

def Lean.Xml.Parser.EntityDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.EntityDecl = HOrElse.hOrElse Lean.Xml.Parser.GEDecl fun x => Lean.Xml.Parser.PEDecl

source

def Lean.Xml.Parser.PublicID :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.PublicID = SeqLeft.seqLeft (SeqLeft.seqLeft (Lean.Parsec.skipString "PUBLIC") fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.PubidLiteral

source

def Lean.Xml.Parser.NotationDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.NotationDecl = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipString ") fun x => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.Name) fun x => HOrElse.hOrElse Lean.Xml.Parser.ExternalID fun x => Lean.Xml.Parser.PublicID) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 62)

source

def Lean.Xml.Parser.markupDecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.markupDecl = HOrElse.hOrElse Lean.Xml.Parser.elementDecl fun x => HOrElse.hOrElse Lean.Xml.Parser.AttlistDecl fun x => HOrElse.hOrElse Lean.Xml.Parser.EntityDecl fun x => HOrElse.hOrElse Lean.Xml.Parser.NotationDecl fun x => HOrElse.hOrElse Lean.Xml.Parser.PI fun x => SeqRight.seqRight Lean.Xml.Parser.Comment fun x => pure ()

source

def Lean.Xml.Parser.DeclSep :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.DeclSep = HOrElse.hOrElse Lean.Xml.Parser.PEReference fun x => SeqRight.seqRight Lean.Xml.Parser.S fun x => pure ()

source

def Lean.Xml.Parser.intSubset :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.intSubset = SeqRight.seqRight (Lean.Parsec.many (HOrElse.hOrElse Lean.Xml.Parser.markupDecl fun x => Lean.Xml.Parser.DeclSep)) fun x => pure ()

source

def Lean.Xml.Parser.doctypedecl :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.doctypedecl = do Lean.Parsec.skipString " SeqLeft.seqLeft (SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Xml.Parser.Name) fun x => optional (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Xml.Parser.ExternalID)) fun x => pure ()) fun x => optional Lean.Xml.Parser.S SeqRight.seqRight (optional (SeqLeft.seqLeft (SeqLeft.seqLeft (SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 91)) fun x => Lean.Xml.Parser.intSubset) fun x => Lean.Parsec.skipChar (Char.ofNat 93)) fun x => optional Lean.Xml.Parser.S)) fun x => Lean.Parsec.skipChar (Char.ofNat 62)

source

def Lean.Xml.Parser.prolog :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.prolog = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (optional Lean.Xml.Parser.XMLdecl) fun x => Lean.Parsec.many Lean.Xml.Parser.Misc) fun x => optional (SeqLeft.seqLeft Lean.Xml.Parser.doctypedecl fun x => Lean.Parsec.many Lean.Xml.Parser.Misc)) fun x => pure ()

source

def Lean.Xml.Parser.Attribute :

Lean.Parsec (String × String)

Equations

Lean.Xml.Parser.Attribute = do let name ← Lean.Xml.Parser.Name Lean.Xml.Parser.Eq let value ← Lean.Xml.Parser.AttValue pure (name, value)

source

def Lean.Xml.Parser.elementPrefix :

Lean.Parsec (Array Lean.Xml.Content → Lean.Xml.Element)

Equations

Lean.Xml.Parser.elementPrefix = do Lean.Parsec.skipChar (Char.ofNat 60) let name ← Lean.Xml.Parser.Name let attributes ← Lean.Parsec.many (SeqRight.seqRight Lean.Xml.Parser.S fun x => Lean.Xml.Parser.Attribute) SeqRight.seqRight (optional Lean.Xml.Parser.S) fun x => pure () pure (Lean.Xml.Element.Element name (Std.RBMap.fromList (Array.toList attributes) compare))

source

def Lean.Xml.Parser.EmptyElemTag (elem : Array Lean.Xml.Content → Lean.Xml.Element) :

Lean.Parsec Lean.Xml.Element

Equations

Lean.Xml.Parser.EmptyElemTag elem = SeqRight.seqRight (Lean.Parsec.skipString "/>") fun x => pure (elem #[])

source

def Lean.Xml.Parser.STag (elem : Array Lean.Xml.Content → Lean.Xml.Element) :

Lean.Parsec (Array Lean.Xml.Content → Lean.Xml.Element)

Equations

Lean.Xml.Parser.STag elem = SeqRight.seqRight (Lean.Parsec.skipChar (Char.ofNat 62)) fun x => pure elem

source

def Lean.Xml.Parser.ETag :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.ETag = SeqRight.seqRight (SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipString ") fun x => Lean.Xml.Parser.Name) fun x => optional Lean.Xml.Parser.S) fun x => Lean.Parsec.skipChar (Char.ofNat 62)

source

def Lean.Xml.Parser.CDStart :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.CDStart = Lean.Parsec.skipString "

source

def Lean.Xml.Parser.CDEnd :

Lean.Parsec Unit

Equations

Lean.Xml.Parser.CDEnd = Lean.Parsec.skipString "]]>"

source

def Lean.Xml.Parser.CData :

Lean.Parsec String

Equations

Lean.Xml.Parser.CData = Lean.Parsec.manyChars (SeqRight.seqRight (Lean.Parsec.notFollowedBy (Lean.Parsec.skipString "]]>")) fun x => Lean.Parsec.anyChar)

source

def Lean.Xml.Parser.CDSect :

Lean.Parsec String

Equations

Lean.Xml.Parser.CDSect = SeqLeft.seqLeft (SeqRight.seqRight Lean.Xml.Parser.CDStart fun x => Lean.Xml.Parser.CData) fun x => Lean.Xml.Parser.CDEnd

source

def Lean.Xml.Parser.CharData :

Lean.Parsec String

Equations

Lean.Xml.Parser.CharData = SeqRight.seqRight (Lean.Parsec.notFollowedBy (Lean.Parsec.skipString "]]>")) fun x => Lean.Parsec.manyChars (Lean.Parsec.satisfy fun c => decide (c ≠ Char.ofNat 60 ∧ c ≠ Char.ofNat 38))

source

partial def Lean.Xml.Parser.content :

Lean.Parsec (Array Lean.Xml.Content)

source

partial def Lean.Xml.Parser.element :

Lean.Parsec Lean.Xml.Element

source

def Lean.Xml.Parser.document :

Lean.Parsec Lean.Xml.Element

Equations

Lean.Xml.Parser.document = SeqLeft.seqLeft (SeqLeft.seqLeft (SeqRight.seqRight Lean.Xml.Parser.prolog fun x => Lean.Xml.Parser.element) fun x => Lean.Parsec.many Lean.Xml.Parser.Misc) fun x => Lean.Parsec.eof

source

def Lean.Xml.parse (s : String) :

Except String Lean.Xml.Element

Equations

Lean.Xml.parse s = match Lean.Xml.Parser.document (String.mkIterator s) with | Lean.Parsec.ParseResult.success x res => Except.ok res | Lean.Parsec.ParseResult.error it err => Except.error (toString "offset " ++ toString (Nat.repr it.i) ++ toString ": " ++ toString err ++ toString "\n" ++ toString (String.Iterator.extract (String.Iterator.prevn it 10) it) ++ toString "")