0 | module Control.Lens.Prism
  1 |
  2 | import Data.Profunctor
  3 | import Control.Lens.Optic
  4 | import Control.Lens.Indexed
  5 | import Control.Lens.Iso
  6 |
  7 | %default total
  8 |
  9 |
 10 | ------------------------------------------------------------------------------
 11 | -- Type definitions
 12 | ------------------------------------------------------------------------------
 13 |
 14 |
 15 | public export
 16 | record IsPrism p where
 17 |   constructor MkIsPrism
 18 |   runIsPrism : Choice p
 19 |
 20 | export %hint
 21 | prismToIso : IsPrism p => IsIso p
 22 | prismToIso @{MkIsPrism _} = MkIsIso %search
 23 |
 24 | export %hint
 25 | indexedPrism : IsPrism p => IsPrism (Indexed i p)
 26 | indexedPrism @{MkIsPrism _} = MkIsPrism %search
 27 |
 28 |
 29 | ||| A prism is a first-class reference to one of the cases of a sum type.
 30 | ||| Prisms allow one to determine whether a value matches the focused case
 31 | ||| and extract the corresponding data if it does.
 32 | |||
 33 | ||| More precisely, a `Prism` is an `Optional` that can be flipped to obtain
 34 | ||| a `Getter` in the opposite direction.
 35 | public export
 36 | 0 Prism : (s,t,a,b : Type) -> Type
 37 | Prism = Optic IsPrism
 38 |
 39 | ||| `Prism'` is the `Simple` version of `Prism`.
 40 | public export
 41 | 0 Prism' : (s,a : Type) -> Type
 42 | Prism' = Simple Prism
 43 |
 44 | public export
 45 | 0 IndexedPrism : (i,s,t,a,b : Type) -> Type
 46 | IndexedPrism = IndexedOptic IsPrism
 47 |
 48 | public export
 49 | 0 IndexedPrism' : (i,s,a : Type) -> Type
 50 | IndexedPrism' = Simple . IndexedPrism
 51 |
 52 |
 53 | ------------------------------------------------------------------------------
 54 | -- Utilities for prisms
 55 | ------------------------------------------------------------------------------
 56 |
 57 |
 58 | ||| Construct a prism from injection and projection functions.
 59 | public export
 60 | prism : (b -> t) -> (s -> Either t a) -> Prism s t a b
 61 | prism inj prj @{MkIsPrism _} = dimap prj (either id inj) . right
 62 |
 63 | ||| Construct a simple prism from injection and projection functions.
 64 | public export
 65 | prism' : (b -> s) -> (s -> Maybe a) -> Prism s s a b
 66 | prism' inj prj = prism inj (\x => maybe (Left x) Right (prj x))
 67 |
 68 | public export
 69 | iprism : (b -> t) -> (s -> Either t (i, a)) -> IndexedPrism i s t a b
 70 | iprism inj prj @{_} @{ind} = prism inj prj . indexed @{ind}
 71 |
 72 | public export
 73 | iprism' : (b -> s) -> (s -> Maybe (i, a)) -> IndexedPrism i s s a b
 74 | iprism' inj prj = iprism inj (\x => maybe (Left x) Right (prj x))
 75 |
 76 |
 77 | ||| Extract injection and projection functions from a prism.
 78 | public export
 79 | getPrism : Prism s t a b -> (b -> t, s -> Either t a)
 80 | getPrism l = l @{MkIsPrism choice} (id, Right)
 81 |   where
 82 |     Profunctor (\x,y => (b -> y, x -> Either y a)) where
 83 |       dimap f g (inj, prj) = (g . inj, either (Left . g) Right . prj . f)
 84 |
 85 |     [choice] GenStrong Either (\x,y => (b -> y, x -> Either y a)) where
 86 |       strongl (inj, prj) = (Left . inj, either (either (Left . Left) Right . prj) (Left . Right))
 87 |       strongr (inj, prj) = (Right . inj, either (Left . Left) (either (Left . Right) Right . prj))
 88 |
 89 | ||| Extract injection and projection functions from a prism.
 90 | public export
 91 | withPrism : Prism s t a b -> ((b -> t) -> (s -> Either t a) -> r) -> r
 92 | withPrism l f = uncurry f (getPrism l)
 93 |
 94 |
 95 | ||| Construct a prism that uses a predicate to determine if a value matches.
 96 | public export
 97 | nearly : a -> (a -> Bool) -> Prism' a ()
 98 | nearly x p = prism' (const x) (guard . p)
 99 |
100 | ||| Construct a prism that matches only one value.
101 | public export
102 | only : Eq a => a -> Prism' a ()
103 | only x = nearly x (x ==)
104 |
105 |
106 | ||| Create a prism that operates on `Either` values from two other prisms.
107 | |||
108 | ||| This can be seen as dual to `alongside`.
109 | public export
110 | without : Prism s t a b -> Prism s' t' a' b' -> Prism (Either s s') (Either t t') (Either a a') (Either b b')
111 | without l l' =
112 |   let (inj1, prj1) = getPrism l
113 |       (inj2, prj2) = getPrism l'
114 |   in prism (bimap inj1 inj2) (either (bimap Left Left . prj1) (bimap Right Right . prj2))
115 |
116 | ||| Lift a prism through a `Traversable` container.
117 | |||
118 | ||| The constructed prism will only match if all of the inner elements of the
119 | ||| `Traversable` container match.
120 | public export
121 | below : Traversable f => Prism' s a -> Prism' (f s) (f a)
122 | below l = withPrism l $ \inj,prj =>
123 |   prism (map inj) $ \s => mapFst (const s) (traverse prj s)
124 |
125 | ||| Lift a prism through part of a product type.
126 | public export
127 | aside : Prism s t a b -> Prism (e, s) (e, t) (e, a) (e, b)
128 | aside l = withPrism l $ \inj,prj => prism (map inj) $ \(e,s) => bimap (e,) (e,) (prj s)
129 |