
  0 | module Control.Lens.Cons
  1 | 
  2 | import Data.Profunctor
  3 | import Control.Lens.Optic
  4 | import Control.Lens.Iso
  5 | import Control.Lens.Prism
  6 | import Control.Lens.Review
  7 | import Control.Lens.Optional
  8 | 
  9 | %default total
 10 | 
 11 | 
 12 | ||| An interface that provides a way to detach and inspect elements from the
 13 | ||| left side of a sequence.
 14 | public export
 15 | interface Cons s t a b | s where
 16 |   ||| An isomorphism that can inspect the left side of a sequence.
 17 |   consIso : Iso s t (Maybe (a, s)) (Maybe (b, t))
 18 | 
 19 |   ||| A prism that can attach or detach a value from the left side of a
 20 |   ||| sequence.
 21 |   cons_ : Prism s t (a, s) (b, t)
 22 |   cons_ = consIso . prism Just (\case
 23 |     Nothing => Left Nothing
 24 |     Just x => Right x)
 25 | 
 26 | ||| Access the head (left-most element) of a sequence, if it is non-empty.
 27 | public export
 28 | head_ : Cons s s a a => Optional' s a
 29 | head_ @{_} @{MkIsOptional _} = cons_ . first
 30 | 
 31 | ||| Access the tail (all but the left-most element) of a sequence, if it is
 32 | ||| non-empty.
 33 | public export
 34 | tail_ : Cons s s a a => Optional' s s
 35 | tail_ @{_} @{MkIsOptional _} = cons_ . second
 36 | 
 37 | ||| Use a `Cons` implementation to construct an empty sequence.
 38 | public export
 39 | nil : Cons s s a a => s
 40 | nil = review consIso Nothing
 41 | 
 42 | 
 43 | ||| An interface that provides a way to detach and inspect elements from the
 44 | ||| right side of a sequence.
 45 | public export
 46 | interface Snoc s t a b | s where
 47 |   ||| An isomorphism that can inspect the right side of a sequence.
 48 |   snocIso : Iso s t (Maybe (s, a)) (Maybe (t, b))
 49 | 
 50 |   ||| This is a prism that can attach or detach a value from the right side of a
 51 |   ||| sequence.
 52 |   snoc_ : Prism s t (s, a) (t, b)
 53 |   snoc_ = snocIso . prism Just (\case
 54 |     Nothing => Left Nothing
 55 |     Just x => Right x)
 56 | 
 57 | ||| Access all but the right-most element of a sequence, if it is non-empty.
 58 | public export
 59 | init_ : Snoc s s a a => Optional' s s
 60 | init_ @{_} @{MkIsOptional _} = snoc_ . first
 61 | 
 62 | ||| Access the last (right-most) element of a sequence, if it is non-empty.
 63 | public export
 64 | last_ : Snoc s s a a => Optional' s a
 65 | last_ @{_} @{MkIsOptional _} = snoc_ . second
 66 | 
 67 | ||| Use a `Snoc` implementation to construct an empty sequence.
 68 | public export
 69 | lin : Snoc s s a a => s
 70 | lin = review snocIso Nothing
 71 |