Package parser-comb-def: Definition of stream parser combinators

Information

name	parser-comb-def
version	1.83
description	Definition of stream parser combinators
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2014-11-04
checksum	fcd38ea1bffc7be4eb681d09fa66b22ef4a97266
requires	bool option parser-stream
show	Data.Bool Data.List Data.Option Data.Pair Parser Parser.Stream

Files

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

Defined Type Operator

Parser
- parser

Defined Constants

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

Theorems

⊦ parseAll = mkParser parseAll.pa

⊦ parseNone = mkParser parseNone.pn

⊦ ∀a. mkParser (destParser a) = a

⊦ ∀p. parse p eof = none

⊦ ∀p. parse p error = none

⊦ ∀f. parseOption f = partialMap f parseAll

⊦ ∀a s. parseNone.pn a s = none

⊦ ∀r. isParser r ⇔ destParser (mkParser r) = r

⊦ ∀a s. parseAll.pa a s = some (a, s)

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

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

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

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

⊦ ∀f g p. mapToken f g p = mkParser (mapToken.pf f g p)

⊦ ∀p a s. parse p (cons a s) = destParser p a s

⊦ ∀p e. inverse p e ⇔ ∀x s. parse p (append (e x) s) = some (x, s)

⊦ ∀p.
isParser p ⇔
∀x xs. case p x xs of none → ⊤ | some (y, xs') → isSuffix xs' xs

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

⊦ ∀f p a s.
    partialMap.pf f p a s =
    case destParser p a s of
      none → none
    | some (b, s') → case f b of none → none | some c → some (c, s')

⊦ ∀f g p b s.
    mapToken.pf f g p b s =
    case destParser p (g b) (map g s) of
      none → none
    | some (c, s') → some (c, map f s')

⊦ ∀pb pc a s.
    parsePair.pbc pb pc a s =
    case destParser pb a s of
      none → none
    | some (b, s') →
        case parse pc s' of
          none → none
        | some (c, s'') → some ((b, c), s'')

External Type Operators

→
bool
Data
- List
  - list
- Option
  - option
- Pair
  - ×
Parser
- Stream
  - stream

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - cond
  - ⊤
- Option
  - case
  - none
  - some
- Pair
  - ,
Parser
- Stream
  - append
  - cons
  - eof
  - error
  - isSuffix
  - map

Assumptions

⊦ ⊤

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

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

⊦ (∀) = λp. p = λx. ⊤

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

⊦ ∀b f. case b f none = b

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

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

⊦ ∀f₀ f₁ f₂.
    ∃fn.
      fn error = f₀ ∧ fn eof = f₁ ∧
      ∀a₀ a₁. fn (cons a₀ a₁) = f₂ a₀ a₁ (fn a₁)