def fill_decided_success

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

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/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
import bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend as TransformLaws

580def fill_decided_success(+shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +index: U32,
581  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, -original: Core.Tensor<shape>,
582  converted: {U32.to_nat(index) == cursor : Nat},
583  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
584  -rec: @tensor: Core.Tensor<shape> -> FillSuccess<shape, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
585  FillSuccess<shape, Core.fill_values_decided(shape, cursor, index, value, original,
586    tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), decision)>:
587  match decision:
588    case Shape.BFalse{equal}:
589      FillSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor),
590        AllocationProof.natural_equal_true(U32.to_nat(index), cursor, converted), equal))}
591    case Shape.BTrue{equal}:
592      FillSuccess{{\{FillSuccess: successful => successful} :
593        FillSuccess<shape, Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor),
594          Core.write_flat(shape, original, index, value))> ->
595        {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>,
596          Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor),
597            Core.write_flat(shape, original, index, value))) == True{} : Bool}}(
598              fill_step_success(shape, rest, cursor, Core.write_flat(shape, original, index, value),
599                {\{TransformTotality.WriteSuccess: successful => successful} : TransformTotality.WriteSuccess<shape, original, index, value> ->
600                  {TransformTotality.write_succeeded(shape, Core.write_flat(shape, original, index, value)) == True{} : Bool}}(
601                    TransformLaws.tensor_write_valid_success(shape, original, index, value, inside)), rec))}