def decided_walks

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

378# Below the output's element count, `expected` reads the inputs at the cells
379# the build's index walks name.
380def decided_walks(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic, +position: Nat,
381  decision: Shape.BoolCase<Nat.is_lt(position, Shape.elements(Shape.output_shape(plan)))>,
382  +bound: {True{} == Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))) : Bool}) ->
383  {Elementwise.expected_indices(operation, left, right, Elementwise.flat_input_indices(plan, Shape.flat_checked.finish(Shape.output_shape(plan), position, decision))) ==
384    Elementwise.expected_left(operation, right,
385      U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)),
386      Core.checked_observe_dynamic(left,
387        U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)))) : Maybe<&2, F32>}:
388  match decision:
389    case Shape.BFalse{equal}:
390      Empty.absurd({None{} ==
391        Elementwise.expected_left(operation, right,
392          U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)),
393          Core.checked_observe_dynamic(left,
394            U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)))) : Maybe<&2, F32>},
395        Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))), True{}, equal,
396          Equal.sym(Bool, True{}, Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))), bound))))
397    case Shape.BTrue{equal}:
398      Equal.cong(U32 & U32, Maybe<&2, F32>, indices => Elementwise.expected_indices(operation, left, right, Done{indices}),
399        (Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, Shape.index_map(plan), Shape.FIndex{position, equal})),
400          Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, Shape.index_map(plan), Shape.FIndex{position, equal}))),
401        (U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)),
402          U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position))),
403        walk_pair(plan, Shape.index_map(plan), position, equal))