0 | module Text.ILex.Parser
  1 |
  2 | import Derive.Prelude
  3 | import Data.Buffer
  4 | import public Data.Prim.Bits32
  5 | import public Data.ByteString
  6 | import public Data.Linear.Ref1
  7 | import public Text.Bounds
  8 | import public Text.ParseError
  9 | import public Text.ILex.RExp
 10 | import public Text.ILex.Lexer
 11 |
 12 | %default total
 13 | %language ElabReflection
 14 |
 15 | --------------------------------------------------------------------------------
 16 | -- FFI
 17 | --------------------------------------------------------------------------------
 18 |
 19 | %foreign "scheme:(lambda (x i) (make-vector x i))"
 20 |          "javascript:lambda:(i,x,w) => Array(i).fill(x)"
 21 | prim__newMachine : Bits32 -> AnyPtr -> PrimIO AnyPtr
 22 |
 23 | %foreign "scheme:(lambda (x i) (vector-ref x i))"
 24 |          "javascript:lambda:(x,bi) => x[bi]"
 25 | prim__machineGet : AnyPtr -> Bits32 -> AnyPtr
 26 |
 27 | %foreign "scheme:(lambda (x i w) (vector-set! x i w))"
 28 |          "javascript:lambda:(x,i,w) => {x[i] = w}"
 29 | prim__machineSet : AnyPtr -> Bits32 -> (val : AnyPtr) -> PrimIO ()
 30 |
 31 | ||| An interface for mutable parser stacks `s` that allows
 32 | ||| the parse loop to register the byte string corresponding to
 33 | ||| the currently parsed token.
 34 | public export
 35 | interface HasBytes (0 s : Type -> Type) where
 36 |   constructor MkHB
 37 |   bytes : s q -> Ref q ByteString
 38 |
 39 | export
 40 | record Arr32 (n : Bits32) (a : Type) where
 41 |   constructor A32
 42 |   ptr : AnyPtr
 43 |
 44 | export %inline
 45 | at : Arr32 n a -> Index n -> a
 46 | at (A32 p) x = believe_me $ prim__machineGet p x.val
 47 |
 48 | public export
 49 | record Entry (n : Bits32) (a : Type) where
 50 |   constructor E
 51 |   index : Index n
 52 |   value : a
 53 |
 54 | export %inline
 55 | entry : Cast t (Index n) => t -> a -> Entry n a
 56 | entry x v = E (cast x) v
 57 |
 58 | export
 59 | arr32 : (n : Bits32) -> (dflt : a) -> List (Entry n a) -> Arr32 n a
 60 | arr32 n dflt es =
 61 |   run1 $ \t =>
 62 |    let p # t := ffi (prim__newMachine n (believe_me dflt)) t
 63 |     in fill es p t
 64 |
 65 |   where
 66 |     fill : List (Entry n a) -> AnyPtr -> F1 x (Arr32 n a)
 67 |     fill []             p t = A32 p # t
 68 |     fill (E x d :: xs) p t =
 69 |      let _ # t := ffi (prim__machineSet p x.val (believe_me d)) t
 70 |       in fill xs p t
 71 |
 72 | public export
 73 | 0 Lex1 : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
 74 | Lex1 q r s = Arr32 r (DFA q r s)
 75 |
 76 | ||| A parser is a system of automata, where each
 77 | ||| lexicographic token determines the next automaton
 78 | ||| state plus lexer to use.
 79 | public export
 80 | record P1 (q,e : Type) (a : Type) where
 81 |   constructor P
 82 |   {states    : Bits32}
 83 |   {0 state   : Type -> Type}
 84 |   init       : Index states
 85 |   stck       : F1 q (state q)
 86 |   lex        : Lex1 q states state
 87 |   chunk      : state q -> F1 q (Maybe a)
 88 |   err        : Arr32 states (state q -> F1 q e)
 89 |   eoi        : Index states -> state q -> F1 q (Either e a)
 90 |   {auto hasb : HasBytes state}
 91 |
 92 | public export
 93 | 0 PST : (p : P1 q e a) -> Type
 94 | PST p = p.state q
 95 |
 96 | public export
 97 | 0 PIx : (p : P1 q e a) -> Type
 98 | PIx p = Index p.states
 99 |
100 | public export
101 | 0 PStep : (p : P1 q e a) -> Type
102 | PStep p = Step1 q p.states p.state
103 |
104 | ||| An array of arrays describing a lexer's state machine.
105 | public export
106 | 0 PByteStep : Nat -> (p : P1 q e a) -> Type
107 | PByteStep n p = IArray 256 (Transition n q p.states p.state)
108 |
109 | ||| An array of arrays describing a lexer's state machine.
110 | public export
111 | 0 PStepper : Nat -> (p : P1 q e a) -> Type
112 | PStepper n p = IArray (S n) (PByteStep n p)
113 |
114 | export
115 | arrFail :
116 |      (0 s : Type -> Type)
117 |   -> Arr32 r (s q -> F1 q e)
118 |   -> Index r
119 |   -> s q
120 |   -> F1 q (Either e x)
121 | arrFail s arr ix st t =
122 |  let eo      := arr `at` ix
123 |      err # t := eo st t
124 |   in Left err # t
125 |
126 | export %inline
127 | fail : (p : P1 q e a) -> PIx p -> PST p -> F1 q (Either e x)
128 | fail p = arrFail p.state $ p.err
129 |
130 | export
131 | lastStep : (p : P1 q e a) -> PStep p -> PIx p -> PST p -> F1 q (Either e a)
132 | lastStep p f st stck t =
133 |   let r # t := f (stck # t)
134 |       _ # t := write1 (bytes @{p.hasb} stck) "" t
135 |    in p.eoi r stck t
136 |
137 | public export
138 | 0 Parser1 : (e : Type) -> (a : Type) -> Type
139 | Parser1 e a = {0 q : _} -> P1 q e a
140 |
141 | export %inline
142 | lex1 : {r : _} -> List (Entry r (DFA q r s)) -> Lex1 q r s
143 | lex1 es = arr32 r (dfa []) es
144 |