Network.TLS.Parsing

Reexports

Definitions

record Parserializer : Type -> Type -> Type -> Type -> Type

  bidirectional serializer
  `decode` is assumed to be the inverse of `encode` and vice versa

Totality: total
Visibility: public export
Constructor: 

MkParserializer : (a -> List c) -> Parser i e a -> Parserializer c i e a

Projections:

.decode : Parserializer c i e a -> Parser i e a

.encode : Parserializer c i e a -> a -> List c

.encode : Parserializer c i e a -> a -> List c

Visibility: public export

encode : Parserializer c i e a -> a -> List c

Visibility: public export

.decode : Parserializer c i e a -> Parser i e a

Visibility: public export

decode : Parserializer c i e a -> Parser i e a

Visibility: public export

apair : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (a, b)

Visibility: export

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

  infixr for `apair`

Visibility: export
Fixity Declaration: infixr operator, level 5

map : (a -> b) -> (b -> a) -> Parserializer c i e a -> Parserializer c i e b

Visibility: export

mapEither : (Semigroup e, Monoid i) => (a -> Either e b) -> (b -> a) -> Parserializer c i e a -> Parserializer c i e b

Visibility: export

(*>) : (Semigroup e, Monoid i) => Parserializer c i e () -> Parserializer c i e a -> Parserializer c i e a

Visibility: export
Fixity Declaration: infixl operator, level 3

(<*) : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e () -> Parserializer c i e a

Visibility: export
Fixity Declaration: infixl operator, level 3

aeither : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (Either a b)

Visibility: export

(<|>) : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (Either a b)

Visibility: export
Fixity Declaration: infixr operator, level 2

record Posed : Type -> Type

  essentially (Nat, `a`), where Nat denotes the position, usually starts with 0

Totality: total
Visibility: public export
Constructor: 

MkPosed : Nat -> a -> Posed a

Projections:

.get : Posed a -> a

.pos : Posed a -> Nat

.pos : Posed a -> Nat

Visibility: public export

pos : Posed a -> Nat

Visibility: public export

.get : Posed a -> a

Visibility: public export

get : Posed a -> a

Visibility: public export

p_get : Cons (Posed c) i => Parser i e c

  `Parser.token` but for `Posed`

Visibility: export

prepend_length : Nat -> List Bits8 -> List Bits8

  prepend the length of `body` into `n` bytes in big endian

Visibility: export

p_nat : (Semigroup e, (Monoid i, Cons (Posed Bits8) i)) => Nat -> Parser i e Nat

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

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

under : e -> Parserializer c i (SimpleError e) a -> Parserializer c i (SimpleError e) a

  put parser error messages under another message
  used for creating a treeish error message

Visibility: export

token : (Semigroup e, (Cons (Posed c) i, Monoid i)) => Parserializer c i e c

  parserialize a single posed token

Visibility: export

ntokens : (Semigroup e, (Cons (Posed c) i, Monoid i)) => (n : Nat) -> Parserializer c i e (Vect n c)

  parserialize `n` posed tokens

Visibility: export

lengthed : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parserializer Bits8 i (SimpleError String) a -> Parserializer Bits8 i (SimpleError String) a

  parserialize the next `n` bytes in big endian style as a length describing the number of bytes of the following data to be fed to `pser`

Visibility: export

lengthed_list : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parserializer Bits8 i (SimpleError String) a -> Parserializer Bits8 i (SimpleError String) (List a)

  parserialize the next `n` bytes in big endian style as a length describing the number of bytes of the following data to be fed to `pser`
  when `pser` completes, the result becomes an entry in the resulting list
  when there are exactly zero bytes left, the list of results is returned
  if under feeding `pser` for the last entry, the parser fails

Visibility: export

lengthed_list1 : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parserializer Bits8 i (SimpleError String) a -> Parserializer Bits8 i (SimpleError String) (List1 a)

  `lengthed_list` but `List1`

Visibility: export

nat : Semigroup e => (Cons (Posed Bits8) i, Monoid i) => Nat -> Parserializer Bits8 i e Nat

  basically the parserializer version of `p_nat`

Visibility: export

is : (Cons (Posed Bits8) i, Monoid i) => Vect (S k) Bits8 -> Parserializer Bits8 i (SimpleError String) ()

  parserialize a list of bytes with nice error messages specialized for displaying byte sequences

Visibility: export