Data/Lens.ad

Outline



Content


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262



-- very poor man's lenses
module Data.Lens (
  -- Basic Defintions for Lenses, Getters and Setters
  Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable(..)constructor `Getter`
field `getterGet`
,
  Setterrecord-type `Data.Lens.Setter`
   kind `* -> * -> * -> *`
   executable(..)constructor `Setter`
field `setterSet`
,
  Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable(..)constructor `Lens`
field `lensGet`
field `lensSet`
,
  SimpleLensabbreviation-type `Data.Lens.SimpleLens`
   kind `* -> * -> *`
   type `SimpleLens 's 'a` abbreviates type `Lens 's 's 'a 'a`
   executable(..)definition of abbreviation-type,
  SimpleSetterabbreviation-type `Data.Lens.SimpleSetter`
   kind `* -> * -> *`
   type `SimpleSetter 's 'b` abbreviates type `Setter 's 's 'b`
   executable(..)definition of abbreviation-type,

  IsGettertype-class `Data.Lens.IsGetter`
   arguments: ('v :: *) ('a :: *) ('b :: *)
   functional deps: 'v -> 'a 'b(..)class-constant `toGetter`
class-constant `view`
,
  IsSettertype-class `Data.Lens.IsSetter`
   arguments: ('v :: *) ('s :: *) ('t :: *) ('b :: *)
   functional deps: 'v -> 's 't 'b(..)class-constant `set`
class-constant `toSetter`
,
  toconstant `Data.Lens.to`
   constant
   type `('a -> 'b) -> Getter 'a 'b`
   executable,
  (^.)constant `Data.Lens.view`
   constant of type-class `IsGetter`
   type `'v -> 'a -> 'b`
   executable,
  simpleLensToGetterconstant `Data.Lens.simpleLensToGetter`
   constant
   type `SimpleLens 'a 'b -> Getter 'a 'b`
   executable,

  -- Tuple lenses
  Elem1type-class `Data.Lens.Elem1`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem1`
,
  Elem2type-class `Data.Lens.Elem2`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem2`
,
  Elem3type-class `Data.Lens.Elem3`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem3`
,
  Elem4type-class `Data.Lens.Elem4`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem4`
,
  Elem5type-class `Data.Lens.Elem5`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem5`
,
  Elem6type-class `Data.Lens.Elem6`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem6`
,
  Elem7type-class `Data.Lens.Elem7`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem7`
,
  Elem8type-class `Data.Lens.Elem8`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem8`
,
  Elem9type-class `Data.Lens.Elem9`
   arguments: ('s :: *) ('t :: *) ('a :: *) ('b :: *)
   functional deps: 's -> 'a, 's 'b -> 't(..)class-constant `elem9`
,

  -- Templates for building lenses corresponding to record fields
  BuildRecordFieldLenstemplate `Data.Lens.BuildRecordFieldLens`
   argument-types: (ConstID, String)
   return-type: -,
  BuildRecordFieldLensestemplate `Data.Lens.BuildRecordFieldLenses`
   argument-type: TypeID
   return-type: -,
  BuildRecordFieldLensesPrefixtemplate `Data.Lens.BuildRecordFieldLensesPrefix`
   argument-types: (String, TypeID)
   return-type: -,
  BuildRecordFieldLensesSuffixtemplate `Data.Lens.BuildRecordFieldLensesSuffix`
   argument-types: (String, TypeID)
   return-type: -
) where

{-# severity similar-namessimilar names used for different entities - #-}

-- | a very poor mans lens. Essentially it is a tuple of a get and set function. The getter-part can
-- get a certain part out of some bigger data. The setter sets this part to a new value. Setting might change the type of the
-- output. For example, it is possible to set the second element of a tuple to a different type than its type in the input tuple.
-- This changes the type of the output so. ``Lens 's 't 'a 'b`` describes functions for getting a value of type 'a out of a value of
-- type 's and a for updating a value of type 's with a value of type 'b to get a value of type 't.
recordtype Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*` := Lens <|
     lensGet :: 'stype-variable `'s`
   kind `*` -> 'atype-variable `'a`
   kind `*`,
     lensSet :: 'stype-variable `'s`
   kind `*` -> 'btype-variable `'b`
   kind `*` -> 'ttype-variable `'t`
   kind `*`
  |>

-- | very often, the type is not changed by setting. This is then called a simple lens.
type SimpleLensabbreviation-type `Data.Lens.SimpleLens`
   kind `* -> * -> *`
   type `SimpleLens 's 'a` abbreviates type `Lens 's 's 'a 'a`
   executable 'stype-variable `'s`
   kind `*` 'atype-variable `'a`
   kind `*` := Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'stype-variable `'s`
   kind `*` 'atype-variable `'a`
   kind `*` 'atype-variable `'a`
   kind `*`

-- | a datatype for just the getter part of lenses
recordtype Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*` := Getter <|
     getterGet :: 'atype-variable `'a`
   kind `*` -> 'btype-variable `'b`
   kind `*`
  |>

-- | constructor for getters mimicking Haskell naming
declare toconstant `Data.Lens.to`
   constant
   type `('a -> 'b) -> Getter 'a 'b`
   executable :: ('atype-variable `'a`
   kind `*` -> 'btype-variable `'b`
   kind `*`) -> Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`
define toconstant `Data.Lens.to`
   constant
   type `('a -> 'b) -> Getter 'a 'b`
   executable := Getterconstant `Data.Lens.Getter`
   constructor of record-type `Getter`
   type `('a -> 'b) -> Getter 'a 'b`
   executable
{-# inline toconstant `Data.Lens.to`
   constant
   type `('a -> 'b) -> Getter 'a 'b`
   executable #-}

-- | the setter part of a lens, however, Setters without Getters are quite rare
recordtype Setterrecord-type `Data.Lens.Setter`
   kind `* -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'btype-variable `'b`
   kind `*` := Setter <|
     setterSet :: 'stype-variable `'s`
   kind `*` -> 'btype-variable `'b`
   kind `*` -> 'ttype-variable `'t`
   kind `*`
  |>

type SimpleSetterabbreviation-type `Data.Lens.SimpleSetter`
   kind `* -> * -> *`
   type `SimpleSetter 's 'b` abbreviates type `Setter 's 's 'b`
   executable 'stype-variable `'s`
   kind `*` 'btype-variable `'b`
   kind `*` := Setterrecord-type `Data.Lens.Setter`
   kind `* -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'stype-variable `'s`
   kind `*` 'btype-variable `'b`
   kind `*`


-- | type-class for accessing Lenses and Getters with a common interface
class IsGetter 'vtype-variable `'v`
   kind `*` 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*` | 'v -> 'a 'b where
  declare viewconstant `Data.Lens.view`
   constant of type-class `IsGetter`
   type `'v -> 'a -> 'b`
   executable :: 'vtype-variable `'v`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> 'btype-variable `'b`
   kind `*`

  declare toGetterconstant `Data.Lens.toGetter`
   constant of type-class `IsGetter`
   type `'v -> Getter 'a 'b`
   executable :: 'vtype-variable `'v`
   kind `*` -> Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`
  define toGetterconstant `Data.Lens.toGetter`
   default instance of type-class constant
   type `('v -> 'a -> 'b) -> 'v -> Getter 'a 'b`
   executable := Getterconstant `Data.Lens.Getter`
   constructor of record-type `Getter`
   type `('a -> 'b) -> Getter 'a 'b`
   executable .constant `Prelude.Function.(.)`
   constant of type-class `Dot`
   type `'a -> 'b -> 'c`
   type in context `(('a -> 'b) -> Getter 'a 'b) -> ('v -> 'a -> 'b) -> 'v -> Getter 'a 'b`
   executable
   statically resolved type-class instance viewconstant `Data.Lens.view`
   constant of type-class `IsGetter`
   type `'v -> 'a -> 'b`
   executable
   same type-class instance
  {-# inline toGetterconstant `Data.Lens.toGetter`
   default instance of type-class constant
   type `('v -> 'a -> 'b) -> 'v -> Getter 'a 'b`
   executable #-}
end-class

alias (^.) := viewconstant `Data.Lens.view`
   constant of type-class `IsGetter`
   type `'v -> 'a -> 'b`
   executable

-- | type-class for accessing Lenses and Setters with a common interface
class IsSetter 'vtype-variable `'v`
   kind `*` 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'btype-variable `'b`
   kind `*` | 'v -> 's 't 'b where
  declare setconstant `Data.Lens.set`
   constant of type-class `IsSetter`
   type `'v -> 's -> 'b -> 't`
   executable :: 'vtype-variable `'v`
   kind `*` -> 'stype-variable `'s`
   kind `*` -> 'btype-variable `'b`
   kind `*` -> 'ttype-variable `'t`
   kind `*`

  declare toSetterconstant `Data.Lens.toSetter`
   constant of type-class `IsSetter`
   type `'v -> Setter 's 't 'b`
   executable :: 'vtype-variable `'v`
   kind `*` -> Setterrecord-type `Data.Lens.Setter`
   kind `* -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'btype-variable `'b`
   kind `*`
  define toSetterconstant `Data.Lens.toSetter`
   default instance of type-class constant
   type `('v -> 's -> 'b -> 't) -> 'v -> Setter 's 't 'b`
   executable := Setterconstant `Data.Lens.Setter`
   constructor of record-type `Setter`
   type `('s -> 'b -> 't) -> Setter 's 't 'b`
   executable .constant `Prelude.Function.(.)`
   constant of type-class `Dot`
   type `'a -> 'b -> 'c`
   type in context `(('s -> 'b -> 't) -> Setter 's 't 'b) -> ('v -> 's -> 'b -> 't) -> 'v -> Setter 's 't 'b`
   executable
   statically resolved type-class instance setconstant `Data.Lens.set`
   constant of type-class `IsSetter`
   type `'v -> 's -> 'b -> 't`
   executable
   same type-class instance
  {-# inline toSetterconstant `Data.Lens.toSetter`
   default instance of type-class constant
   type `('v -> 's -> 'b -> 't) -> 'v -> Setter 's 't 'b`
   executable #-}
end-class

instance IsGettertype-class `Data.Lens.IsGetter`
   arguments: ('v :: *) ('a :: *) ('b :: *)
   functional deps: 'v -> 'a 'b (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`) 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*` where
  define viewconstant `Data.Lens.view`
   constant of type-class instance `IsGetter (Getter 'a 'b) 'a 'b`
   type `Getter 'a 'b -> 'a -> 'b`
   executable := getterGetconstant `Data.Lens.getterGet`
   field of record-type `Getter`
   type `Getter 'a 'b -> 'a -> 'b`
   executable
  {-# inline viewconstant `Data.Lens.view`
   constant of type-class instance `IsGetter (Getter 'a 'b) 'a 'b`
   type `Getter 'a 'b -> 'a -> 'b`
   executable #-}
end-instance

instance IsGettertype-class `Data.Lens.IsGetter`
   arguments: ('v :: *) ('a :: *) ('b :: *)
   functional deps: 'v -> 'a 'b (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`) 'stype-variable `'s`
   kind `*` 'atype-variable `'a`
   kind `*` where
  define viewconstant `Data.Lens.view`
   constant of type-class instance `IsGetter (Lens 's 't 'a 'b) 's 'a`
   type `Lens 's 't 'a 'b -> 's -> 'a`
   executable := lensGetconstant `Data.Lens.lensGet`
   field of record-type `Lens`
   type `Lens 's 't 'a 'b -> 's -> 'a`
   executable
  {-# inline viewconstant `Data.Lens.view`
   constant of type-class instance `IsGetter (Lens 's 't 'a 'b) 's 'a`
   type `Lens 's 't 'a 'b -> 's -> 'a`
   executable #-}
end-instance

-- | a version of toGetter for Lenses with extra type constraints
declare simpleLensToGetterconstant `Data.Lens.simpleLensToGetter`
   constant
   type `SimpleLens 'a 'b -> Getter 'a 'b`
   executable :: SimpleLensabbreviation-type `Data.Lens.SimpleLens`
   kind `* -> * -> *`
   type `SimpleLens 's 'a` abbreviates type `Lens 's 's 'a 'a`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*` -> Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`
define simpleLensToGetterconstant `Data.Lens.simpleLensToGetter`
   constant
   type `SimpleLens 'a 'b -> Getter 'a 'b`
   executable slvariable `sl`
   type `SimpleLens 'a 'b` := toGetterconstant `Data.Lens.toGetter`
   constant of type-class `IsGetter`
   type `'v -> Getter 'a 'b`
   type in context `SimpleLens 'a 'b -> Getter 'a 'b`
   executable
   statically resolved type-class instance slvariable `sl`
   type `SimpleLens 'a 'b`
{-# inline simpleLensToGetterconstant `Data.Lens.simpleLensToGetter`
   constant
   type `SimpleLens 'a 'b -> Getter 'a 'b`
   executable #-}

instance IsSettertype-class `Data.Lens.IsSetter`
   arguments: ('v :: *) ('s :: *) ('t :: *) ('b :: *)
   functional deps: 'v -> 's 't 'b (Setterrecord-type `Data.Lens.Setter`
   kind `* -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'btype-variable `'b`
   kind `*`) 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'btype-variable `'b`
   kind `*` where
  define setconstant `Data.Lens.set`
   constant of type-class instance `IsSetter (Setter 's 't 'b) 's 't 'b`
   type `Setter 's 't 'b -> 's -> 'b -> 't`
   executable := setterSetconstant `Data.Lens.setterSet`
   field of record-type `Setter`
   type `Setter 's 't 'b -> 's -> 'b -> 't`
   executable
  {-# inline setconstant `Data.Lens.set`
   constant of type-class instance `IsSetter (Setter 's 't 'b) 's 't 'b`
   type `Setter 's 't 'b -> 's -> 'b -> 't`
   executable #-}
end-instance

instance IsSettertype-class `Data.Lens.IsSetter`
   arguments: ('v :: *) ('s :: *) ('t :: *) ('b :: *)
   functional deps: 'v -> 's 't 'b (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`) 'stype-variable `'s`
   kind `*` 'ttype-variable `'t`
   kind `*` 'btype-variable `'b`
   kind `*` where
  define setconstant `Data.Lens.set`
   constant of type-class instance `IsSetter (Lens 's 't 'a 'b) 's 't 'b`
   type `Lens 's 't 'a 'b -> 's -> 'b -> 't`
   executable := lensSetconstant `Data.Lens.lensSet`
   field of record-type `Lens`
   type `Lens 's 't 'a 'b -> 's -> 'b -> 't`
   executable
  {-# inline setconstant `Data.Lens.set`
   constant of type-class instance `IsSetter (Lens 's 't 'a 'b) 's 't 'b`
   type `Lens 's 't 'a 'b -> 's -> 'b -> 't`
   executable #-}
end-instance

-- --------------------------------------
-- combine lenses, getters and setters
-- --------------------------------------

declare combineGetterconstant `Data.Lens.combineGetter`
   constant
   type `(IsGetter 'g1 'a 'b, IsGetter 'g2 'b 'c) => 'g1 -> 'g2 -> 'a -> 'c`
   executable :: (IsGettertype-class `Data.Lens.IsGetter`
   arguments: ('v :: *) ('a :: *) ('b :: *)
   functional deps: 'v -> 'a 'b 'g1type-variable `'g1`
   kind `*` 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`, IsGettertype-class `Data.Lens.IsGetter`
   arguments: ('v :: *) ('a :: *) ('b :: *)
   functional deps: 'v -> 'a 'b 'g2type-variable `'g2`
   kind `*` 'btype-variable `'b`
   kind `*` 'ctype-variable `'c`
   kind `*`) => 'g1type-variable `'g1`
   kind `*` -> 'g2type-variable `'g2`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> 'ctype-variable `'c`
   kind `*`
define combineGetterconstant `Data.Lens.combineGetter`
   constant
   type `(IsGetter 'g1 'a 'b, IsGetter 'g2 'b 'c) => 'g1 -> 'g2 -> 'a -> 'c`
   executable g1variable `g1`
   type `'g1` g2variable `g2`
   type `'g2` := viewconstant `Data.Lens.view`
   constant of type-class `IsGetter`
   type `'v -> 'a -> 'b`
   type in context `'g2 -> 'b -> 'c`
   executable
   type-class instance from argument g2variable `g2`
   type `'g2` .constant `Prelude.Function.(.)`
   constant of type-class `Dot`
   type `'a -> 'b -> 'c`
   type in context `('b -> 'c) -> ('a -> 'b) -> 'a -> 'c`
   executable
   statically resolved type-class instance viewconstant `Data.Lens.view`
   constant of type-class `IsGetter`
   type `'v -> 'a -> 'b`
   type in context `'g1 -> 'a -> 'b`
   executable
   type-class instance from argument g1variable `g1`
   type `'g1`
{-# inline combineGetterconstant `Data.Lens.combineGetter`
   constant
   type `(IsGetter 'g1 'a 'b, IsGetter 'g2 'b 'c) => 'g1 -> 'g2 -> 'a -> 'c`
   executable #-}

instance Dottype-class `Prelude.Function.Dot`
   arguments: ('a :: *) ('b :: *) ('c :: *)
   functional deps: 'a 'b -> 'c (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`) (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'b2type-variable `'b2`
   kind `*` 'ctype-variable `'c`
   kind `*`) (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'ctype-variable `'c`
   kind `*`) | 'b2type-variable `'b2`
   kind `*` -> 'btype-variable `'b`
   kind `*`  where
  define (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Getter 'a 'b) (Getter 'b2 'c) (Getter 'a 'c) | 'b2  ->  'b`
   type `Getter 'a 'b -> Getter 'b 'c -> Getter 'a 'c`
   executable g1variable `g1`
   type `Getter 'a 'b` g2variable `g2`
   type `Getter 'b 'c` := Getterconstant `Data.Lens.Getter`
   constructor of record-type `Getter`
   type `('a -> 'b) -> Getter 'a 'b`
   type in context `('a -> 'c) -> Getter 'a 'c`
   executable $constant `Prelude.Function.($)`
   constant
   type `('a -> 'b) -> 'a -> 'b`
   type in context `(('a -> 'c) -> Getter 'a 'c) -> ('a -> 'c) -> Getter 'a 'c`
   executable combineGetterconstant `Data.Lens.combineGetter`
   constant
   type `(IsGetter 'g1 'a 'b, IsGetter 'g2 'b 'c) => 'g1 -> 'g2 -> 'a -> 'c`
   type in context `Getter 'a 'b -> Getter 'b 'c -> 'a -> 'c`
   executable g1variable `g1`
   type `Getter 'a 'b` g2variable `g2`
   type `Getter 'b 'c`
  {-# inline (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Getter 'a 'b) (Getter 'b2 'c) (Getter 'a 'c) | 'b2  ->  'b`
   type `Getter 'a 'b -> Getter 'b 'c -> Getter 'a 'c`
   executable #-}
end-instance

instance Dottype-class `Prelude.Function.Dot`
   arguments: ('a :: *) ('b :: *) ('c :: *)
   functional deps: 'a 'b -> 'c (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*`) (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 'b2type-variable `'b2`
   kind `*` 'xtype-variable `'x`
   kind `*` 'ctype-variable `'c`
   kind `*` 'ytype-variable `'y`
   kind `*`) (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'ctype-variable `'c`
   kind `*`) | 'b2type-variable `'b2`
   kind `*` -> 'btype-variable `'b`
   kind `*` where
  define (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Getter 'a 'b) (Lens 'b2 'x 'c 'y) (Getter 'a 'c) | 'b2  ->  'b`
   type `Getter 'a 'b -> Lens 'b 'x 'c 'y -> Getter 'a 'c`
   executable g1variable `g1`
   type `Getter 'a 'b` g2variable `g2`
   type `Lens 'b 'x 'c 'y` := Getterconstant `Data.Lens.Getter`
   constructor of record-type `Getter`
   type `('a -> 'b) -> Getter 'a 'b`
   type in context `('a -> 'c) -> Getter 'a 'c`
   executable $constant `Prelude.Function.($)`
   constant
   type `('a -> 'b) -> 'a -> 'b`
   type in context `(('a -> 'c) -> Getter 'a 'c) -> ('a -> 'c) -> Getter 'a 'c`
   executable combineGetterconstant `Data.Lens.combineGetter`
   constant
   type `(IsGetter 'g1 'a 'b, IsGetter 'g2 'b 'c) => 'g1 -> 'g2 -> 'a -> 'c`
   type in context `Getter 'a 'b -> Lens 'b 'x 'c 'y -> 'a -> 'c`
   executable g1variable `g1`
   type `Getter 'a 'b` g2variable `g2`
   type `Lens 'b 'x 'c 'y`
  {-# inline (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Getter 'a 'b) (Lens 'b2 'x 'c 'y) (Getter 'a 'c) | 'b2  ->  'b`
   type `Getter 'a 'b -> Lens 'b 'x 'c 'y -> Getter 'a 'c`
   executable #-}
end-instance

instance Dottype-class `Prelude.Function.Dot`
   arguments: ('a :: *) ('b :: *) ('c :: *)
   functional deps: 'a 'b -> 'c (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'xtype-variable `'x`
   kind `*` 'btype-variable `'b`
   kind `*` 'ytype-variable `'y`
   kind `*`) (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'b2type-variable `'b2`
   kind `*` 'ctype-variable `'c`
   kind `*`) (Getterrecord-type `Data.Lens.Getter`
   kind `* -> * -> *`
   executable 'atype-variable `'a`
   kind `*` 'ctype-variable `'c`
   kind `*`) | 'b2type-variable `'b2`
   kind `*` -> 'btype-variable `'b`
   kind `*` where
  define (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Lens 'a 'x 'b 'y) (Getter 'b2 'c) (Getter 'a 'c) | 'b2  ->  'b`
   type `Lens 'a 'x 'b 'y -> Getter 'b 'c -> Getter 'a 'c`
   executable g1variable `g1`
   type `Lens 'a 'x 'b 'y` g2variable `g2`
   type `Getter 'b 'c` := Getterconstant `Data.Lens.Getter`
   constructor of record-type `Getter`
   type `('a -> 'b) -> Getter 'a 'b`
   type in context `('a -> 'c) -> Getter 'a 'c`
   executable $constant `Prelude.Function.($)`
   constant
   type `('a -> 'b) -> 'a -> 'b`
   type in context `(('a -> 'c) -> Getter 'a 'c) -> ('a -> 'c) -> Getter 'a 'c`
   executable combineGetterconstant `Data.Lens.combineGetter`
   constant
   type `(IsGetter 'g1 'a 'b, IsGetter 'g2 'b 'c) => 'g1 -> 'g2 -> 'a -> 'c`
   type in context `Lens 'a 'x 'b 'y -> Getter 'b 'c -> 'a -> 'c`
   executable g1variable `g1`
   type `Lens 'a 'x 'b 'y` g2variable `g2`
   type `Getter 'b 'c`
  {-# inline (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Lens 'a 'x 'b 'y) (Getter 'b2 'c) (Getter 'a 'c) | 'b2  ->  'b`
   type `Lens 'a 'x 'b 'y -> Getter 'b 'c -> Getter 'a 'c`
   executable #-}
end-instance


declare combineSetterconstant `Data.Lens.combineSetter`
   constant
   type `(IsGetter 'g1 's1 'a, IsSetter 'g1 's1 't1 'b, IsSetter 'g2 'a 'b 'a2) => 'g1 -> 'g2 -> 's1 -> 'a2 -> 't1`
   executable :: (IsGettertype-class `Data.Lens.IsGetter`
   arguments: ('v :: *) ('a :: *) ('b :: *)
   functional deps: 'v -> 'a 'b 'g1type-variable `'g1`
   kind `*` 's1type-variable `'s1`
   kind `*` 'atype-variable `'a`
   kind `*`, IsSettertype-class `Data.Lens.IsSetter`
   arguments: ('v :: *) ('s :: *) ('t :: *) ('b :: *)
   functional deps: 'v -> 's 't 'b 'g1type-variable `'g1`
   kind `*` 's1type-variable `'s1`
   kind `*` 't1type-variable `'t1`
   kind `*` 'btype-variable `'b`
   kind `*`, IsSettertype-class `Data.Lens.IsSetter`
   arguments: ('v :: *) ('s :: *) ('t :: *) ('b :: *)
   functional deps: 'v -> 's 't 'b 'g2type-variable `'g2`
   kind `*` 'atype-variable `'a`
   kind `*` 'btype-variable `'b`
   kind `*` 'a2type-variable `'a2`
   kind `*`) => 'g1type-variable `'g1`
   kind `*` -> 'g2type-variable `'g2`
   kind `*` -> 's1type-variable `'s1`
   kind `*` -> 'a2type-variable `'a2`
   kind `*` -> 't1type-variable `'t1`
   kind `*`
define combineSetterconstant `Data.Lens.combineSetter`
   constant
   type `(IsGetter 'g1 's1 'a, IsSetter 'g1 's1 't1 'b, IsSetter 'g2 'a 'b 'a2) => 'g1 -> 'g2 -> 's1 -> 'a2 -> 't1`
   executable g1variable `g1`
   type `'g1` g2variable `g2`
   type `'g2` v1variable `v1`
   type `'s1` x2variable `x2`
   type `'a2` :=
  let val v2variable `v2`
   type `'a` = viewconstant `Data.Lens.view`
   constant of type-class `IsGetter`
   type `'v -> 'a -> 'b`
   type in context `'g1 -> 's1 -> 'a`
   executable
   type-class instance from argument g1variable `g1`
   type `'g1` v1variable `v1`
   type `'s1`
      val v2'variable `v2'`
   type `'b` = setconstant `Data.Lens.set`
   constant of type-class `IsSetter`
   type `'v -> 's -> 'b -> 't`
   type in context `'g2 -> 'a -> 'a2 -> 'b`
   executable
   type-class instance from argument g2variable `g2`
   type `'g2` v2variable `v2`
   type `'a` x2variable `x2`
   type `'a2`
      val v1'variable `v1'`
   type `'t1` = setconstant `Data.Lens.set`
   constant of type-class `IsSetter`
   type `'v -> 's -> 'b -> 't`
   type in context `'g1 -> 's1 -> 'b -> 't1`
   executable
   type-class instance from argument g1variable `g1`
   type `'g1` v1variable `v1`
   type `'s1` v2'variable `v2'`
   type `'b`
  in v1'variable `v1'`
   type `'t1` end
{-# inline combineSetterconstant `Data.Lens.combineSetter`
   constant
   type `(IsGetter 'g1 's1 'a, IsSetter 'g1 's1 't1 'b, IsSetter 'g2 'a 'b 'a2) => 'g1 -> 'g2 -> 's1 -> 'a2 -> 't1`
   executable #-}

instance Dottype-class `Prelude.Function.Dot`
   arguments: ('a :: *) ('b :: *) ('c :: *)
   functional deps: 'a 'b -> 'c (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 's1type-variable `'s1`
   kind `*` 't1type-variable `'t1`
   kind `*` 'a1type-variable `'a1`
   kind `*` 'b1type-variable `'b1`
   kind `*`) (Setterrecord-type `Data.Lens.Setter`
   kind `* -> * -> * -> *`
   executable 's2type-variable `'s2`
   kind `*` 't2type-variable `'t2`
   kind `*` 'b2type-variable `'b2`
   kind `*`) (Setterrecord-type `Data.Lens.Setter`
   kind `* -> * -> * -> *`
   executable 's1type-variable `'s1`
   kind `*` 't1type-variable `'t1`
   kind `*` 'b2type-variable `'b2`
   kind `*`) | 'a1type-variable `'a1`
   kind `*` -> 's2type-variable `'s2`
   kind `*`, 'b1type-variable `'b1`
   kind `*` -> 't2type-variable `'t2`
   kind `*` where
  define (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Lens 's1 't1 'a1 'b1) (Setter 's2 't2 'b2) (Setter 's1 't1 'b2) | 'a1  ->  's2, 'b1  ->  't2`
   type `Lens 's1 't1 's2 't2 -> Setter 's2 't2 'b2 -> Setter 's1 't1 'b2`
   executable g1variable `g1`
   type `Lens 's1 't1 's2 't2` g2variable `g2`
   type `Setter 's2 't2 'b2` := Setterconstant `Data.Lens.Setter`
   constructor of record-type `Setter`
   type `('s -> 'b -> 't) -> Setter 's 't 'b`
   type in context `('s1 -> 'b2 -> 't1) -> Setter 's1 't1 'b2`
   executable $constant `Prelude.Function.($)`
   constant
   type `('a -> 'b) -> 'a -> 'b`
   type in context `(('s1 -> 'b2 -> 't1) -> Setter 's1 't1 'b2) -> ('s1 -> 'b2 -> 't1) -> Setter 's1 't1 'b2`
   executable combineSetterconstant `Data.Lens.combineSetter`
   constant
   type `(IsGetter 'g1 's1 'a, IsSetter 'g1 's1 't1 'b, IsSetter 'g2 'a 'b 'a2) => 'g1 -> 'g2 -> 's1 -> 'a2 -> 't1`
   type in context `Lens 's1 't1 's2 't2 -> Setter 's2 't2 'b2 -> 's1 -> 'b2 -> 't1`
   executable g1variable `g1`
   type `Lens 's1 't1 's2 't2` g2variable `g2`
   type `Setter 's2 't2 'b2`
  {-# inline (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Lens 's1 't1 'a1 'b1) (Setter 's2 't2 'b2) (Setter 's1 't1 'b2) | 'a1  ->  's2, 'b1  ->  't2`
   type `Lens 's1 't1 's2 't2 -> Setter 's2 't2 'b2 -> Setter 's1 't1 'b2`
   executable #-}
end-instance

instance Dottype-class `Prelude.Function.Dot`
   arguments: ('a :: *) ('b :: *) ('c :: *)
   functional deps: 'a 'b -> 'c (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 's1type-variable `'s1`
   kind `*` 't1type-variable `'t1`
   kind `*` 'a1type-variable `'a1`
   kind `*` 'b1type-variable `'b1`
   kind `*`) (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 's2type-variable `'s2`
   kind `*` 't2type-variable `'t2`
   kind `*` 'a2type-variable `'a2`
   kind `*` 'b2type-variable `'b2`
   kind `*`) (Lensrecord-type `Data.Lens.Lens`
   kind `* -> * -> * -> * -> *`
   executable 's1type-variable `'s1`
   kind `*` 't1type-variable `'t1`
   kind `*` 'a2type-variable `'a2`
   kind `*` 'b2type-variable `'b2`
   kind `*`) | 'a1type-variable `'a1`
   kind `*` -> 's2type-variable `'s2`
   kind `*`, 'b1type-variable `'b1`
   kind `*` -> 't2type-variable `'t2`
   kind `*` where
  define (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Lens 's1 't1 'a1 'b1) (Lens 's2 't2 'a2 'b2) (Lens 's1 't1 'a2 'b2) | 'a1  ->  's2, 'b1  ->  't2`
   type `Lens 's1 't1 's2 't2 -> Lens 's2 't2 'a2 'b2 -> Lens 's1 't1 'a2 'b2`
   executable g1variable `g1`
   type `Lens 's1 't1 's2 't2` g2variable `g2`
   type `Lens 's2 't2 'a2 'b2` := Lensconstant `Data.Lens.Lens`
   constructor of record-type `Lens`
   type `('s -> 'a) -> ('s -> 'b -> 't) -> Lens 's 't 'a 'b`
   type in context `('s1 -> 'a2) -> ('s1 -> 'b2 -> 't1) -> Lens 's1 't1 'a2 'b2`
   executable (combineGetterconstant `Data.Lens.combineGetter`
   constant
   type `(IsGetter 'g1 'a 'b, IsGetter 'g2 'b 'c) => 'g1 -> 'g2 -> 'a -> 'c`
   type in context `Lens 's1 't1 's2 't2 -> Lens 's2 't2 'a2 'b2 -> 's1 -> 'a2`
   executable g1variable `g1`
   type `Lens 's1 't1 's2 't2` g2variable `g2`
   type `Lens 's2 't2 'a2 'b2`) (combineSetterconstant `Data.Lens.combineSetter`
   constant
   type `(IsGetter 'g1 's1 'a, IsSetter 'g1 's1 't1 'b, IsSetter 'g2 'a 'b 'a2) => 'g1 -> 'g2 -> 's1 -> 'a2 -> 't1`
   type in context `Lens 's1 't1 's2 't2 -> Lens 's2 't2 'a2 'b2 -> 's1 -> 'b2 -> 't1`
   executable g1variable `g1`
   type `Lens 's1 't1 's2 't2` g2variable `g2`
   type `Lens 's2 't2 'a2 'b2`)
  {-# inline (.)constant `Prelude.Function.(.)`
   constant of type-class instance `Dot (Lens 's1 't1 'a1 'b1) (Lens 's2 't2 'a2 'b2) (Lens 's1 't1 'a2 'b2) | 'a1  ->  's2, 'b1  ->  't2`
   type `Lens 's1 't1 's2 't2 -> Lens 's2 't2 'a2 'b2 -> Lens 's1 't1 'a2 'b2`
   executable #-}
end-instance




-- --------------------------------------
-- Lenses for tuples
-- --------------------------------------

-- Tuples with distinct number of elements are different types in ADATT. Nevertheless
-- using the same syntax for accessing elements is useful. For this purpose type-classes
-- for accessing the i-th element of any tuple with at least i elements are introduced
-- and instantiated using code-generation


template BuildTupleElemLensClass (m :: Nat) := '''
class Elem{{=mtemplate-variable `m`
   type Nat=}} \'s \'t \'a \'b | \'s -> \'a, \'s \'b -> \'t where
  declare elem{{=mtemplate-variable `m`
   type Nat=}} :: Lens \'s \'t \'a \'b
end-class
'''

template BuildTupleElemLenses (n :: Nat) := '''
{{ name-scope {
     var tyVarstemplate-variable `tyVars`
   type [String] := !GetTypeVarsNumberedtemplate `Prelude.Template.GetTypeVarsNumbered`
   argument-types: (String, Nat)
   return-type: [String]
   does not compute text("a", ntemplate-variable `n`
   type Nat);
     var xstemplate-variable `xs`
   type [String] := generateNames("x", ntemplate-variable `n`
   type Nat);
   }
}}
{{% for var mtemplate-variable `m`
   type Nat := 1 to ntemplate-variable `n`
   type Nat %}}
{{ var xs'template-variable `xs'`
   type [String] := xstemplate-variable `xs`
   type [String]; xs'template-variable `xs'`
   type [String][mtemplate-variable `m`
   type Nat-1] := "_";
   var xs''template-variable `xs''`
   type [String] := xstemplate-variable `xs`
   type [String]; xs''template-variable `xs''`
   type [String][mtemplate-variable `m`
   type Nat-1] := "y";
   var tyVars'template-variable `tyVars'`
   type [String] := tyVarstemplate-variable `tyVars`
   type [String]; tyVars'template-variable `tyVars'`
   type [String][mtemplate-variable `m`
   type Nat-1] := "'y"; }}
instance Elem{{=mtemplate-variable `m`
   type Nat=}} {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
   argument-type: [String]
   return-type: String
   does not compute text(tyVarstemplate-variable `tyVars`
   type [String]) =}} \'x \'z \'y | \'x -> {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
   argument-type: [String]
   return-type: String
   does not compute text(tyVars'template-variable `tyVars'`
   type [String]) =}}, \'z -> {{= tyVarstemplate-variable `tyVars`
   type [String][mtemplate-variable `m`
   type Nat-1] =}} where
  define elem{{=mtemplate-variable `m`
   type Nat=}} := Lens #{{= mtemplate-variable `m`
   type Nat =}} (fn {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
   argument-type: [String]
   return-type: String
   does not compute text(xs'template-variable `xs'`
   type [String]) =}} y -> {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
   argument-type: [String]
   return-type: String
   does not compute text(xs''template-variable `xs''`
   type [String]) =}})
  \{-# inline elem{{=mtemplate-variable `m`
   type Nat=}} #-\}
end-instance

{{% end-for %}}
'''

generate-codegenerated code:

class Elem1 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem1 :: Lens 's 't 'a 'b
end-class

class Elem2 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem2 :: Lens 's 't 'a 'b
end-class

class Elem3 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem3 :: Lens 's 't 'a 'b
end-class

class Elem4 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem4 :: Lens 's 't 'a 'b
end-class

class Elem5 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem5 :: Lens 's 't 'a 'b
end-class

class Elem6 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem6 :: Lens 's 't 'a 'b
end-class

class Elem7 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem7 :: Lens 's 't 'a 'b
end-class

class Elem8 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem8 :: Lens 's 't 'a 'b
end-class

class Elem9 's 't 'a 'b | 's -> 'a, 's 'b -> 't where
  declare elem9 :: Lens 's 't 'a 'b
end-class

instance Elem1 ('a1, 'a2) 'x 'z 'y | 'x -> ('y, 'a2), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2) y -> (y, x2))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2) 'x 'z 'y | 'x -> ('a1, 'y), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _) y -> (x1, y))
  {-# inline elem2 #-}
end-instance

instance Elem1 ('a1, 'a2, 'a3) 'x 'z 'y | 'x -> ('y, 'a2, 'a3), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2, x3) y -> (y, x2, x3))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2, 'a3) 'x 'z 'y | 'x -> ('a1, 'y, 'a3), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _, x3) y -> (x1, y, x3))
  {-# inline elem2 #-}
end-instance

instance Elem3 ('a1, 'a2, 'a3) 'x 'z 'y | 'x -> ('a1, 'a2, 'y), 'z -> 'a3 where
  define elem3 := Lens #3 (fn (x1, x2, _) y -> (x1, x2, y))
  {-# inline elem3 #-}
end-instance

instance Elem1 ('a1, 'a2, 'a3, 'a4) 'x 'z 'y | 'x -> ('y, 'a2, 'a3, 'a4), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2, x3, x4) y -> (y, x2, x3, x4))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2, 'a3, 'a4) 'x 'z 'y | 'x -> ('a1, 'y, 'a3, 'a4), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _, x3, x4) y -> (x1, y, x3, x4))
  {-# inline elem2 #-}
end-instance

instance Elem3 ('a1, 'a2, 'a3, 'a4) 'x 'z 'y | 'x -> ('a1, 'a2, 'y, 'a4), 'z -> 'a3 where
  define elem3 := Lens #3 (fn (x1, x2, _, x4) y -> (x1, x2, y, x4))
  {-# inline elem3 #-}
end-instance

instance Elem4 ('a1, 'a2, 'a3, 'a4) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'y), 'z -> 'a4 where
  define elem4 := Lens #4 (fn (x1, x2, x3, _) y -> (x1, x2, x3, y))
  {-# inline elem4 #-}
end-instance

instance Elem1 ('a1, 'a2, 'a3, 'a4, 'a5) 'x 'z 'y | 'x -> ('y, 'a2, 'a3, 'a4, 'a5), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2, x3, x4, x5) y -> (y, x2, x3, x4, x5))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2, 'a3, 'a4, 'a5) 'x 'z 'y | 'x -> ('a1, 'y, 'a3, 'a4, 'a5), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _, x3, x4, x5) y -> (x1, y, x3, x4, x5))
  {-# inline elem2 #-}
end-instance

instance Elem3 ('a1, 'a2, 'a3, 'a4, 'a5) 'x 'z 'y | 'x -> ('a1, 'a2, 'y, 'a4, 'a5), 'z -> 'a3 where
  define elem3 := Lens #3 (fn (x1, x2, _, x4, x5) y -> (x1, x2, y, x4, x5))
  {-# inline elem3 #-}
end-instance

instance Elem4 ('a1, 'a2, 'a3, 'a4, 'a5) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'y, 'a5), 'z -> 'a4 where
  define elem4 := Lens #4 (fn (x1, x2, x3, _, x5) y -> (x1, x2, x3, y, x5))
  {-# inline elem4 #-}
end-instance

instance Elem5 ('a1, 'a2, 'a3, 'a4, 'a5) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'y), 'z -> 'a5 where
  define elem5 := Lens #5 (fn (x1, x2, x3, x4, _) y -> (x1, x2, x3, x4, y))
  {-# inline elem5 #-}
end-instance

instance Elem1 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) 'x 'z 'y | 'x -> ('y, 'a2, 'a3, 'a4, 'a5, 'a6), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2, x3, x4, x5, x6) y -> (y, x2, x3, x4, x5, x6))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) 'x 'z 'y | 'x -> ('a1, 'y, 'a3, 'a4, 'a5, 'a6), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _, x3, x4, x5, x6) y -> (x1, y, x3, x4, x5, x6))
  {-# inline elem2 #-}
end-instance

instance Elem3 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) 'x 'z 'y | 'x -> ('a1, 'a2, 'y, 'a4, 'a5, 'a6), 'z -> 'a3 where
  define elem3 := Lens #3 (fn (x1, x2, _, x4, x5, x6) y -> (x1, x2, y, x4, x5, x6))
  {-# inline elem3 #-}
end-instance

instance Elem4 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'y, 'a5, 'a6), 'z -> 'a4 where
  define elem4 := Lens #4 (fn (x1, x2, x3, _, x5, x6) y -> (x1, x2, x3, y, x5, x6))
  {-# inline elem4 #-}
end-instance

instance Elem5 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'y, 'a6), 'z -> 'a5 where
  define elem5 := Lens #5 (fn (x1, x2, x3, x4, _, x6) y -> (x1, x2, x3, x4, y, x6))
  {-# inline elem5 #-}
end-instance

instance Elem6 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'y), 'z -> 'a6 where
  define elem6 := Lens #6 (fn (x1, x2, x3, x4, x5, _) y -> (x1, x2, x3, x4, x5, y))
  {-# inline elem6 #-}
end-instance

instance Elem1 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) 'x 'z 'y | 'x -> ('y, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2, x3, x4, x5, x6, x7) y -> (y, x2, x3, x4, x5, x6, x7))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) 'x 'z 'y | 'x -> ('a1, 'y, 'a3, 'a4, 'a5, 'a6, 'a7), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _, x3, x4, x5, x6, x7) y -> (x1, y, x3, x4, x5, x6, x7))
  {-# inline elem2 #-}
end-instance

instance Elem3 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) 'x 'z 'y | 'x -> ('a1, 'a2, 'y, 'a4, 'a5, 'a6, 'a7), 'z -> 'a3 where
  define elem3 := Lens #3 (fn (x1, x2, _, x4, x5, x6, x7) y -> (x1, x2, y, x4, x5, x6, x7))
  {-# inline elem3 #-}
end-instance

instance Elem4 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'y, 'a5, 'a6, 'a7), 'z -> 'a4 where
  define elem4 := Lens #4 (fn (x1, x2, x3, _, x5, x6, x7) y -> (x1, x2, x3, y, x5, x6, x7))
  {-# inline elem4 #-}
end-instance

instance Elem5 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'y, 'a6, 'a7), 'z -> 'a5 where
  define elem5 := Lens #5 (fn (x1, x2, x3, x4, _, x6, x7) y -> (x1, x2, x3, x4, y, x6, x7))
  {-# inline elem5 #-}
end-instance

instance Elem6 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'y, 'a7), 'z -> 'a6 where
  define elem6 := Lens #6 (fn (x1, x2, x3, x4, x5, _, x7) y -> (x1, x2, x3, x4, x5, y, x7))
  {-# inline elem6 #-}
end-instance

instance Elem7 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'y), 'z -> 'a7 where
  define elem7 := Lens #7 (fn (x1, x2, x3, x4, x5, x6, _) y -> (x1, x2, x3, x4, x5, x6, y))
  {-# inline elem7 #-}
end-instance

instance Elem1 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('y, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2, x3, x4, x5, x6, x7, x8) y -> (y, x2, x3, x4, x5, x6, x7, x8))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('a1, 'y, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _, x3, x4, x5, x6, x7, x8) y -> (x1, y, x3, x4, x5, x6, x7, x8))
  {-# inline elem2 #-}
end-instance

instance Elem3 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('a1, 'a2, 'y, 'a4, 'a5, 'a6, 'a7, 'a8), 'z -> 'a3 where
  define elem3 := Lens #3 (fn (x1, x2, _, x4, x5, x6, x7, x8) y -> (x1, x2, y, x4, x5, x6, x7, x8))
  {-# inline elem3 #-}
end-instance

instance Elem4 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'y, 'a5, 'a6, 'a7, 'a8), 'z -> 'a4 where
  define elem4 := Lens #4 (fn (x1, x2, x3, _, x5, x6, x7, x8) y -> (x1, x2, x3, y, x5, x6, x7, x8))
  {-# inline elem4 #-}
end-instance

instance Elem5 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'y, 'a6, 'a7, 'a8), 'z -> 'a5 where
  define elem5 := Lens #5 (fn (x1, x2, x3, x4, _, x6, x7, x8) y -> (x1, x2, x3, x4, y, x6, x7, x8))
  {-# inline elem5 #-}
end-instance

instance Elem6 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'y, 'a7, 'a8), 'z -> 'a6 where
  define elem6 := Lens #6 (fn (x1, x2, x3, x4, x5, _, x7, x8) y -> (x1, x2, x3, x4, x5, y, x7, x8))
  {-# inline elem6 #-}
end-instance

instance Elem7 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'y, 'a8), 'z -> 'a7 where
  define elem7 := Lens #7 (fn (x1, x2, x3, x4, x5, x6, _, x8) y -> (x1, x2, x3, x4, x5, x6, y, x8))
  {-# inline elem7 #-}
end-instance

instance Elem8 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'y), 'z -> 'a8 where
  define elem8 := Lens #8 (fn (x1, x2, x3, x4, x5, x6, x7, _) y -> (x1, x2, x3, x4, x5, x6, x7, y))
  {-# inline elem8 #-}
end-instance

instance Elem1 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('y, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9), 'z -> 'a1 where
  define elem1 := Lens #1 (fn (_, x2, x3, x4, x5, x6, x7, x8, x9) y -> (y, x2, x3, x4, x5, x6, x7, x8, x9))
  {-# inline elem1 #-}
end-instance

instance Elem2 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'y, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9), 'z -> 'a2 where
  define elem2 := Lens #2 (fn (x1, _, x3, x4, x5, x6, x7, x8, x9) y -> (x1, y, x3, x4, x5, x6, x7, x8, x9))
  {-# inline elem2 #-}
end-instance

instance Elem3 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'a2, 'y, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9), 'z -> 'a3 where
  define elem3 := Lens #3 (fn (x1, x2, _, x4, x5, x6, x7, x8, x9) y -> (x1, x2, y, x4, x5, x6, x7, x8, x9))
  {-# inline elem3 #-}
end-instance

instance Elem4 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'y, 'a5, 'a6, 'a7, 'a8, 'a9), 'z -> 'a4 where
  define elem4 := Lens #4 (fn (x1, x2, x3, _, x5, x6, x7, x8, x9) y -> (x1, x2, x3, y, x5, x6, x7, x8, x9))
  {-# inline elem4 #-}
end-instance

instance Elem5 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'y, 'a6, 'a7, 'a8, 'a9), 'z -> 'a5 where
  define elem5 := Lens #5 (fn (x1, x2, x3, x4, _, x6, x7, x8, x9) y -> (x1, x2, x3, x4, y, x6, x7, x8, x9))
  {-# inline elem5 #-}
end-instance

instance Elem6 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'y, 'a7, 'a8, 'a9), 'z -> 'a6 where
  define elem6 := Lens #6 (fn (x1, x2, x3, x4, x5, _, x7, x8, x9) y -> (x1, x2, x3, x4, x5, y, x7, x8, x9))
  {-# inline elem6 #-}
end-instance

instance Elem7 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'y, 'a8, 'a9), 'z -> 'a7 where
  define elem7 := Lens #7 (fn (x1, x2, x3, x4, x5, x6, _, x8, x9) y -> (x1, x2, x3, x4, x5, x6, y, x8, x9))
  {-# inline elem7 #-}
end-instance

instance Elem8 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'y, 'a9), 'z -> 'a8 where
  define elem8 := Lens #8 (fn (x1, x2, x3, x4, x5, x6, x7, _, x9) y -> (x1, x2, x3, x4, x5, x6, x7, y, x9))
  {-# inline elem8 #-}
end-instance

instance Elem9 ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'a9) 'x 'z 'y | 'x -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8, 'y), 'z -> 'a9 where
  define elem9 := Lens #9 (fn (x1, x2, x3, x4, x5, x6, x7, x8, _) y -> (x1, x2, x3, x4, x5, x6, x7, x8, y))
  {-# inline elem9 #-}
end-instance

 '''
  {{ -- max number of tuple elements for which to generate classes and instances
     var maxtemplate-variable `max`
   type Nat := 9  }}
  {{% for var mtemplate-variable `m`
   type Nat := 1 to maxtemplate-variable `max`
   type Nat %}}
  {{! BuildTupleElemLensClasstemplate `Data.Lens.BuildTupleElemLensClass`
   argument-type: Nat
   return-type: -(mtemplate-variable `m`
   type Nat) !}}

  {{% end-for %}}
  {{% for var mtemplate-variable `m`
   type Nat := 2 to maxtemplate-variable `max`
   type Nat %}}
  {{! BuildTupleElemLensestemplate `Data.Lens.BuildTupleElemLenses`
   argument-type: Nat
   return-type: -(mtemplate-variable `m`
   type Nat) !}}
  {{% end-for %}}
'''


-- --------------------------------------
-- Lenses for tuples
-- --------------------------------------

-- It is useful to have lenses corresponding to record fields.
-- There are templates to automatically generate such lenses.

-- - BuildRecordFieldLens (field, lensName)
-- generate a lens with name "lensName" for the record field field

-- - BuildRecordFieldLensesSuffix (suffix, type)
-- generate lenses for all fields of record-type "type", whose name ends with given suffix. The lens name is the field-name without the suffix.

-- - BuildRecordFieldLensesPrefix (prefix, type)
-- generate lenses for all fields of record-type "type", whose name starts with given prefix. The lens name is the field-name without the prefix.

-- - BuildRecordFieldLenses (type)
-- short for "BuildRecordFieldLensesSuffix("_", type)


template BuildRecordFieldLens (field :: ConstID, lensName :: String ) := '''
{{ var tyIDtemplate-variable `tyID`
   type TypeID := fieldtemplate-variable `field`
   type ConstID.baseType;
   var (_, tyWithArgstemplate-variable `tyWithArgs`
   type String) := !TypeWithArgstemplate `Prelude.Template.TypeWithArgs`
   argument-types: (Bool, TypeID)
   return-types: ([String], String)
   does not compute text(True, tyIDtemplate-variable `tyID`
   type TypeID);
   var fstemplate-variable `fs`
   type [ConstID] := tyIDtemplate-variable `tyID`
   type TypeID.fields;
}}
declare {{= lensNametemplate-variable `lensName`
   type String =}} :: Lens {{= tyWithArgstemplate-variable `tyWithArgs`
   type String =}} _ _ _
define {{= lensNametemplate-variable `lensName`
   type String =}} := <|
    {{= const lensGetconstant `Data.Lens.lensGet`
   field of record-type `Lens`
   type `Lens 's 't 'a 'b -> 's -> 'a`
   executable =}} := {{= fieldtemplate-variable `field`
   type ConstID =}},
    {{= const lensSetconstant `Data.Lens.lensSet`
   field of record-type `Lens`
   type `Lens 's 't 'a 'b -> 's -> 'b -> 't`
   executable =}} := fn r v -> <|
        {{% foreach var fitemplate-variable `fi`
   type Nat in fstemplate-variable `fs`
   type [ConstID].indices %}}
        {{= fstemplate-variable `fs`
   type [ConstID][fitemplate-variable `fi`
   type Nat] =}} := {{% if (fstemplate-variable `fs`
   type [ConstID][fitemplate-variable `fi`
   type Nat] == fieldtemplate-variable `field`
   type ConstID) %}}v{{% else %}}{{=fstemplate-variable `fs`
   type [ConstID][fitemplate-variable `fi`
   type Nat]=}} r{{% end-if %}}{{% if (fitemplate-variable `fi`
   type Nat+1 < fstemplate-variable `fs`
   type [ConstID].length) %}},{{% end-if %}}
        {{% end-foreach %}}
      |>
  |>
'''


template BuildRecordFieldLensesSuffix (suffix :: String, tyID :: TypeID) := '''
{{% foreach var ftemplate-variable `f`
   type ConstID in tyIDtemplate-variable `tyID`
   type TypeID.fields %}}
{{% if (endsWith(suffixtemplate-variable `suffix`
   type String, ftemplate-variable `f`
   type ConstID.name)) %}}
{{! BuildRecordFieldLenstemplate `Data.Lens.BuildRecordFieldLens`
   argument-types: (ConstID, String)
   return-type: -(ftemplate-variable `f`
   type ConstID, dropEnd(suffixtemplate-variable `suffix`
   type String.length, ftemplate-variable `f`
   type ConstID.name)) !}}

{{% end-if %}}
{{% end-foreach %}}'''

template BuildRecordFieldLensesPrefix (pre :: String, tyID :: TypeID) := '''
{{% foreach var ftemplate-variable `f`
   type ConstID in tyIDtemplate-variable `tyID`
   type TypeID.fields %}}
{{% if (startsWith(pretemplate-variable `pre`
   type String, ftemplate-variable `f`
   type ConstID.name)) %}}
{{! BuildRecordFieldLenstemplate `Data.Lens.BuildRecordFieldLens`
   argument-types: (ConstID, String)
   return-type: -(ftemplate-variable `f`
   type ConstID, drop(pretemplate-variable `pre`
   type String.length, ftemplate-variable `f`
   type ConstID.name)) !}}

{{% end-if %}}
{{% end-foreach %}}'''

template BuildRecordFieldLenses (tyID :: TypeID) := '''{{! BuildRecordFieldLensesSuffixtemplate `Data.Lens.BuildRecordFieldLensesSuffix`
   argument-types: (String, TypeID)
   return-type: -("_", tyIDtemplate-variable `tyID`
   type TypeID) !}}'''

end-moduleend of module Data.Lens