0 | module Text.ByteBounds
  1 |
  2 | import Data.Array.Core
  3 | import Data.Bits
  4 | import Data.ByteString
  5 | import Derive.Prelude
  6 | import public Text.Bounds
  7 | import public Text.FC
  8 | import public Text.ParseError
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          Position
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| Position in a byte string or stream.
 18 | public export
 19 | record BytePos where
 20 |   constructor BP
 21 |   pos  : Nat
 22 |
 23 | %runElab derive "BytePos" [Show,Eq,Ord,FromInteger]
 24 |
 25 | public export %inline
 26 | Interpolation BytePos where
 27 |   interpolate = show . pos
 28 |
 29 | ||| Increases the position by the given length
 30 | ||| of a byte sequence.
 31 | export
 32 | incLen : Nat -> BytePos -> BytePos
 33 | incLen (S n) (BP p) = BP (n+p)
 34 | incLen _     p      = p
 35 |
 36 | ||| Computes the end position of a token by reducing
 37 | ||| the start position of the next token by one
 38 | ||| (unless this is a zero-byte token corresponding to the
 39 | ||| end of input).
 40 | export
 41 | endPos : (from, till : Nat) -> BytePos
 42 | endPos from till =
 43 |   case prim__lt_Integer (cast from) (cast till) of
 44 |     0 => BP till
 45 |     _ => BP (pred till)
 46 |
 47 | --------------------------------------------------------------------------------
 48 | --          ByteBounds
 49 | --------------------------------------------------------------------------------
 50 |
 51 | ||| A pair of `BytePos`s, describing a range in a byte stream, or `NoBB` for
 52 | ||| use - for instance - with programmatically created tokens.
 53 | public export
 54 | data ByteBounds : Type where
 55 |   BB   : (start, end : BytePos) -> ByteBounds
 56 |   NoBB : ByteBounds
 57 |
 58 | %runElab derive "ByteBounds" [Show,Eq]
 59 |
 60 | export
 61 | Interpolation ByteBounds where
 62 |   interpolate (BB s e) = if s == e then "\{s}" else "\{s}--\{e}"
 63 |   interpolate NoBB     = ""
 64 |
 65 | public export
 66 | Semigroup ByteBounds where
 67 |   NoBB     <+> y        = y
 68 |   x        <+> NoBB     = x
 69 |   BB s1 e1 <+> BB s2 e2 = BB (min s1 s2) (max e1 e2)
 70 |
 71 | public export
 72 | Monoid ByteBounds where
 73 |   neutral = NoBB
 74 |
 75 | public export
 76 | interface MapBounds (0 a : Type) where
 77 |   mapBounds : (ByteBounds -> ByteBounds) -> a -> a
 78 |
 79 | export %inline
 80 | clearBounds : MapBounds a => a -> a
 81 | clearBounds = mapBounds (const NoBB)
 82 |
 83 | export %inline
 84 | MapBounds ByteBounds where mapBounds = id
 85 |
 86 | export
 87 | MapBounds a => MapBounds (Maybe a) where
 88 |   mapBounds = map . mapBounds
 89 |
 90 | export
 91 | MapBounds a => MapBounds (List a) where
 92 |   mapBounds = map . mapBounds
 93 |
 94 | export
 95 | MapBounds a => MapBounds (SnocList a) where
 96 |   mapBounds = map . mapBounds
 97 |
 98 | export
 99 | MapBounds a => MapBounds b => MapBounds (a,b) where
100 |   mapBounds f (x,y) = (mapBounds f x, mapBounds f y)
101 |
102 | export
103 | MapBounds a => MapBounds b => MapBounds (Either a b) where
104 |   mapBounds f (Left x)  = Left $ mapBounds f x
105 |   mapBounds f (Right x) = Right $ mapBounds f x
106 |
107 | export %inline
108 | fromPos : Cast t ByteBounds => BytePos -> t -> ByteBounds
109 | fromPos p x = BB p p <+> cast x
110 |
111 | export %inline
112 | tillPos : Cast t ByteBounds => t -> BytePos -> ByteBounds
113 | tillPos x p = cast x <+> BB p p
114 |
115 | export %inline
116 | Cast BytePos ByteBounds where cast b = BB b b
117 |
118 | --------------------------------------------------------------------------------
119 | --          ByteBounded
120 | --------------------------------------------------------------------------------
121 |
122 | ||| Pairs a value with the bounds in the byte stream from where it was parsed.
123 | public export
124 | record ByteBounded ty where
125 |   constructor B
126 |   val    : ty
127 |   bounds : ByteBounds
128 |
129 | %runElab derive "ByteBounded" [Show,Eq]
130 |
131 | export
132 | fromBytePos : ByteBounded a -> BytePos -> ByteBounded a
133 | fromBytePos (B v $ BB (BP s) (BP e)) (BP p) = B v $ BB (BP $ s+p) (BP $ e+p)
134 | fromBytePos (B v NoBB)               p      = B v $ BB p p
135 |
136 | -- implements of `(<*>)`
137 | app : ByteBounded (a -> b) -> ByteBounded a -> ByteBounded b
138 | app (B vf b1) (B va b2) = B (vf va) (b1 <+> b2)
139 |
140 | -- implements `(>>=)`
141 | bind : ByteBounded a -> (a -> ByteBounded b) -> ByteBounded b
142 | bind (B va b1) f =
143 |   let B vb b2 = f va
144 |    in B vb (b1 <+> b2)
145 |
146 | export
147 | Functor ByteBounded where
148 |   map f (B val bs) = B (f val) bs
149 |
150 | export %inline
151 | Applicative ByteBounded where
152 |   pure v = B v neutral
153 |   (<*>) = app
154 |
155 | export %inline
156 | Monad ByteBounded where
157 |   (>>=) = bind
158 |
159 | export
160 | Foldable ByteBounded where
161 |   foldr c n b = c b.val n
162 |   foldl c n b = c n b.val
163 |   foldMap f b = f b.val
164 |   null _ = False
165 |   toList b = [b.val]
166 |
167 | export
168 | Traversable ByteBounded where
169 |   traverse f (B v bs) = (`B` bs) <$> f v
170 |
171 | export %inline
172 | MapBounds (ByteBounded a) where mapBounds f = {bounds $= f}
173 |
174 | --------------------------------------------------------------------------------
175 | --          Conversion to Bounds
176 | --------------------------------------------------------------------------------
177 |
178 | public export
179 | record PositionMap where
180 |   [noHints]
181 |   constructor PM
182 |   size : Nat
183 |   arr  : IArray size Position
184 |
185 | %runElab derive "PositionMap" [Show]
186 |
187 | export
188 | Eq PositionMap where
189 |   PM _ x == PM _ y = heq x y
190 |
191 | export %inline
192 | bytePositionMapFrom : Position -> ByteString -> PositionMap
193 | bytePositionMapFrom p (BS n bv) = PM (S n) $ positionMapFrom p bv
194 |
195 | export %inline
196 | stringPositionMapFrom : Position -> String -> PositionMap
197 | stringPositionMapFrom p = bytePositionMapFrom p . fromString
198 |
199 | export %inline
200 | bytePositionMap : ByteString -> PositionMap
201 | bytePositionMap (BS n bv) = PM (S n) $ positionMap bv
202 |
203 | export %inline
204 | stringPositionMap : String -> PositionMap
205 | stringPositionMap = bytePositionMap . fromString
206 |
207 | parameters {auto pm : PositionMap}
208 |   export %inline
209 |   position : BytePos -> Maybe Position
210 |   position (BP n) =
211 |     case tryLT n of
212 |       Just0 x  => Just $ atNat pm.arr n @{x}
213 |       Nothing0 => Nothing
214 |
215 |   export
216 |   toBounds : ByteBounds -> Bounds
217 |   toBounds NoBB               = NoBounds
218 |   toBounds (BB x y) =
219 |    let Just px := position x | _ => NoBounds
220 |        Just py := position y | _ => NoBounds
221 |     in BS px py
222 |
223 |   export
224 |   toBounded : ByteBounded a -> Bounded a
225 |   toBounded (B v bs) = B v $ toBounds bs
226 |
227 | public export
228 | 0 BBErr : Type -> Type
229 | BBErr e = ByteBounded (InnerError e)
230 |
231 | ||| Converts an error with byte bounds to a `ParseError` by pairing it with
232 | ||| an origin and the parsed string.
233 | export
234 | toParseError : Origin -> String -> BBErr e -> ParseError e
235 | toParseError o s err =
236 |  let mp := stringPositionMap s
237 |   in toParseError o s (toBounded err)
238 |
239 | --------------------------------------------------------------------------------
240 | --          Conversion to Bounds
241 | --------------------------------------------------------------------------------
242 |
243 | public export
244 | record ByteContext where
245 |   constructor BC
246 |   origin  : Origin
247 |   bounds  : ByteBounds
248 |
249 | %runElab derive "ByteContext" [Show,Eq]
250 |
251 | export
252 | Interpolation ByteContext where
253 |   interpolate (BC o NoBB) = interpolate o
254 |   interpolate (BC o bs)   = "\{o}: \{bs}"
255 |
256 | export %inline
257 | MapBounds ByteContext where mapBounds f = {bounds $= f}
258 |
259 | public export
260 | record ByteError e where
261 |   constructor BE
262 |   origin  : Origin
263 |   bounds  : ByteBounds
264 |   content : Maybe ByteString
265 |   error   : e
266 |
267 | %runElab derive "ByteError" [Show,Eq]
268 |
269 | export %inline
270 | MapBounds (ByteError e) where mapBounds f = {bounds $= f}
271 |
272 | public export
273 | 0 ByteErr : Type -> Type
274 | ByteErr = ByteError . InnerError
275 |
276 | export
277 | byteError : Origin -> ByteBounded e -> ByteError e
278 | byteError o (B err bs) = BE o bs Nothing err
279 |
280 | boundsPart : ByteBounds -> String
281 | boundsPart NoBB     = ""
282 | boundsPart (BB s e) =
283 |   case s == e of
284 |     True  => ", byte \{s}"
285 |     False => ", bytes \{s}--\{e}"
286 |
287 | export
288 | prettyByteErr : Interpolation e => ByteError e -> String
289 | prettyByteErr (BE o bb m err) =
290 |   case m of
291 |     Nothing => "Error at \{o}\{boundsPart bb}: \{err}"
292 |     Just bs =>
293 |      let mp := bytePositionMap bs
294 |       in interpolate $ toParseError o (toString bs) (toBounded $ B err bb)
295 |
296 | export %inline
297 | Interpolation e => Interpolation (ByteError e) where
298 |   interpolate = prettyByteErr
299 |