def reshape_built_failure

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1686

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
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/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping

1686def reshape_built_failure(+input: Shape.Shape, +target: Shape.Shape, built: Shape.ConstructResult<Shape.dimensions(target)>, -source: Core.Tensor<input>,
1687  different: {False{} == Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) : Bool},
1688  complete: {ShapeLaws.built(Shape.dimensions(target), built) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>}) ->
1689  {Transforms.reshape_built(input, source, Shape.dimensions(target), built) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} :
1690    Result<&2, &1, Transforms.Error, Core.Dynamic>}:
1691  match built:
1692    case Shape.SError{error}:
1693      Empty.absurd({Transforms.reshape_built(input, source, Shape.dimensions(target), Shape.SError{error}) ==
1694        Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>},
1695          Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Mapping.metadata_present, None{}, Some{Shape.dimensions(target)}, complete)))
1696    case Shape.SBuilt{+output, preserved}:
1697      reshape_decided_failure(input, output, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))), source,
1698        %Equal.sym(Nat, Shape.elements(input), Shape.logical_numel(Shape.dimensions(input)), Shape.elements_exact(input)) :
1699          {False{} == Nat.is_eq(_, Shape.elements(output)) : Bool}
1700        %Equal.sym(Nat, Shape.elements(output), Shape.logical_numel(Shape.dimensions(output)), Shape.elements_exact(output)) :
1701          {False{} == Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), _) : Bool}
1702        %Equal.sym(List<&2, U32>, Shape.dimensions(output), Shape.dimensions(target), preserved) :
1703          {False{} == Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(_)) : Bool}
1704        different)