def left_out

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

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

133def left_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, B: Array<F32>, +position: Nat,
134  pair: Array<F32> & F32, -exact: {pair == Array.get(F32, A, left_at(plan, position)) : Array<F32> & F32},
135  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
136  Fact<CellOut(operation, plan, dl, dr, A, B, position, Elementwise.cell_left(operation, B, right_at(plan, position), pair))>:
137  (kept, x) = pair
138  right_out(operation, plan, dl, dr, A, B, position, x, kept, Array.get(F32, B, right_at(plan, position)), {==},
139    {\{Fact: q => q} : Fact<({Some{Refinement.second(F32, (kept, x))} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>})> ->
140      {Some{Refinement.second(F32, (kept, x))} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>}}(
141      read_value(dl, A, A, left_at(plan, position), (kept, x), exact, {==}, left_valid)),
142    {\{Fact: q => q} : Fact<({Refinement.first(F32, (kept, x)) == A : Array<F32>})> -> {Refinement.first(F32, (kept, x)) == A : Array<F32>}}(
143      read_keeps(dl, A, A, left_at(plan, position), (kept, x), exact, {==}, left_valid)),
144    right_valid)