
   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       => let s2 # t := f (stck # t) in ploop s2 k t
 100 |          Move   nxt f => psucc st dfa (dfa `at` nxt) empty f   x k t
 101 |          MoveE  nxt   => pstep st dfa (dfa `at` nxt) empty     x k t
 102 |          DoneBS f     =>
 103 |           let _  # t := writeBS buf x k bytes t
 104 |               s2 # t := f (stck # t)
 105 |            in ploop s2 k t
 106 |          _           =>
 107 |           let _  # t := writeBS buf x k bytes t
 108 |            in fail parser st stck t
 109 | 
 110 |   psucc st dfa cur prev f from 0 t =
 111 |    let m # t := P1.chunk parser stck t
 112 |        _ # t := writeBSP prev buf from 0 bytes t
 113 |     in Right (LST st stck dfa cur $ Just f, m) # t
 114 |   psucc st dfa cur prev f from (S k) t =
 115 |    let byte := buf `ix` k
 116 |     in case cur `atByte` byte of
 117 |          Keep         => psucc st dfa cur prev f from k t
 118 |          Done f       => let s2 # t := f (stck # t) in ploop s2 k t
 119 |          Move   nxt f => psucc st dfa (dfa `at` nxt) prev f from k t
 120 |          MoveE  nxt   => pstep st dfa (dfa `at` nxt) prev   from k t
 121 |          DoneBS f     =>
 122 |           let _  # t := writeBSP prev buf from k bytes t
 123 |               s2 # t := f (stck # t)
 124 |            in ploop s2 k t
 125 |          Bottom       =>
 126 |           let _  # t := writeBSP prev buf from (S k) bytes t
 127 |               s2 # t := f (stck # t)
 128 |            in ploop s2 (S k) t
 129 | 
 130 |   pstep st dfa cur prev from 0 t =
 131 |    let m # t := P1.chunk parser stck t
 132 |        _ # t := writeBSP prev buf from 0 bytes t
 133 |     in Right (LST st stck dfa cur Nothing, m) # t
 134 |   pstep st dfa cur prev from (S k) t =
 135 |    let byte := buf `ix` k
 136 |     in case cur `atByte` byte of
 137 |          Keep         => pstep st dfa cur prev from k t
 138 |          Done f       => let s2 # t := f (stck # t) in ploop s2 k t
 139 |          Move   nxt f => psucc st dfa (dfa `at` nxt) prev f from k t
 140 |          MoveE  nxt   => pstep st dfa (dfa `at` nxt) prev   from k t
 141 |          DoneBS f     =>
 142 |           let _  # t := writeBSP prev buf from k bytes t
 143 |               s2 # t := f (stck # t)
 144 |            in ploop s2 k t
 145 |          Bottom       =>
 146 |           let _  # t := writeBSP prev buf from k bytes t
 147 |            in fail parser st stck t
 148 | 
 149 | pparseFrom p lst@(LST st sk dfa cur tok) pos buf t =
 150 |   case pos of
 151 |     0   => Right (lst, Nothing) # t
 152 |     S k =>
 153 |      let byte     := buf `ix` k
 154 |          bytes    := bytes @{p.hasb} sk
 155 |          prev # t := read1 bytes t
 156 |       in case cur `atByte` byte of
 157 |            Keep         => case tok of
 158 |              Just f  => psucc p sk buf bytes st dfa cur prev f x k t
 159 |              Nothing => pstep p sk buf bytes st dfa cur prev   x k t
 160 |            Done   f     => let s2 # t := f (sk # t) in ploop p sk buf bytes s2 k t
 161 |            DoneBS f     =>
 162 |             let _  # t := writeBSP prev buf x k bytes t
 163 |                 s2 # t := f (sk # t)
 164 |              in ploop p sk buf bytes s2 k t
 165 |            Move   nxt f => psucc p sk buf bytes st dfa (dfa `at` nxt) prev f x k t
 166 |            MoveE  nxt   => pstep p sk buf bytes st dfa (dfa `at` nxt) prev   x k t
 167 |            Bottom     => case tok of
 168 |              Just f  => let s2 # t := f (sk # t) in ploop p sk buf bytes s2 (S k) t
 169 |              Nothing => fail p st sk t
 170 |