def source_extend

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:519

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/reduction_LAWS.bend as Laws

519def source_extend(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
520  +accumulator: F32, +head: F32, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
521  next: Laws.LoopMeaning(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head), result),
522  -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
523  -observed: {Core.checked_observe(shape, original, U32.from_nat(cursor)) == Some{head} : Maybe<&2, F32>},
524  -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
525  Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, result):
526  match result:
527    case Fail{error}:
528      Unit{}
529    case Done{pair}:
530      (retained, value) = pair
531      Laws.SumMeaning{values, logical, fold} = next
532      Laws.SumMeaning{head <> values,
533        Laws.LogicalStep{exact, observed, logical_original(fuel, shape, original, tensor, 1n+cursor, values, logical, kept)}, fold}