def allocated_model

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

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/tensor/permute_build_proof.bend as PermuteBuild

1035def allocated_model(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, source: Core.Tensor<input>,
1036  allocated: Result<&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>>) ->
1037  Transforms.PublicModel<input, axes, source, Transforms.copy_allocated(input, axes, plan, source, allocated)>:
1038  match allocated:
1039    case Fail{error}:
1040      Transforms.PublicModel{Unit{}}
1041    case Done{target}:
1042      copy_pack_model(input, axes, plan, source, Transforms.built(input, axes, plan, source, target),
1043        PermuteBuild.built_meaning(input, axes, plan, source, target))