Package parser-stream: Parse streams

Information

nameparser-stream
version1.110
descriptionParse streams
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
checksum6349b379ee43af78943d33678d44d508fb615fe9
requiresbase
showData.Bool
Data.List
Data.Pair
Function
Number.Natural
Parser.Stream
Relation

Files

Defined Type Operator

Defined Constants

Theorems

wellFounded isProperSuffix

¬(error = eof)

length eof = 0

length error = 0

fromList [] = eof

xs. isSuffix xs xs

xs. ¬isProperSuffix xs eof

xs. ¬isProperSuffix xs error

xs. ¬isProperSuffix xs xs

toList eof = ([], )

toList error = ([], )

xs. append [] xs = xs

f. map f eof = eof

f. map f error = error

l. fromList l = append l eof

l. length (fromList l) = length l

l. toList (fromList l) = (l, )

xs. length xs = length (fst (toList xs))

xs. isSuffix xs eof xs = eof

xs. isSuffix xs error xs = error

x xs. ¬(eof = cons x xs)

x xs. ¬(error = cons x xs)

xs ys. isProperSuffix xs ys isSuffix xs ys

x xs. length (cons x xs) = suc (length xs)

e b f. case e b f eof = b

e b f. case e b f error = e

h t. fromList (h :: t) = cons h (fromList t)

l1 l2. fromList (l1 @ l2) = append l1 (fromList l2)

xs ys. isProperSuffix xs ys length xs < length ys

xs ys. isSuffix xs ys length xs length ys

l xs. length (append l xs) = length l + length xs

xs y ys. isProperSuffix xs (cons y ys) isSuffix xs ys

xs ys. isSuffix xs ys xs = ys isProperSuffix xs ys

h t xs. append (h :: t) xs = cons h (append t xs)

xs ys zs. append (xs @ ys) zs = append xs (append ys zs)

xs ys zs.
    isProperSuffix xs ys isProperSuffix ys zs isProperSuffix xs zs

xs ys zs. isProperSuffix xs ys isSuffix ys zs isProperSuffix xs zs

xs ys zs. isSuffix xs ys isProperSuffix ys zs isProperSuffix xs zs

xs ys zs. isSuffix xs ys isSuffix ys zs isSuffix xs zs

xs ys e. toList xs = (ys, e) length xs = length ys

f x xs. map f (cons x xs) = cons (f x) (map f xs)

surjective (λ(l, b). append l (if b then error else eof))

xs. xs = error xs = eof x xt. xs = cons x xt

p. (xs. (ys. isProperSuffix ys xs p ys) p xs) xs. p xs

e b f x xs. case e b f (cons x xs) = f x xs

x xs y ys. cons x xs = cons y ys x = y xs = ys

p. p error p eof (x xs. p xs p (cons x xs)) xs. p xs

l xs ys e. toList (append l xs) = (l @ ys, e) toList xs = (ys, e)

f xs ys e. toList xs = (ys, e) toList (map f xs) = (map f ys, e)

length error = 0 length eof = 0
  x xs. length (cons x xs) = length xs + 1

(xs. append [] xs = xs)
  h t xs. append (h :: t) xs = cons h (append t xs)

x xs. toList (cons x xs) = let (l, e) toList xs in (x :: l, e)

e b f.
    fn. fn error = e fn eof = b x xs. fn (cons x xs) = f x xs (fn xs)

(f. map f error = error) (f. map f eof = eof)
  f x xs. map f (cons x xs) = cons (f x) (map f xs)

h.
    (f g xs.
       (ys. isProperSuffix ys xs f ys = g ys) h f xs = h g xs)
    fn. xs. fn xs = h fn xs

toList error = ([], ) toList eof = ([], )
  x xs. toList (cons x xs) = let (l, e) toList xs in (x :: l, e)

(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

External Type Operators

External Constants

Assumptions

¬

¬

length [] = 0

bit0 0 = 0

t. t t

n. 0 n

n. n n

m. wellFounded (measure m)

p. p

x. id x = x

t. t ¬t

(¬) = λp. p

() = λp. p ((select) p)

a. ∃!x. x = a

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(suc n = 0)

n. 0 + n = n

m. m + 0 = m

l. [] @ l = l

f. map f [] = []

r. wellFounded r irreflexive r

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. even (2 * n)

n. bit1 n = suc (bit0 n)

m. m 0 = 1

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

n. even (suc n) ¬even n

m. m 0 m = 0

x. (fst x, snd x) = x

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

h t. ¬(h :: t = [])

p x. p x p ((select) p)

n. bit0 (suc n) = suc (suc (bit0 n))

f y. (let x y in f x) = f y

x. a b. x = (a, b)

x y. x = y y = x

t1 t2. t1 t2 t2 t1

m n. m + n = n + m

m n. m < n m n

r x. irreflexive r ¬r x x

n. 2 * n = n + n

h t. length (h :: t) = suc (length t)

m n. ¬(m < n n m)

m n. ¬(m n n < m)

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

() = λp q. (λf. f p q) = λf. f

f. surjective f y. x. y = f x

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

t1 t2. ¬(t1 t2) t1 ¬t2

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m = suc n m = n

r s. subrelation r s wellFounded s wellFounded r

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. even (m * n) even m even n

m n. even (m + n) even m even n

m n. m suc n = m * m n

p. (x. p x) a b. p (a, b)

f g. (x. f x = g x) f = g

p a. (x. a = x p x) p a

() = λp q. r. (p r) (q r) r

m n. m n m < n m = n

m n. m n n m m = n

f. fn. a b. fn (a, b) = f a b

m n. m < n d. n = m + suc d

m x y. measure m x y m x < m y

p q. (x. p q x) p x. q x

p q. (x. p q x) p x. q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

t1 t2 t3. (t1 t2) t3 t1 t2 t3

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m * (n * p) = m * n * p

p m n. m + p = n + p m = n

l h t. (h :: t) @ l = h :: t @ l

p x. (y. p y y = x) (select) p = x

r. (x. y. r x y) f. x. r x (f x)

m n. m suc n m = suc n m n

m n. m * n = 0 m = 0 n = 0

f h t. map f (h :: t) = f h :: map f t

p. p 0 (n. p n p (suc n)) n. p n

m n. m n = 0 m = 0 ¬(n = 0)

r s. subrelation r s x y. r x y s x y

(∃!) = λp. () p x y. p x p y x = y

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x

e f. ∃!fn. fn 0 = e n. fn (suc n) = f (fn n) n

p. p [] (h t. p t p (h :: t)) l. p l

m n p. m * n = m * p m = 0 n = p

m n p. m * n m * p m = 0 n p

m n p. m * n < m * p ¬(m = 0) n < p

h1 h2 t1 t2. h1 :: t1 = h2 :: t2 h1 = h2 t1 = t2

a b a' b'. (a, b) = (a', b') a = a' b = b'

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p2 p1) (q1 q2) (p1 q1) p2 q2

p. (x. ∃!y. p x y) f. x y. p x y f x = y

p c x y. p (if c then x else y) (c p x) (¬c p y)

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)

p. (∃!x. p x) (x. p x) x x'. p x p x' x = x'

r. wellFounded r p. (x. (y. r y x p y) p x) x. p x