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 | ||| Primitive backend data types, and their interaction with Idris.
17 | |||
18 | ||| This module contains a number of interfaces (`Primitive.Num`, `Primitive.Eq` etc.). These
19 | ||| indicate what operations 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 | ||| For example, primitive types satisfying `Primitive.Ord` have a notion of ordering.
22 | module Primitive
23 |
24 | import Compiler.LiteralRW
25 | import public Compiler.Xla.XlaData
26 |
27 | %hide Prelude.Num
28 | %hide Prelude.Neg
29 | %hide Prelude.Abs
30 | %hide Prelude.Integral
31 | %hide Prelude.Fractional
32 |
33 | export interface Primitive dtype => Num dtype where
34 | export interface Num dtype => Neg dtype where
35 | export interface Num dtype => Abs dtype where
36 | export interface Num dtype => Integral dtype where
37 | export interface Num dtype => Fractional dtype where
38 |
39 | export Num U32 where
40 | export Num U64 where
41 | export Num S32 where
42 | export Num S64 where
43 | export Num F64 where
44 |
45 | export Neg S32 where
46 | export Neg S64 where
47 | export Neg F64 where
48 |
49 | export Abs S32 where
50 | export Abs S64 where
51 | export Abs F64 where
52 |
53 | export Integral U32 where
54 | export Integral U64 where
55 | export Integral S32 where
56 | export Integral S64 where
57 |
58 | export Fractional F64 where
59 |
60 | %hide Prelude.Eq
61 | %hide Prelude.Ord
62 |
63 | export interface Primitive dtype => Eq dtype where
64 |
65 | export Eq PRED where
66 | export Eq U32 where
67 | export Eq U64 where
68 | export Eq S32 where
69 | export Eq S64 where
70 | export Eq F64 where
71 |
72 | ||| A `PrimitiveRW dtype idr` means that values of type `idr` can be used to construct backend
73 | ||| data with data type `dtype`.
74 | export
75 | interface LiteralRW dtype idr => PrimitiveRW dtype idr | dtype where
76 |
77 | export PrimitiveRW PRED Bool where
78 | export PrimitiveRW S32 Int32 where
79 | export PrimitiveRW U32 Nat where
80 | export PrimitiveRW U64 Nat where
81 | export PrimitiveRW F64 Double where
82 |