0 | module Control.Lens.Review
 1 |
 2 | import Data.Profunctor
 3 | import Data.Profunctor.Costrong
 4 | import Control.Lens.Optic
 5 | import Control.Lens.Prism
 6 | import Control.Lens.Getter
 7 |
 8 | %default total
 9 |
10 |
11 | ------------------------------------------------------------------------------
12 | -- Type definitions
13 | ------------------------------------------------------------------------------
14 |
15 |
16 | public export
17 | record IsReview p where
18 |   constructor MkIsReview
19 |   runIsReview : (Bifunctor p, Costrong p, Choice p)
20 |
21 | export %hint
22 | reviewToPrism : IsReview p => IsPrism p
23 | reviewToPrism @{MkIsReview _} = MkIsPrism %search
24 |
25 |
26 | ||| A review is an optic whose only capability is being flipped into a `Getter`
27 | ||| in the other direction.
28 | |||
29 | ||| Any `Prism` or `Iso` can be used as a review.
30 | public export
31 | 0 Review : (s,a : Type) -> Type
32 | Review = Simple (Optic IsReview)
33 |
34 |
35 | ------------------------------------------------------------------------------
36 | -- Utilities for Reviews
37 | ------------------------------------------------------------------------------
38 |
39 |
40 | lphantom : (Bifunctor p, Profunctor p) => p b c -> p a c
41 | lphantom = mapFst absurd . lmap {a=Void} absurd
42 |
43 | ||| Construct a review from an injection function.
44 | ||| Analogous to `to` for getters.
45 | public export
46 | unto : (a -> s) -> Review s a
47 | unto f @{MkIsReview _} = lphantom . rmap f
48 |
49 | ||| Flip a `Getter` to form a `Review`.
50 | public export
51 | un : Getter s a -> Review a s
52 | un = unto . view
53 |
54 |
55 | ||| Turn an optic around to inject a focus value into the larger data structure
56 | ||| after applying a function to it.
57 | ||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
58 | public export
59 | reviews : Review s a -> (e -> a) -> (e -> s)
60 | reviews l = runCoforget . l . MkCoforget
61 |
62 | ||| Turn an optic around to inject a focus value into the larger data structure.
63 | ||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
64 | public export
65 | review : Review s a -> a -> s
66 | review l = reviews l id
67 |
68 | export infixr 8 ^$
69 |
70 | ||| Turn an optic around to inject a focus value into the larger data structure.
71 | ||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
72 | |||
73 | ||| This is the operator form of `review`.
74 | public export
75 | (^$) : Review s a -> a -> s
76 | (^$) = review
77 |
78 | ||| Flip a `Prism`, `Iso` or `Review` to form a `Getter` in the other direction.
79 | public export
80 | re : Review s a -> Getter a s
81 | re = to . review
82 |