law reduce_shape_error

bendtorch-core@0.1.0.0 · src/autograd/reduce_LAWS.bend:152

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

152# When the broadcast planner rejects the target and contribution shapes,
153# reduce_to fails with exactly that planner error and returns the contribution
154# owner. For example [2] to [0] fails with IncompatibleBroadcast instead of
155# returning an empty tensor.
156law reduce_shape_error:
157  for input: Core.Dynamic
158  for +target: Shape.Shape
159  for error: Shape.Error
160  for rejected: {Shape.broadcast_checked(target, Totality.dynamic_shape(input)) == Fail{error} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}
161  {Reduce.reduce_to(input, target) == (input, Fail{Reduce.TensorError{Core.ShapeError{error}}}) : Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}