Byte parsers

@[reducible, inline]

abbrev Parser.ByteParser (ε : Type) (g : Grade) (α : Type) : Type

Equations

• Parser.ByteParser ε g α = Parser ByteArray UInt8 ε g α

def Parser.runBytes {α ε : Type} {g : Grade} (p : ByteParser ε g α) (b : ByteArray) : Except ε α

Equations

• Parser.runBytes p b = Parser.runOn p (Input.ofByteArray b)

def Parser.runBytesOption {α ε : Type} {ge gc : Necessity} (p : ByteParser ε { errors := ge, consumes := gc } α) (b : ByteArray) : Option α

Equations

• Parser.runBytesOption p b = (Parser.runBytes p b).toOption

def Parser.Byte.take1 (k : ℕ) : ByteParser Error conditional ByteArray

Consume exactly k + 1 bytes.

Equations

• Parser.Byte.take1 k = (fun (x : List.Vector UInt8 (k + 1)) => x.toList.toByteArray) <$>ᵍ Parser.count1 k Parser.anyTok

def Parser.Byte.takeRest : ByteParser Error flexible ByteArray

Consume all remaining input.

Equations

• Parser.Byte.takeRest = List.toByteArray <$>ᵍ Parser.anyTok.many

theorem Parser.Byte.many_go_anyTok_restSize {n : ℕ} (t : Input ByteArray n) : (many.go anyTok t).restSize = 0

theorem Parser.Byte.many_go_anyTok_result {n : ℕ} (t : Input ByteArray n) : (many.go anyTok t).result = List.drop t.pos t.buf.data.toList

@[reducible, inline]

abbrev Parser.Byte.uint8 : ByteParser Error conditional UInt8

Read an unsigned 8-bit integer.

Equations

• Parser.Byte.uint8 = Parser.anyTok

def Parser.Byte.int8 : ByteParser Error conditional Int8

Read a signed 8-bit integer.

Equations

• Parser.Byte.int8 = (fun (x : UInt8) => x.toInt8) <$>ᵍ Parser.Byte.uint8

def Parser.Byte.uint16be : ByteParser Error conditional UInt16

Read a big-endian unsigned 16-bit integer.

Equations

• Parser.Byte.uint16be = Parser.Byte.uint8 >>=ᵍ fun (hi : UInt8) => Parser.Byte.uint8 >>=ᵍ fun (lo : UInt8) => gpure (hi.toUInt16 <<< 8 ||| lo.toUInt16)

def Parser.Byte.uint16le : ByteParser Error conditional UInt16

Read a little-endian unsigned 16-bit integer.

Equations

• Parser.Byte.uint16le = Parser.Byte.uint8 >>=ᵍ fun (lo : UInt8) => Parser.Byte.uint8 >>=ᵍ fun (hi : UInt8) => gpure (hi.toUInt16 <<< 8 ||| lo.toUInt16)

def Parser.Byte.uint32be : ByteParser Error conditional UInt32

Read a big-endian unsigned 32-bit integer.

Equations

• Parser.Byte.uint32be = Parser.Byte.uint16be >>=ᵍ fun (hi : UInt16) => Parser.Byte.uint16be >>=ᵍ fun (lo : UInt16) => gpure (hi.toUInt32 <<< 16 ||| lo.toUInt32)

def Parser.Byte.uint32le : ByteParser Error conditional UInt32

Read a little-endian unsigned 32-bit integer.

Equations

• Parser.Byte.uint32le = Parser.Byte.uint16le >>=ᵍ fun (lo : UInt16) => Parser.Byte.uint16le >>=ᵍ fun (hi : UInt16) => gpure (hi.toUInt32 <<< 16 ||| lo.toUInt32)

def Parser.Byte.uint64be : ByteParser Error conditional UInt64

Read a big-endian unsigned 64-bit integer.

Equations

• Parser.Byte.uint64be = Parser.Byte.uint32be >>=ᵍ fun (hi : UInt32) => Parser.Byte.uint32be >>=ᵍ fun (lo : UInt32) => gpure (hi.toUInt64 <<< 32 ||| lo.toUInt64)

def Parser.Byte.uint64le : ByteParser Error conditional UInt64

Read a little-endian unsigned 64-bit integer.

Equations

• Parser.Byte.uint64le = Parser.Byte.uint32le >>=ᵍ fun (lo : UInt32) => Parser.Byte.uint32le >>=ᵍ fun (hi : UInt32) => gpure (hi.toUInt64 <<< 32 ||| lo.toUInt64)

def Parser.Byte.int16be : ByteParser Error conditional Int16

Read a big-endian signed 16-bit integer.

Equations

• Parser.Byte.int16be = (fun (x : UInt16) => x.toInt16) <$>ᵍ Parser.Byte.uint16be

def Parser.Byte.int16le : ByteParser Error conditional Int16

Read a little-endian signed 16-bit integer.

Equations

• Parser.Byte.int16le = (fun (x : UInt16) => x.toInt16) <$>ᵍ Parser.Byte.uint16le

def Parser.Byte.int32be : ByteParser Error conditional Int32

Read a big-endian signed 32-bit integer.

Equations

• Parser.Byte.int32be = (fun (x : UInt32) => x.toInt32) <$>ᵍ Parser.Byte.uint32be

def Parser.Byte.int32le : ByteParser Error conditional Int32

Read a little-endian signed 32-bit integer.

Equations

• Parser.Byte.int32le = (fun (x : UInt32) => x.toInt32) <$>ᵍ Parser.Byte.uint32le

def Parser.Byte.int64be : ByteParser Error conditional Int64

Read a big-endian signed 64-bit integer.

Equations

• Parser.Byte.int64be = (fun (x : UInt64) => x.toInt64) <$>ᵍ Parser.Byte.uint64be

def Parser.Byte.int64le : ByteParser Error conditional Int64

Read a little-endian signed 64-bit integer.

Equations

• Parser.Byte.int64le = (fun (x : UInt64) => x.toInt64) <$>ᵍ Parser.Byte.uint64le