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 | ||| Definitions and utilities for datasets.
17 | module Data
18 |
19 | import Tensor
20 |
21 | %prefix_record_projections off
22 |
23 | ||| Observed pairs of data points from feature and target domains. Data sets such as this are
24 | ||| commonly used in supervised learning settings.
25 | |||
26 | ||| @features The shape of the feature domain.
27 | ||| @targets The shape of the target domain.
28 | public export
29 | record Dataset (0 featureShape, targetShape : Shape) where
30 |   constructor MkDataset
31 |   {s : Nat}
32 |
33 |   ||| The feature data
34 |   features : Tensor (S s :: featureShape) F64
35 |
36 |   ||| The target data
37 |   targets : Tensor (S s :: targetShape) F64
38 |
39 | %prefix_record_projections on
40 |
41 | ||| Concatenate two datasets along their leading axis.
42 | export
43 | concat : Dataset features targets -> Dataset features targets -> Dataset features targets
44 | concat (MkDataset {s = s} x y) (MkDataset {s = s'} x' y') =
45 |   MkDataset {s = s + S s'} (concat 0 x x') (concat 0 y y')
46 |
47 | export
48 | Taggable (Dataset f t) where
49 |   tag (MkDataset f t) = [| MkDataset (tag f) (tag t) |]
50 |