def allocated_fill_success

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

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/word_conversion.bend as WordConversion
import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation

620def allocated_fill_success(+shape: Shape.Shape, +values: List<&2, F32>,
621  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, certificate: Allocation.TensorDone<shape, result>,
622  counted: {List.length(&2, F32, values) == Shape.elements(shape) : Nat}) ->
623  FillSuccess<shape, Core.from_values_new(shape, values, result)>:
624  match result:
625    case Fail{error}:
626      FillSuccess{Empty.absurd({False{} == True{} : Bool},
627        {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.sym(Bool, True{}, False{},
628          Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Bool,
629            Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>), Done{tensor}, Fail{error}, same)))} :
630          Allocation.TensorDone<shape, Fail{error}> -> Empty}(certificate))}
631    case Done{tensor}:
632      fill_success(values, shape, tensor, 0n,
633        %Equal.sym(Nat, List.length(&2, F32, values), Shape.elements(shape), counted) : Shape.LE(_, Shape.elements(shape))
634        Shape.LE.from(Shape.elements(shape), Shape.elements(shape),
635          Equal.sym(Bool, Nat.is_le(Shape.elements(shape), Shape.elements(shape)), True{}, WordConversion.le_reflexive(Shape.elements(shape)))))