
  0 | module Data.String.Lens
  1 | 
  2 | import Data.String
  3 | import public Control.Lens
  4 | import Data.List.Lens
  5 | 
  6 | %default total
  7 | 
  8 | 
  9 | ||| An isomorphism between a string and a list of characters.
 10 | |||
 11 | ||| ```idris
 12 | ||| unpacked = from packed
 13 | ||| ```
 14 | public export
 15 | unpacked : Iso' String (List Char)
 16 | unpacked = iso unpack pack
 17 | 
 18 | ||| An isomorphism between a list of characters and a string.
 19 | |||
 20 | ||| ```idris
 21 | ||| packed = from unpacked
 22 | ||| ```
 23 | public export
 24 | packed : Iso' (List Char) String
 25 | packed = iso pack unpack
 26 | 
 27 | ||| An isomorphism between a string and its reverse.
 28 | public export
 29 | reversed : Iso' String String
 30 | reversed = involuted reverse
 31 | 
 32 | 
 33 | public export
 34 | Ixed Nat Char String where
 35 |   ix k = unpacked . ix k
 36 | 
 37 | public export
 38 | Cons String String Char Char where
 39 |   consIso = iso strUncons (maybe "" $ uncurry strCons)
 40 |   cons_ = prism' (uncurry strCons) strUncons
 41 | 
 42 | snoc : String -> Char -> String
 43 | snoc s c = s ++ singleton c
 44 | 
 45 | unsnoc : String -> Maybe (String, Char)
 46 | unsnoc s =
 47 |   case length s of
 48 |     Z => Nothing
 49 |     (S n) => Just (substr Z n s,
 50 |                     assert_total $ strIndex s (cast n))
 51 | 
 52 | public export
 53 | Snoc String String Char Char where
 54 |   snocIso = iso unsnoc (maybe "" $ uncurry snoc)
 55 |   snoc_ = prism' (uncurry snoc) unsnoc
 56 | 
 57 | public export
 58 | Each String String Char Char where
 59 |   each = unpacked . traversed
 60 | 
 61 | public export
 62 | Num i => IEach i String String Char Char where
 63 |   ieach = unpacked . itraversed
 64 |