0 | module Text.ILex.Runner
  1 |
  2 | import Data.Buffer
  3 | import Text.ILex.Internal.Runner
  4 | import public Text.ParseError
  5 | import public Text.FC
  6 | import public Text.ILex.Parser
  7 | import public Text.ILex.Interfaces
  8 |
  9 | %default total
 10 |
 11 | ||| Tries to parse a byte vector into a value.
 12 | export
 13 | run : {n : _} -> Parser1 e a -> IBuffer n -> Either e a
 14 |
 15 | ||| Like `run` but processes a UTF-8 string instead.
 16 | export %inline
 17 | runString : Parser1 e a -> String -> Either e a
 18 | runString l s = run l (fromString s)
 19 |
 20 | ||| Like `run` but processes a `ByteString` instead.
 21 | export %inline
 22 | runBytes : Parser1 e a -> ByteString -> Either e a
 23 | runBytes l (BS s bv) = run l (toIBuffer bv)
 24 |
 25 | ||| Like `run` but processes a `ByteString` instead.
 26 | export
 27 | runList : Parser1 e a -> List ByteString -> Either e a
 28 |
 29 | ||| Like `run` but fails with a proper parse error
 30 | ||| including error bounds and highlighting of
 31 | ||| the section where an error occurred.
 32 | export %inline
 33 | parse :
 34 |      {n : _}
 35 |   -> Parser1 (BBErr e) a
 36 |   -> Origin
 37 |   -> IBuffer n
 38 |   -> Either (ParseError e) a
 39 | parse l o buf = mapFst (toParseError o (toString buf 0 n)) (run l buf)
 40 |
 41 | ||| Like `parse` but processes a UTF-8 string instead.
 42 | export %inline
 43 | parseString :
 44 |      Parser1 (BBErr e) a
 45 |   -> Origin
 46 |   -> String
 47 |   -> Either (ParseError e) a
 48 | parseString l o s = parse l o (fromString s)
 49 |
 50 | ||| Like `parse` but processes a `ByteString` instead.
 51 | export %inline
 52 | parseBytes :
 53 |      Parser1 (BBErr e) a
 54 |   -> Origin
 55 |   -> ByteString
 56 |   -> Either (ParseError e) a
 57 | parseBytes l o bs = mapFst (toParseError o (toString bs)) (runBytes l bs)
 58 |
 59 | --------------------------------------------------------------------------------
 60 | -- Lexer run loop
 61 | --------------------------------------------------------------------------------
 62 |
 63 | ||| Lexing state.
 64 | |||
 65 | ||| This encapsulates the current state as well as
 66 | ||| the remainder of the previous chunk that marks
 67 | ||| the beginning of the current token.
 68 | public export
 69 | record LexState (p : P1 q e a) where
 70 |   constructor LST
 71 |   {0 sts  : Nat}
 72 |   state   : PIx p
 73 |   stack   : PST p
 74 |   dfa     : PStepper sts p
 75 |   cur     : PByteStep sts p
 76 |   tok     : PStep p
 77 |
 78 | export
 79 | init : (n : Nat) -> IBuffer n -> (p : P1 q e a) -> F1 q (LexState p)
 80 | init n buf p t =
 81 |  let stck # t := p.stck n buf t
 82 |      L _ dfa  := p.lex `at` p.init
 83 |   in LST p.init stck dfa (dfa `at` 0) Err # t
 84 |
 85 | ||| Result of a partial lexing step: In such a step, we lex
 86 | ||| till the end of a chunk of bytes, allowing for a remainder of
 87 | ||| bytes that could not yet be identified as a tokens.
 88 | public export
 89 | 0 LoopRes : (p : P1 q e a) -> Type
 90 | LoopRes p = F1 q (Either e (LexState p))
 91 |
 92 | export
 93 | lastStep : (p : P1 q e a) -> LexState p -> F1 q (Either e a)
 94 | lastStep p (LST st sk _ _ tok) t =
 95 |   case tok of
 96 |     Err => case getBytes @{p.hasb} t of
 97 |       BS 0 _ # t => p.eoi st sk t
 98 |       _      # t => fail p st sk t
 99 |     Run f =>
100 |      let st2 # t := f (E sk t)
101 |          _   # t := toFinalPos @{p.hasb} t
102 |       in p.eoi st2 sk t
103 |     Ign   =>
104 |      let _   # t := toFinalPos @{p.hasb} t
105 |       in p.eoi st sk t
106 |
107 | parameters {0 q,e,a : Type}
108 |            {0 n     : Nat}
109 |            (parser  : P1 q e a)
110 |            (sk      : PST parser)
111 |            (buf     : IBuffer n)
112 |            (rfrom   : Ref q (LTENat n))
113 |            (rtill   : Ref q (LTENat n))
114 |
115 |   %inline
116 |   stp : Fun1 q parser.state x -> (0 till : Nat) -> Ix till n => F1 q x
117 |   stp f till t =
118 |     let _ # t := write1 rtill (lteNat till) t
119 |      in f (E sk t)
120 |
121 |   step :
122 |        (st          : PIx parser)
123 |     -> (dfa         : PStepper k parser)
124 |     -> (cur         : PByteStep k parser)
125 |     -> (pos         : Nat)
126 |     -> {auto posIx  : Ix pos n}
127 |     -> LoopRes parser
128 |
129 |   succ :
130 |        (st          : PIx parser)
131 |     -> (dfa         : PStepper k parser)
132 |     -> (cur         : PByteStep k parser)
133 |     -> (last        : PRun parser)
134 |     -> (pos         : Nat)
135 |     -> {auto posIx  : Ix pos n}
136 |     -> LoopRes parser
137 |
138 |   igno :
139 |        (st          : PIx parser)
140 |     -> (dfa         : PStepper k parser)
141 |     -> (cur         : PByteStep k parser)
142 |     -> (pos         : Nat)
143 |     -> {auto posIx  : Ix pos n}
144 |     -> LoopRes parser
145 |
146 |   loop : (st : PIx parser) -> (pos : Nat) -> (x : Ix pos n) => LoopRes parser
147 |   loop st 0     t =
148 |    let _ # t   := write1 rfrom (lteNat 0) t
149 |        _ # t   := write1 rtill (lteNat 0) t
150 |        L _ dfa := parser.lex `at` st
151 |     in Right (LST st sk dfa (dfa `at` 0) Err) # t
152 |   loop st (S k) t =
153 |    let _ # t   := write1 rfrom (lteNat $ S k) t
154 |        L _ dfa := parser.lex `at` st
155 |        cur     := dfa `at` 0
156 |     in case cur `atByte` (buf `ix` k) of
157 |          Done f       => let s2 # t := stp f k t in loop s2 k t
158 |          Ignore       => loop st k t
159 |          Move   nxt f => succ st dfa (dfa `at` nxt) f k t
160 |          MoveI  nxt   => igno st dfa (dfa `at` nxt)   k t
161 |          MoveE  nxt   => step st dfa (dfa `at` nxt)   k t
162 |          _            => stp (failFun1 parser st) k t
163 |
164 |   succ st dfa cur f 0     t =
165 |    let _ # t := write1 rtill (lteNat 0) t
166 |     in Right (LST st sk dfa cur (Run f)) # t
167 |   succ st dfa cur f (S k) t =
168 |    let byte := buf `ix` k
169 |     in case cur `atByte` byte of
170 |          Keep         => succ st dfa cur f k t
171 |          Done f       => let s2 # t := stp f k t in loop s2 k t
172 |          Ignore       => loop st k t
173 |          Move   nxt f => succ st dfa (dfa `at` nxt) f k t
174 |          MoveI  nxt   => igno st dfa (dfa `at` nxt)   k t
175 |          MoveE  nxt   => step st dfa (dfa `at` nxt)   k t
176 |          Bottom       => let s2 # t := stp f (S k) t in loop s2 (S k) t
177 |
178 |   igno st dfa cur 0     t =
179 |    let _ # t := write1 rtill (lteNat 0) t
180 |     in Right (LST st sk dfa cur Ign) # t
181 |   igno st dfa cur (S k) t =
182 |    let byte := buf `ix` k
183 |     in case cur `atByte` byte of
184 |          Keep         => igno st dfa cur   k t
185 |          Done f       => let s2 # t := stp f k t in loop s2 k t
186 |          Ignore       => loop st k t
187 |          Move   nxt f => succ st dfa (dfa `at` nxt) f k t
188 |          MoveI  nxt   => igno st dfa (dfa `at` nxt)   k t
189 |          MoveE  nxt   => step st dfa (dfa `at` nxt)   k t
190 |          Bottom       => loop st (S k) t
191 |
192 |   step st dfa cur 0     t =
193 |    let _ # t := write1 rtill (lteNat 0) t
194 |     in Right (LST st sk dfa cur Err) # t
195 |   step st dfa cur (S k) t =
196 |    let byte := buf `ix` k
197 |     in case cur `atByte` byte of
198 |          Keep         => step st dfa cur k t
199 |          Done f       => let s2 # t := stp f k t in loop s2 k t
200 |          Ignore       => loop st k t
201 |          Move   nxt f => succ st dfa (dfa `at` nxt) f k t
202 |          MoveI  nxt   => igno st dfa (dfa `at` nxt)   k t
203 |          MoveE  nxt   => step st dfa (dfa `at` nxt)   k t
204 |          Bottom       => stp (failFun1 parser st) k t
205 |
206 | export
207 | stepState :
208 |      {n : Nat}
209 |   -> IBuffer n
210 |   -> (p : P1 q e a)
211 |   -> LexState p
212 |   -> LoopRes p
213 | stepState {n = 0}   buf p lst t = Right lst # t
214 | stepState {n = S k} buf p (LST st skOld dfa cr tok) t =
215 |  let bs   # t := getBytes @{p.hasb} @{skOld} t
216 |      BP o # t := startPos {hb = p.hasb, sk = skOld} t
217 |      rf   # t := ref1 (first $ S k) t
218 |      rt   # t := ref1 (first $ S k) t
219 |      sk       := Parser.copy @{p.hasb} (S k) o bs buf rf rt skOld
220 |      byte     := at buf 0
221 |   in case cr `atByte` byte of
222 |        Keep         => case tok of
223 |          Run f  => succ p sk buf rf rt st dfa cr f k t
224 |          Ign    => igno p sk buf rf rt st dfa cr   k t
225 |          Err    => step p sk buf rf rt st dfa cr   k t
226 |        Done f       =>
227 |         let s2 # t := stp p sk buf rf rt f k t
228 |          in loop p sk buf rf rt s2 k t
229 |        Ignore       => loop p sk buf rf rt st k t
230 |        Move   nxt f => succ p sk buf rf rt st dfa (dfa `at` nxt) f k t
231 |        MoveI  nxt   => igno p sk buf rf rt st dfa (dfa `at` nxt)   k t
232 |        MoveE  nxt   => step p sk buf rf rt st dfa (dfa `at` nxt)   k t
233 |        Bottom     => case tok of
234 |          Run f  =>
235 |           let s2 # t := stp p sk buf rf rt f (S k) t
236 |               ske    := Parser.copy @{p.hasb} (S k) (o+bs.size) empty buf rf rt sk
237 |            in loop p ske buf rf rt s2 (S k) t
238 |          Ign    =>
239 |           let ske    := Parser.copy @{p.hasb} (S k) (o+bs.size) empty buf rf rt sk
240 |            in loop p ske buf rf rt st (S k) t
241 |          Err => stp p sk buf rf rt (failFun1 p st) k t
242 |
243 | run p buf =
244 |  run1 $ \t =>
245 |    let lst        # t := Runner.init n buf p t
246 |        Right lst2 # t := stepState buf p lst t | Left x # t => Left x # t
247 |     in lastStep p lst2 t
248 |
249 | loopAll : (p : P1 q e a) -> LexState p -> List ByteString -> F1 q (Either e a)
250 | loopAll p lst []              t = lastStep p lst t
251 | loopAll p lst (BS n bv :: xs) t =
252 |   case stepState (toIBuffer bv) p lst t of
253 |     Left x     # t => Left x # t
254 |     Right lst2 # t => loopAll p lst2 xs t
255 |
256 | runList p bs =
257 |   run1 $ \t =>
258 |    let lst # t := Runner.init 0 empty p t
259 |     in loopAll p lst bs t
260 |