0 | module Text.ILex.FS
  1 |
  2 | import Data.Buffer
  3 | import public FS
  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.
 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 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 | export %inline
 46 | streamParseFrom :
 47 |      {auto has : Has (ByteError e) es}
 48 |   -> {auto lft : ELift1 q f}
 49 |   -> Origin
 50 |   -> (prs      : P1 q (ByteBounded e) a)
 51 |   -> Pull f ByteString es x
 52 |   -> Pull f a es x
 53 | streamParseFrom o = streamParseErr (byteError o)
 54 |
 55 | ||| Converts a stream of byte strings to a list of tokens of
 56 | ||| type `a`.
 57 | |||
 58 | ||| This can be used with any non-backtracking parsers, but for large
 59 | ||| amounts of data, the mutable parser stack must accumulate completely
 60 | ||| parsed values and emit them after every chunk of bytes has been
 61 | ||| processed.
 62 | export %inline
 63 | streamParse :
 64 |      {auto has : Has e es}
 65 |   -> {auto lft : ELift1 q f}
 66 |   -> (prs      : P1 q e a)
 67 |   -> Pull f ByteString es x
 68 |   -> Pull f a es x
 69 | streamParse = streamParseErr id
 70 |
 71 | export %inline
 72 | streamValErr :
 73 |      {auto has : Has ex es}
 74 |   -> {auto lft : ELift1 q f}
 75 |   -> (err   : e -> ex)
 76 |   -> (dflts : Lazy a)
 77 |   -> (prs : P1 q e a)
 78 |   -> Stream f es ByteString
 79 |   -> Pull f o es a
 80 | streamValErr err dflt prs = P.lastOr dflt . streamParseErr err prs
 81 |
 82 | export %inline
 83 | streamValFrom :
 84 |      {auto has : Has (ByteError e) es}
 85 |   -> {auto lft : ELift1 q f}
 86 |   -> Origin
 87 |   -> (dflts : Lazy a)
 88 |   -> (prs : P1 q (ByteBounded e) a)
 89 |   -> Stream f es ByteString
 90 |   -> Pull f o es a
 91 | streamValFrom o = streamValErr (byteError o)
 92 |
 93 | export %inline
 94 | streamVal :
 95 |      {auto has : Has e es}
 96 |   -> {auto lft : ELift1 q f}
 97 |   -> (dflts : Lazy a)
 98 |   -> (prs : P1 q e a)
 99 |   -> Stream f es ByteString
100 |   -> Pull f o es a
101 | streamVal = streamValErr id
102 |