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