0 | module Text.ILex.State.Streaming
 1 |
 2 | import Data.Linear.Ref1
 3 | import Syntax.T1
 4 | import Text.ByteBounds
 5 | import Text.ILex.Interfaces
 6 | import Text.ILex.Parser
 7 | import Text.ILex.State.Derive
 8 | import Text.ILex.Util
 9 | import Text.ParseError
10 |
11 | %default total
12 | %language ElabReflection
13 |
14 | ||| A parser state that can be use for streaming lists of values
15 | ||| such as declarations in a programming language.
16 | |||
17 | ||| The parser stack is stored in mutable field `stack_`, while
18 | ||| the values parsed so far are stored in `values_`.
19 | |||
20 | ||| In addition, support for working with nested block comments
21 | ||| is included. This is somewhat opinionated, but client code
22 | ||| can just ignore it and use an error lexer for the comment field.
23 | public export
24 | record State (e,s,a : Type) (r : Bits32) (q : Type) where
25 |   [search q]
26 |   constructor SS
27 |   -- Position and token bounds
28 |   bufSize_    : Nat
29 |   prev_       : ByteString
30 |   cur_        : IBuffer bufSize_
31 |   prevOffset_ : Nat
32 |   curOffset_  : Nat
33 |   from_       : Ref q (LTENat bufSize_)
34 |   till_       : Ref q (LTENat bufSize_)
35 |   positions_  : Ref q (SnocList BytePos)
36 |
37 |   -- Current state
38 |   stack_      : Ref q s
39 |   state_      : Ref q (Index r)
40 |   values_     : Ref q (SnocList a)
41 |
42 |   -- Working with string literals
43 |   strings_    : Ref q (SnocList String)
44 |
45 |   -- Error handling
46 |   error_      : Ref q (Maybe $ BBErr e)
47 |
48 |   -- Block comments
49 |   comment     : Index r
50 |   depth       : Ref q Nat
51 |
52 | %runElab derive "State" [FullState]
53 |
54 | export
55 | init :
56 |      (comment : Index r)
57 |   -> (stack   : s)
58 |   -> (n : Nat)
59 |   -> IBuffer n
60 |   -> F1 q (State e s a r q)
61 | init c v n buf = T1.do
62 |   rf <- ref1 (first n)
63 |   rt <- ref1 (first n)
64 |   ps <- ref1 [<]
65 |   sk <- ref1 v
66 |   st <- ref1 c
67 |   ds <- ref1 [<]
68 |   ss <- ref1 [<]
69 |   er <- ref1 Nothing
70 |   dp <- ref1 Z
71 |   pure (SS n empty buf 0 0 rf rt ps sk st ds ss er c dp)
72 |
73 | export %inline
74 | pushValue : State e s a r q => a -> s -> Index r -> F1 q (Index r)
75 | pushValue @{st} d sk x t =
76 |  let _ # t := push1 st.values_ d t
77 |   in writeAs st.stack_ sk x t
78 |
79 | export
80 | values : State e s a r q -> F1 q (Either x $ List a)
81 | values st t =
82 |  let sd # t := replace1 st.values_ [<] t
83 |   in Right (sd <>> []) # t
84 |
85 | export
86 | valuesChunk : State e s a r q -> F1 q (Maybe $ List a)
87 | valuesChunk st t =
88 |  let sd # t := replace1 st.values_ [<] t
89 |   in maybeList sd # t
90 |