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