def mismatch_decided

bendtorch-core@0.1.0.0 · src/tensor/reshape_contract.bend:204

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
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/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof

204def mismatch_decided(+input: Shape.Shape, +target: Shape.Shape, +output: Shape.Shape, -tensor: Core.Tensor<input>,
205  decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(output))>,
206  preserved: {Shape.dimensions(output) == Shape.dimensions(target) : List<&2, U32>},
207  different: {Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) == False{} : Bool}) ->
208  {Transforms.reshape_decided(input, output, tensor, decision) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>}:
209  match decision:
210    case Shape.BFalse{no}:
211      {==}
212    case Shape.BTrue{yes}:
213      Empty.absurd({Transforms.reshape_decided(input, output, tensor, Shape.BTrue{yes}) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>},
214        Nats.contradiction(Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))),
215          AllocationProof.natural_equal_true(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)),
216            Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(output)), Shape.logical_numel(Shape.dimensions(target)), Transforms.elements_equal(input, output, yes),
217              Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(output), Shape.dimensions(target), preserved))),
218          Equal.sym(Bool, Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))), False{}, different)))