def cell_out

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

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

151def cell_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, A: Array<F32>, B: Array<F32>, +position: Nat,
152  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
153  Fact<CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))>:
154  %Equal.sym(F32 & (Array<F32> & Array<F32>), cell_of(operation, plan, position, A, B, True{}),
155    Elementwise.cell(operation, Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)),
156      Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position, A, B, True{}),
157    WalkProof.cell_at_walk(operation, plan, position, A, B, True{})) :
158    Fact<CellOut(operation, plan, dl, dr, A, B, position, _)>
159  left_out(operation, plan, dl, dr, A, B, position, Array.get(F32, A, left_at(plan, position)), {==}, left_valid, right_valid)