def expected_value

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:400

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

400def expected_value(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32, -left: Core.Dynamic, -right: Core.Dynamic,
401  +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32,
402  -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
403  left_model: ReadValueModel<left, left_index, left_value>, right_model: ReadValueModel<right, right_index, right_value>) ->
404  ExpectedValue<operation, plan, index, left, right, left_value, right_value>:
405  ReadValueModel{left_equal} = left_model
406  ReadValueModel{right_equal} = right_model
407  ExpectedValue{
408    %indices_exact : {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_indices(operation, left, right, _) : Maybe<&2, F32>}
409    %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(left, left_index), Some{left_value}, left_equal) :
410      {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_left(operation, right, right_index, _) : Maybe<&2, F32>}
411    %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(right, right_index), Some{right_value}, right_equal) :
412      {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_right(operation, left_value, _) : Maybe<&2, F32>}
413    {==}}