~/jendhub

def words_first

bendtorch-core@0.1.0.0 · src/tensor/permute_values.bend:75

import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
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 Contracts

75# The First half of a clone lists the same words.
76def words_first(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
77  {Contracts.words(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), count) == Contracts.words(shape, fill, ops, count) : List<&2, F32>}:
78  match count:
79    case 0n:
80      {==}
81    case 1n+previous:
82      +position = U32.from_nat(previous)
83      words_snoc(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), previous,
84        Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), position), Replayed.value(shape, fill, ops, position),
85        Contracts.words(shape, fill, ops, previous), words_first(shape, fill, ops, previous), half_keeps(shape, fill, ops, position))

Uses (11)

Used by (1)