Vocabulary Projection

A bounded vocabulary retains token ids in first-occurrence order. Local id zero is reserved for an explicit unknown token; tokens beyond capacity map to it. Token streams remain tensors while the reverse lookup uses a hash map of vocabulary metadata.

structure TorchLean.text.VocabularyProjection (capacity : ℕ) : Type

Original token ids and reverse lookup for an assigned prefix of a fixed-capacity vocabulary.

• originals : Tensor ℕ [capacity]

  Original token ids in local-id order; only the assigned prefix is used.

• size : ℕ

  Number of assigned local ids, including the reserved unknown-token slot.

• size_le_capacity : self.size ≤ capacity

  The assigned prefix fits in the storage tensor.

• toLocalMap : Std.HashMap ℕ ℕ

  Lookup from original token ids to their assigned local ids.

• unknownToken : ℕ

  Original token id returned when decoding an unassigned local id.

def TorchLean.text.VocabularyProjection.toLocal {capacity : ℕ} (vocab : VocabularyProjection capacity) (id : ℕ) : ℕ

Map an original token id to its assigned local id, defaulting to the unknown-token slot.

def TorchLean.text.VocabularyProjection.toOriginal {capacity : ℕ} (vocab : VocabularyProjection capacity) (localId : ℕ) : ℕ

Decode an assigned local id, using the explicit unknown token for an unassigned id.

def TorchLean.text.VocabularyProjection.singleton (capacity unknownToken : ℕ) [NeZero capacity] : VocabularyProjection capacity

Start a vocabulary with one reserved unknown token.

def TorchLean.text.VocabularyProjection.extend {capacity : ℕ} {shape : Shape} (vocab : VocabularyProjection capacity) (tokens : Tensor ℕ shape) : VocabularyProjection capacity

Extend in row-major token order, retaining existing ids when capacity is full.

def TorchLean.text.VocabularyProjection.fromTokens (capacity unknownToken : ℕ) [NeZero capacity] {shape : Shape} (tokens : Tensor ℕ shape) : VocabularyProjection capacity

Build a vocabulary from a token tensor, reserving local id zero for unknownToken.

def TorchLean.text.VocabularyProjection.encode {capacity : ℕ} {shape : Shape} (vocab : VocabularyProjection capacity) (tokens : Tensor ℕ shape) : Tensor ℕ shape

Project every token while retaining the shape of the original stream or batch.

def TorchLean.text.VocabularyProjection.decode {capacity : ℕ} {shape : Shape} (vocab : VocabularyProjection capacity) (tokens : Tensor ℕ shape) : Tensor ℕ shape

Decode every local token while retaining the stream or batch shape.