
   0 | module Text.Bounds
   1 | 
   2 | import Data.Array.Core
   3 | import Data.Array.Mutable
   4 | import Data.Bits
   5 | import Data.ByteString
   6 | import Derive.Prelude
   7 | 
   8 | %default total
   9 | 
  10 | %language ElabReflection
  11 | 
  12 | --------------------------------------------------------------------------------
  13 | --          Position
  14 | --------------------------------------------------------------------------------
  15 | 
  16 | ||| Position in a string as a pair of natural numbers.
  17 | ||| Both numbers are zero-based.
  18 | public export
  19 | record Position where
  20 |   [noHints]
  21 |   constructor P
  22 |   ||| The current line in a string (0-based)
  23 |   line : Nat
  24 |   ||| The current column in a string (0-based)
  25 |   col  : Nat
  26 | 
  27 | %runElab derive "Position" [Show,Eq,Ord]
  28 | 
  29 | public export
  30 | Interpolation Position where
  31 |   interpolate (P l c) = show (l+1) ++ ":" ++ show (c+1)
  32 | 
  33 | ||| Appends the second position to the first.
  34 | |||
  35 | ||| If the second is on a single line, the column is added.
  36 | ||| Otherwise, the line is added and the column of the second
  37 | ||| is used.
  38 | export
  39 | Semigroup Position where
  40 |   P l1 c1 <+> P 0  c2 = P l1 (c1+c2)
  41 |   P l1 c1 <+> P l2 c2 = P (l1+l2) c2
  42 | 
  43 | export
  44 | Monoid Position where
  45 |   neutral = P 0 0
  46 | 
  47 | ||| The beginning of a string. This is an alias for `P 0 0`.
  48 | public export
  49 | begin : Position
  50 | begin = P 0 0
  51 | 
  52 | ||| Increase the current column by one.
  53 | public export %inline
  54 | incCol : Position -> Position
  55 | incCol = {col $= S}
  56 | 
  57 | ||| Increase the current line by one, resetting the
  58 | ||| column to 0.
  59 | public export %inline
  60 | incLine : Position -> Position
  61 | incLine p = P (S p.line) 0
  62 | 
  63 | ||| Increase the current column by the given number of steps.
  64 | public export %inline
  65 | addCol : Nat -> Position -> Position
  66 | addCol n = {col $= (+ n)}
  67 | 
  68 | ||| Computes `p2` relative to `p1`, that is, given an earlier
  69 | ||| position `p1`, returns the number of lines and columns
  70 | ||| necessary to advance from `p1` to `p2`.
  71 | export
  72 | relativeTo : (p2,p1 : Position) -> Position
  73 | relativeTo (P l c) (P ls cs) =
  74 |   if l <= ls then P 0 (c `minus` cs) else P (l `minus` ls) c
  75 | 
  76 | ||| Advances the given text position by the characters encountered
  77 | ||| in the given string.
  78 | |||
  79 | ||| A line feed character ('\n'; codepoint `0x0A`) will increase
  80 | ||| the current line by one and reset the column to zero. Every
  81 | ||| other character will increase the column by one.
  82 | export
  83 | incString : String -> Position -> Position
  84 | incString s (P l c) = go l c (unpack s)
  85 |   where
  86 |     go : Nat -> Nat -> List Char -> Position
  87 |     go l c []        = P l c
  88 |     go l c ('\n' :: xs) = go (S l) 0 xs
  89 |     go l c (x    :: xs) = go l (S c) xs
  90 | 
  91 | %inline
  92 | isStartByte : Bits8 -> Bool
  93 | isStartByte b = (b .&. 128) == 0 || (b .&. 0b1100_0000) == 0b1100_0000
  94 | 
  95 | ||| Advances the given text position by one byte in a UTF-8 string.
  96 | |||
  97 | ||| A line feed character (byte '0x0a') increases the line by one and
  98 | ||| resets the column to zero. The first byte of any other UTF-8 character
  99 | ||| increases the column by one. Any other UTF-8 byte leaves the
 100 | ||| position unchanged.
 101 | export
 102 | incByte : Bits8 -> Position -> Position
 103 | incByte 0x0a p = incLine p
 104 | incByte b    p = if isStartByte b then incCol p else p
 105 | 
 106 | ||| Advances the given text position by the bytes encountered
 107 | ||| in the given string.
 108 | |||
 109 | ||| A line feed byte (`0x0A`) will increase
 110 | ||| the current line by one and reset the column to zero. Every
 111 | ||| other start character of a unicode code point will advance
 112 | ||| the column by one.
 113 | export
 114 | incBytes : ByteString -> Position -> Position
 115 | incBytes (BS n bv) (P l c) = go l c n
 116 |   where
 117 |     go : Nat -> Nat -> (k : Nat) -> (x : Ix k n) => Position
 118 |     go l c 0     = P l c
 119 |     go l c (S k) =
 120 |       case bv `ix` k of
 121 |         0x0a => go (S l) 0 k
 122 |         b    => case isStartByte b of
 123 |           True => go l (S c) k
 124 |           _    => go l c k
 125 | 
 126 | parameters (bv : ByteVect n)
 127 |            (m  : MArray s (S n) Position)
 128 | 
 129 |   skip : (k : Nat) -> (ix : Ix k n) => Position -> F1' s
 130 | 
 131 |   fillMap : (k : Nat) -> (ix : Ix k n) => Position -> F1' s
 132 |   fillMap 0     p t = () # t
 133 |   fillMap (S k) p t =
 134 |    let _ # t := setIx m _ {x = succIx ix}  p t
 135 |     in case ByteVect.ix bv k of
 136 |          0x0a => fillMap k (incLine p) t
 137 |          b    => case b < 128 of
 138 |            True  => fillMap k (incCol p) t
 139 |            False => skip k p t
 140 | 
 141 |   skip 0     p t = () # t
 142 |   skip (S k) p t =
 143 |    let _ # t := setIx m _ {x = succIx ix} p t
 144 |     in if isStartByte (ByteVect.ix bv k)
 145 |           then fillMap (S k) (incCol p) t
 146 |           else skip k p t
 147 | 
 148 | setLast : {n : _} -> MArray s (S n) Position -> F1' s
 149 | setLast {n = 0} m t = () # t
 150 | setLast {n = S k} m t =
 151 |  let p # t := Array.Core.get m (weaken last) t
 152 |   in Array.Core.set m last (incCol p) t
 153 | 
 154 | ||| From a byte vector, generates an array that maps each
 155 | ||| byte index to the corresponding text position (line and column),
 156 | ||| starting from the given start position.
 157 | |||
 158 | ||| The line number is increased after a line feed (`'\n'`) character.
 159 | export
 160 | positionMapFrom :
 161 |      {n : _}
 162 |   -> Position
 163 |   -> ByteVect n
 164 |   -> IArray (S n) Position
 165 | positionMapFrom p bv =
 166 |   run1 $ \t =>
 167 |    let m # t := marray1 (S n) p t
 168 |        _ # t := fillMap bv m n p t
 169 |        _ # t := setLast m t
 170 |     in unsafeFreeze m t
 171 | 
 172 | ||| From a byte vector, generates an array that maps each
 173 | ||| byte index to the corresponding text position (line and column).
 174 | |||
 175 | ||| The line number is increased after a line feed (`'\n'`) character.
 176 | export %inline
 177 | positionMap : {n : _} -> ByteVect n -> IArray (S n) Position
 178 | positionMap = positionMapFrom (P 0 0)
 179 | 
 180 | ||| Adjusts the current position by one character.
 181 | |||
 182 | ||| If the character is a line break, a new line will be strated and
 183 | ||| the column set to zero, otherwise, the column is increase by one.
 184 | public export %inline
 185 | next : Char -> Position -> Position
 186 | next '\n' = incLine
 187 | next _    = incCol
 188 | 
 189 | --------------------------------------------------------------------------------
 190 | --          Bounds
 191 | --------------------------------------------------------------------------------
 192 | 
 193 | ||| A pair of `Position`s, describing a text range, or `NoBounds` for
 194 | ||| use - for instance - with programmatically created tokens.
 195 | public export
 196 | data Bounds : Type where
 197 |   BS : (start, end : Position) -> Bounds
 198 |   NoBounds : Bounds
 199 | 
 200 | %runElab derive "Bounds" [Show,Eq]
 201 | 
 202 | namespace Bounds
 203 |   export
 204 |   relativeTo : Bounds -> Position -> Bounds
 205 |   relativeTo NoBounds _ = NoBounds
 206 |   relativeTo (BS s e) p = BS (s `relativeTo` p) (e `relativeTo` p)
 207 | 
 208 |   ||| Convert a single `Position` to a range one character wide.
 209 |   public export %inline
 210 |   oneChar : Position -> Bounds
 211 |   oneChar p = BS p $ incCol p
 212 | 
 213 | export
 214 | Interpolation Bounds where
 215 |   interpolate (BS s e) = if s == e then "\{s}" else "\{s}--\{e}"
 216 |   interpolate NoBounds = ""
 217 | 
 218 | public export
 219 | Semigroup Bounds where
 220 |   NoBounds <+> y        = y
 221 |   x        <+> NoBounds = x
 222 |   BS s1 e1 <+> BS s2 e2 = BS (min s1 s2) (max e1 e2)
 223 | 
 224 | public export
 225 | Monoid Bounds where
 226 |   neutral = NoBounds
 227 | 
 228 | --------------------------------------------------------------------------------
 229 | --          Bounded
 230 | --------------------------------------------------------------------------------
 231 | 
 232 | ||| Pairs a value with the textual bounds from where it was parsed.
 233 | public export
 234 | record Bounded ty where
 235 |   constructor B
 236 |   val    : ty
 237 |   bounds : Bounds
 238 | 
 239 | %runElab derive "Bounded" [Show,Eq]
 240 | 
 241 | ||| Smart costructor for `Bounded`.
 242 | public export
 243 | bounded : a -> (start,end : Position) -> Bounded a
 244 | bounded v s e = B v $ BS s e
 245 | 
 246 | ||| Smart costructor for `Bounded`.
 247 | public export %inline
 248 | oneChar : a -> Position -> Bounded a
 249 | oneChar v p = B v $ oneChar p
 250 | 
 251 | ||| Implementation of `(<*>)`
 252 | public export
 253 | app : Bounded (a -> b) -> Bounded a -> Bounded b
 254 | app (B vf b1) (B va b2) = B (vf va) (b1 <+> b2)
 255 | 
 256 | ||| Implementation of `(>>=)`
 257 | public export
 258 | bind : Bounded a -> (a -> Bounded b) -> Bounded b
 259 | bind (B va b1) f =
 260 |   let B vb b2 = f va
 261 |    in B vb (b1 <+> b2)
 262 | 
 263 | export
 264 | fromPosition : Bounded a -> Position -> Bounded a
 265 | fromPosition (B v $ BS s e) y = B v $ BS (y <+> s) (y <+> e)
 266 | fromPosition (B v NoBounds) y = B v $ BS y (incCol y)
 267 | 
 268 | public export
 269 | Functor Bounded where
 270 |   map f (B val bs) = B (f val) bs
 271 | 
 272 | public export %inline
 273 | Applicative Bounded where
 274 |   pure v = B v neutral
 275 |   (<*>) = app
 276 | 
 277 | public export %inline
 278 | Monad Bounded where
 279 |   (>>=) = bind
 280 | 
 281 | public export
 282 | Foldable Bounded where
 283 |   foldr c n b = c b.val n
 284 |   foldl c n b = c n b.val
 285 |   foldMap f b = f b.val
 286 |   null _ = False
 287 |   toList b = [b.val]
 288 | 
 289 | public export
 290 | Traversable Bounded where
 291 |   traverse f (B v bs) = (`B` bs) <$> f v
 292 | 
 293 | export %inline
 294 | noBounds : Bounded t -> Bounded t
 295 | noBounds = {bounds := NoBounds}
 296 |