def construction_values_complete

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend as Totality

670def construction_values_complete(+dimensions: List<&2, U32>, +shape: Shape.Shape,
671  +preserved: {Shape.dimensions(shape) == dimensions : List<&2, U32>},
672  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, certificate: Totality.TensorDone<shape, result>) ->
673  Totality.ConstructionDone<dimensions, Core.construct_values(shape, result)>:
674  match result:
675    case Fail{error}:
676      Totality.ConstructionDone{
677        Empty.absurd(Totality.ConstructionWitness<dimensions, Fail{error}>,
678          {\{Totality.TensorDone: witness => successful => readable => Arith.clash(successful)} :
679            Totality.TensorDone<shape, Fail{error}> -> Empty}(certificate)),
680        {\{Totality.TensorDone: witness => successful => readable => successful} :
681          Totality.TensorDone<shape, Fail{error}> -> {False{} == True{} : Bool}}(certificate), Unit{}}
682    case Done{tensor}:
683      Totality.ConstructionDone{Totality.ConstructionWitness{shape, tensor, {==}, preserved}, {==}, index => inside =>
684        TransformProof.read_success_status(shape, tensor, index, TransformProof.read_success(shape, tensor, index,
685          %Equal.sym(List<&2, U32>, Shape.dimensions(shape), dimensions, preserved) :
686            {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
687          inside))}