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 | --------------------------------------------------------------------------------
 37 | --          ByteBounds
 38 | --------------------------------------------------------------------------------
 39 |
 40 | ||| A pair of `BytePos`s, describing a range in a byte stream, or `NoBB` for
 41 | ||| use - for instance - with programmatically created tokens.
 42 | public export
 43 | data ByteBounds : Type where
 44 |   BB   : (start, end : BytePos) -> ByteBounds
 45 |   NoBB : ByteBounds
 46 |
 47 | %runElab derive "ByteBounds" [Show,Eq]
 48 |
 49 | export
 50 | Interpolation ByteBounds where
 51 |   interpolate (BB s e) = if s == e then "\{s}" else "\{s}--\{e}"
 52 |   interpolate NoBB     = ""
 53 |
 54 | public export
 55 | Semigroup ByteBounds where
 56 |   NoBB     <+> y        = y
 57 |   x        <+> NoBB     = x
 58 |   BB s1 e1 <+> BB s2 e2 = BB (min s1 s2) (max e1 e2)
 59 |
 60 | public export
 61 | Monoid ByteBounds where
 62 |   neutral = NoBB
 63 |
 64 | --------------------------------------------------------------------------------
 65 | --          ByteBounded
 66 | --------------------------------------------------------------------------------
 67 |
 68 | ||| Pairs a value with the bounds in the byte stream from where it was parsed.
 69 | public export
 70 | record ByteBounded ty where
 71 |   constructor B
 72 |   val    : ty
 73 |   bounds : ByteBounds
 74 |
 75 | %runElab derive "ByteBounded" [Show,Eq]
 76 |
 77 | export
 78 | fromBytePos : ByteBounded a -> BytePos -> ByteBounded a
 79 | fromBytePos (B v $ BB (BP s) (BP e)) (BP p) = B v $ BB (BP $ s+p) (BP $ e+p)
 80 | fromBytePos (B v NoBB)               p      = B v $ BB p p
 81 |
 82 | -- implements of `(<*>)`
 83 | app : ByteBounded (a -> b) -> ByteBounded a -> ByteBounded b
 84 | app (B vf b1) (B va b2) = B (vf va) (b1 <+> b2)
 85 |
 86 | -- implements `(>>=)`
 87 | bind : ByteBounded a -> (a -> ByteBounded b) -> ByteBounded b
 88 | bind (B va b1) f =
 89 |   let B vb b2 = f va
 90 |    in B vb (b1 <+> b2)
 91 |
 92 | export
 93 | Functor ByteBounded where
 94 |   map f (B val bs) = B (f val) bs
 95 |
 96 | export %inline
 97 | Applicative ByteBounded where
 98 |   pure v = B v neutral
 99 |   (<*>) = app
100 |
101 | export %inline
102 | Monad ByteBounded where
103 |   (>>=) = bind
104 |
105 | export
106 | Foldable ByteBounded where
107 |   foldr c n b = c b.val n
108 |   foldl c n b = c n b.val
109 |   foldMap f b = f b.val
110 |   null _ = False
111 |   toList b = [b.val]
112 |
113 | export
114 | Traversable ByteBounded where
115 |   traverse f (B v bs) = (`B` bs) <$> f v
116 |
117 | --------------------------------------------------------------------------------
118 | --          Conversion to Bounds
119 | --------------------------------------------------------------------------------
120 |
121 | public export
122 | record PositionMap where
123 |   [noHints]
124 |   constructor PM
125 |   size : Nat
126 |   arr  : IArray size Position
127 |
128 | %runElab derive "PositionMap" [Show]
129 |
130 | export
131 | Eq PositionMap where
132 |   PM _ x == PM _ y = heq x y
133 |
134 | export %inline
135 | bytePositionMapFrom : Position -> ByteString -> PositionMap
136 | bytePositionMapFrom p (BS n bv) = PM (S n) $ positionMapFrom p bv
137 |
138 | export %inline
139 | stringPositionMapFrom : Position -> String -> PositionMap
140 | stringPositionMapFrom p = bytePositionMapFrom p . fromString
141 |
142 | export %inline
143 | bytePositionMap : ByteString -> PositionMap
144 | bytePositionMap (BS n bv) = PM (S n) $ positionMap bv
145 |
146 | export %inline
147 | stringPositionMap : String -> PositionMap
148 | stringPositionMap = bytePositionMap . fromString
149 |
150 | parameters {auto pm : PositionMap}
151 |   export %inline
152 |   position : BytePos -> Maybe Position
153 |   position (BP n) =
154 |     case tryLT n of
155 |       Just0 x  => Just $ atNat pm.arr n @{x}
156 |       Nothing0 => Nothing
157 |
158 |   export
159 |   toBounds : ByteBounds -> Bounds
160 |   toBounds NoBB               = NoBounds
161 |   toBounds (BB x y) =
162 |    let Just px := position x | _ => NoBounds
163 |        Just py := position y | _ => NoBounds
164 |     in BS px py
165 |
166 |   export
167 |   toBounded : ByteBounded a -> Bounded a
168 |   toBounded (B v bs) = B v $ toBounds bs
169 |
170 | public export
171 | 0 BBErr : Type -> Type
172 | BBErr e = ByteBounded (InnerError e)
173 |
174 | ||| Converts an error with byte bounds to a `ParseError` by pairing it with
175 | ||| an origin and the parsed string.
176 | export
177 | toParseError : Origin -> String -> BBErr e -> ParseError e
178 | toParseError o s err =
179 |  let mp := stringPositionMap s
180 |   in toParseError o s (toBounded err)
181 |
182 | --------------------------------------------------------------------------------
183 | --          Conversion to Bounds
184 | --------------------------------------------------------------------------------
185 |
186 | public export
187 | record ByteContext where
188 |   constructor BC
189 |   origin  : Origin
190 |   bounds  : ByteBounds
191 |
192 | %runElab derive "ByteContext" [Show,Eq]
193 |
194 | export
195 | Interpolation ByteContext where
196 |   interpolate (BC o NoBB) = interpolate o
197 |   interpolate (BC o bs)   = "\{o}: \{bs}"
198 |
199 | public export
200 | record ByteError e where
201 |   constructor BE
202 |   origin  : Origin
203 |   bounds  : ByteBounds
204 |   content : Maybe ByteString
205 |   error   : e
206 |
207 | %runElab derive "ByteError" [Show,Eq]
208 |
209 | public export
210 | 0 ByteErr : Type -> Type
211 | ByteErr = ByteError . InnerError
212 |
213 | export
214 | byteError : Origin -> ByteBounded e -> ByteError e
215 | byteError o (B err bs) = BE o bs Nothing err
216 |
217 | boundsPart : ByteBounds -> String
218 | boundsPart NoBB     = ""
219 | boundsPart (BB s e) =
220 |   case s == e of
221 |     True  => ", byte \{s}"
222 |     False => ", bytes \{s}--\{e}"
223 |
224 | export
225 | prettyByteErr : Interpolation e => ByteError e -> String
226 | prettyByteErr (BE o bb m err) =
227 |   case m of
228 |     Nothing => "Error at \{o}\{boundsPart bb}: \{err}"
229 |     Just bs =>
230 |      let mp := bytePositionMap bs
231 |       in interpolate $ toParseError o (toString bs) (toBounded $ B err bb)
232 |
233 | export %inline
234 | Interpolation e => Interpolation (ByteError e) where
235 |   interpolate = prettyByteErr
236 |