src/tensor/math_totality.bend

bendtorch-core@0.1.0.0 · 34 lines · 8 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
5
6type Status<-error: Data, -value: Type, -result: Result<&2, &1, error, value>> is Data:
7  Status{-successful: {Result.is_done(&2, &1, error, value, result) == True{} : Bool}}
8
9type DoneWitness<-error: Data, -value: Type, -result: Result<&2, &1, error, value>> is Data:
10  DoneWitness{-returned: value, -exact: {Done{returned} == result : Result<&2, &1, error, value>}}
11
12type Success<-error: Data, -value: Type, -result: Result<&2, &1, error, value>> is Data:
13  Success{-successful: {Result.is_done(&2, &1, error, value, result) == True{} : Bool},
14    -witness: DoneWitness<error, value, result>}
15
16type MatrixInputs<-left: Shape.Shape, -right: Shape.Shape> is Data:
17  MatrixInputs{-rows: U32, -inner: U32, -right_inner: U32, -columns: U32,
18    -left_dimensions: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>},
19    -right_dimensions: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
20    -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
21    -output_supported: Shape.LE(Shape.logical_numel([rows, columns]), 1048576n)}
22
23type MatrixBounds<-rows: U32, -inner: U32, -right_inner: U32, -columns: U32> is Data:
24  MatrixBounds{-compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
25    -supported: Shape.LE(Shape.logical_numel([rows, columns]), 1048576n)}
26
27type Impossible is Data:
28  Impossible{-empty: Empty}
29
30type RankTwo<-shape: Shape.Shape> is Data:
31  RankTwo{-rank: {Shape.rank_dimensions(Shape.dimensions(shape)) == 2n : Nat}}
32
33type ReadStatus<-shape: Shape.Shape, -pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>> is Data:
34  ReadStatus{-successful: {TransformTotality.read_succeeded(shape, pair) == True{} : Bool}}