CNN PyTorch Fixture Export

PyTorch exporter for the small 2-block ConvNet round-trip fixture.

This exporter is meant to mirror the "classic demo CNN" shape that shows up in many TorchLean examples: two Conv2d + ReLU + MaxPool2d blocks, then Flatten, then a single Linear head.

Instead of taking a long positional list of naturals, we use small configuration records so call sites stay readable and it's easy to extend the shape later.

structure Export.CNNPyTorch.Conv2dCfg : Type

Configuration for a PyTorch nn.Conv2d layer.

• inChannels : ℕ

  Input channels (in_channels).

• outChannels : ℕ

  Output channels (out_channels).

• kernelH : ℕ

  Kernel height.

• kernelW : ℕ

  Kernel width.

• stride : ℕ

  Stride (applied to both spatial dims).

• padding : ℕ

  Zero-padding (applied to both spatial dims).

structure Export.CNNPyTorch.MaxPool2dCfg : Type

Configuration for a PyTorch nn.MaxPool2d layer.

• kernelH : ℕ

  Pool kernel height.

• kernelW : ℕ

  Pool kernel width.

• stride : ℕ

  Pool stride (applied to both spatial dims).

structure Export.CNNPyTorch.Cnn2Cfg : Type

Configuration for the 2-block CNN exporter.

• className : String

  Class name to use in the generated Python.

• inputC : ℕ

  Input image channels.

• inputH : ℕ

  Input image height.

• inputW : ℕ

  Input image width.

• conv1 : Conv2dCfg

  conv 1.

• pool1 : MaxPool2dCfg

  pool 1.

• conv2 : Conv2dCfg

  conv 2.

• pool2 : MaxPool2dCfg

  pool 2.

• flatSize : ℕ

  flat Size.

• fcOut : ℕ

  fc Out.

def Export.CNNPyTorch.generateCnn2PyTorchClass (cfg : Cnn2Cfg) : String

Render the 2-block CNN as a Python nn.Module class definition.

def Export.CNNPyTorch.generateCNNPyTorchClass (inC outC inH inW kH kW stride1 padding1 stride2 padding2 poolKH poolKW poolStride1 poolStride2 flatSize : ℕ) (className : String := "CNN") : String

Backwards-compatible wrapper for generateCnn2PyTorchClass.

Call sites that pass a long positional list of naturals can use this adapter.

def Export.CNNPyTorch.generateCNNWithWeights (convW1 convB1 convW2 convB2 linearW linearB : String) (inC outC inH inW kH kW stride1 padding1 stride2 padding2 poolKH poolKW poolstride1 poolstride2 flatSize : ℕ) (className : String := "CNN") : String

Generate a Python CNN module plus a helper that loads explicit weights from string literals.

This is mainly used for demos: you can paste JSON/Lean-rendered weight arrays into Python and run the model without writing an extra serializer.