def step_indices_retains

bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:298

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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

298def step_indices_retains(+operation: Elementwise.Operation, -shape: Shape.Shape, +index: U32,
299  state: Elementwise.State<shape>, result: Result<&2, &1, Core.Error, U32 & U32>) ->
300  StepSources<shape,
301    step_left_owner(shape, Elementwise.Continue{state}), step_right_owner(shape, Elementwise.Continue{state}),
302    Elementwise.step_indices(operation, shape, index, state, result)>:
303  Elementwise.State{left, right, output} = state
304  match result:
305    case Fail{error}:
306      StepSources{property => {==}, property => {==}}
307    case Done{indices}:
308      (+left_index, +right_index) = indices
309      step_sources_reify(shape, left, right,
310        Elementwise.step_left(operation, shape, index, right, output, right_index, Core.read_dynamic(left, left_index)),
311        {\{SourceModel: same => step_left_retains(operation, shape, index, left, right, right, output, right_index,
312        Core.read_dynamic(left, left_index), same, property => {==})} :
313        SourceModel<left, dynamic_read_owner(Core.read_dynamic(left, left_index))> ->
314        StepSources<shape, left, right, Elementwise.step_left(operation, shape, index, right, output, right_index, Core.read_dynamic(left, left_index))>}(
315          dynamic_read_retains(left, left_index)))