|
1 | 1 | module Type.Row |
2 | 2 | ( module Prim.Row |
3 | 3 | , module RProxy |
4 | | - , module Prim.RowList |
5 | | - , module RLProxy |
6 | | - , class ListToRow |
7 | | - , class RowListRemove |
8 | | - , class RowListSet |
9 | | - , class RowListNub |
10 | | - , class RowListAppend |
11 | 4 | , RowApply |
12 | 5 | , type (+) |
13 | 6 | ) where |
14 | 7 |
|
15 | 8 | import Prim.Row (class Lacks, class Nub, class Cons, class Union) |
16 | | -import Prim.RowList (kind RowList, Cons, Nil, class RowToList) |
17 | | -import Type.Equality (class TypeEquals) |
18 | | -import Type.Data.Symbol as Symbol |
19 | | -import Type.Data.Boolean as Boolean |
20 | 9 | import Type.Data.Row (RProxy(..)) as RProxy |
21 | | -import Type.Data.RowList (RLProxy) |
22 | | -import Type.Data.RowList (RLProxy(..)) as RLProxy |
23 | | - |
24 | | - |
25 | | --- | Convert a RowList to a row of types. |
26 | | --- | The inverse of this operation is `RowToList`. |
27 | | -class ListToRow (list :: RowList) |
28 | | - (row :: # Type) | |
29 | | - list -> row |
30 | | - |
31 | | -instance listToRowNil |
32 | | - :: ListToRow Nil () |
33 | | - |
34 | | -instance listToCons |
35 | | - :: ( ListToRow tail tailRow |
36 | | - , Cons label ty tailRow row ) |
37 | | - => ListToRow (Cons label ty tail) row |
38 | | - |
39 | | --- | Remove all occurences of a given label from a RowList |
40 | | -class RowListRemove (label :: Symbol) |
41 | | - (input :: RowList) |
42 | | - (output :: RowList) |
43 | | - | label input -> output |
44 | | - |
45 | | -instance rowListRemoveNil |
46 | | - :: RowListRemove label Nil Nil |
47 | | - |
48 | | -instance rowListRemoveCons |
49 | | - :: ( RowListRemove label tail tailOutput |
50 | | - , Symbol.Equals label key eq |
51 | | - , Boolean.If eq |
52 | | - (RLProxy tailOutput) |
53 | | - (RLProxy (Cons key head tailOutput)) |
54 | | - (RLProxy output) |
55 | | - ) |
56 | | - => RowListRemove label (Cons key head tail) output |
57 | | - |
58 | | --- | Add a label to a RowList after removing other occurences. |
59 | | -class RowListSet (label :: Symbol) |
60 | | - (typ :: Type) |
61 | | - (input :: RowList) |
62 | | - (output :: RowList) |
63 | | - | label typ input -> output |
64 | | - |
65 | | -instance rowListSetImpl |
66 | | - :: ( TypeEquals (Symbol.SProxy label) (Symbol.SProxy label') |
67 | | - , TypeEquals typ typ' |
68 | | - , RowListRemove label input lacking ) |
69 | | - => RowListSet label typ input (Cons label' typ' lacking) |
70 | | - |
71 | | --- | Remove label duplicates, keeps earlier occurrences. |
72 | | -class RowListNub (input :: RowList) |
73 | | - (output :: RowList) |
74 | | - | input -> output |
75 | | - |
76 | | -instance rowListNubNil |
77 | | - :: RowListNub Nil Nil |
78 | | - |
79 | | -instance rowListNubCons |
80 | | - :: ( TypeEquals (Symbol.SProxy label) (Symbol.SProxy label') |
81 | | - , TypeEquals head head' |
82 | | - , TypeEquals (RLProxy nubbed) (RLProxy nubbed') |
83 | | - , RowListRemove label tail removed |
84 | | - , RowListNub removed nubbed ) |
85 | | - => RowListNub (Cons label head tail) (Cons label' head' nubbed') |
86 | | - |
87 | | --- Append two row lists together |
88 | | -class RowListAppend (lhs :: RowList) |
89 | | - (rhs :: RowList) |
90 | | - (out :: RowList) |
91 | | - | lhs rhs -> out |
92 | | - |
93 | | -instance rowListAppendNil |
94 | | - :: TypeEquals (RLProxy rhs) (RLProxy out) |
95 | | - => RowListAppend Nil rhs out |
96 | | - |
97 | | -instance rowListAppendCons |
98 | | - :: ( RowListAppend tail rhs out' |
99 | | - , TypeEquals (RLProxy (Cons label head out')) (RLProxy out) ) |
100 | | - => RowListAppend (Cons label head tail) rhs out |
101 | 10 |
|
102 | 11 | -- | Type application for rows. |
103 | 12 | type RowApply (f :: # Type -> # Type) (a :: # Type) = f a |
|
0 commit comments