def next_run

bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:296

import Base
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

296def next_run(+d: Nat, -A: Array<F32>, -low: List<&2, Nat>, -high: List<&2, Nat>, -accumulator: F32,
297  -rec: F32 -> Array<F32> -> F32 & Array<F32>, pair: F32 & Array<F32>,
298  -first: Parallel.Fact<FiberRun<d, A, low, accumulator, pair>>,
299  -next: @value: F32 -> @array: Array<F32> -> @-same: {array == A : Array<F32>} -> Parallel.Fact<FiberRun<d, A, high, value, rec(value, array)>>) ->
300  Parallel.Fact<FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, Reduce.walk_next(rec, pair)>>:
301  (value, array) = pair
302  Parallel.Fact{{\{FiberRun: words => seen => total => kept =>
303    {\{FiberRun: rest => more => after => back =>
304      FiberRun{List.append(&2, F32, words, rest),
305        {\{Parallel.Fact: p => p} : Parallel.Fact<Obs(d, A, List.append(&2, Nat, low, high), List.append(&2, F32, words, rest))> ->
306          Obs(d, A, List.append(&2, Nat, low, high), List.append(&2, F32, words, rest))}(obs_append(d, A, low, words, high, rest, seen, more)),
307        %Equal.sym(F32, fsum(List.append(&2, F32, words, rest), accumulator), fsum(rest, fsum(words, accumulator)),
308          fsum_append(words, rest, accumulator)) : {Pair.fst(F32, Array<F32>, rec(value, array)) == _ : F32}
309        %total : {Pair.fst(F32, Array<F32>, rec(value, array)) == fsum(rest, _) : F32}
310        after,
311        back}} :
312      FiberRun<d, A, high, value, rec(value, array)> -> FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, rec(value, array)>}(
313      {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, high, value, rec(value, array)>> -> FiberRun<d, A, high, value, rec(value, array)>}(
314        next(value)(array)(kept)))} :
315    FiberRun<d, A, low, accumulator, (value, array)> -> FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, rec(value, array)>}(
316    {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, low, accumulator, (value, array)>> -> FiberRun<d, A, low, accumulator, (value, array)>}(first))}