def build_cells

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

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

714# Whatever the split, every cell of the parallel build holds what CellIs
715# names: the generic law of `Parallel.build`, with the reduce cell.
716def build_cells(+depth: Nat, +splits: Nat, +d: Nat, -A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +count: Nat,
717  +base: Nat, array: Array<F32>, -same: {array == A : Array<F32>}, -valid: Model.Balanced(F32, d, A)) ->
718  Parallel.Fact<Cells(depth, d, A, rows, extents, count, base, Reduce.build(depth, splits, rows, extents, count, base, array))>:
719  -split = {\{Parallel.Fact: q => q} : Parallel.Fact<({Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit} &
720    {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit})> ->
721    {Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit} &
722    {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit}}(
723    halves_equal(d, A, Array.clone(F32, A), {==}, valid))
724  -cells = {\{Generic.Fact: q => q} :
725    Generic.Fact<Generic.Cells(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, extents}), (A, Unit{}), depth, count, base,
726      Reduce.build(depth, splits, rows, extents, count, base, array))> ->
727    Generic.Cells(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, extents}), (A, Unit{}), depth, count, base,
728      Reduce.build(depth, splits, rows, extents, count, base, array))}(
729    Generic.build_cells(~Reduce.Fibers, ~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.fibers, ~Reduce.split, ~Reduce.cell_at,
730      Reduce.Fibers{rows, extents}, (A, Unit{}), depth, splits, count, base, (array, Unit{}),
731      Equal.cong(Array<F32>, Array<F32> & Unit, a => (a, Unit{}), array, A, same),
732      at => inside => {\{Parallel.Fact: q => q} :
733        Parallel.Fact<({Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, at, A, inside)) == (A, Unit{}) : Array<F32> & Unit})> ->
734        {Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, at, A, inside)) == (A, Unit{}) : Array<F32> & Unit}}(
735        cell_keeps(d, A, rows, extents, at, inside, valid)),
736      Pair.fst({Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit},
737        {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit}, split),
738      Pair.snd({Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit},
739        {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit}, split)))
740  Parallel.Fact{path => {\{Parallel.Fact: q => q} :
741    Parallel.Fact<CellSpec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count),
742      Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path))> ->
743    CellSpec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count),
744      Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path))}(
745    cell_spec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count),
746      Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path), cells(path), valid))}