0 | module Text.ILex.Stack
  1 |
  2 | import Data.Linear.Ref1
  3 | import Syntax.T1
  4 | import Text.ByteBounds
  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 |   bufSize_    : Nat
 37 |   prev_       : ByteString
 38 |   cur_        : IBuffer bufSize_
 39 |   prevOffset_ : Nat
 40 |   curOffset_  : Nat
 41 |   from_       : Ref q (LTENat bufSize_)
 42 |   till_       : Ref q (LTENat bufSize_)
 43 |   positions_  : Ref q (SnocList BytePos)
 44 |
 45 |   -- Custom stack type
 46 |   stack_     : Ref q a
 47 |
 48 |   -- Current state
 49 |   state_     : Ref q (Index r)
 50 |
 51 |   -- Working with string literals
 52 |   strings_   : Ref q (SnocList String)
 53 |
 54 |   -- Error handling
 55 |   error_     : Ref q (Maybe $ BBErr e)
 56 |
 57 | %runElab derive "Stack" [FullStack]
 58 |
 59 | ||| Initializes a new parser stack.
 60 | export
 61 | init : (0 p : 0 < r) => a -> (n : Nat) -> IBuffer n -> F1 q (Stack e a r q)
 62 | init v n buf = T1.do
 63 |   rf <- ref1 (first n)
 64 |   rt <- ref1 (first n)
 65 |   ps <- ref1 [<]
 66 |   sk <- ref1 v
 67 |   st <- ref1 (I 0)
 68 |   ss <- ref1 [<]
 69 |   er <- ref1 Nothing
 70 |   pure (S n empty buf 0 0 rf rt ps sk st ss er)
 71 |
 72 | --------------------------------------------------------------------------------
 73 | -- Lexer
 74 | --------------------------------------------------------------------------------
 75 |
 76 | public export
 77 | 0 Tok : Type -> Type
 78 | Tok = ByteBounded
 79 |
 80 | public export
 81 | 0 Toks : Type -> Type
 82 | Toks = List . Tok
 83 |
 84 | public export
 85 | 0 Skot : Type -> Type
 86 | Skot = SnocList . ByteBounded
 87 |
 88 | public export
 89 | 0 L1 : (q,e : Type) -> (a : Type) -> Type
 90 | L1 q e a = P1 q (BBErr e) (Toks a)
 91 |
 92 | public export
 93 | 0 Lexer : (e : Type) -> Type -> Type
 94 | Lexer e a = {0 q : Type} -> L1 q e a
 95 |
 96 | parameters {auto hb   : HasBytes s}
 97 |            {auto hs   : HasStack s (Skot a)}
 98 |            (x         : RExp True)
 99 |            {auto 0 lt : 0 < r}
100 |
101 |   export %inline
102 |   pushBounded : s q => a -> F1 q (Index r)
103 |   pushBounded v = bounded' v >>= \b => pushStackAs b 0
104 |
105 |   export %inline
106 |   tok : a -> (RExp True, Step q r s)
107 |   tok v = step x (pushBounded v)
108 |
109 |   export %inline
110 |   byteTok : (ByteString -> a) -> (RExp True, Step q r s)
111 |   byteTok f = bytes x (pushBounded . f)
112 |
113 |   export %inline
114 |   stringTok : (String -> a) -> (RExp True, Step q r s)
115 |   stringTok f = string x (pushBounded . f)
116 |
117 | export
118 | lexEOI :
119 |      {auto 0 lt : 0 < r}
120 |   -> {auto stk : HasStack s (SnocList a)}
121 |   -> {auto err : HasBBErr s e}
122 |   -> {auto bts : HasBytes s}
123 |   -> Index r
124 |   -> s q
125 |   -> F1 q (Either (BBErr e) $ List a)
126 | lexEOI i sk =
127 |   if i == Ini
128 |      then getList (stack sk) >>= pure . Right
129 |      else unexpected [] sk >>= pure . Left
130 |
131 | export
132 | lexer : {r : _} -> (0 lt : 0 < r) => Steps q r (Stack e (Skot a) r) -> L1 q e a
133 | lexer m = P Ini (init [<]) (lex1 [E Ini $ dfa m]) snocChunk (errs []) lexEOI
134 |
135 | --------------------------------------------------------------------------------
136 | -- Values
137 | --------------------------------------------------------------------------------
138 |
139 | %runElab deriveParserState "VSz" "VST" ["VIni", "VErr", "VDone"]
140 |
141 | ||| Description of lexicographic tokens
142 | public export
143 | data Token : (e, a : Type) -> Type where
144 |   ||| Marks a terminal state that does not produce a token.
145 |   ||| This can be used for comments or whitespace that should be
146 |   ||| ignored.
147 |   Ignore : Token e a
148 |
149 |   ||| A constant token that allows us to emit a value directly.
150 |   Const  : a -> Token e a
151 |
152 |   ||| A token that needs to be parsed from its corresponding bytestring.
153 |   Txt    : (String -> Either e a) -> Token e a
154 |
155 |   ||| A token that needs to be parsed from its corresponding bytestring.
156 |   Bytes  : (ByteString -> Either e a) -> Token e a
157 |
158 | export %inline
159 | const : a -> Token e a
160 | const = Const
161 |
162 | export %inline
163 | txt : (String -> a) -> Token e a
164 | txt f = Txt (Right . f)
165 |
166 | export %inline
167 | bytes : (ByteString -> a) -> Token e a
168 | bytes f = Bytes (Right . f)
169 |
170 | toStep :
171 |      (RExpOf True b, Token e a)
172 |   -> (RExpOf True b, Step q VSz (Stack e (Maybe a) VSz))
173 | toStep (x,c) =
174 |   case c of
175 |     Ignore  => ignore x
176 |     Const v => step x (putStackAs (Just v) VDone)
177 |     Txt f   =>
178 |       string x $ \s => case f s of
179 |         Right v => putStackAs (Just v) VDone
180 |         Left e  => failHere (Custom e) VErr
181 |     Bytes f =>
182 |       bytes x $ \s => case f s of
183 |         Right v => putStackAs (Just v) VDone
184 |         Left e  => failHere (Custom e) VErr
185 |
186 | ignore :
187 |      (RExpOf True b, Token e a)
188 |   -> Maybe (RExpOf True b, Step q VSz (Stack e (Maybe a) VSz))
189 | ignore (x,Ignore) = Just $ ignore x
190 | ignore _          = Nothing
191 |
192 | valEOI : VST -> Stack e (Maybe a) VSz q -> F1 q (Either (BBErr e) a)
193 | valEOI i sk =
194 |   if i == VDone || i == VIni
195 |      then replace1 sk.stack_ Nothing >>= \case
196 |             Just v  => pure (Right v)
197 |             Nothing => unexpected [] sk >>= pure . Left
198 |      else unexpected [] sk >>= pure . Left
199 |
200 | public export
201 | 0 PVal1 : (q,e : Type) -> (a : Type) -> Type
202 | PVal1 q e a = P1 q (BBErr e) a
203 |
204 | ||| Parser for simple values based on regular expressions.
205 | export
206 | value : Maybe a -> TokenMap (Token e a) -> PVal1 q e a
207 | value mv m =
208 |  let iniSteps  := E VIni $ dfa (map toStep m)
209 |      doneSteps := E VDone $ dfa (mapMaybe ignore m)
210 |      states    := lex1 [iniSteps, doneSteps]
211 |   in P VIni (init mv) states noChunk (errs []) valEOI
212 |