Package parser-comb-def: Definition of stream parser combinators
Information
| name | parser-comb-def |
| version | 1.90 |
| description | Definition of stream parser combinators |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2015-03-05 |
| checksum | e7480a2a14977821a61f6629f6cd3ba5e6efbe0e |
| requires | base parser-stream |
| show | Data.Bool Data.List Data.Option Data.Pair Parser Parser.Stream |
Files
- Package tarball parser-comb-def-1.90.tgz
- Theory source file parser-comb-def.thy (included in the package tarball)
Defined Type Operator
- Parser
- parser
Defined Constants
- Parser
- any
- apply
- dest
- filter
- invariant
- inverse
- map
- mapPartial
- mapPartial.prs
- mk
- none
- orelse
- orelse.prs
- pair
- sequence
- sequence.prs
- some
- strongInverse
- token
- token.prs
Theorems
⊦ any = some (Function.const ⊤)
⊦ none = token (Function.const none)
⊦ ∀a. mk (dest a) = a
⊦ ∀p. apply p eof = none
⊦ ∀p. apply p error = none
⊦ ∀f. token f = mk (token.prs f)
⊦ ∀p. sequence p = mk (sequence.prs p)
⊦ ∀r. invariant r ⇔ dest (mk r) = r
⊦ ∀p1 p2. orelse p1 p2 = mk (orelse.prs p1 p2)
⊦ ∀p f. mapPartial p f = mk (mapPartial.prs p f)
⊦ ∀p. some p = token (λx. if p x then some x else none)
⊦ ∀p f. map p f = mapPartial p (λx. some (f x))
⊦ ∀p x xs. apply p (cons x xs) = dest p x xs
⊦ ∀p f. filter p f = mapPartial p (λx. if f x then some x else none)
⊦ ∀p1 p2. pair p1 p2 = sequence (map p1 (λx. map p2 (λy. (x, y))))
⊦ ∀f x xs.
token.prs f x xs = case f x of none → none | some y → some (y, xs)
⊦ ∀p e. inverse p e ⇔ ∀x xs. apply p (append (e x) xs) = some (x, xs)
⊦ ∀p1 p2 x xs.
orelse.prs p1 p2 x xs =
case dest p1 x xs of none → dest p2 x xs | some yys → some yys
⊦ ∀p.
invariant p ⇔
∀x xs. case p x xs of none → ⊤ | some (y, ys) → isSuffix ys xs
⊦ ∀p x xs.
sequence.prs p x xs =
case dest p x xs of none → none | some (q, ys) → apply q ys
⊦ ∀p e.
strongInverse p e ⇔
inverse p e ∧
∀xs y ys. apply p xs = some (y, ys) ⇒ xs = append (e y) ys
⊦ ∀p f x xs.
mapPartial.prs p f x xs =
case dest p x xs of
none → none
| some (y, ys) → case f y of none → none | some z → some (z, ys)
External Type Operators
- →
- bool
- Data
- List
- list
- Option
- option
- Pair
- ×
- List
- Parser
- Stream
- stream
- Stream
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- cond
- ⊤
- Option
- case
- none
- some
- Pair
- ,
- Bool
- Function
- Function.const
- Parser
- Stream
- append
- cons
- eof
- error
- isSuffix
- Stream
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
⊦ ∀e b f.
∃fn. fn error = e ∧ fn eof = b ∧ ∀x xs. fn (cons x xs) = f x xs (fn xs)