Decoding and encoding iterators

Decoders and encoders transform pure iterators, Std.Iter over Id, of one kind of token into another: bytes into code units, code units into characters, and back.

A decoder d : δ with [Decoder δ τ σ] reads one token of type σ from the tokens of type τ at an iterator: Decoder.decode d it continues with the token and the iterator after it, with a DecodeError.Kind and the iterator after the ill-formed input, or with the end of the input. It looks ahead by stepping copies of it, so it needs no buffer. DecodeIterator δ ι repeats it over an iterator of type ι. A strict decoding iterator stops at ill-formed input, where it.decodeError? tells why, it.decodeFailure? finds the first ill-formed input ahead, and it.decodeContinue? goes on after it; a lossy one yields Decoder.replacement d instead and goes on after the ill-formed input. it.decodeFold folds over the tokens and returns the iterator where decoding stopped. DecodeError.Kind and DecodeError have ToString instances for error messages.

An encoder e : ε with [Encoder ε σ τ] gives the tokens of type τ that encode a token of type σ, and EncodeIterator ε ι yields them for each token of an iterator of type ι.

Each step of these iterators either moves the inner iterator strictly forward or, for encoders, yields a token that is still pending from the last one. The inner iterator is it.decodeBase or it.encodeBase, and it.encodeBoundary tells whether nothing is pending. Decoders always stop between two tokens, so the position of the inner iterator is the position of the error.

def Unicode.Advanced {ι τ : Type} [Std.Iterator ι Id τ] (it' it : Std.Iter τ) : Prop

it' is reachable from it by one or more plausible successor steps.

Equations

• Unicode.Advanced it' it = it'.finitelyManySteps!.Rel it.finitelyManySteps!

theorem Unicode.Advanced.trans {ι τ : Type} [Std.Iterator ι Id τ] {it'' it' it : Std.Iter τ} : Advanced it'' it' → Advanced it' it → Advanced it'' it

theorem Unicode.Advanced.of_yield {ι τ : Type} [Std.Iterator ι Id τ] {it' it : Std.Iter τ} {out : τ} (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) : Advanced it' it

theorem Unicode.Advanced.of_skip {ι τ : Type} [Std.Iterator ι Id τ] {it' it : Std.Iter τ} (h : it.IsPlausibleStep (Std.IterStep.skip it')) : Advanced it' it

@[inline]

def Unicode.nextToken {ι τ : Type} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] {β : Sort u_1} (it : Std.Iter τ) (yield : (rest : Std.Iter τ) → Advanced rest it → τ → β) (done : Unit → β) : β

Steps it past any skip steps. Calls yield with the next token and the iterator after it, or done at the end of the input. Written in continuation-passing style, and inlined, so that specialization avoids allocating an intermediate result. Further skip steps go through a loop that returns data rather than taking yield: a continuation passed into that loop would become a closure, allocated for every token even when nothing skips.

Equations

• One or more equations did not get rendered due to their size.

inductive Unicode.DecodeError.Kind : Type

Why input is ill-formed.

• illFormedUTF8 : Kind

  A maximal subpart of an ill-formed UTF-8 byte sequence.

• unpairedSurrogate : Kind

  A UTF-16 surrogate code unit that is not part of a surrogate pair.

• notScalarValue : Kind

  A UTF-32 code unit that is not a Unicode scalar value.

• incompleteCodeUnit : Kind

  An incomplete code unit at the end of the bytes of UTF-16 or UTF-32 code units.

@[instance_reducible]

instance Unicode.DecodeError.instInhabitedKind : Inhabited Kind

Equations

• Unicode.DecodeError.instInhabitedKind = { default := Unicode.DecodeError.instInhabitedKind.default }

@[instance_reducible]

instance Unicode.DecodeError.instDecidableEqKind : DecidableEq Kind

Equations

• Unicode.DecodeError.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Unicode.DecodeError.instReprKind : Repr Kind

Equations

• Unicode.DecodeError.instReprKind = { reprPrec := Unicode.DecodeError.instReprKind.repr }

def Unicode.DecodeError.instReprKind.repr : Kind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Unicode.DecodeError.Kind.toString : Kind → String

A description of ill-formed input of kind k, for error messages.

Equations

• Unicode.DecodeError.Kind.illFormedUTF8.toString = "ill-formed UTF-8"
• Unicode.DecodeError.Kind.unpairedSurrogate.toString = "unpaired surrogate"
• Unicode.DecodeError.Kind.notScalarValue.toString = "not a Unicode scalar value"
• Unicode.DecodeError.Kind.incompleteCodeUnit.toString = "incomplete code unit"

@[instance_reducible]

instance Unicode.instToStringKind : ToString DecodeError.Kind

Equations

• Unicode.instToStringKind = { toString := Unicode.DecodeError.Kind.toString }

structure Unicode.DecodeError : Type

Ill-formed input: why, and where. The position is the index of the first token of the ill-formed input: of the code unit for UTF-16 and UTF-32, and of the byte for UTF-8 and the encoding schemes, counting a byte order mark or signature.

• kind : Kind

  Why the input is ill-formed.

• pos : Nat

  The index of the first token of the ill-formed input, in code units or bytes.

@[instance_reducible]

instance Unicode.instInhabitedDecodeError : Inhabited DecodeError

Equations

• Unicode.instInhabitedDecodeError = { default := Unicode.instInhabitedDecodeError.default }

@[instance_reducible]

instance Unicode.instDecidableEqDecodeError : DecidableEq DecodeError

Equations

• Unicode.instDecidableEqDecodeError = Unicode.instDecidableEqDecodeError.decEq

def Unicode.instDecidableEqDecodeError.decEq (x✝ x✝¹ : DecodeError) : Decidable (x✝ = x✝¹)

Equations

• Unicode.instDecidableEqDecodeError.decEq { kind := a, pos := a_1 } { kind := b, pos := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Unicode.instReprDecodeError.repr : DecodeError → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Unicode.instReprDecodeError : Repr DecodeError

Equations

• Unicode.instReprDecodeError = { reprPrec := Unicode.instReprDecodeError.repr }

def Unicode.DecodeError.toString (e : DecodeError) : String

A description of the error e for error messages, such as unpaired surrogate at offset 2. The offset is e.pos, in code units or bytes as the decoding function tells.

Equations

• e.toString = toString e.kind ++ toString " at offset " ++ toString e.pos

@[instance_reducible]

instance Unicode.instToStringDecodeError : ToString DecodeError

Equations

• Unicode.instToStringDecodeError = { toString := Unicode.DecodeError.toString }

Decoders

class Unicode.Decoder (δ : Type) (τ σ : outParam Type) : Type 1

A decoder d : δ reads tokens of type σ from tokens of type τ.

• replacement : δ → σ

  The token that lossy decoding yields for ill-formed input.

• decode {ι : Type} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] {β : Type} (d : δ) (it : Std.Iter τ) (yield : (rest : Std.Iter τ) → Advanced rest it → σ → β) (error : DecodeError.Kind → (rest : Std.Iter τ) → Advanced rest it → β) (done : Unit → β) : β

  Decodes one token from it. Calls yield with the token and the iterator after it, error with the error and the iterator after the ill-formed input, or done at the end of the input.

structure Unicode.DecodeIterator (δ ι : Type) {τ σ : Type} [Decoder δ τ σ] : Type

Iterator over the tokens decoded by decoder from an iterator of type ι.

• decoder : δ

  The decoder.

• lossy : Bool

  Whether ill-formed input yields Decoder.replacement decoder rather than ending.

• inner : Std.Iter τ

  The input iterator.

@[instance_reducible]

instance Unicode.DecodeIterator.instIteratorId {δ ι τ σ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] : Std.Iterator (DecodeIterator δ ι) Id σ

Equations

• One or more equations did not get rendered due to their size.

theorem Unicode.DecodeIterator.advanced_of_successor {δ ι τ σ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] {it' it : Std.IterM Id σ} (h : it'.IsPlausibleSuccessorOf it) : Advanced it'.internalState.inner it.internalState.inner

Every step moves the input iterator strictly forward.

instance Unicode.DecodeIterator.instFiniteId {δ ι τ σ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Std.Iterators.Finite ι Id] : Std.Iterators.Finite (DecodeIterator δ ι) Id

@[instance_reducible, instance 100]

instance Unicode.DecodeIterator.instIteratorLoopIdOfMonad {δ ι τ σ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] {m : Type u_1 → Type u_2} [Monad m] : Std.IteratorLoop (DecodeIterator δ ι) Id m

Equations

• Unicode.DecodeIterator.instIteratorLoopIdOfMonad = Std.IteratorLoop.defaultImplementation

@[implemented_by _private.UnicodeFormat.Iterator.Basic.0.Unicode.DecodeIterator.forInImpl]

def Unicode.DecodeIterator.forIn {δ ι τ σ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] {n : Type → Type} [Monad n] (lift : (γ δ : Type) → (γ → n δ) → Id γ → n δ) (γ : Type) (Pl : σ → γ → ForInStep γ → Prop) (it : Std.IterM Id σ) (init : γ) (f : (b : σ) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) : n γ

The loop behind for loops and the Std.Iterators consumers on decoding iterators. Logically it is Std.IteratorLoop.defaultImplementation, which steps the iterator one token at a time; it is implemented by decoding directly from the input iterator.

Equations

• Unicode.DecodeIterator.forIn lift γ Pl it init f = Std.IteratorLoop.forIn lift γ Pl it init f

@[instance_reducible]

instance Unicode.DecodeIterator.instIteratorLoopIdOfMonad_1 {δ ι τ σ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] {n : Type → Type} [Monad n] : Std.IteratorLoop (DecodeIterator δ ι) Id n

Equations

• Unicode.DecodeIterator.instIteratorLoopIdOfMonad_1 = { forIn := Unicode.DecodeIterator.forIn }

instance Unicode.DecodeIterator.instLawfulIteratorLoopId {δ ι τ σ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] {n : Type → Type} [Monad n] : Std.LawfulIteratorLoop (DecodeIterator δ ι) Id n

@[inline]

def Std.Iter.decodeBase {δ ι τ σ : Type} [Unicode.Decoder δ τ σ] (it : Iter σ) : Iter τ

The input iterator, at the start of the next token to decode.

Equations

• it.decodeBase = it.internalState.inner

def Std.Iter.decodeError? {δ ι τ σ : Type} [Unicode.Decoder δ τ σ] [Iterator ι Id τ] [Iterators.Productive ι Id] (it : Iter σ) : Option Unicode.DecodeError.Kind

The error in the input at it, if the input there is ill-formed. When a strict decoding iterator stops, this is why: none means that it reached the end of the input.

Equations

• One or more equations did not get rendered due to their size.

def Std.Iter.decodeContinue? {δ ι τ σ : Type} [Unicode.Decoder δ τ σ] [Iterator ι Id τ] [Iterators.Productive ι Id] (it : Iter σ) : Option (Unicode.DecodeError.Kind × { next : Iter σ // Unicode.Advanced next it })

The kind of the ill-formed input at it, if there is one, and the iterator after it, with the same decoder and mode. A strict decoding iterator stops at ill-formed input: this is how a client such as a parser goes on after it. The iterator after the ill-formed input comes with the proof that it is reachable from it, for clients that track progress.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iter.decodeIsLossy {δ ι τ σ : Type} [Unicode.Decoder δ τ σ] (it : Iter σ) : Bool

Whether it yields Decoder.replacement for ill-formed input rather than ending there.

Equations

• it.decodeIsLossy = it.internalState.lossy

@[inline]

def Unicode.Decoder.iter {δ ι τ σ : Type} [Decoder δ τ σ] (d : δ) (it : Std.Iter τ) : Std.Iter σ

Decodes the tokens of it with d, stopping at the first ill-formed input.

A for loop or fold over the result ends at ill-formed input just as at the end of the input. To tell them apart, fold with decodeFold, which also returns the iterator where decoding stopped, and check decodeError? there, find the first ill-formed input ahead with decodeFailure?, or decode with Decoder.iterLossy instead.

Equations

• Unicode.Decoder.iter d it = { internalState := { decoder := d, lossy := false, inner := it } }

@[inline]

def Unicode.Decoder.iterLossy {δ ι τ σ : Type} [Decoder δ τ σ] (d : δ) (it : Std.Iter τ) : Std.Iter σ

Decodes the tokens of it with d, replacing each ill-formed input with Decoder.replacement d.

Equations

• Unicode.Decoder.iterLossy d it = { internalState := { decoder := d, lossy := true, inner := it } }

@[irreducible, specialize #[]]

def Unicode.Decoder.foldUntilError {δ ι τ σ γ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] (d : δ) (f : γ → σ → γ) (init : γ) (it : Std.Iter τ) : γ × Option (DecodeError.Kind × Std.Iter τ)

Decodes the tokens of it with d and folds them with f from init, up to the first ill-formed input. Returns the result, and the kind of error and the iterator at the ill-formed input, if any.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible, specialize #[]]

def Unicode.Decoder.foldLossy {δ ι τ σ γ : Type} [Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] (d : δ) (f : γ → σ → γ) (init : γ) (it : Std.Iter τ) : γ

Decodes the tokens of it with d and folds them with f from init, with Decoder.replacement d for each ill-formed input.

Equations

• One or more equations did not get rendered due to their size.

def Std.Iter.decodeFailure? {δ ι τ σ : Type} [Unicode.Decoder δ τ σ] [Iterator ι Id τ] [Iterators.Finite ι Id] (it : Iter σ) : Option (Unicode.DecodeError.Kind × Iter σ)

The first ill-formed input from it on, if any: its kind, and the iterator with the same decoder at its start. A strict decoding iterator stops there, so this finds where and why a parser or a loop over it would see the end of the input early.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iter.decodeFold {δ ι τ σ : Type} [Unicode.Decoder δ τ σ] [Iterator ι Id τ] [Iterators.Finite ι Id] {γ : Type} (f : γ → σ → γ) (init : γ) (it : Iter σ) : γ × Iter σ

Folds f over the tokens of it from init, and returns the result with the iterator where decoding stopped: at the end of the input, or for a strict decoding iterator at ill-formed input. There, decodeError? tells why and decodeContinue? goes on after it. A for loop or fold gives the result alone.

Equations

• One or more equations did not get rendered due to their size.

Encoders

class Unicode.Encoder (ε : Type) (σ τ : outParam Type) : Type

An encoder e : ε writes each token of type σ as tokens of type τ.

• length : ε → σ → Nat

  The number of tokens that encode x.

• unit : ε → σ → Nat → τ

  The token at index i of the encoding of x, for i < length e x.

structure Unicode.EncodeIterator (ε ι : Type) {σ τ : Type} [Encoder ε σ τ] : Type

Iterator over the tokens that encoder writes for each token of an iterator of type ι. The encoding of the last input token current has length tokens, of which those before index have been yielded.

• encoder : ε

  The encoder.

• inner : Std.Iter σ

  The input iterator, after current.

• current : σ

  The last input token.

• index : Nat

  The index of the next token of the encoding of current.

• length : Nat

  The number of tokens of the encoding of current.

@[reducible]

def Unicode.EncodeIterator.PlausibleStep {ε ι σ τ : Type} [Encoder ε σ τ] [Std.Iterator ι Id σ] (it : Std.IterM Id τ) : Std.IterStep (Std.IterM Id τ) τ → Prop

Plausible steps: yield a pending token, or read the next input token.

Equations

• One or more equations did not get rendered due to their size.
• Unicode.EncodeIterator.PlausibleStep it Std.IterStep.done = (¬it.internalState.index < it.internalState.length ∧ it.internalState.inner.IsPlausibleStep Std.IterStep.done)

@[instance_reducible]

instance Unicode.EncodeIterator.instIteratorId {ε ι σ τ : Type} [Encoder ε σ τ] [Std.Iterator ι Id σ] : Std.Iterator (EncodeIterator ε ι) Id τ

Equations

• One or more equations did not get rendered due to their size.

instance Unicode.EncodeIterator.instFiniteId {ε ι σ τ : Type} [Encoder ε σ τ] [Std.Iterator ι Id σ] [Std.Iterators.Finite ι Id] : Std.Iterators.Finite (EncodeIterator ε ι) Id

@[instance_reducible, instance 100]

instance Unicode.EncodeIterator.instIteratorLoopIdOfMonad {ε ι σ τ : Type} [Encoder ε σ τ] [Std.Iterator ι Id σ] {m : Type u_1 → Type u_2} [Monad m] : Std.IteratorLoop (EncodeIterator ε ι) Id m

Equations

• Unicode.EncodeIterator.instIteratorLoopIdOfMonad = Std.IteratorLoop.defaultImplementation

@[implemented_by _private.UnicodeFormat.Iterator.Basic.0.Unicode.EncodeIterator.forInImpl]

def Unicode.EncodeIterator.forIn {ε ι σ τ : Type} [Encoder ε σ τ] [Std.Iterator ι Id σ] {n : Type x → Type x'} [Monad n] [Std.Iterators.Productive ι Id] (lift : (γ : Type) → (δ : Type x) → (γ → n δ) → Id γ → n δ) (γ : Type x) (Pl : τ → γ → ForInStep γ → Prop) (it : Std.IterM Id τ) (init : γ) (f : (b : τ) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) : n γ

The loop behind for loops and the Std.Iterators consumers on encoding iterators. Logically it is Std.IteratorLoop.defaultImplementation, which steps the iterator one token at a time; it is implemented by reading the input iterator directly.

Equations

• Unicode.EncodeIterator.forIn lift γ Pl it init f = Std.IteratorLoop.forIn lift γ Pl it init f

@[instance_reducible]

instance Unicode.EncodeIterator.instIteratorLoopIdOfMonadOfProductive {ε ι σ τ : Type} [Encoder ε σ τ] [Std.Iterator ι Id σ] {n : Type x → Type x'} [Monad n] [Std.Iterators.Productive ι Id] : Std.IteratorLoop (EncodeIterator ε ι) Id n

Equations

• Unicode.EncodeIterator.instIteratorLoopIdOfMonadOfProductive = { forIn := Unicode.EncodeIterator.forIn }

instance Unicode.EncodeIterator.instLawfulIteratorLoopId {ε ι σ τ : Type} [Encoder ε σ τ] [Std.Iterator ι Id σ] {n : Type x → Type x'} [Monad n] [Std.Iterators.Productive ι Id] : Std.LawfulIteratorLoop (EncodeIterator ε ι) Id n

@[inline]

def Std.Iter.encodeBase {ε ι σ τ : Type} [Unicode.Encoder ε σ τ] (it : Iter τ) : Iter σ

The input iterator, after the token whose encoding is being yielded.

Equations

• it.encodeBase = it.internalState.inner

@[inline]

def Std.Iter.encodeBoundary {ε ι σ τ : Type} [Unicode.Encoder ε σ τ] (it : Iter τ) : Bool

Whether the encoding of the last input token has been yielded entirely.

Equations

• it.encodeBoundary = decide (it.internalState.length ≤ it.internalState.index)

@[inline]

def Unicode.Encoder.iter {ε ι σ τ : Type} [Encoder ε σ τ] [Inhabited σ] (e : ε) (it : Std.Iter σ) : Std.Iter τ

Encodes the tokens of it with e.

Equations

• Unicode.Encoder.iter e it = { internalState := { encoder := e, inner := it, current := default, index := 0, length := 0 } }