TorchLean Module Runtime Facade

Executable module operations for advanced runtime and example code.

@[reducible, inline]

abbrev TorchLean.Module.ScalarModule (α : Type) [Context α] [DecidableEq Spec.Shape] (paramShapes inputShapes : List Spec.Shape) : Type

Executable module instance with mutable runtime parameters and optimizer state.

@[reducible, inline]

abbrev TorchLean.Module.ScalarModuleDef (paramShapes inputShapes : List Spec.Shape) : Type 1

The module-definition type used by Module runtime operations.

def TorchLean.Module.instantiate {α : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] {paramShapes inputShapes : List Shape} (opts : Options) (defn : ScalarModuleDef paramShapes inputShapes) (cast : Float → α := Runtime.ofFloat) : IO (ScalarModule α paramShapes inputShapes)

Instantiate an executable runtime module from a public ScalarModuleDef.

This is the generic public entrypoint for custom runtime tasks outside the standard supervised module constructors such as Module.instantiateMse or Module.instantiateCrossEntropyOneHot.

def TorchLean.Module.predict1 {σ τ : Shape} {α : Type} [Runtime.TensorScalar α] [DecidableEq Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options) (model : nn.Sequential σ τ) (m : ScalarModule α (nn.paramShapes model) [σ, τ]) (x : Tensor.T α σ) : IO (Tensor.T α τ)

Run one inference step through a supervised runtime module.

This is the public sibling of the direct runtime pattern nn.eval1 opts model m.trainer.params x.

def TorchLean.Module.predict1NoGrad {σ τ : Shape} {α : Type} [Runtime.TensorScalar α] [DecidableEq Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options) (model : nn.Sequential σ τ) (m : ScalarModule α (nn.paramShapes model) [σ, τ]) (x : Tensor.T α σ) : IO (Tensor.T α τ)

Run one no-grad inference step through a supervised runtime module.

Use this for sampling/reporting paths that should not build an autograd tape.

def TorchLean.Module.instantiateMse {σ τ : Shape} {α : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options) (model : nn.Sequential σ τ) (reduction : LossReduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) (cast : Float → α := Runtime.ofFloat) : IO (ScalarModule α (nn.paramShapes model) [σ, τ])

Instantiate a supervised MSE module directly from a sequential model.

def TorchLean.Module.instantiateCrossEntropyOneHot {σ τ : Shape} {α : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options) (model : nn.Sequential σ τ) (reduction : LossReduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) (cast : Float → α := Runtime.ofFloat) : IO (ScalarModule α (nn.paramShapes model) [σ, τ])

Instantiate a supervised one-hot cross-entropy module directly from a sequential model.

def TorchLean.Module.instantiateModuleDefModel {σ τ : Shape} {α : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options) (model : nn.Sequential σ τ) (moduleDefOf : (model : nn.Sequential σ τ) → ScalarModuleDef (nn.paramShapes model) [σ, τ]) (cast : Float → α := Runtime.ofFloat) : IO (ScalarModule α (nn.paramShapes model) [σ, τ])

Instantiate a custom supervised runtime module directly from a sequential model.

Use this when a public example keeps the ordinary nn.Sequential model surface but needs a custom loss/module definition instead of the standard MSE or cross-entropy module constructors.

def TorchLean.Module.instantiatePpoActorCritic {stateShape : Shape} {batch nActions : ℕ} {α : Type} [Fact (0 < batch)] [Fact (0 < nActions)] [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options) (actor : nn.Sequential stateShape (Spec.Shape.dim batch (Spec.Shape.dim nActions Spec.Shape.scalar))) (critic : nn.Sequential stateShape (Spec.Shape.dim batch (Spec.Shape.dim 1 Spec.Shape.scalar))) (cast : Float → α := Runtime.ofFloat) : IO (ScalarModule α (nn.paramShapes actor ++ nn.paramShapes critic) [stateShape, Spec.Shape.dim batch (Spec.Shape.dim nActions Spec.Shape.scalar), Spec.Shape.dim batch Spec.Shape.scalar, Spec.Shape.dim batch Spec.Shape.scalar, Spec.Shape.dim batch (Spec.Shape.dim 1 Spec.Shape.scalar)])

Instantiate the standard PPO actor-critic supervised runtime module from rollout-shaped actor and critic networks.

def TorchLean.Module.withCrossEntropyOneHotModel {σ τ : Shape} {α β : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (reduction : LossReduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (nn.paramShapes model) [σ, τ] → IO β) : IO β

Build a sequential model, instantiate a one-hot cross-entropy runtime module for it, and continue with both values.

This packages the common public example pattern nn.withModel mkModel fun model => let m ← Module.instantiateCrossEntropyOneHot ....

def TorchLean.Module.withMseModel {σ τ : Shape} {α β : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (reduction : LossReduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (nn.paramShapes model) [σ, τ] → IO β) : IO β

Build a sequential model, instantiate an MSE runtime module for it, and continue with both values.

def TorchLean.Module.withModuleDefModel {σ τ : Shape} {α β : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (moduleDefOf : (model : nn.Sequential σ τ) → ScalarModuleDef (nn.paramShapes model) [σ, τ]) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (nn.paramShapes model) [σ, τ] → IO β) : IO β

Build a sequential model, instantiate a custom supervised runtime module for it, and continue with both values.

This packages the common public example pattern nn.withModel mkModel fun model => let m ← Module.instantiate ... (moduleDefOf model).

def TorchLean.Module.withScalarLossModel {σ τ : Shape} {α β : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (loss : {α : Type} → [inst : Runtime.TensorScalar α] → [inst_1 : DecidableEq Shape] → Runtime.Autograd.TorchLean.Program α [τ, τ] Shape.scalar) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (nn.paramShapes model) [σ, τ] → IO β) : IO β

Build a sequential model, instantiate a runtime module for a custom scalar loss program, and continue with both values.

This is the custom-loss sibling of withMseModel / withCrossEntropyOneHotModel. Use it when the model is ordinary nn.Sequential, but the loss needs task-specific logic beyond the standard MSE or cross-entropy module constructors.

def TorchLean.Module.lossScalar {σ τ : Shape} {α : Type} [Runtime.TensorScalar α] [DecidableEq Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (model : nn.Sequential σ τ) (m : ScalarModule α (nn.paramShapes model) [σ, τ]) (sample : SupervisedSample α σ τ) : IO α

Evaluate one supervised sample through a runtime module and return the scalar loss value.

This packages the common public example pattern Module.forward ...; Tensor.toScalar.

def TorchLean.Module.adamHandle {α : Type} [Runtime.TensorScalar α] [DecidableEq Shape] {paramShapes inputShapes : List Shape} (m : ScalarModule α paramShapes inputShapes) (lr beta1 beta2 epsilon : α) : have opt := Runtime.Autograd.TorchLean.adam lr beta1 beta2 epsilon; IO (NN.API.TorchLean.Optim.Handle α paramShapes inputShapes opt.State)

Create an Adam optimizer handle bound to a concrete runtime module.

This packages the common public example pattern optim.runtimeAdam ...; optim.handle m opt.

def TorchLean.Module.adamWHandle {α : Type} [Runtime.TensorScalar α] [DecidableEq Shape] {paramShapes inputShapes : List Shape} (m : ScalarModule α paramShapes inputShapes) (lr weightDecay beta1 beta2 epsilon : α) : have opt := Runtime.Autograd.TorchLean.adamw lr weightDecay beta1 beta2 epsilon; IO (NN.API.TorchLean.Optim.Handle α paramShapes inputShapes opt.State)

Create an AdamW optimizer handle bound to a concrete runtime module.

def TorchLean.Module.sgdHandle {α : Type} [Runtime.TensorScalar α] [DecidableEq Shape] {paramShapes inputShapes : List Shape} (m : ScalarModule α paramShapes inputShapes) (lr : α) : have opt := Runtime.Autograd.TorchLean.sgd lr; IO (NN.API.TorchLean.Optim.Handle α paramShapes inputShapes opt.State)

Create an SGD optimizer handle bound to a concrete runtime module.

def TorchLean.Module.optimizerInputs {α : Type} [Runtime.TensorScalar α] [Runtime.Scalar α] [DecidableEq Shape] {paramShapes inputShapes : List Shape} (m : ScalarModule α paramShapes inputShapes) (cfg : NN.API.TorchLean.Trainer.Optimizer) : IO (TensorPack α inputShapes → IO Unit)

Create a one-step update function for any typed module input pack from the public optimizer config used by the trainer API.

This is the generic bridge for custom training loops: richer examples can keep their own control flow while still choosing SGD/Adam/AdamW through the same optim.* config surface as Trainer.RunConfig.

def TorchLean.Module.optimizerStep {α : Type} {σ τ : Shape} [Runtime.TensorScalar α] [Runtime.Scalar α] [DecidableEq Shape] {paramShapes : List Shape} (m : ScalarModule α paramShapes [σ, τ]) (cfg : NN.API.TorchLean.Trainer.Optimizer) : IO (SupervisedSample α σ τ → IO Unit)

Create a sample-step function from the public optimizer config used by the trainer API.

This is the bridge for custom training loops: richer examples can keep their own control flow while still choosing SGD/Adam/AdamW through the same optim.* config surface as Trainer.RunConfig.