def dropped_reshaped

bendtorch-core@0.1.0.0 · src/autograd/sum_dims_PROOF.bend:121

import Base
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
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend as SumDims
import bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend as Laws

121# Without keepdim, summed reshapes what it gives with keepdim.
122def dropped_reshaped(+dropped: List<&2, U32>, pair: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>) ->
123  {SumDims.summed(dropped, False{}, pair) == Laws.reshaped(dropped, SumDims.summed(dropped, True{}, pair)) :
124    Core.Dynamic & Result<&2, &1, SumDims.Error, Core.Dynamic>}:
125  match pair:
126    case Tuple{input, Fail{error}}:
127      {==}
128    case Tuple{input, Done{output}}:
129      Equal.cong(Result<&2, &1, SumDims.Error, Core.Dynamic>, Core.Dynamic & Result<&2, &1, SumDims.Error, Core.Dynamic>,
130        result => (input, result), SumDims.transformed(Transforms.reshape_dynamic(output, dropped)),
131        Laws.reshape_as_sum(Transforms.reshape_dynamic(output, dropped)), reshape_renamed(Transforms.reshape_dynamic(output, dropped)))