def shift

bendtorch-core@0.1.0.0 · src/tensor/index_map.bend:35

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

35def shift(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +input: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
36  +output: Shape.Shape, +cursor: Nat, -K: Storage.Storage -> Storage.Storage -> Type,
37  next: K(source(~P, ~map, plan, input, fill, ops, 1n+cursor), target(~P, ~map, 1n+cursor, plan, input, fill, ops, output))) ->
38  K(Replayed.storage(input, fill, Replayed.snoc(List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, cursor)),
39      StorageLaws.Read{U32.from_nat(map(plan, cursor))})),
40    Replayed.storage(output, 0.0, Replayed.snoc(writes(~P, ~map, cursor, plan, input, fill, ops),
41      StorageLaws.Write{U32.from_nat(cursor),
42        Replayed.value(input, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, cursor)), U32.from_nat(map(plan, cursor)))}))):
43  +read = {StorageLaws.Read{U32.from_nat(map(plan, cursor))} : StorageLaws.Op}
44  +seen = List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, cursor))
45  +word = U32.from_nat(map(plan, cursor))
46  +history = writes(~P, ~map, cursor, plan, input, fill, ops)
47  -written = Replayed.storage(output, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(cursor), Replayed.value(input, fill, seen, word)}))
48  %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, list => Replayed.storage(input, fill, list),
49    List.append(&2, StorageLaws.Op, ops, Replayed.snoc(Pointwise.reads(~P, ~map, plan, cursor), read)), Replayed.snoc(seen, read),
50    PointwiseProof.append_snoc(ops, Pointwise.reads(~P, ~map, plan, cursor), read)) :
51    K(_, written)
52  %Equal.cong(F32, Storage.Storage, value => Replayed.storage(output, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(cursor), value})),
53    Replayed.value(input, fill, ops, word), Replayed.value(input, fill, seen, word),
54    Equal.sym(F32, Replayed.value(input, fill, seen, word), Replayed.value(input, fill, ops, word),
55      PointwiseProof.value_reads(~P, ~map, plan, cursor, input, fill, ops, word))) :
56    K(source(~P, ~map, plan, input, fill, ops, 1n+cursor), _)
57  next