Executable Modules

Executable module operations for manual runtime and example code.

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

Instantiate an executable runtime module from a ScalarModuleDef.

This handles custom runtime tasks that do not use the standard supervised constructors such as Module.instantiateMse or Module.instantiateCrossEntropyOneHot.

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

Run one inference step through a supervised runtime module.

Public sibling of the direct runtime pattern model.predict opts m.trainer.params x.

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

Instantiate a supervised MSE module directly from a sequential model.

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

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

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

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

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

def TorchLean.Module.instantiateModuleDefModelFloat {σ τ : Shape} (opts : Options) (model : nn.Sequential σ τ) (moduleDefOf : (model : nn.Sequential σ τ) → ScalarModuleDef (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ]) : IO (ScalarModule Float (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ])

Float specialization of instantiateModuleDefModel with storage-first initialization.

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

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

def TorchLean.Module.withCrossEntropyOneHotModel {σ τ : Shape} {α β : Type} [Context α] [DecidableEq Shape] [Runtime.FromFloat α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (reduction : Loss.Reduction := Loss.Reduction.mean) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (Runtime.Autograd.TorchLean.NN.Seq.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} [Context α] [DecidableEq Shape] [Runtime.FromFloat α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (reduction : Loss.Reduction := Loss.Reduction.mean) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (Runtime.Autograd.TorchLean.NN.Seq.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} [Context α] [DecidableEq Shape] [Runtime.FromFloat α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (moduleDefOf : (model : nn.Sequential σ τ) → ScalarModuleDef (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ]) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (Runtime.Autograd.TorchLean.NN.Seq.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} [Context α] [DecidableEq Shape] [Runtime.FromFloat α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (loss : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → Runtime.Autograd.TorchLean.Program α [τ, τ] Shape.scalar) (cast : Float → α := Runtime.ofFloat) (k : (model : nn.Sequential σ τ) → ScalarModule α (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ] → IO β) : IO β

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

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

def TorchLean.Module.withScalarLossModelFloat {σ τ : Shape} {β : Type} (mkModel : nn.M (nn.Sequential σ τ)) (opts : Options) (loss : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → Runtime.Autograd.TorchLean.Program α [τ, τ] Shape.scalar) (k : (model : nn.Sequential σ τ) → ScalarModule Float (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ] → IO β) : IO β

Float specialization of withScalarLossModel with storage-first parameter initialization.

def TorchLean.Module.lossScalar {σ τ : Shape} {α : Type} [Context α] [DecidableEq Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (model : nn.Sequential σ τ) (m : ScalarModule α (Runtime.Autograd.TorchLean.NN.Seq.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} [Context α] [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 (OptimizerHandle α 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} [Context α] [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 (OptimizerHandle α paramShapes inputShapes opt.State)

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

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

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

def TorchLean.Module.optimizerInputs {α : Type} [Context α] [Runtime.FromFloat α] [DecidableEq Shape] {paramShapes inputShapes : List Shape} (m : ScalarModule α paramShapes inputShapes) (cfg : Trainer.Manual.OptimizerConfig) : 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.

Generic bridge for custom training loops: richer examples can keep their own control flow while still choosing a public optim.* config through the same API as Trainer.RunConfig.

def TorchLean.Module.optimizerStep {α : Type} {σ τ : Shape} [Context α] [Runtime.FromFloat α] [DecidableEq Shape] {paramShapes : List Shape} (m : ScalarModule α paramShapes [σ, τ]) (cfg : Trainer.Manual.OptimizerConfig) : IO (SupervisedSample α σ τ → IO Unit)

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

Bridge for custom training loops: richer examples can keep their own control flow while still choosing a public optim.* config through the same API as Trainer.RunConfig.