type AddStep

bendtorch-core@0.1.0.0 · src/tensor/gather_LAWS.bend:286

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather

286type AddStep<-dg: Nat, -G: Array<F32>, -di: Nat, -I: Array<U32>, -kind: Gather.Lookup, -count: Nat, -inner: Nat, -o: Nat, -i: Nat, -r: Nat,
287  -rest: Nat, -k: Nat, -acc: F32, -value: F32> is Data:
288  Skips{-j: U32,
289    -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(entry_at(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>},
290    -other: {Nat.is_eq(U32.to_nat(j), i) == False{} : Bool},
291    -next: Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, value)}
292  Adds{-j: U32,
293    -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(entry_at(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>},
294    -same: {Nat.is_eq(U32.to_nat(j), i) == True{} : Bool},
295    -x: F32,
296    -word: {Model.observe(F32, dg, G, Refinement.route(dg, U32.from_nat(position(count, inner, o, k, r)))) == Some{x} : Maybe<&2, F32>},
297    -next: Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x), value)}