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 | ||| An interface for mutable parser stacks `s` that facilitates
 74 | ||| parsing string tokens containing escape sequences.
 75 | public export
 76 | interface HasBytes (0 s : Type -> Type) where
 77 |   constructor MkHB
 78 |   ||| Returns the remainder of the previous bytestring that should
 79 |   ||| be used as the beginning of the current token.
 80 |   prev      : s q -> Ref q ByteString
 81 |
 82 |   ||| The byte vector currently being processed.
 83 |   cur       : s q -> Ref q ByteString
 84 |
 85 |   ||| Absolute start position of the current token from the beginning
 86 |   ||| of the whole byte stream processed so far.
 87 |   offset    : s q -> Ref q Nat
 88 |
 89 |   ||| Start position of the current token relative to `cur`.
 90 |   |||
 91 |   ||| If this is negative, the current token will also include
 92 |   ||| `prev`. Reference `len` will still hold the full length
 93 |   ||| of the token.
 94 |   relpos    : s q -> Ref q Integer
 95 |
 96 |   ||| Length of the current token
 97 |   len       : s q -> Ref q Nat
 98 |
 99 |   ||| Stack of positions used to keep track of the positions of
100 |   ||| opening parentheses and brackets.
101 |   positions : s q -> Ref q (SnocList BytePos)
102 |
103 | ||| Returns the current substring of the byte vector
104 | ||| (corresponding to the position and length of the current
105 | ||| token).
106 | |||
107 | ||| The remainder of the previous bytestring is prefixed in case
108 | ||| we are currently at position zero.
109 | export %inline
110 | getBytes : HasBytes s => (sk : s q) => F1 q ByteString
111 | getBytes = T1.do
112 |   bs   <- read1 (cur sk)
113 |   p    <- read1 (relpos sk)
114 |   l    <- read1 (len sk)
115 |   case prim__lt_Integer p 0 of
116 |     0 => pure (substring (cast p) l bs)
117 |     n => read1 (prev sk) >>= \pre =>
118 |            pure (pre <+> take (cast $ cast l + p) bs)
119 |
120 | ||| A parser is a system of automata, where each
121 | ||| lexicographic token determines the next automaton
122 | ||| state plus lexer to use.
123 | public export
124 | record P1 (q,e : Type) (a : Type) where
125 |   constructor P
126 |   {states    : Bits32}
127 |   {0 state   : Type -> Type}
128 |   init       : Index states
129 |   stck       : F1 q (state q)
130 |   lex        : Lex1 q states state
131 |   chunk      : state q -> F1 q (Maybe a)
132 |   err        : Arr32 states (state q -> F1 q e)
133 |   eoi        : Index states -> state q -> F1 q (Either e a)
134 |   {auto hasb : HasBytes state}
135 |
136 | public export
137 | 0 PST : (p : P1 q e a) -> Type
138 | PST p = p.state q
139 |
140 | public export
141 | 0 PIx : (p : P1 q e a) -> Type
142 | PIx p = Index p.states
143 |
144 | public export
145 | 0 PStep : (p : P1 q e a) -> Type
146 | PStep p = Step q p.states p.state
147 |
148 | public export
149 | 0 PRun : (p : P1 q e a) -> Type
150 | PRun p = Run1 q p.states p.state
151 |
152 | public export
153 | 0 PIgn : (p : P1 q e a) -> Type
154 | PIgn p = Ign1 q p.states p.state
155 |
156 | ||| An array of arrays describing a lexer's state machine.
157 | public export
158 | 0 PByteStep : Nat -> (p : P1 q e a) -> Type
159 | PByteStep n p = IArray 256 (Transition n q p.states p.state)
160 |
161 | ||| An array of arrays describing a lexer's state machine.
162 | public export
163 | 0 PStepper : Nat -> (p : P1 q e a) -> Type
164 | PStepper n p = IArray (S n) (PByteStep n p)
165 |
166 | export
167 | arrFail :
168 |      (0 s : Type -> Type)
169 |   -> Arr32 r (s q -> F1 q e)
170 |   -> Index r
171 |   -> s q
172 |   -> F1 q (Either e x)
173 | arrFail s arr ix st t =
174 |  let eo      := arr `at` ix
175 |      err # t := eo st t
176 |   in Left err # t
177 |
178 | export %inline
179 | fail : (p : P1 q e a) -> PIx p -> PST p -> F1 q (Either e x)
180 | fail p = arrFail p.state p.err
181 |
182 | public export
183 | 0 Parser1 : (e : Type) -> (a : Type) -> Type
184 | Parser1 e a = {0 q : _} -> P1 q e a
185 |
186 | export %inline
187 | lex1 : {r : _} -> List (Entry r (DFA q r s)) -> Lex1 q r s
188 | lex1 es = arr32 r (dfa []) es
189 |