def fill_decision_model

bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:460

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/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof

460def fill_decision_model(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +index: U32,
461  -original: Core.Tensor<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
462  -rec: @tensor: Core.Tensor<shape> -> FillOutcome<shape, tensor, rest, 1n+cursor, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
463  FillOutcome<shape, original, value <> rest, cursor, Core.fill_values_decided(shape, cursor, index, value, original,
464    tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), decision)>:
465  match decision:
466    case Shape.BFalse{equal}:
467      FillOutcome{Unit{}}
468    case Shape.BTrue{equal}:
469      FillOutcome{
470        {\{FillOutcome: meaning => meaning} :
471          FillOutcome<shape, original, value <> rest, cursor,
472            Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Core.write_flat(shape, original, index, value))> ->
473          FillMeaning(shape, original, value <> rest, cursor,
474            Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Core.write_flat(shape, original, index, value)))}(fill_write_pair(shape, value, rest, cursor, index, original, Core.write_flat(shape, original, index, value), {==},
475                Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), CoreProof.checked_update_model(shape, original, index, value), rec))}