0 | module Text.ILex.FS
 1 |
 2 | import public FS
 3 | import public Text.ILex
 4 | import Syntax.T1
 5 | import Text.ILex.Char.UTF8
 6 | import Text.ILex.Internal.Runner
 7 | import Text.ILex.Runner1
 8 |
 9 | %default total
10 |
11 | parameters (p : P1 q e a)
12 |
13 |   ||| Tries to read the last token of an input stream and
14 |   ||| append it to the already accumulated list of tokens.
15 |   export
16 |   appLast : PIx p -> PST p -> Maybe (PStep p) -> F1 q (Either e a)
17 |   appLast st sk tok =
18 |     read1 (bytes @{p.hasb} sk) >>= \case
19 |       BS 0 _ => p.eoi st sk
20 |       _      => case tok of
21 |         Just f  => lastStep p f st sk
22 |         Nothing => fail p st sk
23 |
24 | ||| Converts a stream of byte strings to a list of tokens of
25 | ||| type `a`.
26 | |||
27 | ||| This can be used with any non-backtracking parsers, but for large
28 | ||| amounts of data, the mutable parser stack must accumulate completely
29 | ||| parsed values and emit them after every chunk of bytes has been
30 | ||| processed.
31 | export
32 | streamParse :
33 |      {auto has : Has (ParseError e) es}
34 |   -> {auto lft : ELift1 q f}
35 |   -> (prs      : P1 q (BoundedErr e) a)
36 |   -> {auto hap : HasPosition prs.state}
37 |   -> Origin
38 |   -> Pull f ByteString es x
39 |   -> Pull f a es x
40 | streamParse prs o pl = Prelude.do
41 |   st      <- lift1 (init prs)
42 |   posprev <- lift1 {s = q} (getPosition @{st.stack} @{hap})
43 |   prev    <- readref {s = q} (bytes @{prs.hasb} st.stack)
44 |   go prev posprev empty st pl
45 |
46 |   where
47 |     toErr : ByteString -> Position -> ByteString -> BoundedErr e -> ParseError e
48 |     toErr prev posprev bs (B x bnds) =
49 |      -- We are in the middle of an UTF-8-encoded byte sequence.
50 |      -- If we start with the remainder of a multi-byte codepoint,
51 |      -- we drop the corresponding bytes and increas the position's
52 |      -- column by one.
53 |      let pos  := incBytes prev posprev
54 |          bs'  := dropWhile (not . isStartByte) bs
55 |          pos' := if bs'.size < bs.size then incCol pos else pos
56 |       in PE o bnds (bnds `relativeTo` pos') (Just $ toString bs') x
57 |
58 |     -- Position and ByteString correspond to the previously processed
59 |     -- chunk of data and the text position of its first byte. This is
60 |     -- used to print the error context in case of an excpetion. If tokens
61 |     -- can be larger than a single chunk of data, this might not be enough
62 |     -- to print a proper error context.
63 |     go :
64 |          (prev0    : ByteString)
65 |       -> (posprev0 : Position)
66 |       -> (bs0      : ByteString)
67 |       -> LexState prs
68 |       -> Pull f ByteString es x
69 |       -> Pull f a es x
70 |     go prev0 posprev0 bs0 st p =
71 |       assert_total $ P.uncons p >>= \case
72 |         Left res      =>
73 |           lift1 {s = q} (appLast prs st.state st.stack st.tok) >>= \case
74 |             Left x  => throw (toErr prev0 posprev0 bs0 x)
75 |             Right v => emit v $> res
76 |         Right (bs1,p2) => Prelude.do
77 |           posprev1 <- lift1 {s = q} (getPosition @{st.stack} @{hap})
78 |           prev1    <- readref {s = q} (bytes @{prs.hasb} st.stack)
79 |           lift1 (pparseBytes prs st bs1) >>= \case
80 |             Left x        => throw (toErr prev0 posprev0 (bs0 <+> bs1) x)
81 |             Right (st2,m) => consMaybe m (go prev1 posprev1 bs1 st2 p2)
82 |
83 | export %inline
84 | streamVal :
85 |      {auto has : Has (ParseError e) es}
86 |   -> {auto lft : ELift1 q f}
87 |   -> (dflts : Lazy a)
88 |   -> (prs : P1 q (BoundedErr e) a)
89 |   -> {auto hap : HasPosition prs.state}
90 |   -> {auto hab : HasBytes prs.state}
91 |   -> Origin
92 |   -> Stream f es ByteString
93 |   -> Pull f o es a
94 | streamVal dflt prs o = P.lastOr dflt . streamParse prs o
95 |