IndexMap.shift: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/index_map.bend as IndexMap
Lines 35-57 of bendtorch-core@0.1.0.0/src/tensor/index_map.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/index_map.bend&start_line=35&end_line=57

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/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof

def shift(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +input: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
  +output: Shape.Shape, +cursor: Nat, -K: Storage.Storage -> Storage.Storage -> Type,
  next: K(source(~P, ~map, plan, input, fill, ops, 1n+cursor), target(~P, ~map, 1n+cursor, plan, input, fill, ops, output))) ->
  K(Replayed.storage(input, fill, Replayed.snoc(List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, cursor)),
      StorageLaws.Read{U32.from_nat(map(plan, cursor))})),
    Replayed.storage(output, 0.0, Replayed.snoc(writes(~P, ~map, cursor, plan, input, fill, ops),
      StorageLaws.Write{U32.from_nat(cursor),
        Replayed.value(input, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, cursor)), U32.from_nat(map(plan, cursor)))}))):
  +read = {StorageLaws.Read{U32.from_nat(map(plan, cursor))} : StorageLaws.Op}
  +seen = List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, cursor))
  +word = U32.from_nat(map(plan, cursor))
  +history = writes(~P, ~map, cursor, plan, input, fill, ops)
  -written = Replayed.storage(output, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(cursor), Replayed.value(input, fill, seen, word)}))
  %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, list => Replayed.storage(input, fill, list),
    List.append(&2, StorageLaws.Op, ops, Replayed.snoc(Pointwise.reads(~P, ~map, plan, cursor), read)), Replayed.snoc(seen, read),
    PointwiseProof.append_snoc(ops, Pointwise.reads(~P, ~map, plan, cursor), read)) :
    K(_, written)
  %Equal.cong(F32, Storage.Storage, value => Replayed.storage(output, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(cursor), value})),
    Replayed.value(input, fill, ops, word), Replayed.value(input, fill, seen, word),
    Equal.sym(F32, Replayed.value(input, fill, seen, word), Replayed.value(input, fill, ops, word),
      PointwiseProof.value_reads(~P, ~map, plan, cursor, input, fill, ops, word))) :
    K(source(~P, ~map, plan, input, fill, ops, 1n+cursor), _)
  next

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_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/storage/LAWS.bend&name=Op
  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/pointwise.bend&name=reads
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend&name=append_snoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend&name=value_reads
  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/contracts/replayed.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/index_map.bend&name=source
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/index_map.bend&name=target
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/index_map.bend&name=writes