ParallelProofs.build_cells: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as ParallelProofs
Lines 207-227 of bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&start_line=207&end_line=227

import Base
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Build

# Whatever the split, every cell of the parallel build holds what the
# one-thread tree computes there from `start`.
def build_cells(~Q: Data, ~P: Data, ~A: Type, ~B: Type, ~prepare: @+q: Q -> P, ~split: (A & B) -> (A & B) & (A & B), ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
  +q: Q, -start: (A & B), +depth: Nat, +splits: Nat, +count: Nat, +base: Nat, state: (A & B), -at: {state == start : (A & B)},
  -keeps: Keeps(~P, ~A, ~B, ~cell, prepare(q), start),
  -first: {Pair.fst((A & B), (A & B), split(start)) == start : (A & B)}, -second: {Pair.snd((A & B), (A & B), split(start)) == start : (A & B)}) ->
  Fact<Cells(~P, ~A, ~B, ~cell, prepare(q), start, depth, count, base, Build.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state))>:
  match depth splits:
    case 1n+inner 1n+rest:
      fork_cells(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, start, inner, count, base, state, split(state), {==},
        l => r => Build.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, inner, rest, count, base, (l, r)),
        l => r => Build.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, inner, rest, count, Build.upper(inner, base), (l, r)),
        at, first, second,
        l => r => at => build_cells(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, start, inner, rest, count, base, (l, r), at, keeps, first, second),
        l => r => at => build_cells(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, start, inner, rest, count, Build.upper(inner, base), (l, r), at, keeps, first, second))
    case 0n _:
      facts_cells(~P, ~A, ~B, ~cell, prepare(q), start, 0n, count, base, Build.tree(~P, ~A, ~B, ~cell, prepare(q), 0n, count, base, state),
        tree_facts(~P, ~A, ~B, ~cell, prepare(q), start, 0n, count, base, state, at, keeps))
    case 1n+inner 0n:
      facts_cells(~P, ~A, ~B, ~cell, prepare(q), start, 1n+inner, count, base, Build.tree(~P, ~A, ~B, ~cell, prepare(q), 1n+inner, count, base, state),
        tree_facts(~P, ~A, ~B, ~cell, prepare(q), start, 1n+inner, count, base, state, at, keeps))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=tree
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=upper
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=facts_cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=fork_cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=tree_facts