def build_cell

bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:205

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

205# An inside cell of the parallel build holds what `want` names there: the
206# generic law of `Parallel.build`, with the elementwise cell.
207def build_cell(+depth: Nat, +splits: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +count: Nat, +base: Nat,
208  +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +path: Model.Path(depth),
209  -inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool},
210  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
211  Fact<{Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) ==
212    want(operation, plan, dl, dr, A, B, Nat.add(Model.offset(depth, path), base)) : Maybe<&2, F32>}>:
213  +position = Nat.add(Model.offset(depth, path), base)
214  -split = {\{Fact: q => q} : Fact<({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>} &
215    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>})> ->
216    {Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>} &
217    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>}}(
218    split_equal(dl, dr, A, B, left_valid, right_valid))
219  Fact{Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path),
220    Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{}))},
221    want(operation, plan, dl, dr, A, B, position),
222    %inside : {Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) ==
223      Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, _))} : Maybe<&2, F32>}
224    {\{Generic.Fact: q => q} :
225      Generic.Fact<Generic.Cells(~Elementwise.Walk, ~Array<F32>, ~Array<F32>, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base,
226        Elementwise.build(depth, splits, operation, plan, count, base, A, B))> ->
227      Generic.Cells(~Elementwise.Walk, ~Array<F32>, ~Array<F32>, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base,
228        Elementwise.build(depth, splits, operation, plan, count, base, A, B))}(
229      Generic.build_cells(~Elementwise.Request, ~Elementwise.Walk, ~Array<F32>, ~Array<F32>, ~Elementwise.walk, ~Elementwise.split, ~Elementwise.cell_at,
230        Elementwise.Request{operation, plan}, (A, B), depth, splits, count, base, (A, B), {==},
231        at => inside => {\{Fact: q => q} : Fact<({Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array<F32> & Array<F32>})> ->
232          {Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array<F32> & Array<F32>}}(
233          cell_keeps(operation, plan, dl, dr, A, B, at, inside, left_valid, right_valid)),
234        Pair.fst({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>},
235          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>}, split),
236        Pair.snd({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>},
237          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>}, split)))(path),
238    Pair.snd({Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array<F32> & Array<F32>},
239      {Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{}))} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>},
240      {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> ->
241        CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}(
242        cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid))))}