0 | module Text.ILex.FS
  1 |
  2 | import Data.Buffer
  3 | import Data.SnocList
  4 | import Syntax.T1
  5 | import Text.ByteRange
  6 | import Text.ILex.Char.UTF8
  7 | import public FS.Posix
  8 | import public Text.ILex
  9 |
 10 | %hide Data.Linear.(.)
 11 | %default total
 12 |
 13 | ||| Converts a stream of byte strings to a list of tokens of
 14 | ||| type `a`.
 15 | |||
 16 | ||| This can be used with any non-backtracking parsers, but for large
 17 | ||| amounts of data, the mutable parser stack must accumulate completely
 18 | ||| parsed values and emit them after every chunk of bytes has been
 19 | ||| processed in order not to overflow system memory.
 20 | export
 21 | streamParseErr :
 22 |      {auto has : Has ex es}
 23 |   -> {auto lft : ELift1 q f}
 24 |   -> (err      : e -> ex)
 25 |   -> (prs      : P1 q e a)
 26 |   -> Pull f ByteString es x
 27 |   -> Pull f a es x
 28 | streamParseErr err prs pl = Prelude.do
 29 |   st      <- lift1 (init 0 empty prs)
 30 |   go st pl
 31 |
 32 |   where
 33 |     onErr : HSum [e] -> HSum es
 34 |     onErr (Here x) = inject (err x)
 35 |
 36 |     go : LexState prs -> Pull f ByteString es x -> Pull f a es x
 37 |     go st p =
 38 |       assert_total $ P.uncons p >>= \case
 39 |         Left res      => Prelude.do
 40 |           v <- mapErrors onErr $ eliftEither {s = q} (lastStep prs st)
 41 |           emit v $> res
 42 |         Right (BS n bv,p2) => Prelude.do
 43 |           st2 <- mapErrors onErr $ eliftEither (stepState (toIBuffer bv) prs st)
 44 |           m   <- lift1 (prs.chunk st2.stack)
 45 |           consMaybe m (go st2 p2)
 46 |
 47 | ||| Like `streamParseErr`, where the parse error is converted to
 48 | ||| an error of type `ByteError e`.
 49 | export %inline
 50 | streamParseFrom :
 51 |      {auto has : Has (ByteError e) es}
 52 |   -> {auto lft : ELift1 q f}
 53 |   -> Origin
 54 |   -> (prs      : P1 q (ByteBounded e) a)
 55 |   -> Pull f ByteString es x
 56 |   -> Pull f a es x
 57 | streamParseFrom o = streamParseErr (byteError o)
 58 |
 59 | ||| Converts a stream of byte strings to a list of tokens of
 60 | ||| type `a`.
 61 | |||
 62 | ||| This can be used with any non-backtracking parsers, but for large
 63 | ||| amounts of data, the mutable parser stack must accumulate completely
 64 | ||| parsed values and emit them after every chunk of bytes has been
 65 | ||| processed.
 66 | export %inline
 67 | streamParse :
 68 |      {auto has : Has e es}
 69 |   -> {auto lft : ELift1 q f}
 70 |   -> (prs      : P1 q e a)
 71 |   -> Pull f ByteString es x
 72 |   -> Pull f a es x
 73 | streamParse = streamParseErr id
 74 |
 75 | ||| Runs a non-streaming parser to completion, emitting
 76 | ||| the last (and only) emitted value or the given default value.
 77 | export %inline
 78 | streamValErr :
 79 |      {auto has : Has ex es}
 80 |   -> {auto lft : ELift1 q f}
 81 |   -> (err   : e -> ex)
 82 |   -> (dflts : Lazy a)
 83 |   -> (prs : P1 q e a)
 84 |   -> Stream f es ByteString
 85 |   -> Pull f o es a
 86 | streamValErr err dflt prs = P.lastOr dflt . streamParseErr err prs
 87 |
 88 | export %inline
 89 | streamValFrom :
 90 |      {auto has : Has (ByteError e) es}
 91 |   -> {auto lft : ELift1 q f}
 92 |   -> Origin
 93 |   -> (dflts : Lazy a)
 94 |   -> (prs : P1 q (ByteBounded e) a)
 95 |   -> Stream f es ByteString
 96 |   -> Pull f o es a
 97 | streamValFrom o = streamValErr (byteError o)
 98 |
 99 | export %inline
100 | streamVal :
101 |      {auto has : Has e es}
102 |   -> {auto lft : ELift1 q f}
103 |   -> (dflts : Lazy a)
104 |   -> (prs : P1 q e a)
105 |   -> Stream f es ByteString
106 |   -> Pull f o es a
107 | streamVal = streamValErr id
108 |
109 | --------------------------------------------------------------------------------
110 | -- Error Localization
111 | --------------------------------------------------------------------------------
112 |
113 | ||| Re-runs a stream of bytes to provide proper text bounds
114 | ||| (start and end line as well as start and end column)
115 | ||| of some byte bounds.
116 | export
117 | locateBounds :
118 |      {auto h : HasIO (f es)}
119 |   -> ByteBounds
120 |   -> Stream f es ByteString
121 |   -> Pull f o es (Maybe TextBounds)
122 | locateBounds NoBB           bs = pure Nothing
123 | locateBounds (BB start end) bs =
124 |      P.scans1 None (appendChunk start end) bs
125 |   |> P.takeThrough (not . isDone)
126 |   |> P.lastOr None
127 |   |> map (textBounds start end)
128 |
129 | parameters {auto ph : PollH e}
130 |            {auto he : Has Errno es}
131 |            (0 x     : Type)
132 |            {auto hb : Has (ByteError x) es}
133 |            {auto hf : Has (FCErr x) es}
134 |
135 |   ||| Streams again the origin (if any) of a parsing error,
136 |   ||| adding the content to the error in order to provide an
137 |   ||| exact error location.
138 |   |||
139 |   ||| Attention: This will try and read the whole content of the
140 |   ||| origin into memory! If you are streaming a truly huge file,
141 |   ||| you will be better off with just accepting the less precise
142 |   ||| error message with only the byte bounds of the erroneous token.
143 |   export
144 |   locError : AsyncPull e o es a -> AsyncPull e o es a
145 |   locError =
146 |     handleError (ByteError x) $ \x => case x.origin of
147 |       FileSrc p => Prelude.do
148 |         m <- locateBounds x.bounds (readBytes p)
149 |         maybe (throw x) (throw . toFCErr x) m
150 |       Virtual   => throw x
151 |