def reshape_built_model

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

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

1099def reshape_built_model(+input: Shape.Shape, source: Core.Tensor<input>, -dimensions: List<&2, U32>,
1100  built: Shape.ConstructResult<dimensions>) -> ReshapeBuiltModel<input, source, dimensions, built>:
1101  match built:
1102    case Shape.SError{error}:
1103      ReshapeBuiltModel{Unit{}}
1104    case Shape.SBuilt{+target, preserved}:
1105      ReshapeBuiltModel{
1106        {\{ReshapeDecidedModel: meaning => meaning} :
1107          ReshapeDecidedModel<input, target, source, dimensions, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(target)))> ->
1108            Transforms.ReshapeMeaning(input, source, dimensions,
1109              Transforms.reshape_decided(input, target, source, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(target)))))}(
1110                reshape_decided_model(input, target, source, dimensions, preserved,
1111                  Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(target)))))}