Package parser-comb-def: Definition of the basic parser combinators

Information

Files

• Package tarball parser-comb-def-1.0.tgz
• Theory file parser-comb-def.thy (included in the package tarball)

Defined Type Operator

• Parser
  • Parser.parser

Defined Constants

• Parser
  • Parser.destParser
  • Parser.inverse
  • Parser.isParser
  • Parser.map
  • Parser.mkParser
  • Parser.parse
  • Parser.parseAll
    • Parser.parseAll.pa
  • Parser.parseNone
    • Parser.parseNone.pn
  • Parser.parseOption
  • Parser.parsePair
    • Parser.parsePair.pbc
  • Parser.parseSome
  • Parser.partialMap
    • Parser.partialMap.pf
  • Parser.strongInverse

Theorems

⊦ Parser.parseAll = Parser.mkParser Parser.parseAll.pa

⊦ Parser.parseNone = Parser.mkParser Parser.parseNone.pn

⊦ ∀f. Parser.parseOption f = Parser.partialMap f Parser.parseAll

⊦ ∀a s. Parser.parseNone.pn a s = Data.Option.none

⊦ ∀a s. Parser.parseAll.pa a s = Data.Option.some (Data.Pair., a s)

⊦ ∀pb pc.
    Parser.parsePair pb pc = Parser.mkParser (Parser.parsePair.pbc pb pc)

⊦ ∀f p. Parser.partialMap f p = Parser.mkParser (Parser.partialMap.pf f p)

⊦ ∀p.
    Parser.parseSome p =
    Parser.parseOption
      (λa. if p a then Data.Option.some a else Data.Option.none)

⊦ ∀f p. Parser.map f p = Parser.partialMap (λb. Data.Option.some (f b)) p

⊦ (∀a. Parser.mkParser (Parser.destParser a) = a) ∧
  ∀r. Parser.isParser r ⇔ Parser.destParser (Parser.mkParser r) = r

⊦ ∀p e.
    Parser.inverse p e ⇔
    ∀x s.
      Parser.parse p (Parser.Stream.append (e x) s) =
      Data.Option.some (Data.Pair., x s)

⊦ ∀p.
    Parser.isParser p ⇔
    ∀x xs.
      Data.Option.case T
        (λ(Data.Pair., y xs'). Parser.Stream.isSuffix xs' xs) (p x xs)

⊦ (∀p. Parser.parse p Parser.Stream.error = Data.Option.none) ∧
  (∀p. Parser.parse p Parser.Stream.eof = Data.Option.none) ∧
  ∀p a s.
    Parser.parse p (Parser.Stream.stream a s) = Parser.destParser p a s

⊦ ∀p e.
    Parser.strongInverse p e ⇔
    Parser.inverse p e ∧
    ∀s x s'.
      Parser.parse p s = Data.Option.some (Data.Pair., x s') ⇒
      s = Parser.Stream.append (e x) s'

⊦ ∀f p a s.
    Parser.partialMap.pf f p a s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s').
         Data.Option.case Data.Option.none
           (λc. Data.Option.some (Data.Pair., c s')) (f b))
      (Parser.destParser p a s)

⊦ ∀pb pc a s.
    Parser.parsePair.pbc pb pc a s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s').
         Data.Option.case Data.Option.none
           (λ(Data.Pair., c s'').
              Data.Option.some (Data.Pair., (Data.Pair., b c) s''))
           (Parser.parse pc s')) (Parser.destParser pb a s)

Input Type Operators

• →
• bool
• Data
  • List
    • Data.List.list
  • Option
    • Data.Option.option
  • Pair
    • Data.Pair.*
• Parser
  • Stream
    • Parser.Stream.stream

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • cond
    • select
    • T
  • Option
    • Data.Option.case
    • Data.Option.none
    • Data.Option.some
  • Pair
    • Data.Pair.,
• Parser
  • Stream
    • Parser.Stream.append
    • Parser.Stream.eof
    • Parser.Stream.error
    • Parser.Stream.isSuffix
    • Parser.Stream.stream

Assumptions

⊦ T

⊦ (∃) = λP. P ((select) P)

⊦ ∀t. (∀x. t) ⇔ t

⊦ (∀) = λP. P = λx. T

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ (∧) = λp q. (λf. f p q) = λf. f T T

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ (∀b f. Data.Option.case b f Data.Option.none = b) ∧
  ∀b f a. Data.Option.case b f (Data.Option.some a) = f a

⊦ ∀f0 f1 f2.
    ∃fn.
      fn Parser.Stream.error = f0 ∧ fn Parser.Stream.eof = f1 ∧
      ∀a0 a1. fn (Parser.Stream.stream a0 a1) = f2 a0 a1 (fn a1)