Data.Compress.Utils.Parser

(source)

Definitions

interface Cons : Type -> Type -> Type

Parameters: a, s
Methods:

singleton : a -> s
uncons : s -> Maybe (a, s)

Implementations:

Cons Char String
Cons a (List a)
Cons Bool Bitstream

singleton : Cons a s => a -> s

Visibility: public export

uncons : Cons a s => s -> Maybe (a, s)

Visibility: public export

record Bitstream : Type

Totality: total
Visibility: public export
Constructor:

MkBitstream : List (Fin 8, Bits8) -> Bitstream

Projection:

.content : Bitstream -> List (Fin 8, Bits8)

Hints:

Cons Bool Bitstream
Monoid Bitstream
Semigroup Bitstream

.content : Bitstream -> List (Fin 8, Bits8)

Visibility: public export

content : Bitstream -> List (Fin 8, Bits8)

Visibility: public export

fromBits8 : List Bits8 -> Bitstream

Visibility: export

toBits8 : Bitstream -> List Bits8

Visibility: export

is_byte_aligned : Bitstream -> Bool

Visibility: export

data Parser : Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Fail : e -> Parser i e a
Pure : i -> a -> Parser i e a
More : (i -> Parser i e a) -> Parser i e a
Alt : Parser i e a -> Lazy (Parser i e a) -> Parser i e a

Hint:

Functor (Parser i e)

transform : (i -> Either e i') -> (i' -> Either e i) -> Parser i e a -> Parser i' e a

Visibility: public export

map_error : (e -> e') -> Parser i e a -> Parser i e' a

  maps over the errors of the parser

Visibility: public export

(<|>) : Semigroup e => Parser i e a -> Lazy (Parser i e a) -> Parser i e a

Visibility: public export
Fixity Declaration: infixr operator, level 2

fail : e -> Parser i e a

  fail with an error

Visibility: public export

feed : (Semigroup e, Semigroup i) => i -> Parser i e a -> Parser i e a

  feed input into the parser incrementally

Visibility: public export

pure : Monoid i => a -> Parser i e a

Visibility: public export

(<*>) : (Semigroup e, Monoid i) => Parser i e (a -> b) -> Lazy (Parser i e a) -> Parser i e b

Visibility: public export
Fixity Declaration: infixl operator, level 3

(<*) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e a

Visibility: public export
Fixity Declaration: infixl operator, level 3

(*>) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e b

Visibility: public export
Fixity Declaration: infixl operator, level 3

(>>=) : (Semigroup e, Monoid i) => Parser i e a -> (a -> Parser i e b) -> Parser i e b

Visibility: public export
Fixity Declaration: infixl operator, level 1

more : (i -> Parser i e a) -> Parser i e a

Visibility: public export

peek : Cons c i => Parser i e c

  peek into the next token without consuming it

Visibility: public export

token : Cons c i => Parser i e c

  reads the next token

Visibility: public export

count : (Semigroup e, Monoid i) => (k : Nat) -> Parser i e a -> Parser i e (Vect k a)

  run `p` `k` times and collect the results

Visibility: public export

option : (Semigroup e, Monoid i) => a -> Parser i e a -> Parser i e a

  return the result of `p` if it succeeds, otherwise return `x`

Visibility: public export

some : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List1 a)

Visibility: public export

many : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List a)

Visibility: public export

data SimpleError : Type -> Type

  example: `SimpleError String`

Totality: total
Visibility: public export
Constructors:

Msg : a -> SimpleError a
Alt : SimpleError a -> SimpleError a -> SimpleError a
Under : a -> SimpleError a -> SimpleError a

Hints:

Semigroup (SimpleError a)
Show a => Show (SimpleError a)

msg : e -> SimpleError e

Visibility: public export

under : e -> Parser i (SimpleError e) a -> Parser i (SimpleError e) a

Visibility: public export

bit_getbyte : Parser Bitstream e Bits8

Visibility: export

p_nat : Semigroup e => Nat -> Parser (List Bits8) e Nat

  parse the next `n` bytes as a natural number in big endian style

Visibility: export

p_be_nat : Semigroup e => Nat -> Parser (List Bits8) e Nat

Visibility: export

le_nat : Semigroup e => Nat -> Parser Bitstream e Nat

Visibility: export

p_exact : (Cons c i, Monoid i) => Nat -> Parser i (SimpleError String) a -> Parser i (SimpleError String) a

  make sure that `p` MUST consume at least `n` tokens, fails otherwise

Visibility: public export

ifA : Monoid i => Bool -> Lazy (Parser i e a) -> Parser i e (Maybe a)

Visibility: export

for : (Semigroup e, (Monoid i, Traversable f)) => f a -> (a -> Lazy (Parser i e b)) -> Parser i e (f b)

Visibility: export

take_until : (Semigroup e, Monoid i) => (a -> Bool) -> Parser i e a -> Parser i e (List a)

Visibility: export

get_bit : Num n => Parser Bitstream (SimpleError String) n

Visibility: export

get_bits : Fin 32 -> Parser Bitstream (SimpleError String) Bits32

Visibility: export

get_huff : Fin 32 -> Parser Bitstream (SimpleError String) Bits32

Visibility: export