Executable lowering of sequential GraphSpec chains #
This module lowers a chain directly to an execution-polymorphic TorchLean.Program. Parameters
remain ordered by the chain's type-level ABI and are split at the same structural boundaries as in
the pure interpreter.
def
NN.GraphSpec.Chain.toProgram
{ps : List Spec.Shape}
{σ τ : Spec.Shape}
(g : Chain ps σ τ)
{α : Type}
[TorchLean.Storage α]
[Context α]
:
Runtime.Autograd.Model.Program α (ps ++ [σ]) τ
Lower a sequential Chain to an execution-polymorphic TorchLean program.
Instances For
def
NN.GraphSpec.Chain.toProgram.lowerRefList
{α : Type}
[TorchLean.Storage α]
[Context α]
{m : Type → Type}
(_instM : Monad m)
(_instOps : Runtime.Autograd.Torch.Ops m α)
{ps : List Spec.Shape}
{σ τ : Spec.Shape}
(g : Chain ps σ τ)
(rs : Runtime.Autograd.Torch.RefList (fun (s : Spec.Shape) => Runtime.Autograd.Torch.Ops.Ref m α s) (ps ++ [σ]))
:
have Ref := fun (s : Spec.Shape) => Runtime.Autograd.Torch.Ops.Ref m α s;
m (Ref τ)