def planned_success

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1964

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof

1964def planned_success(+input: Shape.Shape, +axes: List<&2, U32>, planned: Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, source: Core.Tensor<input>,
1965  -successful: {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, planned) == True{} : Bool}) ->
1966  Totality.PublicSuccess<input, Transforms.copy_planned(input, axes, source, planned)>:
1967  match planned:
1968    case Fail{error}:
1969      Totality.PublicSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1970    case Done{+plan}:
1971      allocated_success(input, axes, plan, Core.new(Layout.output(input, axes, plan), 0.0), source,
1972        AllocationProof.core_new_done(Layout.output(input, axes, plan), 0.0))