Package parser-fold: The fold parsers

Information

name	parser-fold
version	1.2
description	The fold parsers
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
checksum	aaf76f2e8fb780359c264ce6d0c6c94a23bba8bf
requires	base parser-comb parser-stream
show	Data.Bool Data.Option Data.Pair Data.Sum Number.Natural Parser Parser.Stream

Files

Package tarball parser-fold-1.2.tgz
Theory source file parser-fold.thy (included in the package tarball)

Defined Constants

Parser
- fold
  - fold.prs
- foldN

Theorems

⊦ ∀f s. invariant (fold.prs f s)

⊦ ∀f. fold f = Function.∘ mk (fold.prs f)

⊦ ∀f s. fold f s = mk (fold.prs f s)

⊦ ∀f s. dest (fold f s) = fold.prs f s

⊦ ∀f s. apply (fold f s) = case none none (λx xs. fold.prs f s x xs)

⊦ ∀f s x xs.
    fold.prs f s x xs =
    case f x s of
      none → none
    | some y →
        case y of
          left z → some (z, xs)
        | right t →
            case xs of
              error → none
            | eof → none
            | cons z zs → fold.prs f t z zs

⊦ ∀f n s.
    foldN f n s =
    fold
      (λx (m, t).
         map (λu. if m = 0 then left u else right (m - 1, u)) (f x t))
      (n, s)

External Type Operators

→
bool
Data
- Option
  - option
- Pair
  - ×
- Sum
  - +
Number
- Natural
  - natural
Parser
- parser
- Stream
  - stream

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - cond
  - ⊥
  - ⊤
- Option
  - case
  - map
  - none
  - some
- Pair
  - ,
- Sum
  - case
  - left
  - right
Function
- Function.∘
Number
- Natural
  - -
  - bit1
  - zero
Parser
- apply
- dest
- invariant
- mk
- Stream
  - case
  - cons
  - eof
  - error
  - isProperSuffix
  - isSuffix

Assumptions

⊦ ⊤

⊦ ∀xs. isSuffix xs xs

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

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

⊦ ∀t. (λx. t x) = t

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

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀p. apply p eof = none

⊦ ∀p. apply p error = none

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

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀b f. case b f none = b

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀r. invariant r ⇔ dest (mk r) = r

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀xs ys. isProperSuffix xs ys ⇒ isSuffix xs ys

⊦ ∀x. x = none ∨ ∃a. x = some a

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

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

⊦ ∀b f a. case b f (some a) = f a

⊦ ∀f g a. case f g (left a) = f a

⊦ ∀f g b. case f g (right b) = g b

⊦ ∀f g x. Function.∘ f g x = f (g x)

⊦ ∀xs y ys. isProperSuffix xs (cons y ys) ⇔ isSuffix xs ys

⊦ ∀f g. (∀x. f x = g x) ⇔ f = g

⊦ ∀x. (∃a. x = left a) ∨ ∃b. x = right b

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b

⊦ ∀p x xs. apply p (cons x xs) = dest p x xs

⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)

⊦ ∀xs. xs = error ∨ xs = eof ∨ ∃x xt. xs = cons x xt

⊦ ∀p g h. ∃f. ∀x. f x = if p x then f (g x) else h x

⊦ ∀p q. (∀x. p x ∧ q x) ⇔ (∀x. p x) ∧ ∀x. q x

⊦ ∀p. p error ∧ p eof ∧ (∀x xs. p xs ⇒ p (cons x xs)) ⇒ ∀xs. p xs

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

⊦ (∀e b f. case e b f error = e) ∧ (∀e b f. case e b f eof = b) ∧
∀e b f x xs. case e b f (cons x xs) = f x xs