def cell_keeps

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

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/elementwise_walk_proof.bend as WalkProof

161# Every cell hands both input arrays back.
162def cell_keeps(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +position: Nat,
163  inside: Bool, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
164  Fact<{Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, inside)) == (A, B) : Array<F32> & Array<F32>}>:
165  match inside:
166    case False{}:
167      Fact{
168        %Equal.sym(F32 & (Array<F32> & Array<F32>), cell_of(operation, plan, position, A, B, False{}),
169          Elementwise.cell(operation, Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)),
170            Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position, A, B, False{}),
171          WalkProof.cell_at_walk(operation, plan, position, A, B, False{})) :
172          {Pair.snd(F32, Array<F32> & Array<F32>, _) == (A, B) : Array<F32> & Array<F32>}
173        {==}}
174    case True{}:
175      Fact{Pair.fst({Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array<F32> & Array<F32>},
176        {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>},
177        {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> ->
178          CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}(
179          cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid)))}