
   0 | module Internal.String
   1 | 
   2 | import Data.List
   3 | import Data.List1
   4 | import Data.Maybe
   5 | import Data.String
   6 | import Data.String.Extra
   7 | 
   8 | %default total
   9 | 
  10 | namespace List
  11 |   private
  12 |   partial
  13 |   range : Nat -> List Nat
  14 |   range n =
  15 |     reverse (drop 1 (iterate next n))
  16 |       where
  17 |         next : Nat -> Maybe Nat
  18 |         next (S k) = Just k
  19 |         next Z = Nothing
  20 |   
  21 |   private
  22 |   partial
  23 |   zipWithIndex : List a -> List (a, Nat)
  24 |   zipWithIndex l =
  25 |     zip l (range (length l))
  26 |   
  27 |   export
  28 |   partial
  29 |   findAll : Eq a => List a -> List a -> List Nat
  30 |   findAll l k =
  31 |     reverse (findAllHelper l k 0 [])
  32 |     where
  33 |       findAllHelper : List a -> List a -> Nat -> List Nat -> List Nat
  34 |       findAllHelper l k index acc =
  35 |         case l of
  36 |           [] =>
  37 |             acc
  38 |           _ =>
  39 |             let
  40 |               nextAcc =
  41 |                 if isPrefixOf k l then
  42 |                   (index :: acc)
  43 |                 else
  44 |                   acc
  45 |             in
  46 |               findAllHelper (drop 1 l) k (index + 1) nextAcc
  47 |   
  48 |   export
  49 |   partial
  50 |   replace : Eq a => List a -> List a -> List a -> List a
  51 |   replace l k v =
  52 |     let
  53 |       matches = findAll l k
  54 |       repl = reverse v
  55 |       skipLen = case length k of
  56 |         Z =>
  57 |           0 -- This is really impossible but we haven't refined our types to say so
  58 |         (S Z) =>
  59 |           0
  60 |         (S k) =>
  61 |           k
  62 |     in
  63 |       reverse $ fst $ foldl (\(acc, skip), (c, i) =>
  64 |         case skip of
  65 |           Just (S k) =>
  66 |             (acc, Just k)
  67 |           _ =>
  68 |             if isJust (find (== i) matches) then
  69 |               -- We need to insert a replacement and then skip N els
  70 |               (repl ++ acc, Just skipLen)
  71 |             else
  72 |               (c :: acc, Nothing)
  73 |       ) ([], (the (Maybe Nat) Nothing)) (zipWithIndex l)
  74 | 
  75 | private
  76 | wrap : String -> String -> String
  77 | wrap sym str =
  78 |   sym ++ str ++ sym
  79 | 
  80 | private
  81 | listOp : (List Char -> List Char) -> String -> String
  82 | listOp op =
  83 |   pack . op . unpack
  84 | 
  85 | export
  86 | partial
  87 | findAll : String -> String -> List Nat
  88 | findAll str lookup =
  89 |   List.findAll (unpack str) (unpack lookup)
  90 | 
  91 | export
  92 | partial
  93 | replace : String -> String -> String -> String
  94 | replace k v str =
  95 |   pack (List.replace (unpack str) (unpack k) (unpack v))
  96 | 
  97 | export
  98 | filter : (Char -> Bool) -> String -> String
  99 | filter test =
 100 |   pack . filter test . unpack
 101 | 
 102 | export
 103 | showList : (a -> String) -> List a -> String
 104 | showList f els =
 105 |   "[" ++ (join "," (map f els)) ++ "]"
 106 | 
 107 | export
 108 | split : Char -> String -> List String
 109 | split c =
 110 |   ( map pack ) . Prelude.toList . (Data.List.split (== c)) . unpack
 111 | 
 112 | export
 113 | partial
 114 | quote : String -> String
 115 | quote =
 116 |   (wrap "\"")
 117 |   . (replace "\n" "\\n")
 118 |   . (replace "\"" "\\\"")
 119 |