Executable lowering of GraphSpec DAGs

This module lowers typed DAG terms and multi-result blocks into execution-polymorphic TorchLean programs over backend tensor references.

def NN.GraphSpec.DAG.Env.rget {Ref : Spec.Shape → Type} {Γ : List Spec.Shape} {s : Spec.Shape} : Runtime.Autograd.Torch.RefList Ref Γ → Var Γ s → Ref s

Typed environment lookup for backend references.

This is the underlying “variable semantics” for Term.lower.

Lowering to TorchLean programs

def NN.GraphSpec.DAG.Term.lowerArgs {Γ ins : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Runtime.Autograd.Torch.Ops m α] (env : Runtime.Autograd.Torch.RefList (Runtime.Autograd.Model.RefTy m α) Γ) : Args Γ ins → m (Runtime.Autograd.Torch.RefList (Runtime.Autograd.Model.RefTy m α) ins)

Lower a typed argument list by lowering each component term under the same environment.

def NN.GraphSpec.DAG.Term.lower {Γ : List Spec.Shape} {τ : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Runtime.Autograd.Torch.Ops m α] (env : Runtime.Autograd.Torch.RefList (Runtime.Autograd.Model.RefTy m α) Γ) : Term Γ τ → m (Runtime.Autograd.Model.RefTy m α τ)

Lower a typed Term Γ τ into the execution monad m, producing a reference to a tensor of shape τ.

This is the "executable" counterpart of Term.eval: instead of returning a pure TorchLean.Tensor, we emit runtime operations (Runtime.Autograd.Torch.Ops) that allocate tensors and apply primitives.

def NN.GraphSpec.DAG.Block.lower {Γ outs : List Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] {μ : Type → Type} [Monad μ] [Runtime.Autograd.Torch.Ops μ α] (env : Runtime.Autograd.Torch.RefList (Runtime.Autograd.Model.RefTy μ α) Γ) : Block Γ outs → μ (Runtime.Autograd.Torch.RefList (Runtime.Autograd.Model.RefTy μ α) outs)

Lower a multi-output block for an arbitrary TorchLean execution target.