def write_pair_lift

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

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/arith.bend as Arith
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

185def write_pair_lift(+shape: Shape.Shape, -kept: Storage.Storage,
186  pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
187  moved: {write_stored(shape, pair) == kept : Storage.Storage},
188  done: {write_status(shape, pair) == True{} : Bool},
189  -P: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit> -> Type,
190  h: @-fits: {Lifecycle.logical_length(kept) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
191    P((Core.TTensor{kept, fits}, Done{Unit{}}))) -> P(pair):
192  match pair:
193    case (Core.TTensor{storage, valid}, Fail{error}):
194      Empty.absurd(P((Core.TTensor{storage, valid}, Fail{error})), Arith.clash(done))
195    case (Core.TTensor{storage, valid}, Done{Unit{}}):
196      write_shift(shape, storage, kept, Equal.sym(Storage.Storage, storage, kept, moved), P, h)(valid)