def leaf_run

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

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/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

282def leaf_run(+d: Nat, -A: Array<F32>, +base: Nat, -accumulator: F32, -array: Array<F32>, pair: Array<F32> & F32,
283  -exact: {pair == Array.get(F32, array, U32.from_nat(base)) : Array<F32> & F32}, -same: {array == A : Array<F32>},
284  -valid: Model.Balanced(F32, d, A)) ->
285  Parallel.Fact<FiberRun<d, A, [base], accumulator, Reduce.leaf_add(accumulator, pair)>>:
286  (kept, word) = pair
287  Parallel.Fact{FiberRun{[word],
288    ObsStep{Equal.sym(Maybe<&2, F32>, Some{word}, Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))),
289      {\{Parallel.Fact: p => p} : Parallel.Fact<{Some{Refinement.second(F32, (kept, word))} == Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))) : Maybe<&2, F32>}> ->
290        {Some{Refinement.second(F32, (kept, word))} == Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))) : Maybe<&2, F32>}}(
291        Parallel.read_value(d, array, A, U32.from_nat(base), (kept, word), exact, same, valid))), Unit{}},
292    {==},
293    {\{Parallel.Fact: p => p} : Parallel.Fact<{Refinement.first(F32, (kept, word)) == A : Array<F32>}> -> {Refinement.first(F32, (kept, word)) == A : Array<F32>}}(
294      Parallel.read_keeps(d, array, A, U32.from_nat(base), (kept, word), exact, same, valid))}}