16.5. Decoder Monad🔗

Decoding is the inverse of encoding: binary bytes back to structured types. The decoder uses a monadic combinator approach — a Decoder α consumes bytes from a DecodeState and returns Option (α × DecodeState).

structure

Jar.Codec.DecodeState : Type
Jar.Codec.DecodeState : Type

State for the decoder: a ByteArray and a current position.

Constructor

Jar.Codec.DecodeState.mk

Fields

data : ByteArray

pos : Nat

def

Jar.Codec.Decoder (α : Type) : Type
Jar.Codec.Decoder (α : Type) : Type

Decoder monad: a function from state to an optional (result, new state).

def

Jar.Codec.Decoder.run {α : Type} (d : Decoder α) (data : ByteArray) :
  Option α
Jar.Codec.Decoder.run {α : Type}
  (d : Decoder α) (data : ByteArray) :
  Option α

Run a decoder on a ByteArray starting at position 0.

def

Jar.Codec.Decoder.bind {α β : Type} (d : Decoder α)
  (f : α → Decoder β) : Decoder β
Jar.Codec.Decoder.bind {α β : Type}
  (d : Decoder α) (f : α → Decoder β) :
  Decoder β

Bind: sequence two decoders.

def

Jar.Codec.Decoder.readBytes (n : Nat) : Decoder ByteArray
Jar.Codec.Decoder.readBytes (n : Nat) :
  Decoder ByteArray

Read exactly n bytes from the input.

def

Jar.Codec.Decoder.pure {α : Type} (a : α) : Decoder α
Jar.Codec.Decoder.pure {α : Type}
  (a : α) : Decoder α

Pure: return a value without consuming any input.

def

Jar.Codec.Decoder.guard (b : Bool) : Decoder Unit
Jar.Codec.Decoder.guard (b : Bool) :
  Decoder Unit

Guard: fail if condition is false.

def

Jar.Codec.Decoder.readByte : Decoder UInt8
Jar.Codec.Decoder.readByte : Decoder UInt8

Read a single byte.

def

Jar.Codec.Decoder.remaining : Decoder Nat
Jar.Codec.Decoder.remaining : Decoder Nat

Check remaining bytes available.

def

Jar.Codec.Decoder.replicateD {α : Type} (n : Nat) (d : Decoder α) :
  Decoder (Array α)
Jar.Codec.Decoder.replicateD {α : Type}
  (n : Nat) (d : Decoder α) :
  Decoder (Array α)

Decode an array by repeating a decoder exactly n times.