Heterogeneous graph interpretation

An interpreter supplies a scalar family indexed by DType, its storage, available arithmetic, and explicit conversions. Values still contain ordinary TorchLean tensors. Shape erasure reuses Spec.SomeTensor; only the element-type index is added at the interchange boundary.

Ordinary numeric nodes reuse Graph.evalNodeRaw. Typed casts and registered custom operations are dispatched separately, with the result's scalar type fixed by the program's type assignment. Unsupported types and operations return errors. No cast is implemented by relabeling a tensor or converting through host Float. Layout operations reuse Graph.evalTransform and need only storage, not arithmetic. Pointwise operators reuse Graph.evalPointwise, which also needs only storage: a type with an arithmetic dictionary takes their meanings from Spec.PointwiseOp.meaning, and a type without one, such as an integer type, from the interpreter's own pointwise table.

structure NN.IR.Interpreter : Type 1

Scalar representations and operations supplied to the shared typed graph interpreter.

• Scalar : DType → Type

  Actual Lean carrier for each element descriptor.

• storage (dtype : DType) : TorchLean.Storage (self.Scalar dtype)

  Physical tensor representation for that carrier.

• supported : DType → Bool

  Whether this interpreter implements the described element representation.

• arithmetic (dtype : DType) : Option (Context (self.Scalar dtype))

  Optional full arithmetic dictionary, used by the existing numerical operator evaluator.

• cast (source target : DType) : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode → self.Scalar source → Except String (self.Scalar target × FloatLib.Floats.ExecFloat.ConversionStatus)

  Convert one element, retaining flags; failures are explicit.

• pointwise (dtype : DType) : Spec.PointwiseTable (self.Scalar dtype)

  Pointwise operators for element types without an arithmetic dictionary, such as integers. Types with a dictionary use Spec.PointwiseOp.meaning instead; the default lists none.

structure NN.IR.Interpreter.Value (interpreter : Interpreter) : Type

A tensor with both its element descriptor and its shape preserved.

• dtype : DType
• tensor : Spec.SomeTensor (interpreter.Scalar self.dtype)

def NN.IR.Interpreter.Value.shape {interpreter : Interpreter} (value : interpreter.Value) : Spec.Shape

Runtime shape retained by the shared tensor package.

def NN.IR.Interpreter.Value.get {interpreter : Interpreter} (value : interpreter.Value) (dtype : DType) : Except String (Spec.SomeTensor (interpreter.Scalar dtype))

Recover a tensor only after checking its element-type index.

structure NN.IR.Interpreter.Payload (interpreter : Interpreter) : Type

Typed constants, existing homogeneous parameter stores, and extension implementations.

• constant? : ℕ → Option interpreter.Value

  Constants retain their actual scalar carrier, including Boolean and integer tensors.

• homogeneous (dtype : DType) : IR.Payload (interpreter.Scalar dtype)

  Existing numerical payloads, selected at the operation's scalar type.

• call (name : Lean.Name) (output : DType) : Array interpreter.Value → Except String (Spec.SomeTensor (interpreter.Scalar output) × FloatLib.Floats.ExecFloat.ConversionStatus)

  Implement a registered operation at its declared output type; names are not guessed.

def NN.IR.Interpreter.castTensor (interpreter : Interpreter) (source target : DType) (shape : Spec.Shape) (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (tensor : TorchLean.Tensor (interpreter.Scalar source) shape) : Except String (TorchLean.Tensor (interpreter.Scalar target) shape × FloatLib.Floats.ExecFloat.ConversionStatus)

Convert a tensor element by element, accumulating FloatLib's conversion flags.

def NN.IR.Interpreter.evalNode (interpreter : Interpreter) (program : Program) (payload : interpreter.Payload) (arguments values : Array interpreter.Value) (node : Node) : Except String (interpreter.Value × FloatLib.Floats.ExecFloat.ConversionStatus)

Evaluate one node using already computed values and a complete argument table.

def NN.IR.Interpreter.run (interpreter : Interpreter) (program : Program) (payload : interpreter.Payload) (arguments : Array interpreter.Value) : Except String (Array interpreter.Value × FloatLib.Floats.ExecFloat.ConversionStatus)

Evaluate a typed program, returning every intermediate tensor and accumulated cast flags.

def NN.IR.Interpreter.eval (interpreter : Interpreter) (program : Program) (payload : interpreter.Payload) (arguments : Array interpreter.Value) : Except String (Array interpreter.Value × FloatLib.Floats.ExecFloat.ConversionStatus)

Evaluate the designated results in return order, retaining conversion flags.