def planned_mapping
bendtorch-core@0.1.0.0 · src/autograd/broadcast_PROOF.bend:201
import bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend as BroadcastPROOF
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/broadcast.bend as Broadcast
201def planned_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
202 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
203 +sources: {ShapeLaws.planned_dimensions(shape, target, result) == (Shape.dimensions(shape), Shape.dimensions(target)) : List<&2, U32> & List<&2, U32>}) ->
204 WithModel<Core.Packed{shape, tensor}, target, result, Broadcast.planned(Core.Packed{shape, tensor}, target, result)>:
205 match result:
206 case Fail{error}:
207 WithModel{Unit{}}
208 case Done{+plan}:
209 fitted_mapping(Core.Packed{shape, tensor}, target, plan,
210 Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)), {==},
211 Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(shape),
212 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>),
213 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(shape), Shape.dimensions(target)), sources)),
214 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>),
215 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(shape), Shape.dimensions(target)), sources))