law reduce_not_reducible

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

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

163# When the planned broadcast of the target is not the contribution's shape
164# (for example a [2, 3] target for a [3] contribution), reduce_to fails with
165# NotReducible and returns the contribution owner.
166law reduce_not_reducible:
167  for input: Core.Dynamic
168  for +target: Shape.Shape
169  for +plan: Shape.BroadcastPlan
170  for planned: {Shape.broadcast_checked(target, Totality.dynamic_shape(input)) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}
171  for differ: {Shape.dimensions(Shape.output_shape(plan)) != Totality.dimensions(input) : List<&2, U32>}
172  {Reduce.reduce_to(input, target) == (input, Fail{Reduce.NotReducible{}}) : Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}