def step_added

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:523

import Base
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

523def step_added(+dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat,
524  +o: Nat, +i: Nat, +r: Nat, +rest: Nat, +k: Nat, +acc: F32,
525  ih: @+next: F32 -> Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, next,
526    Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (next, (G, I))))>,
527  -result: F32 & (Array<F32> & Array<U32>),
528  st: Stepped<dg, G, di, I, i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc, result>) ->
529  Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, result)>:
530  match st:
531    case Skipped{j, read, other, kept}:
532      Generic.Fact{
533        %Equal.sym(F32 & (Array<F32> & Array<U32>), result, (acc, (G, I)), kept) :
534          StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, _)
535        {\{Generic.Fact: q => q} : Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))> -> StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))}(
536      {\{Generic.Fact: q => Generic.Fact{(Pair.fst(
537          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
538          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))), q),
539        Laws.Skips{j, read_slot(kind, count, inner, o, k, r, di, I, j, read), other, Pair.snd(
540          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
541          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))), q)})}} :
542        Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, acc, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))> ->
543        Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))>}(ih(acc)))}
544    case Taken{j, read, same, x, word, kept}:
545      Generic.Fact{
546        %Equal.sym(F32 & (Array<F32> & Array<U32>), result, (F32.add(acc, x), (G, I)), kept) :
547          StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, _)
548        {\{Generic.Fact: q => q} : Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))> -> StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))}(
549      {\{Generic.Fact: q => Generic.Fact{(Pair.fst(
550          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I)))) == (G, I) : Array<F32> & Array<U32>},
551          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x),
552            Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))), q),
553        Laws.Adds{j, read_slot(kind, count, inner, o, k, r, di, I, j, read), same, x, word, Pair.snd(
554          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I)))) == (G, I) : Array<F32> & Array<U32>},
555          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x),
556            Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))), q)})}} :
557        Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, F32.add(acc, x),
558          Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))> ->
559        Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))>}(ih(F32.add(acc, x))))}