Curried Tensor and Reference Arguments

Convert between shape-indexed packs and curried arguments for tensors or any reference family.

def Runtime.Autograd.Torch.Curried.Fn (α : Type) [TorchLean.Storage α] : List Spec.Shape → Type → Type

Type of a curried function accepting one tensor argument per shape in ss.

For example, Fn α [s₁, s₂] β is Tensor α s₁ → Tensor α s₂ → β.

def Runtime.Autograd.Torch.Curried.curry {α : Type} [TorchLean.Storage α] {β : Type} {ss : List Spec.Shape} : (TorchLean.TensorPack α ss → β) → Fn α ss β

Convert a function on tensor-pack inputs into its curried form.

def Runtime.Autograd.Torch.Curried.uncurry {α : Type} [TorchLean.Storage α] {β : Type} {ss : List Spec.Shape} : Fn α ss β → TorchLean.TensorPack α ss → β

Convert a curried function into a function on tensor-pack inputs.

inductive Runtime.Autograd.Torch.RefList (Ref : Spec.Shape → Type) : List Spec.Shape → Type

A pack of references indexed by their shapes, analogous to TensorPack.

• nil {Ref : Spec.Shape → Type} : RefList Ref []
• cons {Ref : Spec.Shape → Type} {s : Spec.Shape} {ss : List Spec.Shape} : Ref s → RefList Ref ss → RefList Ref (s :: ss)

def Runtime.Autograd.Torch.RefList.append {Ref : Spec.Shape → Type} {ss₁ ss₂ : List Spec.Shape} : RefList Ref ss₁ → RefList Ref ss₂ → RefList Ref (ss₁ ++ ss₂)

Append two RefLists.

def Runtime.Autograd.Torch.RefList.split {Ref : Spec.Shape → Type} {ss₁ ss₂ : List Spec.Shape} : RefList Ref (ss₁ ++ ss₂) → RefList Ref ss₁ × RefList Ref ss₂

Split a RefList Ref (ss₁ ++ ss₂) into its left and right parts.

def Runtime.Autograd.Torch.RefList.splitLast {Ref : Spec.Shape → Type} {ss : List Spec.Shape} {τ : Spec.Shape} : RefList Ref (ss ++ [τ]) → RefList Ref ss × Ref τ

Split a RefList Ref (ss ++ [τ]) into its prefix and last element.

@[simp]

theorem Runtime.Autograd.Torch.RefList.split_append {Ref : Spec.Shape → Type} {ss₁ ss₂ : List Spec.Shape} (xs : RefList Ref ss₁) (ys : RefList Ref ss₂) : (xs.append ys).split = (xs, ys)

Splitting concatenated references recovers the original state blocks.

@[simp]

theorem Runtime.Autograd.Torch.RefList.splitLast_append {Ref : Spec.Shape → Type} {ss : List Spec.Shape} {τ : Spec.Shape} (xs : RefList Ref ss) (x : Ref τ) : (xs.append (cons x nil)).splitLast = (xs, x)

The final reference remains separate from the preceding model state.

@[simp]

theorem Runtime.Autograd.Torch.RefList.append_split {Ref : Spec.Shape → Type} {ss₁ ss₂ : List Spec.Shape} (xs : RefList Ref (ss₁ ++ ss₂)) : xs.split.1.append xs.split.2 = xs

Reassembling the two state blocks restores every original reference.

theorem Runtime.Autograd.Torch.RefList.append_assoc {Ref : Spec.Shape → Type} {a b c : List Spec.Shape} (xs : RefList Ref a) (ys : RefList Ref b) (zs : RefList Ref c) : ⋯ ▸ (xs.append ys).append zs = xs.append (ys.append zs)

Reassociating state blocks changes only their shape-list witness, not their references.

def Runtime.Autograd.Torch.CurriedRef (Ref : Spec.Shape → Type) : List Spec.Shape → Type → Type

A curried function accepting one Ref s argument per shape in ss.

def Runtime.Autograd.Torch.CurriedRef.uncurry {Ref : Spec.Shape → Type} {β : Type} {ss : List Spec.Shape} : CurriedRef Ref ss β → RefList Ref ss → β

Uncurry a curried reference function to accept a RefList.

def Runtime.Autograd.Torch.CurriedRef.curry {Ref : Spec.Shape → Type} {β : Type} {ss : List Spec.Shape} : (RefList Ref ss → β) → CurriedRef Ref ss β

Curry a reference function that consumes a RefList.

@[simp]

theorem Runtime.Autograd.Torch.CurriedRef.uncurry_curry {Ref : Spec.Shape → Type} {β : Type} {ss : List Spec.Shape} (f : RefList Ref ss → β) (xs : RefList Ref ss) : (curry f).uncurry xs = f xs

Binding the curried arguments preserves the complete reference-list computation.

def Runtime.Autograd.Torch.CurriedRef.uncurryPack {α β : Type} [TorchLean.Storage α] {ss : List Spec.Shape} : CurriedRef (fun (s : Spec.Shape) => TorchLean.Tensor α s) ss β → TorchLean.TensorPack α ss → β

Apply a tensor-valued CurriedRef to its shape-indexed tensor pack.