0 | module Text.ILex.Runner1
  1 |
  2 | import public Data.ByteString
  3 | import public Data.Vect
  4 | import public Text.ILex.Parser
  5 | import Text.ILex.Internal.Runner
  6 |
  7 | ||| Lexing state.
  8 | |||
  9 | ||| This encapsulates the current state as well as
 10 | ||| the remainder of the previous chunk that marks
 11 | ||| the beginning of the current token.
 12 | public export
 13 | record LexState (p : P1 q e a) where
 14 |   constructor LST
 15 |   {0 sts  : Nat}
 16 |   state   : PIx p
 17 |   stack   : PST p
 18 |   dfa     : PStepper sts p
 19 |   cur     : PByteStep sts p
 20 |   tok     : Maybe (PStep p)
 21 |
 22 | export
 23 | init : (p : P1 q e a) -> F1 q (LexState p)
 24 | init p t =
 25 |  let stck # t := p.stck t
 26 |      L _ dfa  := p.lex `at` p.init
 27 |   in LST p.init stck dfa (dfa `at` 0) Nothing # t
 28 |
 29 | ||| Result of a partial lexing step: In such a step, we lex
 30 | ||| till the end of a chunk of bytes, allowing for a remainder of
 31 | ||| bytes that could not yet be identified as a tokens.
 32 | public export
 33 | 0 PartRes : (p : P1 q e a) -> Type
 34 | PartRes p = F1 q (Either e (LexState p, Maybe a))
 35 |
 36 | export
 37 | pparseFrom :
 38 |      (p      : P1 q e a)
 39 |   -> (st     : LexState p)
 40 |   -> (pos    : Nat)
 41 |   -> {auto x : Ix pos n}
 42 |   -> IBuffer n
 43 |   -> PartRes p
 44 |
 45 | export
 46 | pparseBytes : (p : P1 q e a) -> LexState p -> ByteString -> PartRes p
 47 | pparseBytes p st (BS s $ BV buf off lte) =
 48 |   pparseFrom p st s {x = offsetToIx off} (take (off+s) buf)
 49 |
 50 | --------------------------------------------------------------------------------
 51 | -- Partial run loop
 52 | --------------------------------------------------------------------------------
 53 |
 54 | parameters {0 q,e,a : Type}
 55 |            {0 n     : Nat}
 56 |            (parser  : P1 q e a)
 57 |            (stck    : PST parser)
 58 |            (buf     : IBuffer n)
 59 |            (bytes   : Ref q ByteString)
 60 |
 61 |   pstep :
 62 |        (st          : PIx parser)
 63 |     -> (dfa         : PStepper k parser)          -- current finite automaton
 64 |     -> (cur         : PByteStep k parser)         -- current automaton state
 65 |     -> (prev        : ByteString)
 66 |     -> (from        : Ix m n)                     -- start of current token
 67 |     -> (pos         : Nat)                        -- reverse position in the byte array
 68 |     -> {auto x      : Ix pos n}                   -- position in the byte array
 69 |     -> {auto 0 lte2 : LTE (ixToNat from) (ixToNat x)}
 70 |     -> PartRes parser
 71 |
 72 |   psucc :
 73 |        (st          : PIx parser)
 74 |     -> (dfa         : PStepper k parser)          -- current finite automaton
 75 |     -> (cur         : PByteStep k parser)         -- current automaton state
 76 |     -> (prev        : ByteString)
 77 |     -> (last        : PStep parser)               -- last encountered terminal state
 78 |     -> (from        : Ix m n)                     -- start of current token
 79 |     -> (pos         : Nat)                        -- reverse position in the byte array
 80 |     -> {auto x      : Ix pos n}                   -- position in the byte array
 81 |     -> {auto 0 lte2 : LTE (ixToNat from) (ixToNat x)}
 82 |     -> PartRes parser
 83 |
 84 |   -- Accumulates lexemes by applying the maximum munch strategy:
 85 |   -- The largest matched lexeme is consumed and kept.
 86 |   -- This consumes at least one byte for the next token and
 87 |   -- immediately aborts with an error in case the current
 88 |   -- byte leads to the zero state.
 89 |   ploop : PIx parser -> (pos : Nat) -> (x : Ix pos n) => PartRes parser
 90 |   ploop st 0     t =
 91 |    let mv  # t := P1.chunk parser stck t
 92 |        L _ dfa := parser.lex `at` st
 93 |        _   # t := write1 bytes empty t
 94 |     in Right (LST st stck dfa (dfa `at` 0) Nothing, mv) # t
 95 |   ploop st (S k) t =
 96 |    let L _ dfa := parser.lex `at` st
 97 |        cur     := dfa `at` 0
 98 |     in case cur `atByte` (buf `ix` k) of
 99 |          Done f       =>
100 |           let _  # t := writeBS buf x k bytes t
101 |               s2 # t := f.run st stck t
102 |            in ploop s2 k t
103 |          Move   nxt f => psucc st dfa (dfa `at` nxt) empty f   x k t
104 |          MoveE  nxt   => pstep st dfa (dfa `at` nxt) empty     x k t
105 |          _           =>
106 |           let _  # t := writeBS buf x k bytes t
107 |            in fail parser st stck t
108 |
109 |   psucc st dfa cur prev f from 0 t =
110 |    let m # t := P1.chunk parser stck t
111 |        _ # t := writeBSP prev buf from 0 bytes t
112 |     in Right (LST st stck dfa cur $ Just f, m) # t
113 |   psucc st dfa cur prev f from (S k) t =
114 |    let byte := buf `ix` k
115 |     in case cur `atByte` byte of
116 |          Keep         => psucc st dfa cur prev f from k t
117 |          Done f       =>
118 |           let _  # t := writeBSP prev buf from k bytes t
119 |               s2 # t := f.run st stck t
120 |            in ploop s2 k t
121 |          Move   nxt f => psucc st dfa (dfa `at` nxt) prev f from k t
122 |          MoveE  nxt   => pstep st dfa (dfa `at` nxt) prev   from k t
123 |          Bottom       =>
124 |           let _  # t := writeBSP prev buf from (S k) bytes t
125 |               s2 # t := f.run st stck t
126 |            in ploop s2 (S k) t
127 |
128 |   pstep st dfa cur prev from 0 t =
129 |    let m # t := P1.chunk parser stck t
130 |        _ # t := writeBSP prev buf from 0 bytes t
131 |     in Right (LST st stck dfa cur Nothing, m) # t
132 |   pstep st dfa cur prev from (S k) t =
133 |    let byte := buf `ix` k
134 |     in case cur `atByte` byte of
135 |          Keep         => pstep st dfa cur prev from k t
136 |          Done f       =>
137 |           let _  # t := writeBSP prev buf from k bytes t
138 |               s2 # t := f.run st stck t
139 |            in ploop s2 k t
140 |          Move   nxt f => psucc st dfa (dfa `at` nxt) prev f from k t
141 |          MoveE  nxt   => pstep st dfa (dfa `at` nxt) prev   from k t
142 |          Bottom       =>
143 |           let _  # t := writeBSP prev buf from k bytes t
144 |            in fail parser st stck t
145 |
146 | pparseFrom p lst@(LST st sk dfa cur tok) pos buf t =
147 |   case pos of
148 |     0   => Right (lst, Nothing) # t
149 |     S k =>
150 |      let byte     := buf `ix` k
151 |          bytes    := bytes @{p.hasb} sk
152 |          prev # t := read1 bytes t
153 |       in case cur `atByte` byte of
154 |            Keep         => case tok of
155 |              Just f  => psucc p sk buf bytes st dfa cur prev f x k t
156 |              Nothing => pstep p sk buf bytes st dfa cur prev   x k t
157 |            Done f       =>
158 |             let _  # t := writeBSP prev buf x k bytes t
159 |                 s2 # t := f.run st sk t
160 |              in ploop p sk buf bytes s2 k t
161 |            Move   nxt f => psucc p sk buf bytes st dfa (dfa `at` nxt) prev f x k t
162 |            MoveE  nxt   => pstep p sk buf bytes st dfa (dfa `at` nxt) prev   x k t
163 |            Bottom     => case tok of
164 |              Just f  => let s2 # t := f.run st sk t in ploop p sk buf bytes s2 (S k) t
165 |              Nothing => fail p st sk t
166 |