Eager Tensor Operations

PyTorch-style tensor operations recorded on the session's tape. Each one runs the CPU or the CUDA kernel of the operation, as the session's device selects, and preserves the typed TensorRef surface.

Tensor ops (eager tape wrappers)

The following definitions are the eager front-end for the tape constructors. Each one:

• takes the session's tape out of s.tape,
• appends a new node with the CPU constructor (Runtime.Autograd.Tape.*) or the CUDA one (Runtime.Autograd.LibTorch.Tape.*), as the session's device selects,
• writes the extended tape back, and
• returns a fresh TensorRef pointing to the new node id.

PyTorch comparison: this is the standard eager autograd mechanism (a dynamic tape of ops).

def Runtime.Autograd.Torch.Internal.EagerSession.execute {α : Type} [TorchLean.Storage α] {sh : Spec.Shape} (s : EagerSession α) (op : NN.Backend.BackendOp) (refs : Array (Option RefIdentity)) (cpu : IO (TensorRef α sh)) (cuda : IO (Option (TensorRef α sh))) : IO (TensorRef α sh)

Dispatch an eager operation through its selected CPU or CUDA capsule.

The selected capsule is bound to the matching handler before any implementation runs. Returning none means the operation has no implementation in this CUDA runtime; there is no per-operation CPU fallback.

def Runtime.Autograd.Torch.Internal.EagerSession.executeRecorded {α : Type} [TorchLean.Storage α] {sh : Spec.Shape} (s : EagerSession α) (op : NN.Backend.BackendOp) (refs : Array (Option RefIdentity)) (cpu cuda : IO ℕ) : IO (TensorRef α sh)

Dispatch two recording actions that return node ids.

Both actions remain delayed until execute validates the references and selects a handler, including any scalar transfers performed by the CUDA action.