def checked_update_pair
bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:468
import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
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
468def checked_update_pair(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32, +value: F32,
469 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, -meaning: Core.UpdateMeaning(shape, original, index, value, pair)) ->
470 CheckedUpdatePair<shape, original, index, value, pair>:
471 (output, result) = pair
472 match result:
473 case Fail{error}:
474 CheckedUpdatePair{Unit{}}
475 case Done{unit}:
476 CheckedUpdatePair{(update_route(shape, original, output, index, value, unit, meaning),
477 (Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, output, index), Core.observe(shape, output, index), Some{value},
478 {\{Core.ObservationModel: equal => equal} :
479 Core.ObservationModel<shape, output, index, update_route(shape, original, output, index, value, unit, meaning)> ->
480 {Core.checked_observe(shape, output, index) == Core.observe(shape, output, index) : Maybe<&2, F32>}}(Core.observation_model(shape, output, index, update_route(shape, original, output, index, value, unit, meaning))),
481 update_value(shape, original, output, index, value, unit, meaning)),
482 other => checked => different =>
483 {\{Tuple: after => physical => (after,
484 {\{CheckedFrame: equal => equal} : CheckedFrame<shape, original, output, other> ->
485 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(checked_frame(shape, original, output, other, checked, after, physical)))
486 } :
487 (Core.ObservationChecked(Core.Packed{shape, output}, other) &
488 {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}) ->
489 (Core.ObservationChecked(Core.Packed{shape, output}, other) &
490 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(update_frame(shape, original, output, index, value, unit, meaning)(other)(checked)(different))))}