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 Spidr.DType
 22 |
 23 | import Derive.Prelude
 24 |
 25 | %language ElabReflection
 26 |
 27 | public export
 28 | data DType = PRED | S8 | S16 | S32 | S64 | U8 | U16 | U32 | U64 | F64
 29 |
 30 | %runElab derive "DType" [Show, Eq]
 31 |
 32 | public export
 33 | idrisType : DType -> Type
 34 | idrisType PRED = Bool
 35 | idrisType S8   = Int8
 36 | idrisType S16  = Int16
 37 | idrisType S32  = Int32
 38 | idrisType S64  = Int64
 39 | idrisType U8   = Bits8
 40 | idrisType U16  = Bits16
 41 | idrisType U32  = Bits32
 42 | idrisType U64  = Bits64
 43 | idrisType F64  = Double
 44 |
 45 | public export
 46 | data Num : DType -> Type where
 47 |   NumS8  : Num S8
 48 |   NumS16 : Num S16
 49 |   NumS32 : Num S32
 50 |   NumS64 : Num S64
 51 |   NumU8  : Num U8
 52 |   NumU16 : Num U16
 53 |   NumU32 : Num U32
 54 |   NumU64 : Num U64
 55 |   NumF64 : Num F64
 56 |
 57 | public export
 58 | data Neg : DType -> Type where
 59 |   NegS8  : Neg S8
 60 |   NegS16 : Neg S16
 61 |   NegS32 : Neg S32
 62 |   NegS64 : Neg S64
 63 |   NegF64 : Neg F64
 64 |
 65 | export %hint
 66 | negNum : DType.Neg dtype -> Num dtype
 67 | negNum NegS8  = NumS8
 68 | negNum NegS16 = NumS16
 69 | negNum NegS32 = NumS32
 70 | negNum NegS64 = NumS64
 71 | negNum NegF64 = NumF64
 72 |
 73 | public export
 74 | data Abs : DType -> Type where
 75 |   AbsS8  : Abs S8
 76 |   AbsS16 : Abs S16
 77 |   AbsS32 : Abs S32
 78 |   AbsS64 : Abs S64
 79 |   AbsU8  : Abs U8
 80 |   AbsU16 : Abs U16
 81 |   AbsU32 : Abs U32
 82 |   AbsU64 : Abs U64
 83 |   AbsF64 : Abs F64
 84 |
 85 | export %hint
 86 | absNum : DType.Abs dtype -> Num dtype
 87 | absNum AbsS8  = NumS8
 88 | absNum AbsS16 = NumS16
 89 | absNum AbsS32 = NumS32
 90 | absNum AbsS64 = NumS64
 91 | absNum AbsU8  = NumU8
 92 | absNum AbsU16 = NumU16
 93 | absNum AbsU32 = NumU32
 94 | absNum AbsU64 = NumU64
 95 | absNum AbsF64 = NumF64
 96 |
 97 | public export
 98 | data Integral : DType -> Type where
 99 |   IntegralS8  : Integral S8
100 |   IntegralS16 : Integral S16
101 |   IntegralS32 : Integral S32
102 |   IntegralS64 : Integral S64
103 |   IntegralU8  : Integral U8
104 |   IntegralU16 : Integral U16
105 |   IntegralU32 : Integral U32
106 |   IntegralU64 : Integral U64
107 |
108 | export %hint
109 | integralNum : DType.Integral dtype -> Num dtype
110 | integralNum IntegralS8  = NumS8
111 | integralNum IntegralS16 = NumS16
112 | integralNum IntegralS32 = NumS32
113 | integralNum IntegralS64 = NumS64
114 | integralNum IntegralU8  = NumU8
115 | integralNum IntegralU16 = NumU16
116 | integralNum IntegralU32 = NumU32
117 | integralNum IntegralU64 = NumU64
118 |
119 | public export
120 | data Fractional : DType -> Type where
121 |   FractionalF64 : Fractional F64
122 |
123 | export %hint
124 | fractionalNum : DType.Fractional dtype -> Num dtype
125 | fractionalNum FractionalF64 = NumF64
126 |
127 | public export
128 | data Ord : DType -> Type where
129 |   OrdS8  : Ord S8
130 |   OrdS16 : Ord S16
131 |   OrdS32 : Ord S32
132 |   OrdS64 : Ord S64
133 |   OrdU8  : Ord U8
134 |   OrdU16 : Ord U16
135 |   OrdU32 : Ord U32
136 |   OrdU64 : Ord U64
137 |   OrdF64 : Ord F64
138 |