def InputAt

bendtorch-core@0.1.0.0 · src/tensor/contracts/matmul_parallel_proof.bend:819

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/storage/LAWS.bend as StorageLaws
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
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

819# What the rest of the product asks of one input's `take`: the kept tensor,
820# replayed with a history that keeps its words, and the copy the build reads,
821# with its source.
822def InputAt(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, -s: Storage.Storage,
823  -Q: Core.Dynamic & Array<F32> -> Type) -> Type:
824  @+kept: List<&2, StorageLaws.Op> ->
825  @values: (@+other: U32 -> {Replayed.value(shape, fill, kept, other) == Replayed.value(shape, fill, ops, other) : F32}) ->
826  @words: {Laws.words(shape, fill, kept, Shape.logical_numel(Shape.dimensions(shape))) == Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))) : List<&2, F32>} ->
827  @+h: List<&2, Api.Effect> -> @+d: Nat -> @+f: F32 -> @+source: Source<shape, fill, ops, h, d, f> ->
828  @-kept_fits: {Lifecycle.logical_length(StorageLaws.replay(kept, s)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
829    Q((Core.Packed{shape, Core.TTensor{StorageLaws.replay(kept, s), kept_fits}}, Api.arr(h, d, f)))