def take_owned_lift

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:322

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
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/elementwise.bend as Elementwise

322# `take` of an owned tensor hands back the First half of its clone and the
323# Second half's array.
324def take_owned_lift(+shape: Shape.Shape, +d: Nat, +n: Nat, -array: Array<F32>, pair: Array<F32> & Array<F32>,
325  -same: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>}, -b: Model.Balanced(F32, d, array),
326  -f: {Storage.bounds(d, n) == True{} : Bool}, -fits: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
327  -Q: (Core.Dynamic & Array<F32>) -> Type,
328  h: @-kept: {Lifecycle.logical_length(StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f))) ==
329    Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
330    Q((Core.Packed{shape, Core.TTensor{StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f)), kept}},
331      Pair.snd(Array<F32>, Array<F32>, pair)))) ->
332  Q(Elementwise.take_owned(shape, d, n, array, pair, same, b, f, fits)):
333  (kept, copy) = pair
334  h(fits)