
   0 | module Text.ILex.Parser
   1 | 
   2 | import Derive.Prelude
   3 | import Data.Buffer
   4 | import Syntax.T1
   5 | import public Data.Prim.Bits32
   6 | import public Data.ByteString
   7 | import public Data.Linear.Ref1
   8 | import public Text.ByteBounds
   9 | import public Text.ParseError
  10 | import public Text.ILex.RExp
  11 | import public Text.ILex.Lexer
  12 | 
  13 | %default total
  14 | %language ElabReflection
  15 | 
  16 | --------------------------------------------------------------------------------
  17 | -- FFI
  18 | --------------------------------------------------------------------------------
  19 | 
  20 | %foreign "scheme:(lambda (x i) (make-vector x i))"
  21 |          "javascript:lambda:(i,x,w) => Array(i).fill(x)"
  22 | prim__newMachine : Bits32 -> AnyPtr -> PrimIO AnyPtr
  23 | 
  24 | %foreign "scheme:(lambda (x i) (vector-ref x i))"
  25 |          "javascript:lambda:(x,bi) => x[bi]"
  26 | prim__machineGet : AnyPtr -> Bits32 -> AnyPtr
  27 | 
  28 | %foreign "scheme:(lambda (x i w) (vector-set! x i w))"
  29 |          "javascript:lambda:(x,i,w) => {x[i] = w}"
  30 | prim__machineSet : AnyPtr -> Bits32 -> (val : AnyPtr) -> PrimIO ()
  31 | 
  32 | export
  33 | record Arr32 (n : Bits32) (a : Type) where
  34 |   constructor A32
  35 |   ptr : AnyPtr
  36 | 
  37 | export %inline
  38 | at : Arr32 n a -> Index n -> a
  39 | at (A32 p) x = believe_me $ prim__machineGet p x.val
  40 | 
  41 | public export
  42 | record Entry (n : Bits32) (a : Type) where
  43 |   constructor E
  44 |   index : Index n
  45 |   value : a
  46 | 
  47 | export %inline
  48 | entry : Cast t (Index n) => t -> a -> Entry n a
  49 | entry x v = E (cast x) v
  50 | 
  51 | export
  52 | arr32 : (n : Bits32) -> (dflt : a) -> List (Entry n a) -> Arr32 n a
  53 | arr32 n dflt es =
  54 |   run1 $ \t =>
  55 |    let p # t := ffi (prim__newMachine n (believe_me dflt)) t
  56 |     in fill es p t
  57 | 
  58 |   where
  59 |     fill : List (Entry n a) -> AnyPtr -> F1 x (Arr32 n a)
  60 |     fill []             p t = A32 p # t
  61 |     fill (E x d :: xs) p t =
  62 |      let _ # t := ffi (prim__machineSet p x.val (believe_me d)) t
  63 |       in fill xs p t
  64 | 
  65 | public export
  66 | 0 Lex1 : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
  67 | Lex1 q r s = Arr32 r (DFA q r s)
  68 | 
  69 | --------------------------------------------------------------------------------
  70 | -- HasBytes Interface
  71 | --------------------------------------------------------------------------------
  72 | 
  73 | public export
  74 | record LTENat (n : Nat) where
  75 |   constructor LN
  76 |   val : Nat
  77 |   {auto 0 prf : LTE val n}
  78 | 
  79 | export %inline
  80 | lteNat : (0 m : Nat) -> Ix m n => LTENat n
  81 | lteNat _ @{x} = LN (ixToNat x) @{ixLTE x}
  82 | 
  83 | export %inline
  84 | first : (0 n : Nat) -> LTENat n
  85 | first n = LN 0
  86 | 
  87 | export %inline
  88 | last : (n : Nat) -> LTENat n
  89 | last n = LN n
  90 | 
  91 | export %inline
  92 | bytesFromTill : IBuffer n -> (from, till : LTENat n) -> ByteString
  93 | bytesFromTill buf (LN from @{lt1}) (LN till @{lt2}) =
  94 |   BS (till `minus` from) (BV buf from $ plusMinusBothLTE _ _ lt1 lt2)
  95 | 
  96 | export %inline
  97 | stringFromTill : IBuffer n -> (from, till : LTENat n) -> String
  98 | stringFromTill buf (LN from @{lt1}) (LN till @{lt2}) =
  99 |   toString buf from (till `minus` from) @{plusMinusBothLTE _ _ lt1 lt2}
 100 | 
 101 | ||| An interface for mutable parser stacks `s` that facilitates
 102 | ||| parsing string tokens containing escape sequences.
 103 | public export
 104 | interface HasBytes (0 s : Type -> Type) where
 105 |   constructor MkHB
 106 |   copy :
 107 |        (size, offset : Nat)
 108 |     -> ByteString
 109 |     -> IBuffer size
 110 |     -> (from, till : Ref q (LTENat size))
 111 |     -> s q
 112 |     -> s q
 113 | 
 114 |   bufSize   : s q -> Nat
 115 | 
 116 |   ||| Remainder of the previous bytestring that should
 117 |   ||| be used as the beginning of the current token.
 118 |   prev      : s q -> ByteString
 119 | 
 120 |   ||| The byte vector currently being processed.
 121 |   cur       : (v : s q) -> IBuffer (bufSize v)
 122 | 
 123 |   ||| Absolute position of the first byte of `prev`.
 124 |   prevOffset    : s q -> Nat
 125 | 
 126 |   ||| Absolute position of the first byte of `cur`
 127 |   ||| (this equals `prevOffset + prev.size` but should be
 128 |   ||| provided as a separate field for reasons of efficiency)
 129 |   curOffset    : s q -> Nat
 130 | 
 131 |   ||| Lower relative token bound (lower position in `cur`)
 132 |   from         : (v : s q) -> Ref q (LTENat (bufSize v))
 133 | 
 134 |   ||| Next relative token bound (upser position + 1 in `cur`)
 135 |   till         : (v : s q) -> Ref q (LTENat (bufSize v))
 136 | 
 137 |   ||| Stack of positions used to keep track of the positions of
 138 |   ||| opening parentheses and brackets.
 139 |   positions : s q -> Ref q (SnocList BytePos)
 140 | 
 141 | ||| Returns the current substring of the byte vector
 142 | ||| (corresponding to the position and length of the current
 143 | ||| token).
 144 | |||
 145 | ||| The remainder of the previous bytestring is prefixed in case
 146 | ||| we are currently at position zero.
 147 | export %inline
 148 | getBytes : HasBytes s => (sk : s q) => F1 q ByteString
 149 | getBytes t =
 150 |   let rf # t := read1 (from sk) t
 151 |       rt # t := read1 (till sk) t
 152 |    in case rf.val of
 153 |         0 => (prev sk <+> bytesFromTill (cur sk) rf rt) # t
 154 |         _ => bytesFromTill (cur sk) rf rt # t
 155 | 
 156 | export %inline
 157 | getString : HasBytes s => (sk : s q) => F1 q String
 158 | getString t =
 159 |   let rf # t := read1 (from sk) t
 160 |       rt # t := read1 (till sk) t
 161 |    in case rf.val of
 162 |         0 => (toString $ prev sk <+> bytesFromTill (cur sk) rf rt) # t
 163 |         _ => stringFromTill (cur sk) rf rt # t
 164 | 
 165 | export %inline
 166 | toFinalPos : HasBytes s => (sk : s q) => F1' q
 167 | toFinalPos t =
 168 |  let _ # t := write1 (from sk) (last $ bufSize sk) t
 169 |   in write1 (till sk) (last $ bufSize sk) t
 170 | 
 171 | ||| A parser is a system of automata, where each
 172 | ||| lexicographic token determines the next automaton
 173 | ||| state plus lexer to use.
 174 | public export
 175 | record P1 (q,e : Type) (a : Type) where
 176 |   constructor P
 177 |   {states    : Bits32}
 178 |   {0 state   : Type -> Type}
 179 |   init       : Index states
 180 |   stck       : (size : Nat) -> IBuffer size -> F1 q (state q)
 181 |   lex        : Lex1 q states state
 182 |   chunk      : state q -> F1 q (Maybe a)
 183 |   err        : Arr32 states (state q -> F1 q e)
 184 |   eoi        : Index states -> state q -> F1 q (Either e a)
 185 |   {auto hasb : HasBytes state}
 186 | 
 187 | public export
 188 | 0 PST : (p : P1 q e a) -> Type
 189 | PST p = p.state q
 190 | 
 191 | public export
 192 | 0 PIx : (p : P1 q e a) -> Type
 193 | PIx p = Index p.states
 194 | 
 195 | public export
 196 | 0 PStep : (p : P1 q e a) -> Type
 197 | PStep p = Step q p.states p.state
 198 | 
 199 | public export
 200 | 0 PRun : (p : P1 q e a) -> Type
 201 | PRun p = Run1 q p.states p.state
 202 | 
 203 | ||| An array of arrays describing a lexer's state machine.
 204 | public export
 205 | 0 PByteStep : Nat -> (p : P1 q e a) -> Type
 206 | PByteStep n p = IArray 256 (Transition n q p.states p.state)
 207 | 
 208 | ||| An array of arrays describing a lexer's state machine.
 209 | public export
 210 | 0 PStepper : Nat -> (p : P1 q e a) -> Type
 211 | PStepper n p = IArray (S n) (PByteStep n p)
 212 | 
 213 | export
 214 | arrFail :
 215 |      (0 s : Type -> Type)
 216 |   -> Arr32 r (s q -> F1 q e)
 217 |   -> Index r
 218 |   -> s q
 219 |   -> F1 q (Either e x)
 220 | arrFail s arr ix st t =
 221 |  let eo      := arr `at` ix
 222 |      err # t := eo st t
 223 |   in Left err # t
 224 | 
 225 | export %inline
 226 | fail : (p : P1 q e a) -> PIx p -> PST p -> F1 q (Either e x)
 227 | fail p = arrFail p.state p.err
 228 | 
 229 | export %inline
 230 | failFun1 : (p : P1 q e a) -> PIx p -> Fun1 q p.state (Either e x)
 231 | failFun1 p st (E sk t) = arrFail p.state p.err st sk t
 232 | 
 233 | public export
 234 | 0 Parser1 : (e : Type) -> (a : Type) -> Type
 235 | Parser1 e a = {0 q : _} -> P1 q e a
 236 | 
 237 | export %inline
 238 | lex1 : {r : _} -> List (Entry r (DFA q r s)) -> Lex1 q r s
 239 | lex1 es = arr32 r (dfa []) es
 240 |