~/jendhub

def write_shift

bendtorch-core@0.1.0.0 · src/tensor/contracts/replayed.bend:174

import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle

174def write_shift(+shape: Shape.Shape, -source: Storage.Storage, -target: Storage.Storage,
175  moved: {target == source : Storage.Storage},
176  -P: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit> -> Type,
177  h: @-fits: {Lifecycle.logical_length(target) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
178    P((Core.TTensor{target, fits}, Done{Unit{}}))) ->
179  @-fits: {Lifecycle.logical_length(source) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
180    P((Core.TTensor{source, fits}, Done{Unit{}})):
181  %moved : (@-fits: {Lifecycle.logical_length(_) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
182    P((Core.TTensor{_, fits}, Done{Unit{}})))
183  h

Uses (12)

Used by (1)