~/jendhub

def array_run_keeps

bendtorch-core@0.1.0.0 · src/tensor/reduction.bend:116

import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

116# A run hands back the array it read.
117def array_run_keeps(-depth: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original), fuel: Nat, +cursor: Nat,
118  -accumulator: F32, -array: Array<F32>, pair: Array<F32> & F32,
119  -exact: {pair == Array.get(F32, array, U32.from_nat(cursor)) : Array<F32> & F32}, -same: {array == original : Array<F32>}) ->
120  Fact<{Pair.snd(F32, Array<F32>, array_run(fuel, cursor, accumulator, pair)) == original : Array<F32>}>:
121  match fuel pair:
122    case 0n Tuple{kept, word}:
123      read_keeps(depth, original, balanced, array, U32.from_nat(cursor), (kept, word), exact, same)
124    case 1n+rest Tuple{kept, word}:
125      array_run_keeps(depth, original, balanced, rest, 1n+cursor, F32.add(accumulator, word), kept,
126        Array.get(F32, kept, U32.from_nat(1n+cursor)), {==},
127        {\{Fact: p => p} : Fact<({array_from((kept, word)) == original : Array<F32>})> -> {kept == original : Array<F32>}}(
128          read_keeps(depth, original, balanced, array, U32.from_nat(cursor), (kept, word), exact, same)))

Uses (14)

Used by (1)