
   0 | module Monocle.Compose
   1 | 
   2 | import Monocle.Fold
   3 | import Monocle.Getter
   4 | import Monocle.Iso
   5 | import Monocle.Lens
   6 | import Monocle.Optional
   7 | import Monocle.Prism
   8 | import Monocle.Setter
   9 | import Monocle.Traversal
  10 | 
  11 | %default total
  12 | 
  13 | ||| Interface for the sequencing of different types of optics.
  14 | |||
  15 | ||| The kind of optic we get as a result is determined by the kinds of optics
  16 | ||| we sequence. For instance, sequencing a Lens with a Prism results in
  17 | ||| an Optional, while sequencing with an Iso does preserve an optic's type.
  18 | public export
  19 | interface OSeq (0 k,l,m : Type -> Type -> Type -> Type -> Type) | k,l where
  20 |   seq : k s t a b -> l a b c d -> m s t c d
  21 | 
  22 | export infixl 0 .>
  23 | 
  24 | public export %inline
  25 | (.>) : {0 k,l,m : _} -> k s t a b -> l a b c d -> OSeq k l m => m s t c d
  26 | f .> g = seq f g
  27 | 
  28 | public export %inline
  29 | OSeq Iso Iso Iso where seq = (~>)
  30 | 
  31 | public export %inline
  32 | OSeq Iso Lens Lens where seq x y = toLens x ~> y
  33 | 
  34 | public export %inline
  35 | OSeq Iso Prism Prism where seq x y = toPrism x ~> y
  36 | 
  37 | public export %inline
  38 | OSeq Iso Optional Optional where seq x y = toOptional x ~> y
  39 | 
  40 | public export %inline
  41 | OSeq Iso Traversal Traversal where seq x y = toTraversal x ~> y
  42 | 
  43 | public export %inline
  44 | OSeq Iso Getter Getter where seq x y = toGetter x ~> y
  45 | 
  46 | public export %inline
  47 | OSeq Iso Setter Setter where seq x y = toSetter x ~> y
  48 | 
  49 | public export %inline
  50 | OSeq Iso Fold Fold where seq x y = toFold x ~> y
  51 | 
  52 | public export %inline
  53 | OSeq Lens Lens Lens where seq = (~>)
  54 | 
  55 | public export %inline
  56 | OSeq Lens Iso Lens where seq x y = x ~> toLens y
  57 | 
  58 | public export %inline
  59 | OSeq Lens Prism Optional where seq x y = toOptional x ~> toOptional y
  60 | 
  61 | public export %inline
  62 | OSeq Lens Optional Optional where seq x y = toOptional x ~> y
  63 | 
  64 | public export %inline
  65 | OSeq Lens Traversal Traversal where seq x y = toTraversal x ~> y
  66 | 
  67 | public export %inline
  68 | OSeq Lens Getter Getter where seq x y = toGetter x ~> y
  69 | 
  70 | public export %inline
  71 | OSeq Lens Setter Setter where seq x y = toSetter x ~> y
  72 | 
  73 | public export %inline
  74 | OSeq Lens Fold Fold where seq x y = toFold x ~> y
  75 | 
  76 | public export %inline
  77 | OSeq Prism Prism Prism where seq = (~>)
  78 | 
  79 | public export %inline
  80 | OSeq Prism Iso Prism where seq x y = x ~> toPrism y
  81 | 
  82 | public export %inline
  83 | OSeq Prism Lens Optional where seq x y = toOptional x ~> toOptional y
  84 | 
  85 | public export %inline
  86 | OSeq Prism Optional Optional where seq x y = toOptional x ~> y
  87 | 
  88 | public export %inline
  89 | OSeq Prism Traversal Traversal where seq x y = toTraversal x ~> y
  90 | 
  91 | public export %inline
  92 | OSeq Prism Getter Fold where seq x y = toFold x ~> toFold y
  93 | 
  94 | public export %inline
  95 | OSeq Prism Setter Setter where seq x y = toSetter x ~> y
  96 | 
  97 | public export %inline
  98 | OSeq Prism Fold Fold where seq x y = toFold x ~> y
  99 | 
 100 | public export %inline
 101 | OSeq Optional Optional Optional where seq = (~>)
 102 | 
 103 | public export %inline
 104 | OSeq Optional Iso Optional where seq x y = x ~> toOptional y
 105 | 
 106 | public export %inline
 107 | OSeq Optional Lens Optional where seq x y = x ~> toOptional y
 108 | 
 109 | public export %inline
 110 | OSeq Optional Prism Optional where seq x y = x ~> toOptional y
 111 | 
 112 | public export %inline
 113 | OSeq Optional Traversal Traversal where seq x y = toTraversal x ~> y
 114 | 
 115 | public export %inline
 116 | OSeq Optional Getter Fold where seq x y = toFold x ~> toFold y
 117 | 
 118 | public export %inline
 119 | OSeq Optional Setter Setter where seq x y = toSetter x ~> y
 120 | 
 121 | public export %inline
 122 | OSeq Optional Fold Fold where seq x y = toFold x ~> y
 123 | 
 124 | public export %inline
 125 | OSeq Traversal Traversal Traversal where seq = (~>)
 126 | 
 127 | public export %inline
 128 | OSeq Traversal Iso Traversal where seq x y = x ~> toTraversal y
 129 | 
 130 | public export %inline
 131 | OSeq Traversal Lens Traversal where seq x y = x ~> toTraversal y
 132 | 
 133 | public export %inline
 134 | OSeq Traversal Prism Traversal where seq x y = x ~> toTraversal y
 135 | 
 136 | public export %inline
 137 | OSeq Traversal Optional Traversal where seq x y = x ~> toTraversal y
 138 | 
 139 | public export %inline
 140 | OSeq Traversal Getter Fold where seq x y = toFold x ~> toFold y
 141 | 
 142 | public export %inline
 143 | OSeq Traversal Setter Setter where seq x y = toSetter x ~> y
 144 | 
 145 | public export %inline
 146 | OSeq Traversal Fold Fold where seq x y = toFold x ~> y
 147 | 
 148 | public export %inline
 149 | OSeq Setter Setter Setter where seq = (~>)
 150 | 
 151 | public export %inline
 152 | OSeq Setter Iso Setter where seq x y = x ~> toSetter y
 153 | 
 154 | public export %inline
 155 | OSeq Setter Lens Setter where seq x y = x ~> toSetter y
 156 | 
 157 | public export %inline
 158 | OSeq Setter Prism Setter where seq x y = x ~> toSetter y
 159 | 
 160 | public export %inline
 161 | OSeq Setter Optional Setter where seq x y = x ~> toSetter y
 162 | 
 163 | public export %inline
 164 | OSeq Setter Traversal Setter where seq x y = x ~> toSetter y
 165 | 
 166 | public export %inline
 167 | OSeq Getter Getter Getter where seq = (~>)
 168 | 
 169 | public export %inline
 170 | OSeq Getter Iso Getter where seq x y = x ~> toGetter y
 171 | 
 172 | public export %inline
 173 | OSeq Getter Lens Getter where seq x y = x ~> toGetter y
 174 | 
 175 | public export %inline
 176 | OSeq Getter Prism Fold where seq x y = toFold x ~> toFold y
 177 | 
 178 | public export %inline
 179 | OSeq Getter Optional Fold where seq x y = toFold x ~> toFold y
 180 | 
 181 | public export %inline
 182 | OSeq Getter Traversal Fold where seq x y = toFold x ~> toFold y
 183 | 
 184 | public export %inline
 185 | OSeq Getter Fold Fold where seq x y = toFold x ~> y
 186 | 
 187 | public export %inline
 188 | OSeq Fold Fold Fold where seq = (~>)
 189 | 
 190 | public export %inline
 191 | OSeq Fold Iso Fold where seq x y = x ~> toFold y
 192 | 
 193 | public export %inline
 194 | OSeq Fold Lens Fold where seq x y = x ~> toFold y
 195 | 
 196 | public export %inline
 197 | OSeq Fold Prism Fold where seq x y = x ~> toFold y
 198 | 
 199 | public export %inline
 200 | OSeq Fold Optional Fold where seq x y = x ~> toFold y
 201 | 
 202 | public export %inline
 203 | OSeq Fold Traversal Fold where seq x y = x ~> toFold y
 204 | 
 205 | public export %inline
 206 | OSeq Fold Getter Fold where seq x y = x ~> toFold y
 207 | 
 208 | export
 209 | atO : Eq k => k -> Optional' (List (k,v)) v
 210 | atO key = eqFirst key fst .> snd
 211 |