0 | ||| A small library introducing string positions
  1 | ||| This can be used as an alternative to unpacking a string into a list of
  2 | ||| characters
  3 | module Data.String.Position
  4 |
  5 | import Data.String
  6 |
  7 | %default total
  8 |
  9 | ||| @ValidPosition points to an existing character into
 10 | ||| @str  its parameter string
 11 | ||| Do NOT publicly export so that users cannot manufacture arbitrary positions
 12 | export
 13 | record ValidPosition (str : String) where
 14 |   constructor MkValidPosition
 15 |   ||| @currentIndex is the valid position into str
 16 |   currentIndex    : Int
 17 |   ||| @parameterLength is the length of the parameter str
 18 |   parameterLength : Int
 19 | -- TODO: add invariants?
 20 | --  0 isLength : length str === parameterLength
 21 | --  0 isIndex  : (0 `LTE` currentIndex, 0 `LT` parameterLength)
 22 |
 23 | ||| A position is either a ValidPosition or the end of the string
 24 | public export
 25 | Position : String -> Type
 26 | Position str = Maybe (ValidPosition str)
 27 |
 28 | ||| Manufacture a position by checking it is strictly inside the string
 29 | export
 30 | mkPosition : (str : String) -> Int -> Position str
 31 | mkPosition str idx
 32 |   = do let len : Int = cast (length str)
 33 |        guard (0 <= idx && idx < len)
 34 |        pure (MkValidPosition idx len)
 35 |
 36 | ||| Move a position (note that we do not need access to the string here)
 37 | export
 38 | mvPosition : ValidPosition str -> Int -> Position str
 39 | mvPosition (MkValidPosition pos len) idx
 40 |   = do guard (0 <= idx && idx < len)
 41 |        pure (MkValidPosition idx len)
 42 |
 43 | ||| Find the initial position inside the input string
 44 | export
 45 | init : (str : String) -> Position str
 46 | init str = mkPosition str 0
 47 |
 48 | ||| Move from a valid position to the next position in the string
 49 | export
 50 | next : ValidPosition str -> Position str
 51 | next (MkValidPosition pos len)
 52 |   = do let idx = pos + 1
 53 |        guard (idx < len)
 54 |        pure (MkValidPosition idx len)
 55 |
 56 | ||| We can safely access the character at a valid position
 57 | export
 58 | index : {str : _} -> ValidPosition str -> Char
 59 | index pos = assert_total (strIndex str pos.currentIndex)
 60 |
 61 | ||| We can successfully uncons the substring starting at a `ValidPosition`.
 62 | ||| Note that we can use `map uncons pos` to uncons the substring starting
 63 | ||| a `Position`.
 64 | export
 65 | uncons : {str : _} -> ValidPosition str -> (Char, Position str)
 66 | uncons pos = (index pos, next pos)
 67 |
 68 | ||| @span keeps munching characters of the substring starting at a given
 69 | ||| position as long as the predicate is true of them. It returns the position
 70 | ||| after the last successful munch.
 71 | ||| Using `subString` to recover the string selected by `span` should yield
 72 | ||| the same result as Data.String's `span`. That is to say we should have:
 73 | ||| ```
 74 | ||| subString pos (Position.span p pos) = String.span p (subString pos Nothing)
 75 | ||| ```
 76 | export
 77 | span : {str : _} -> (Char -> Bool) -> Position str -> Position str
 78 | span p pos = do (c, str) <- map uncons pos
 79 |                 if p c then assert_total (span p str) else pos
 80 |
 81 | ||| @count computes the length of the substring one would obtain if one were
 82 | ||| to filter out characters based on the predicate passed as an argument.
 83 | ||| It replaces the `length (filter p (fastUnpack str))` pattern.
 84 | export
 85 | count : {str : _} -> (Char -> Bool) -> Position str -> Nat
 86 | count p Nothing = 0
 87 | count p (Just pos) =
 88 |   if p (index pos)
 89 |     then S (assert_total (count p (next pos)))
 90 |     else assert_total (count p (next pos))
 91 |
 92 | ||| Distance between a starting position and an end one.
 93 | ||| We assume that the end position is *after* the starting one, otherwise the
 94 | ||| output may be negative.
 95 | export
 96 | distance : (start : Position str) ->
 97 |            (end : Position str) -> Int
 98 | distance Nothing _ = 0
 99 | distance (Just pos) pos' =
100 |   let start = pos.currentIndex
101 |       end = maybe pos.parameterLength currentIndex pos'
102 |   in end - start
103 |
104 | ||| the substring of length `distance start end` that is contained between
105 | ||| start (inclusive) and end (exclusive).
106 | export
107 | subString : {str : _} ->
108 |             (start : Position str) ->
109 |             (end : Position str) -> String
110 | subString Nothing pos' = ""
111 | subString (Just pos) pos' =
112 |   let start = pos.currentIndex
113 |       end = maybe pos.parameterLength currentIndex pos'
114 |   in assert_total (strSubstr start (end - start) str)
115 |