0 | module Control.Lens.Setter
  1 |
  2 | import Data.Contravariant
  3 | import Data.Profunctor
  4 | import Data.Profunctor.Costrong
  5 | import Data.Profunctor.Traversing
  6 | import Data.Profunctor.Mapping
  7 | import Control.Monad.State
  8 | import Control.Lens.Optic
  9 | import Control.Lens.Indexed
 10 | import Control.Lens.Traversal
 11 |
 12 | %default total
 13 |
 14 |
 15 | ------------------------------------------------------------------------------
 16 | -- Type definitions
 17 | ------------------------------------------------------------------------------
 18 |
 19 |
 20 | public export
 21 | record IsSetter p where
 22 |   constructor MkIsSetter
 23 |   runIsSetter : Mapping p
 24 |
 25 | export %hint
 26 | setterToTraversal : IsSetter p => IsTraversal p
 27 | setterToTraversal @{MkIsSetter _} = MkIsTraversal %search
 28 |
 29 | export %hint
 30 | indexedSetter : IsSetter p => IsSetter (Indexed i p)
 31 | indexedSetter @{MkIsSetter _} = MkIsSetter %search
 32 |
 33 |
 34 |
 35 | ||| A setter is an optic that only supports setting, not getting.
 36 | |||
 37 | ||| More specifically, a setter can modify zero or more focus elements. This
 38 | ||| means that all traversals are setters.
 39 | |||
 40 | ||| Setters can be thought of as a generalization of the `Functor` interface,
 41 | ||| allowing one to map over the contents of a structure.
 42 | public export
 43 | 0 Setter : (s,t,a,b : Type) -> Type
 44 | Setter = Optic IsSetter
 45 |
 46 | ||| `Setter'` is the `Simple` version of `Setter`.
 47 | public export
 48 | 0 Setter' : (s,a : Type) -> Type
 49 | Setter' = Simple Setter
 50 |
 51 | ||| An indexed setter allows access to an index while setting.
 52 | public export
 53 | 0 IndexedSetter : (i,s,t,a,b : Type) -> Type
 54 | IndexedSetter = IndexedOptic IsSetter
 55 |
 56 | ||| `IndexedSetter'` is the `Simple` version of `IndexedSetter`.
 57 | public export
 58 | 0 IndexedSetter' : (i,s,a : Type) -> Type
 59 | IndexedSetter' = Simple . IndexedSetter
 60 |
 61 |
 62 | ------------------------------------------------------------------------------
 63 | -- Utilities for setters
 64 | ------------------------------------------------------------------------------
 65 |
 66 |
 67 | ||| Construct a setter from a modifying function.
 68 | public export
 69 | sets : ((a -> b) -> s -> t) -> Setter s t a b
 70 | sets f @{MkIsSetter _} = roam f
 71 |
 72 | ||| Construct an indexed setter from a modifying function.
 73 | public export
 74 | isets : ((i -> a -> b) -> s -> t) -> IndexedSetter i s t a b
 75 | isets f @{MkIsSetter _} @{ind} = roam (f . curry) . indexed @{ind}
 76 |
 77 | ||| Derive a setter from a `Functor` implementation.
 78 | public export
 79 | mapped : Functor f => Setter (f a) (f b) a b
 80 | mapped @{_} @{MkIsSetter _} = map'
 81 |
 82 | ||| Derive a setter from a `Contravariant` implementation.
 83 | public export
 84 | contramapped : Contravariant f => Setter (f a) (f b) b a
 85 | contramapped = sets contramap
 86 |
 87 |
 88 | ||| Modify the focus or focuses of an optic.
 89 | public export
 90 | over : Setter s t a b -> (a -> b) -> s -> t
 91 | over l = l @{MkIsSetter Function}
 92 |
 93 | export infixr 4 %~, %@~, .~, .@~
 94 |
 95 | ||| Modify the focus or focuses of an optic.
 96 | |||
 97 | ||| This is the operator form of `over`.
 98 | public export
 99 | (%~) : Setter s t a b -> (a -> b) -> s -> t
100 | (%~) = over
101 |
102 |
103 | ||| Modify the focus or focuses of an indexed optic, having access to the index.
104 | public export
105 | iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
106 | iover l = l @{MkIsSetter Function} @{Idxed} . uncurry
107 |
108 | ||| Modify the focus or focuses of an indexed optic, having access to the index.
109 | |||
110 | ||| This is the operator form of `iover`.
111 | public export
112 | (%@~) : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
113 | (%@~) = iover
114 |
115 |
116 | ||| Set the focus or focuses of an optic to a constant value.
117 | public export
118 | set : Setter s t a b -> b -> s -> t
119 | set l = over l . const
120 |
121 | ||| Set the focus or focuses of an optic to a constant value.
122 | |||
123 | ||| This is the operator form of `set`.
124 | public export
125 | (.~) : Setter s t a b -> b -> s -> t
126 | (.~) = set
127 |
128 |
129 | ||| Set the focus or focuses of an indexed optic, having access to the index.
130 | public export
131 | iset : IndexedSetter i s t a b -> (i -> b) -> s -> t
132 | iset l = iover l . (const .)
133 |
134 | ||| Set the focus or focuses of an indexed optic, having access to the index.
135 | |||
136 | ||| This is the operator form of `iset`.
137 | public export
138 | (.@~) : IndexedSetter i s t a b -> (i -> b) -> s -> t
139 | (.@~) = iset
140 |
141 |
142 | ------------------------------------------------------------------------------
143 | -- More operators
144 | ------------------------------------------------------------------------------
145 |
146 | export infixr 4 ?~, <.~, <?~, +~, *~, -~, /~, ||~, &&~, <+>~
147 | export infix 4 %=, %@=, .=, .@=, ?=, <.=, <?=, +=, *=, -=, //=, ||=, &&=, <+>=
148 | export infix 1 <~, <<~
149 |
150 | ||| Set the focus of an optic to `Just` a value.
151 | public export
152 | (?~) : Setter s t a (Maybe b) -> b -> s -> t
153 | (?~) l = set l . Just
154 |
155 | ||| Set a value with pass-through.
156 | public export
157 | (<.~) : Setter s t a b -> b -> s -> (b, t)
158 | (<.~) l x = (x,) . set l x
159 |
160 | ||| Set `Just` a value with pass-through.
161 | public export
162 | (<?~) : Setter s t a (Maybe b) -> b -> s -> (b, t)
163 | (<?~) l x = (x,) . (?~) l x
164 |
165 |
166 | ||| Add a constant value to the focus of an optic.
167 | public export
168 | (+~) : Num a => Setter s t a a -> a -> s -> t
169 | (+~) l = over l . (+)
170 |
171 | ||| Multiply the focus of an optic by a constant value.
172 | public export
173 | (*~) : Num a => Setter s t a a -> a -> s -> t
174 | (*~) l = over l . (*)
175 |
176 | ||| Subtract a constant value from the focus of an optic.
177 | public export
178 | (-~) : Neg a => Setter s t a a -> a -> s -> t
179 | (-~) l = over l . flip (-)
180 |
181 | ||| Divide the focus of an optic by a constant value.
182 | public export
183 | (/~) : Fractional a => Setter s t a a -> a -> s -> t
184 | (/~) l = over l . flip (/)
185 |
186 | ||| Logically OR the focus of an optic with a constant value.
187 | |||
188 | ||| Like `(||)`, this operator takes a lazy second argument.
189 | public export
190 | (||~) : Setter s t Bool Bool -> Lazy Bool -> s -> t
191 | (||~) l = over l . flip (||)
192 |
193 | ||| Logically AND the focus of an optic with a constant value.
194 | |||
195 | ||| Like `(&&)`, this operator takes a lazy second argument.
196 | public export
197 | (&&~) : Setter s t Bool Bool -> Lazy Bool -> s -> t
198 | (&&~) l = over l . flip (&&)
199 |
200 | ||| Modify the focus of an optic using the semigroup/monoid operator.
201 | |||
202 | ||| The constant value is applied to the focus from the right:
203 | ||| ```idris
204 | ||| l <+>~ x = over l (<+> x)
205 | ||| ```
206 | public export
207 | (<+>~) : Semigroup a => Setter s t a a -> a -> s -> t
208 | (<+>~) l = over l . flip (<+>)
209 |
210 |
211 | ||| Modify the focus of an optic within a state monad.
212 | public export
213 | (%=) : MonadState s m => Setter s s a b -> (a -> b) -> m ()
214 | (%=) = modify .: over
215 |
216 | ||| Modify the focus of an optic within a state monad, having access to the index.
217 | public export
218 | (%@=) : MonadState s m => IndexedSetter i s s a b -> (i -> a -> b) -> m ()
219 | (%@=) = modify .: iover
220 |
221 | ||| Set the focus of an optic within a state monad.
222 | public export
223 | (.=) : MonadState s m => Setter s s a b -> b -> m ()
224 | (.=) = modify .: set
225 |
226 | ||| Set the focus of an optic within a state monad, having access to the index.
227 | public export
228 | (.@=) : MonadState s m => IndexedSetter i s s a b -> (i -> b) -> m ()
229 | (.@=) = modify .: iset
230 |
231 | ||| Set the focus of an optic within a state monad to `Just` a value.
232 | public export
233 | (?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m ()
234 | (?=) = modify .: (?~)
235 |
236 | ||| Set within a state monad with pass-through.
237 | public export
238 | (<.=) : MonadState s m => Setter s s a b -> b -> m b
239 | (<.=) l x = (l .= x) $> x
240 |
241 | ||| Set to `Just` a value within a state monad with pass-through.
242 | public export
243 | (<?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m b
244 | (<?=) l x = (l ?= x) $> x
245 |
246 | ||| Add a constant value to the focus of an optic within a state monad.
247 | public export
248 | (+=) : Num a => MonadState s m => Setter' s a -> a -> m ()
249 | (+=) = modify .: (+~)
250 |
251 | ||| Multiply the focus of an optic into state by a constant value.
252 | public export
253 | (*=) : Num a => MonadState s m => Setter' s a -> a -> m ()
254 | (*=) = modify .: (*~)
255 |
256 | ||| Subtract a constant value from the focus of an optic within a state monad.
257 | public export
258 | (-=) : Neg a => MonadState s m => Setter' s a -> a -> m ()
259 | (-=) = modify .: (-~)
260 |
261 | ||| Divide the focus of an optic into state by a constant value.
262 | public export
263 | (//=) : Fractional a => MonadState s m => Setter' s a -> a -> m ()
264 | (//=) = modify .: (/~)
265 |
266 | ||| Logically OR the focus of an optic into state with a constant value.
267 | |||
268 | ||| Like `(||)`, this operator takes a lazy second argument.
269 | public export
270 | (||=) : MonadState s m => Setter' s Bool -> Lazy Bool -> m ()
271 | (||=) = modify .: (||~)
272 |
273 | ||| Logically AND the focus of an optic into state with a constant value.
274 | |||
275 | ||| Like `(&&)`, this operator takes a lazy second argument.
276 | public export
277 | (&&=) : MonadState s m => Setter' s Bool -> Lazy Bool -> m ()
278 | (&&=) = modify .: (&&~)
279 |
280 | ||| Modify the focus of an optic into state using the semigroup/monoid operator.
281 | |||
282 | ||| The constant value is applied to the focus from the right.
283 | public export
284 | (<+>=) : Semigroup a => MonadState s m => Setter' s a -> a -> m ()
285 | (<+>=) = modify .: (<+>~)
286 |
287 |
288 | ||| Run a monadic action and set the focus of an optic in state to the result.
289 | |||
290 | ||| This can be thought of as a variation on the do-notation pseudo-operator (<-),
291 | ||| storing the result of a computation within state instead of in a local
292 | ||| variable.
293 | public export
294 | (<~) : MonadState s m => Setter s s a b -> m b -> m ()
295 | (<~) l m = l .= !m
296 |
297 | ||| Run a monadic action and set the focus of an optic in state to the result.
298 | ||| This is different from `(<~)` in that it also passes though the output of
299 | ||| the action.
300 | public export
301 | (<<~) : MonadState s m => Setter s s a b -> m b -> m b
302 | (<<~) l m = l <.= !m
303 |