MatmulParallelProof.input_take: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as MatmulParallelProof
Lines 831-861 of bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&start_line=831&end_line=861

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/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

def input_take(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, -Q: Core.Dynamic & Array<F32> -> Type,
  h: InputAt(shape, fill, ops, StorageLaws.created(Shape.count(shape), fill), Q)) ->
  @-fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
  Q(Elementwise.take(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})):
  Owned.created_lift(Shape.count(shape), fill, Conversion.shape_count_within(shape),
    s => (InputAt(shape, fill, ops, s, Q) -> @-fits: {Lifecycle.logical_length(StorageLaws.replay(ops, s)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
      Q(Elementwise.take(Core.Packed{shape, Core.TTensor{StorageLaws.replay(ops, s), fits}}))),
    zero => k => fits =>
      storage_shift(shape, Storage.Empty{}, StorageLaws.replay(ops, Storage.Empty{}),
        Equal.sym(Storage.Storage, StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops)),
        st => kk => Q(Elementwise.take(Core.Packed{shape, Core.TTensor{st, kk}})),
        kk => storage_shift(shape, StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops),
          st => k2 => Q((Core.Packed{shape, Core.TTensor{st, k2}}, Array.new(F32, 0n, 0.0))),
          k2 => k(ops)(other => {==})({==})(Nil{})(0n)(0.0)(NoCells{zero})(k2))(kk))(fits),
    d => fits_d => f => k => fits =>
      Owned.replay_lift(ops, d, U32.to_nat(Shape.count(shape)), fill, Nil{}, Api.hit_of(U32.to_nat(Shape.count(shape)), ops), {==},
        ArrayCore.new_balanced(F32, d, fill), f, fits_d,
        st => (@-fits: {Lifecycle.logical_length(st) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
          (@-kk: {Lifecycle.logical_length(StorageLaws.step(st, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
            Q((Core.Packed{shape, Core.TTensor{StorageLaws.step(st, StorageLaws.First{}), kk}}, Api.arr(history(shape, ops), d, fill)))) ->
          Q(Elementwise.take(Core.Packed{shape, Core.TTensor{st, fits}}))),
        c => fits2 => kc =>
          take_owned_lift(shape, d, U32.to_nat(Shape.count(shape)), Api.arr(Owned.norm(U32.to_nat(Shape.count(shape)), ops, Nil{}), d, fill),
            Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(shape)), ops, Nil{}), d, fill)), {==}, c, f, fits2, Q, kc))(fits)(
        storage_shift(shape,
          StorageLaws.replay(Replayed.snoc(ops, StorageLaws.First{}), Storage.Owned{d, U32.to_nat(Shape.count(shape)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}),
          StorageLaws.step(StorageLaws.replay(ops, Storage.Owned{d, U32.to_nat(Shape.count(shape)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}), StorageLaws.First{}),
          FromValues.replay_snoc(ops, StorageLaws.First{}, Storage.Owned{d, U32.to_nat(Shape.count(shape)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}),
          st => kk => Q((Core.Packed{shape, Core.TTensor{st, kk}}, Api.arr(history(shape, ops), d, fill))),
          k(Replayed.snoc(ops, StorageLaws.First{}))(other => half_keeps(shape, fill, ops, other))(words_first(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))))(
            history(shape, ops))(d)(fill)(Normal{fits_d, {==}, {==}}))))(h)

Uses (41):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=count
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=created
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=replay
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=hit_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=new_balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=created_lift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=norm
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=replay_empty
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=replay_lift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=InputAt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=Source
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=half_keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=history
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=storage_shift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=take_owned_lift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=words_first
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=snoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=storage
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=replay_snoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=shape_count_within