0 | module Text.ILex.Stack
  1 |
  2 | import Data.Linear.Ref1
  3 | import Syntax.T1
  4 | import Text.Bounds
  5 | import Text.ILex.Derive
  6 | import Text.ILex.Interfaces
  7 | import Text.ILex.Parser
  8 | import Text.ILex.Util
  9 | import Text.ParseError
 10 |
 11 | %hide Prelude.(>>)
 12 | %hide Prelude.(>>=)
 13 | %hide Prelude.pure
 14 | %default total
 15 | %language ElabReflection
 16 |
 17 | --------------------------------------------------------------------------------
 18 | -- General Purpose Stack
 19 | --------------------------------------------------------------------------------
 20 |
 21 | ||| A general-purpose mutable parser stack that can be used in many common
 22 | ||| situation, such as when needing just a lexer or wanting to parse
 23 | ||| a single value of a simple type.
 24 | |||
 25 | ||| For concrete usage examples, see ilex-json and ilex-toml, which both
 26 | ||| make use of this type as their mutable parser state.
 27 | |||
 28 | ||| If you are writing a parser for something complex such as a programming
 29 | ||| language, you're probably going to need quite a few custom fields, so
 30 | ||| feel free to come up with your own.
 31 | public export
 32 | record Stack (e,a : Type) (r : Bits32) (q : Type) where
 33 |   [search q]
 34 |   constructor S
 35 |   -- Position and token bounds
 36 |   line_      : Ref q Nat
 37 |   col_       : Ref q Nat
 38 |   positions_ : Ref q (SnocList Position)
 39 |
 40 |   -- Custom stack type
 41 |   stack_     : Ref q a
 42 |
 43 |   -- Current state
 44 |   state_     : Ref q (Index r)
 45 |
 46 |   -- Working with string literals
 47 |   strings_   : Ref q (SnocList String)
 48 |
 49 |   -- Error handling
 50 |   error_     : Ref q (Maybe $ BoundedErr e)
 51 |
 52 |   -- Last lexed byte string
 53 |   bytes_     : Ref q ByteString
 54 |
 55 | %runElab derive "Stack" [FullStack]
 56 |
 57 | ||| Initializes a new parser stack.
 58 | export
 59 | init : (0 p : 0 < r) => a -> F1 q (Stack e a r q)
 60 | init v = T1.do
 61 |   ln <- ref1 Z
 62 |   cl <- ref1 Z
 63 |   ps <- ref1 [<]
 64 |   sk <- ref1 v
 65 |   st <- ref1 (I 0)
 66 |   ss <- ref1 [<]
 67 |   er <- ref1 Nothing
 68 |   bs <- ref1 empty
 69 |   pure (S ln cl ps sk st ss er bs)
 70 |
 71 | --------------------------------------------------------------------------------
 72 | -- Values
 73 | --------------------------------------------------------------------------------
 74 |
 75 | %runElab deriveParserState "VSz" "VST" ["VIni", "VErr", "VDone"]
 76 |
 77 | ||| Description of lexicographic tokens
 78 | |||
 79 | ||| These are used to convert a lexer state to a token (or an error)
 80 | ||| of the appropriate type. Every lexer state corresponds to exactly
 81 | ||| one convertion. Typically, most lexer states are non-terminal
 82 | ||| states, so they correspond to `Bottom`.
 83 | public export
 84 | data Tok : (e, a : Type) -> Type where
 85 |   ||| Marks a terminal state that does not produce a token.
 86 |   ||| This can be used for comments or whitespace that should be
 87 |   ||| ignored.
 88 |   Ignore : Tok e a
 89 |
 90 |   ||| A constant token that allows us to emit a value directly.
 91 |   Const  : a -> Tok e a
 92 |
 93 |   ||| A token that needs to be parsed from its corresponding bytestring.
 94 |   Txt    : (String -> Either e a) -> Tok e a
 95 |
 96 |   ||| A token that needs to be parsed from its corresponding bytestring.
 97 |   Bytes  : (ByteString -> Either e a) -> Tok e a
 98 |
 99 | export %inline
100 | const : a -> Tok e a
101 | const = Const
102 |
103 | export %inline
104 | txt : (String -> a) -> Tok e a
105 | txt f = Txt (Right . f)
106 |
107 | export %inline
108 | bytes : (ByteString -> a) -> Tok e a
109 | bytes f = Bytes (Right . f)
110 |
111 | toStep :
112 |      (RExpOf True b, Tok e a)
113 |   -> (RExpOf True b, Step q VSz (Stack e (Maybe a) VSz))
114 | toStep (x,c) =
115 |   case c of
116 |     Ignore  => conv' x VIni
117 |     Const v => conv x (\_ => putStackAs (Just v) VDone)
118 |     Txt f   =>
119 |       read x $ \s => case f s of
120 |         Right v => putStackAs (Just v) VDone
121 |         Left e  => failHere (Custom e) VErr
122 |     Bytes f =>
123 |       conv x $ \s => case f s of
124 |         Right v => putStackAs (Just v) VDone
125 |         Left e  => failHere (Custom e) VErr
126 |
127 | ignore :
128 |      (RExpOf True b, Tok e a)
129 |   -> Maybe (RExpOf True b, Step q VSz (Stack e (Maybe a) VSz))
130 | ignore (x,Ignore) = Just $ conv' x VDone
131 | ignore _          = Nothing
132 |
133 | valEOI : VST -> Stack e (Maybe a) VSz q -> F1 q (Either (BoundedErr e) a)
134 | valEOI i sk =
135 |   if i == VDone || i == VIni
136 |      then replace1 sk.stack_ Nothing >>= \case
137 |             Just v  => pure (Right v)
138 |             Nothing => unexpected [] sk >>= pure . Left
139 |      else unexpected [] sk >>= pure . Left
140 |
141 | public export
142 | 0 PVal1 : (q,e : Type) -> (a : Type) -> Type
143 | PVal1 q e a = P1 q (BoundedErr e) a
144 |
145 | ||| Parser for simple values based on regular expressions.
146 | export
147 | value : Maybe a -> TokenMap (Tok e a) -> PVal1 q e a
148 | value mv m =
149 |  let iniSteps  := E VIni $ dfa (map toStep m)
150 |      doneSteps := E VDone $ dfa (mapMaybe ignore m)
151 |      states    := lex1 [iniSteps, doneSteps]
152 |   in P VIni (init mv) states noChunk (errs []) valEOI
153 |
154 | --------------------------------------------------------------------------------
155 | -- Lexer
156 | --------------------------------------------------------------------------------
157 |
158 | parameters {0 r      : Bits32}
159 |            {auto sk  : s q}
160 |            {auto pos : HasPosition s}
161 |            {auto stk : HasStack s (SnocList $ Bounded a)}
162 |            {auto 0 p : 0 < r}
163 |
164 |   export %inline
165 |   lexPushNL : Nat -> a -> F1 q (Index r)
166 |   lexPushNL n tok = T1.do
167 |     bs <- tokenBounds n
168 |     incline 1
169 |     push1 (stack sk) (B tok bs)
170 |     pure Ini
171 |
172 |   export %inline
173 |   lexPush : Nat -> a -> F1 q (Index r)
174 |   lexPush n tok = T1.do
175 |     bs <- tokenBounds n
176 |     push1 (stack sk) (B tok bs)
177 |     pure Ini
178 |
179 | parameters (x          : RExpOf True b)
180 |            {auto pos   : HasPosition s}
181 |            {auto stk   : HasStack s (SnocList $ Bounded a)}
182 |            {auto 0 lt  : 0 < r}
183 |
184 |   ||| Recognizes the given character and uses it to update the parser state
185 |   ||| as specified by `f`.
186 |   |||
187 |   ||| The current column is increased by one *after* invoking `f`.
188 |   export %inline
189 |   ctok : {n : _} -> (0 prf : ConstSize n x) => a -> (RExpOf True b, Step q r s)
190 |   ctok v = go x $ lexPush n v
191 |
192 |   export %inline
193 |   readTok : HasBytes s => (String -> a) -> (RExpOf True b, Step q r s)
194 |   readTok f = goStr x $ \s => lexPush (length s) (f s)
195 |
196 |   export %inline
197 |   convTok : HasBytes s => (ByteString -> a) -> (RExpOf True b, Step q r s)
198 |   convTok f = goBS x $ \bs => lexPush bs.size (f bs)
199 |
200 |   export %inline
201 |   nltok : HasBytes s => a -> (RExpOf True b, Step q r s)
202 |   nltok v = goBS x $ \bs => lexPushNL bs.size v
203 |
204 | export
205 | lexEOI :
206 |      {auto 0 lt : 0 < r}
207 |   -> {auto pos : HasPosition s}
208 |   -> {auto stk : HasStack s (SnocList a)}
209 |   -> {auto err : HasError s e}
210 |   -> {auto bts : HasBytes s}
211 |   -> Index r
212 |   -> s q
213 |   -> F1 q (Either (BoundedErr e) $ List a)
214 | lexEOI i sk =
215 |   if i == Ini
216 |      then getList (stack sk) >>= pure . Right
217 |      else unexpected [] sk >>= pure . Left
218 |
219 | public export
220 | 0 L1 : (q,e : Type) -> (a : Type) -> Type
221 | L1 q e a = P1 q (BoundedErr e) (List $ Bounded a)
222 |
223 | public export
224 | 0 Lexer : (e : Type) -> Type -> Type
225 | Lexer e a = {0 q : Type} -> L1 q e a
226 |
227 | export
228 | lexer :
229 |      {r : _}
230 |   -> {auto 0 lt  : 0 < r}
231 |   -> Steps q r (Stack e (SnocList $ Bounded a) r)
232 |   -> L1 q e a
233 | lexer m =
234 |   P Ini (init [<]) (lex1 [E Ini $ dfa m]) snocChunk (errs []) lexEOI
235 |