Package parser: Stream parsers

Information

nameparser
version1.160
descriptionStream parsers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
homepagehttp://opentheory.gilith.com/?pkg=parser
hol-light-int-filehol-light.int
hol-light-thm-filehol-light.art
haskell-categoryParsing
haskell-int-filehaskell.int
haskell-src-filehaskell.art
haskell-test-filehaskell-test.art
haskell-equality-type"Parser.Stream.stream"
haskell-arbitrary-type"Parser.Stream.stream"
checksum45263b9d88ea494a965d6ea18432ebb6ed338963
requiresbase
showData.Bool
Data.List
Data.Option
Data.Pair
Data.Sum
Function
Number.Natural
Parser
Parser.Stream
Relation

Files

Defined Type Operators

Defined Constants

Theorems

wellFounded isProperSuffix

¬(error = eof)

length eof = 0

length error = 0

fromList [] = eof

xs. isSuffix xs xs

p. invariant (dest p)

f. invariant (token.prs f)

p. invariant (sequence.prs p)

any = some (const )

none = token (const none)

xs. ¬isProperSuffix xs eof

xs. ¬isProperSuffix xs error

xs. ¬isProperSuffix xs xs

inverse any (λx. x :: [])

strongInverse any (λx. x :: [])

toList eof = ([], )

toList error = ([], )

xs. append [] xs = xs

xs. apply none xs = none

f. map f eof = eof

f. map f error = error

p. parse p eof = eof

p. parse p error = error

a. mk (dest a) = a

p. apply p eof = none

p. apply p error = none

p1 p2. invariant (orelse.prs p1 p2)

p f. invariant (mapPartial.prs p f)

f s. invariant (fold.prs f s)

l. fromList l = append l eof

l. length (fromList l) = length l

p. filter any p = some p

f. token f = mk (token.prs f)

f. mapPartial any f = token f

f. dest (token f) = token.prs f

p. sequence p = mk (sequence.prs p)

p. dest (sequence p) = sequence.prs p

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

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

xs. isSuffix xs eof xs = eof

xs. isSuffix xs error xs = error

f. fold f = mk fold.prs f

x xs. ¬(eof = cons x xs)

x xs. ¬(error = cons x xs)

x xs. dest none x xs = none

r. invariant r dest (mk r) = r

xs ys. isProperSuffix xs ys isSuffix xs ys

p xs. length (parse p xs) length xs

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

p1 p2. orelse p1 p2 = mk (orelse.prs p1 p2)

p1 p2. dest (orelse p1 p2) = orelse.prs p1 p2

p f. mapPartial p f = mk (mapPartial.prs p f)

p f. dest (mapPartial p f) = mapPartial.prs p f

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

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

apply any = case none none (λx xs. some (x, 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)

x xs. dest any x xs = some (x, xs)

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

p. some p = token (λx. if p x then some x else none)

p1 p2. dest p1 = dest p2 p1 = p2

p f. map p f = mapPartial p (λx. some (f x))

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

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

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

p f xs. parse (map p f) xs = map f (parse p 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))))

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))

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

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

p.
    apply (some p) =
    case none none (λx xs. if p x then some (x, xs) else none)

f x xs.
    token.prs f x xs = case f x of none none | some y some (y, xs)

f.
    apply (token f) =
    case none none (λx xs. case f x of none none | some y some (y, xs))

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

p x xs. dest (some p) x xs = if p x then some (x, xs) else none

p e l. inverse p e parse p (fromList (concat (map e l))) = fromList l

f e. (x. f (e x) = some x) inverse (token f) (λx. e x :: [])

p1 p2 xs.
    apply (orelse p1 p2) xs =
    case apply p1 xs of none apply p2 xs | some yys some yys

p x xs y ys. dest p x xs = some (y, ys) isSuffix ys xs

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

p e. inverse p e x xs. apply p (append (e x) xs) = some (x, xs)

p e x xs. inverse p e parse p (append (e x) xs) = cons x (parse p xs)

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)

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 xs.
    apply p xs = none
    y ys. apply p xs = some (y, ys) isProperSuffix ys xs

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

p f g e.
    inverse p e (x. f (g x) = x) inverse (map p f) (λx. e (g x))

p.
    invariant p
    x xs. case p x xs of none | some (y, ys) isSuffix ys xs

p xs.
    apply (sequence p) xs =
    case apply p xs of none none | some (y, ys) apply y ys

p f g e.
    inverse p e (x. f (g x) = some x)
    inverse (mapPartial p f) (λx. e (g x))

p x xs.
    dest p x xs = none y ys. dest p x xs = 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 x xs.
    invariant p
    p x xs = none y ys. p x xs = some (y, ys) isSuffix ys xs

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

p e xs ys ye.
    strongInverse p e toList (parse p xs) = (ys, ye)
    ye xs = fromList (concat (map e ys))

(p. apply p error = none) (p. apply p eof = none)
  p x xs. apply p (cons x xs) = dest p x xs

p f xs.
    apply (map p f) xs =
    case apply p xs of none none | some (y, ys) some (f y, ys)

p e.
    strongInverse p e
    inverse p e
    xs y ys. apply p xs = some (y, ys) xs = append (e y) ys

p x xs.
    parse p (cons x xs) =
    case dest p x xs of none error | some (y, ys) cons y (parse p ys)

p xs.
    parse p xs =
    case apply p xs of
      none case xs of error error | eof eof | cons y ys error
    | some (y, ys) cons y (parse p ys)

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

p1 p2 e1 e2.
    inverse p1 e1 inverse p2 e2
    inverse (pair p1 p2) (λ(x1, x2). e1 x1 @ e2 x2)

p1 p2 e1 e2.
    strongInverse p1 e1 strongInverse p2 e2
    strongInverse (pair p1 p2) (λ(x1, x2). e1 x1 @ e2 x2)

p f xs.
    apply (filter p f) xs =
    case apply p xs of
      none none
    | some (y, ys) if f y then some (y, ys) else none

p f x xs.
    dest (map p f) x xs =
    case dest p x xs of none none | some (y, ys) some (f y, ys)

p f xs.
    apply (mapPartial p f) xs =
    case apply p xs of
      none none
    | some (y, ys) case f y of none none | some z some (z, ys)

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

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

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)

p f x xs.
    dest (filter p f) x xs =
    case dest p x xs of
      none none
    | some (y, ys) if f y then some (y, ys) else none

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

f e.
    (x. f (e x) = some x)
    (y1 y2 x. f y1 = some x f y2 = some x y1 = y2)
    strongInverse (token f) (λx. e x :: [])

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)

p f g e.
    strongInverse p e (x. f (g x) = x)
    (y1 y2 x. f y1 = x f y2 = x y1 = y2)
    strongInverse (map p f) (λx. e (g x))

(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

p1 p2 xs.
    apply (pair p1 p2) xs =
    case apply p1 xs of
      none none
    | some (y, ys)
        case apply p2 ys of none none | some (z, zs) some ((y, z), zs)

(p. parse p error = error) (p. parse p eof = eof)
  p x xs.
    parse p (cons x xs) =
    case dest p x xs of none error | some (y, ys) cons y (parse p ys)

p f g e.
    strongInverse p e (x. f (g x) = some x)
    (y1 y2 x. f y1 = some x f y2 = some x y1 = y2)
    strongInverse (mapPartial p f) (λx. e (g x))

p1 p2 x xs.
    dest (pair p1 p2) x xs =
    case dest p1 x xs of
      none none
    | some (y, ys)
        case apply p2 ys of none none | some (z, zs) some ((y, z), zs)

External Type Operators

External Constants

Assumptions

¬

¬

length [] = 0

bit0 0 = 0

concat [] = []

t. t t

n. 0 n

n. n n

m. wellFounded (measure m)

p. p

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.

a. ¬(some a = none)

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

x y. const x y = x

() = λ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 = [])

b f. case b f none = b

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

x. x = none a. x = some a

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

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

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

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

a b. some a = some b a = b

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

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

m n. suc m = suc n m = n

m n. suc m suc n m n

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

r s. subrelation r s wellFounded s wellFounded r

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. (f g) x = f (g x)

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)

l. l = [] h t. l = h :: t

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

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

x. (a. x = left a) b. x = right b

() = λ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

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

m n p. m n n p m p

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 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 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

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

r.
    wellFounded r
    h.
      (f g x. (z. r z x f z = g z) h f x = h g x)
      f. x. f x = h f x