def built_meaning

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:491

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/storage/main.bend as Storage
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

491# The parallel copy meets the copy loop's meaning on every source and target.
492def built_meaning(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, source: Core.Tensor<input>,
493  target: Core.Tensor<Layout.output(input, axes, plan)>) ->
494  Transforms.LoopMeaning(input, axes, plan, source, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Transforms.built(input, axes, plan, source, target)):
495  Core.TTensor{storage, exact} = target
496  match storage:
497    case Storage.Empty{}:
498      Transforms.Prefix{other => {==},
499        other => earlier => Empty.absurd({U32.to_nat(U32.from_nat(other)) == other : Nat}, empty_below(Layout.output(input, axes, plan), other, exact, earlier)),
500        other => earlier => Empty.absurd(Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), Core.TTensor{Storage.Empty{}, exact}}, U32.from_nat(other)),
501          empty_below(Layout.output(input, axes, plan), other, exact, earlier)),
502        other => earlier => Empty.absurd({Core.checked_observe(Layout.output(input, axes, plan), Core.TTensor{Storage.Empty{}, exact}, U32.from_nat(other)) ==
503          Transforms.expected_output(input, axes, plan, source, U32.from_nat(other)) : Maybe<&2, F32>}, empty_below(Layout.output(input, axes, plan), other, exact, earlier))}
504    case Storage.Owned{+d, +n, array, balanced, valid}:
505      owned_meaning(input, axes, plan, d, n, valid, exact, source)