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