def right_out

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

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/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

117def right_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +position: Nat,
118  -x: F32, -la: Array<F32>, pair: Array<F32> & F32, -exact: {pair == Array.get(F32, B, right_at(plan, position)) : Array<F32> & F32},
119  -ex: {Some{x} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>},
120  -el: {la == A : Array<F32>}, -valid: Model.Balanced(F32, dr, B)) ->
121  Fact<CellOut(operation, plan, dl, dr, A, B, position, Elementwise.cell_right(operation, x, la, pair))>:
122  (kept, y) = pair
123  Fact{(pair_equal(la, kept, A, B, el,
124      {\{Fact: q => q} : Fact<({Refinement.first(F32, (kept, y)) == B : Array<F32>})> -> {Refinement.first(F32, (kept, y)) == B : Array<F32>}}(
125        read_keeps(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid))),
126    {\{Fact: q => q} : Fact<({Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>})> ->
127      {Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>}}(
128      pick_value(operation, x, y, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))), ex,
129        {\{Fact: q => q} : Fact<({Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>})> ->
130          {Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>}}(
131          read_value(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid)))))}