0 | {--
  1 | Copyright (C) 2021  Joel Berkeley
  2 |
  3 | This program is free software: you can redistribute it and/or modify
  4 | it under the terms of the GNU Affero General Public License as published
  5 | by the Free Software Foundation, either version 3 of the License, or
  6 | (at your option) any later version.
  7 |
  8 | This program is distributed in the hope that it will be useful,
  9 | but WITHOUT ANY WARRANTY; without even the implied warranty of
 10 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 11 | GNU Affero General Public License for more details.
 12 |
 13 | You should have received a copy of the GNU Affero General Public License
 14 | along with this program.  If not, see <https://www.gnu.org/licenses/>.
 15 | --}
 16 | ||| Tensor data types, and their interaction with Idris.
 17 | |||
 18 | ||| This module contains a number of data types (`Num`, `Eq` etc.) which indicate what operations
 19 | ||| can be performed on primitive data in the backend. They are entirely
 20 | ||| distinct from the Idris interfaces `Prelude.Num` etc. but carry largely the same meaning.
 21 | module DType
 22 |
 23 | import Derive.Prelude
 24 |
 25 | %language ElabReflection
 26 |
 27 | public export
 28 | data DType = PRED | S32 | S64 | U32 | U64 | F64
 29 |
 30 | %runElab derive "DType" [Show, Eq]
 31 |
 32 | public export
 33 | idrisType : DType -> Type
 34 | idrisType PRED = Bool
 35 | idrisType S32  = Int32
 36 | idrisType S64  = Int64
 37 | idrisType U32  = Bits32
 38 | idrisType U64  = Bits64
 39 | idrisType F64  = Double
 40 |
 41 | public export
 42 | data Num : DType -> Type where
 43 |   NumS32 : Num S32
 44 |   NumS64 : Num S64
 45 |   NumU32 : Num U32
 46 |   NumU64 : Num U64
 47 |   NumF64 : Num F64
 48 |
 49 | public export
 50 | data Neg : DType -> Type where
 51 |   NegS32 : Neg S32
 52 |   NegS64 : Neg S64
 53 |   NegF64 : Neg F64
 54 |
 55 | export %hint
 56 | negNum : DType.Neg dtype -> Num dtype
 57 | negNum NegS32 = NumS32
 58 | negNum NegS64 = NumS64
 59 | negNum NegF64 = NumF64
 60 |
 61 | public export
 62 | data Abs : DType -> Type where
 63 |   AbsS32 : Abs S32
 64 |   AbsS64 : Abs S64
 65 |   AbsU32 : Abs U32
 66 |   AbsU64 : Abs U64
 67 |   AbsF64 : Abs F64
 68 |
 69 | export %hint
 70 | absNum : DType.Abs dtype -> Num dtype
 71 | absNum AbsS32 = NumS32
 72 | absNum AbsS64 = NumS64
 73 | absNum AbsU32 = NumU32
 74 | absNum AbsU64 = NumU64
 75 | absNum AbsF64 = NumF64
 76 |
 77 | public export
 78 | data Integral : DType -> Type where
 79 |   IntegralS32 : Integral S32
 80 |   IntegralS64 : Integral S64
 81 |   IntegralU32 : Integral U32
 82 |   IntegralU64 : Integral U64
 83 |
 84 | export %hint
 85 | integralNum : DType.Integral dtype -> Num dtype
 86 | integralNum IntegralS32 = NumS32
 87 | integralNum IntegralS64 = NumS64
 88 | integralNum IntegralU32 = NumU32
 89 | integralNum IntegralU64 = NumU64
 90 |
 91 | public export
 92 | data Fractional : DType -> Type where
 93 |   FractionalF64 : Fractional F64
 94 |
 95 | export %hint
 96 | fractionalNum : DType.Fractional dtype -> Num dtype
 97 | fractionalNum FractionalF64 = NumF64
 98 |
 99 | public export
100 | data Eq : DType -> Type where
101 |   EqPRED : Eq PRED
102 |   EqS32  : Eq S32
103 |   EqS64  : Eq S64
104 |   EqU32  : Eq U32
105 |   EqU64  : Eq U64
106 |   EqF64  : Eq F64
107 |
108 | public export
109 | data Ord : DType -> Type where
110 |   OrdS32 : Ord S32
111 |   OrdS64 : Ord S64
112 |   OrdU32 : Ord U32
113 |   OrdU64 : Ord U64
114 |   OrdF64 : Ord F64
115 |
116 | export %hint
117 | ordEq : DType.Ord dtype -> Eq dtype
118 | ordEq OrdS32 = EqS32
119 | ordEq OrdS64 = EqS64
120 | ordEq OrdU32 = EqU32
121 | ordEq OrdU64 = EqU64
122 | ordEq OrdF64 = EqF64
123 |