
   0 | module Text.Bounds
   1 | 
   2 | import Data.Bits
   3 | import Data.ByteString
   4 | import Derive.Prelude
   5 | 
   6 | %default total
   7 | 
   8 | %language ElabReflection
   9 | 
  10 | --------------------------------------------------------------------------------
  11 | --          Position
  12 | --------------------------------------------------------------------------------
  13 | 
  14 | ||| Position in a string as a pair of natural numbers.
  15 | ||| Both numbers are zero-based.
  16 | public export
  17 | record Position where
  18 |   [noHints]
  19 |   constructor P
  20 |   ||| The current line in a string (0-based)
  21 |   line : Nat
  22 |   ||| The current column in a string (0-based)
  23 |   col  : Nat
  24 | 
  25 | ||| Appends the second position to the first.
  26 | |||
  27 | ||| If the second is on a single line, the column is added.
  28 | ||| Otherwise, the line is added and the column of the second
  29 | ||| is used.
  30 | export
  31 | Semigroup Position where
  32 |   P l1 c1 <+> P 0  c2 = P l1 (c1+c2)
  33 |   P l1 c1 <+> P l2 c2 = P (l1+l2) c2
  34 | 
  35 | export
  36 | Monoid Position where
  37 |   neutral = P 0 0
  38 | 
  39 | ||| The beginning of a string. This is an alias for `P 0 0`.
  40 | public export
  41 | begin : Position
  42 | begin = P 0 0
  43 | 
  44 | ||| Increase the current column by one.
  45 | public export %inline
  46 | incCol : Position -> Position
  47 | incCol = {col $= S}
  48 | 
  49 | ||| Increase the current line by one, resetting the
  50 | ||| column to 0.
  51 | public export %inline
  52 | incLine : Position -> Position
  53 | incLine p = P (S p.line) 0
  54 | 
  55 | ||| Increase the current column by the given number of steps.
  56 | public export %inline
  57 | addCol : Nat -> Position -> Position
  58 | addCol n = {col $= (+ n)}
  59 | 
  60 | ||| Computes `p2` relative to `p1`, that is, given an earlier
  61 | ||| position `p1`, returns the number of lines and columns
  62 | ||| necessary to advance from `p1` to `p2`.
  63 | export
  64 | relativeTo : (p2,p1 : Position) -> Position
  65 | relativeTo (P l c) (P ls cs) =
  66 |   if l <= ls then P 0 (c `minus` cs) else P (l `minus` ls) c
  67 | 
  68 | ||| Advances the given text position by the characters encountered
  69 | ||| in the given string.
  70 | |||
  71 | ||| A line feed character ('\n'; codepoint `0x0A`) will increase
  72 | ||| the current line by one and reset the column to zero. Every
  73 | ||| other character will increase the column by one.
  74 | export
  75 | incString : String -> Position -> Position
  76 | incString s (P l c) = go l c (unpack s)
  77 |   where
  78 |     go : Nat -> Nat -> List Char -> Position
  79 |     go l c []        = P l c
  80 |     go l c ('\n' :: xs) = go (S l) 0 xs
  81 |     go l c (x    :: xs) = go l (S c) xs
  82 | 
  83 | ||| Advances the given text position by the bytes encountered
  84 | ||| in the given string.
  85 | |||
  86 | ||| A line feed byte (`0x0A`) will increase
  87 | ||| the current line by one and reset the column to zero. Every
  88 | ||| other start character of a unicode code point will advance
  89 | ||| the column by one.
  90 | export
  91 | incBytes : ByteString -> Position -> Position
  92 | incBytes (BS n bv) (P l c) = go l c n
  93 |   where
  94 |     go : Nat -> Nat -> (k : Nat) -> (x : Ix k n) => Position
  95 |     go l c 0     = P l c
  96 |     go l c (S k) =
  97 |       case bv `ix` k of
  98 |         0x0a => go (S l) 0 k
  99 |         b    => case b < 128 || b .&. 0b1100_0000 == 0b1100_000 of
 100 |           True => go l (S c) k
 101 |           _    => go l c k
 102 | 
 103 | ||| Adjusts the current position by one character.
 104 | |||
 105 | ||| If the character is a line break, a new line will be strated and
 106 | ||| the column set to zero, otherwise, the column is increase by one.
 107 | public export %inline
 108 | next : Char -> Position -> Position
 109 | next '\n' = incLine
 110 | next _    = incCol
 111 | 
 112 | %runElab derive "Position" [Show,Eq,Ord]
 113 | 
 114 | public export
 115 | Interpolation Position where
 116 |   interpolate (P l c) = show (l+1) ++ ":" ++ show (c+1)
 117 | 
 118 | --------------------------------------------------------------------------------
 119 | --          Bounds
 120 | --------------------------------------------------------------------------------
 121 | 
 122 | ||| A pair of `Position`s, describing a text range, or `NoBounds` for
 123 | ||| use - for instance - with programmatically created tokens.
 124 | public export
 125 | data Bounds : Type where
 126 |   BS : (start, end : Position) -> Bounds
 127 |   NoBounds : Bounds
 128 | 
 129 | %runElab derive "Bounds" [Show,Eq]
 130 | 
 131 | namespace Bounds
 132 |   export
 133 |   relativeTo : Bounds -> Position -> Bounds
 134 |   relativeTo NoBounds _ = NoBounds
 135 |   relativeTo (BS s e) p = BS (s `relativeTo` p) (e `relativeTo` p)
 136 | 
 137 |   ||| Convert a single `Position` to a range one character wide.
 138 |   public export %inline
 139 |   oneChar : Position -> Bounds
 140 |   oneChar p = BS p $ incCol p
 141 | 
 142 | export
 143 | Interpolation Bounds where
 144 |   interpolate (BS s e) = "\{s}--\{e}"
 145 |   interpolate NoBounds = ""
 146 | 
 147 | public export
 148 | Semigroup Bounds where
 149 |   NoBounds <+> y        = y
 150 |   x        <+> NoBounds = x
 151 |   BS s1 e1 <+> BS s2 e2 = BS (min s1 s2) (max e1 e2)
 152 | 
 153 | public export
 154 | Monoid Bounds where
 155 |   neutral = NoBounds
 156 | 
 157 | --------------------------------------------------------------------------------
 158 | --          Bounded
 159 | --------------------------------------------------------------------------------
 160 | 
 161 | ||| Pairs a value with the textual bounds from where it was parsed.
 162 | public export
 163 | record Bounded ty where
 164 |   constructor B
 165 |   val    : ty
 166 |   bounds : Bounds
 167 | 
 168 | %runElab derive "Bounded" [Show,Eq]
 169 | 
 170 | ||| Smart costructor for `Bounded`.
 171 | public export
 172 | bounded : a -> (start,end : Position) -> Bounded a
 173 | bounded v s e = B v $ BS s e
 174 | 
 175 | ||| Smart costructor for `Bounded`.
 176 | public export %inline
 177 | oneChar : a -> Position -> Bounded a
 178 | oneChar v p = B v $ oneChar p
 179 | 
 180 | ||| Implementation of `(<*>)`
 181 | public export
 182 | app : Bounded (a -> b) -> Bounded a -> Bounded b
 183 | app (B vf b1) (B va b2) = B (vf va) (b1 <+> b2)
 184 | 
 185 | ||| Implementation of `(>>=)`
 186 | public export
 187 | bind : Bounded a -> (a -> Bounded b) -> Bounded b
 188 | bind (B va b1) f =
 189 |   let B vb b2 = f va
 190 |    in B vb (b1 <+> b2)
 191 | 
 192 | export
 193 | fromPosition : Bounded a -> Position -> Bounded a
 194 | fromPosition (B v $ BS s e) y = B v $ BS (y <+> s) (y <+> e)
 195 | fromPosition (B v NoBounds) y = B v $ BS y (incCol y)
 196 | 
 197 | public export
 198 | Functor Bounded where
 199 |   map f (B val bs) = B (f val) bs
 200 | 
 201 | public export %inline
 202 | Applicative Bounded where
 203 |   pure v = B v neutral
 204 |   (<*>) = app
 205 | 
 206 | public export %inline
 207 | Monad Bounded where
 208 |   (>>=) = bind
 209 | 
 210 | public export
 211 | Foldable Bounded where
 212 |   foldr c n b = c b.val n
 213 |   foldl c n b = c n b.val
 214 |   foldMap f b = f b.val
 215 |   null _ = False
 216 |   toList b = [b.val]
 217 | 
 218 | public export
 219 | Traversable Bounded where
 220 |   traverse f (B v bs) = (`B` bs) <$> f v
 221 |