def reshape_built_success

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

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/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

1369def reshape_built_success(+input: Shape.Shape, +target: Shape.Shape,
1370  built: Shape.ConstructResult<Shape.dimensions(target)>, source: Core.Tensor<input>,
1371  -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat},
1372  -complete: {ShapeLaws.built(Shape.dimensions(target), built) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>}) ->
1373  ReshapeBuiltSuccess<input, target, source, built>:
1374  match built:
1375    case Shape.SError{error}:
1376      ReshapeBuiltSuccess{Empty.absurd({Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1377        Transforms.reshape_built(input, source, Shape.dimensions(target), Shape.SError{error})) == True{} : Bool},
1378        Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Mapping.metadata_present, None{}, Some{Shape.dimensions(target)}, complete)))}
1379    case Shape.SBuilt{+output, preserved}:
1380      ReshapeBuiltSuccess{
1381        {\{ReshapeDecisionSuccess: success => success} :
1382          ReshapeDecisionSuccess<input, output, source, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output)))> ->
1383            {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1384              Transforms.reshape_decided(input, output, source, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))))) == True{} : Bool}}(
1385                reshape_decision_success(input, output, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))), source,
1386                  Mapping.element_counts_same(input, output,
1387                    Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)),
1388                      Shape.logical_numel(Shape.dimensions(output)), same,
1389                      Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(target), Shape.dimensions(output),
1390                        Equal.sym(List<&2, U32>, Shape.dimensions(output), Shape.dimensions(target), preserved))))))}