TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Runtime.Autograd.Torch.Core.Trainer.GraphOps

Graph Operations #

Interpret Ops programs as typed graph nodes. The recorded graphs serve evaluation, the autograd transforms and their proofs. Training does not use this instance: each trainer step records an eager tape.

source
@[instance_reducible]
instance Runtime.Autograd.Torch.instOpsMWith {α Δ : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} :
Ops (TypedGraph.GraphM.MWith α Δ Γ) α

Ops instance for the typed graph builder monad GraphM.

This interprets Ops primitives by recording typed SSA nodes rather than executing them immediately. Runtime.Autograd.TypedGraph.GraphM builds the graph data; Runtime.Autograd.Torch.TypedGraph packages it for repeated execution.

source
def Runtime.Autograd.Torch.instOpsMWith.read {α : Type} [TorchLean.Storage α] (getValue : {s : Spec.Shape} → ℕ → IO (TorchLean.Tensor α s)) {ss : List Spec.Shape} :
RefList TypedGraph.GraphM.Var ss → IO (TorchLean.TensorPack α ss)
Instances For
    source
    def Runtime.Autograd.Torch.instOpsMWith.writes {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} :
    RefList TypedGraph.GraphM.Var ss → TorchLean.TensorPack α ss → Array (ℕ × Spec.SomeTensor α) → Array (ℕ × Spec.SomeTensor α)
    Instances For