def planned_mapping

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:384

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

384def planned_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
385  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
386  -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>}) ->
387  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, result, Reduce.planned(shape, tensor, target, result))>:
388  match result:
389    case Fail{error}:
390      Holds{Unit{}}
391    case Done{+plan}:
392      fitted_mapping(shape, tensor, target, plan, Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), {==},
393        Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>),
394          (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(target), Shape.dimensions(shape)), sources),
395        Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>),
396          (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(target), Shape.dimensions(shape)), sources))