
   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 | runFrom :
  11 |      {n      : Nat}
  12 |   -> (l      : Parser1 e a)
  13 |   -> (pos    : Nat)
  14 |   -> {auto x : Ix pos n}
  15 |   -> IBuffer n
  16 |   -> Either e a
  17 | 
  18 | ||| Tries to parse a byte vector into a value.
  19 | export %inline
  20 | run : {n : _} -> Parser1 e a -> IBuffer n -> Either e a
  21 | run l buf = runFrom l n buf
  22 | 
  23 | ||| Like `run` but processes a UTF-8 string instead.
  24 | export %inline
  25 | runString : Parser1 e a -> String -> Either e a
  26 | runString l s = run l (fromString s)
  27 | 
  28 | ||| Like `run` but processes a `ByteString` instead.
  29 | export
  30 | runBytes : Parser1 e a -> ByteString -> Either e a
  31 | runBytes l (BS s $ BV buf off lte) =
  32 |   runFrom l s {x = offsetToIx off} (take (off+s) buf)
  33 | 
  34 | ||| Like `run` but fails with a proper parse error
  35 | ||| including error bounds and highlighting of
  36 | ||| the section where an error occurred.
  37 | export %inline
  38 | parse :
  39 |      {n : _}
  40 |   -> Parser1 (BoundedErr e) a
  41 |   -> Origin
  42 |   -> IBuffer n
  43 |   -> Either (ParseError e) a
  44 | parse l o buf = mapFst (toParseError o (toString buf 0 n)) (run l buf)
  45 | 
  46 | ||| Like `parse` but processes a UTF-8 string instead.
  47 | export %inline
  48 | parseString :
  49 |      Parser1 (BoundedErr e) a
  50 |   -> Origin
  51 |   -> String
  52 |   -> Either (ParseError e) a
  53 | parseString l o s = parse l o (fromString s)
  54 | 
  55 | ||| Like `parse` but processes a `ByteString` instead.
  56 | export %inline
  57 | parseBytes :
  58 |      Parser1 (BoundedErr e) a
  59 |   -> Origin
  60 |   -> ByteString
  61 |   -> Either (ParseError e) a
  62 | parseBytes l o bs = mapFst (toParseError o (toString bs)) (runBytes l bs)
  63 | 
  64 | --------------------------------------------------------------------------------
  65 | -- Lexer run loop
  66 | --------------------------------------------------------------------------------
  67 | 
  68 | parameters {0 q,e,a : Type}
  69 |            {0 n     : Nat}
  70 |            (parser  : P1 q e a)
  71 |            (stck    : PST parser)
  72 |            (buf     : IBuffer n)
  73 |            (bytes   : Ref q ByteString)
  74 | 
  75 |   step :
  76 |        (st          : PIx parser)
  77 |     -> (dfa         : PStepper k parser)
  78 |     -> (cur         : PByteStep k parser)
  79 |     -> (from        : Ix m n)
  80 |     -> (pos         : Nat)
  81 |     -> {auto x      : Ix pos n}
  82 |     -> {auto 0 lte2 : LTE (ixToNat from) (ixToNat x)}
  83 |     -> F1 q (Either e a)
  84 | 
  85 |   succ :
  86 |        (st          : PIx parser)
  87 |     -> (dfa         : PStepper k parser)
  88 |     -> (cur         : PByteStep k parser)
  89 |     -> (last        : PStep parser)
  90 |     -> (from        : Ix m n)
  91 |     -> (pos         : Nat)
  92 |     -> {auto x      : Ix pos n}
  93 |     -> {auto 0 lte2 : LTE (ixToNat from) (ixToNat x)}
  94 |     -> F1 q (Either e a)
  95 | 
  96 |   loop : (st : PIx parser) -> (pos : Nat) -> (x : Ix pos n) => F1 q (Either e a)
  97 |   loop st 0     t =
  98 |    let _ # t := write1 bytes "" t
  99 |     in parser.eoi st stck t
 100 |   loop st (S k) t =
 101 |    let L _ dfa := parser.lex `at` st
 102 |        cur     := dfa `at` 0
 103 |     in case cur `atByte` (buf `ix` k) of
 104 |          Done f       => let s2 # t := f (stck # t) in loop s2 k t
 105 |          Move   nxt f => succ st dfa (dfa `at` nxt) f   x k t
 106 |          MoveE  nxt   => step st dfa (dfa `at` nxt)     x k t
 107 |          DoneBS f     =>
 108 |           let _  # t := writeBS buf x k bytes t
 109 |               s2 # t := f (stck # t)
 110 |            in loop s2 k t
 111 |          _            =>
 112 |           let _  # t := writeBS buf x k bytes t
 113 |            in fail parser st stck t
 114 | 
 115 |   succ st dfa cur f from 0     t =
 116 |    let _ # t := writeBS buf from 0 bytes t
 117 |     in lastStep parser f st stck t
 118 |   succ st dfa cur f from (S k) t =
 119 |    let byte := buf `ix` k
 120 |     in case cur `atByte` byte of
 121 |          Keep         => succ st dfa cur f from k t
 122 |          Done f       => let s2 # t := f (stck # t) in loop s2 k t
 123 |          Move   nxt f => succ st dfa (dfa `at` nxt) f from k t
 124 |          MoveE  nxt   => step st dfa (dfa `at` nxt)   from k t
 125 |          DoneBS f     =>
 126 |           let _  # t := writeBS buf from k bytes t
 127 |               s2 # t := f (stck # t)
 128 |            in loop s2 k t
 129 |          Bottom       =>
 130 |           let _  # t := writeBS buf from (S k) bytes t
 131 |               s2 # t := f (stck # t)
 132 |            in loop s2 (S k) t
 133 | 
 134 |   step st dfa cur from 0     t =
 135 |    let _ # t := writeBS buf from 0 bytes t
 136 |     in fail parser st stck t
 137 |   step st dfa cur from (S k) t =
 138 |    let byte := buf `ix` k
 139 |     in case cur `atByte` byte of
 140 |          Keep         => step st dfa cur from k t
 141 |          Done f       => let s2 # t := f (stck # t) in loop s2 k t
 142 |          Move   nxt f => succ st dfa (dfa `at` nxt) f from k t
 143 |          MoveE  nxt   => step st dfa (dfa `at` nxt)   from k t
 144 |          DoneBS f     =>
 145 |           let _  # t := writeBS buf from k bytes t
 146 |               s2 # t := f (stck # t)
 147 |            in loop s2 k t
 148 |          Bottom       =>
 149 |           let _  # t := writeBS buf from k bytes t
 150 |            in fail parser st stck t
 151 | 
 152 | runFrom p pos buf = run1 (go p)
 153 |   where
 154 |     go : P1 q e a -> F1 q (Either e a)
 155 |     go p t =
 156 |      let x # t := stck p t
 157 |       in loop p x buf (bytes @{p.hasb} x) p.init pos t
 158 |