0 | module Text.ILex.Lexer
  1 |
  2 | import public Data.Array
  3 | import public Data.List
  4 | import public Data.Prim.Bits32
  5 | import public Text.ILex.RExp
  6 |
  7 | import Control.Monad.State
  8 |
  9 | import Data.ByteString
 10 | import Data.Linear.Traverse1
 11 | import Data.SortedMap as SM
 12 | import Derive.Prelude
 13 |
 14 | import Text.ILex.Char.UTF8
 15 | import Text.ILex.Internal.DFA
 16 | import Text.ILex.Internal.Types
 17 |
 18 | %default total
 19 | %language ElabReflection
 20 |
 21 | public export
 22 | record Index (n : Bits32) where
 23 |   constructor I
 24 |   val : Bits32
 25 |   {auto 0 prf : val < n}
 26 |
 27 | %runElab deriveIndexed "Index" [Show,Eq,Ord]
 28 |
 29 | export
 30 | toIndex : {r : _} -> Bits32 -> Maybe (Index r)
 31 | toIndex n =
 32 |   case lt n r of
 33 |     Nothing0 => Nothing
 34 |     Just0 v  => Just (I n)
 35 |
 36 | public export
 37 | fromInteger : (n : Integer) -> (0 p : cast n < r) => Index r
 38 | fromInteger n = I (cast n)
 39 |
 40 | public export
 41 | Ini : (0 prf : 0 < n) => Index n
 42 | Ini = I 0
 43 |
 44 | public export
 45 | record Env (q : Type) (s : Type -> Type) where
 46 |   constructor E
 47 |   state : s q
 48 |   1 tok : T1 q
 49 |
 50 | public export
 51 | 0 Step1 : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
 52 | Step1 q r s = s q -> F1 q (Index r)
 53 |
 54 | public export
 55 | 0 Run1 : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
 56 | Run1 q r s = (1 sk : Env q s) -> R1 q (Index r)
 57 |
 58 | public export
 59 | 0 Ign1 : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
 60 | Ign1 q r s = (1 sk : Env q s) -> R1 q ()
 61 |
 62 | public export
 63 | data Step : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type where
 64 |   Run : Run1 q r s -> Step q r s
 65 |   Ign : Ign1 q r s -> Step q r s
 66 |   Err : Step q r s
 67 |
 68 | export %inline
 69 | toState : Index r -> Step q r s
 70 | toState v = Run $ \(E _ t) => v # t
 71 |
 72 | public export
 73 | data Transition :
 74 |      (n : Nat)
 75 |   -> (q : Type)
 76 |   -> (r : Bits32)
 77 |   -> (s : Type -> Type)
 78 |   -> Type where
 79 |   Keep   : Transition n q r s
 80 |   Done   : Run1 q r s -> Transition n q r s
 81 |   Ignore : Ign1 q r s -> Transition n q r s
 82 |   Move   : Fin (S n) -> Run1 q r s -> Transition n q r s
 83 |   MoveI  : Fin (S n) -> Ign1 q r s -> Transition n q r s
 84 |   MoveE  : Fin (S n) -> Transition n q r s
 85 |   Bottom : Transition n q r s
 86 |
 87 | move : Step q r s -> Fin (S n) -> Transition n q r s
 88 | move (Run f) y = Move y f
 89 | move (Ign f) y = MoveI y f
 90 | move Err     y = Bottom
 91 |
 92 | done : Step q r s -> Transition n q r s
 93 | done (Run f) = Done f
 94 | done (Ign f) = Ignore f
 95 | done Err     = Bottom
 96 |
 97 | ||| An array of arrays describing a lexer's state machine.
 98 | public export
 99 | 0 ByteStep : Nat -> (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
100 | ByteStep n q r s = IArray 256 (Transition n q r s)
101 |
102 | ||| An array of arrays describing a lexer's state machine.
103 | public export
104 | 0 Stepper : Nat -> (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
105 | Stepper n q r s = IArray (S n) (ByteStep n q r s)
106 |
107 | ||| A discrete finite automaton (DFA) encoded as
108 | ||| an array of state transitions plus an array
109 | ||| describing the terminal token states.
110 | public export
111 | record DFA q r s where
112 |   constructor L
113 |   ||| Number of non-zero states in the automaton.
114 |   states : Nat
115 |
116 |   ||| State transitions matrix.
117 |   |||
118 |   ||| If `cur` is the current state (encoded as a `Fin (S states)`
119 |   ||| and `b` is the current input byte, the next state is determined
120 |   ||| by `next[cur][b]` (in pseudo C-syntax).
121 |   next   : Stepper states q r s
122 |
123 | --------------------------------------------------------------------------------
124 | -- Lexer Generator
125 | --------------------------------------------------------------------------------
126 |
127 | public export
128 | 0 Steps : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
129 | Steps q r s = TokenMap (Step q r s)
130 |
131 | emptyRow : ByteStep n q r s
132 | emptyRow = fill _ Bottom
133 |
134 | emptyDFA : DFA q r s
135 | emptyDFA = L 0 (fill _ emptyRow)
136 |
137 | -- Extracts the terminal state of a node
138 | -- `Left` : This is a final node with no more state transitions
139 | -- `Right`: This node has additional state transitions
140 | terminals : SortedMap Nat a -> Node -> Maybe (Nat, Either a a)
141 | terminals m (N n (t::_) []) = ((n,) . Left) <$> lookup t m
142 | terminals m (N n (t::_) _)  = ((n,) . Right) <$> lookup t m
143 | terminals _ _               = Nothing
144 |
145 | nonFinal : SortedMap Nat (Either a a) -> Node -> Maybe Node
146 | nonFinal m n =
147 |   case lookup n.pos m of
148 |     Just (Left _) => Nothing
149 |     _             => Just n
150 |
151 | index : {n : _} -> List (Nat,Node) -> SortedMap Nat (Fin (S n))
152 | index ns = SM.fromList $ mapMaybe (\(x,n) => (n.pos,) <$> tryNatToFin x) ns
153 |
154 | node :
155 |      SortedMap Nat (Either (Step q r s) (Step q r s))
156 |   -> (index : SortedMap Nat (Fin (S n)))
157 |   -> (node  : (Nat,Node))
158 |   -> (Nat, ByteStep n q r s)
159 | node terms index (ix, N me _ out) =
160 |   (ix, fromPairs _ Bottom $ mapMaybe pair (out >>= transitions))
161 |   where
162 |     pair : (Bits8,Nat) -> Maybe (Nat, Transition n q r s)
163 |     pair (b,tgt) =
164 |       case lookup tgt terms of
165 |         Nothing        => case tgt == me of
166 |           True  => Just (cast b, Keep)
167 |           False => ((cast b,) . MoveE) <$> lookup tgt index
168 |         Just (Left f)  => Just (cast b, done f)
169 |         Just (Right f) => case tgt == me of
170 |           True  => Just (cast b, Keep)
171 |           False => ((cast b,) . (move f)) <$> lookup tgt index
172 |
173 | ||| A DFA operating on raw bytes.
174 | export
175 | byteDFA : (m : TokenMap8 (Step q r s)) -> DFA q r s
176 | byteDFA m =
177 |   let M tms graph := assert_total $ machine (toDFA m)
178 |       terms       := SM.fromList (mapMaybe (terminals tms . snd) graph)
179 |       nodes       := zipWithIndex $ mapMaybe (nonFinal terms . snd) graph
180 |       S len       := length nodes | 0 => emptyDFA
181 |       ix          := index nodes
182 |       trans       := fromPairs (S len) emptyRow (map (node terms ix) nodes)
183 |    in L len trans
184 |
185 | ||| A utf-8 aware DFA operating on text.
186 | export
187 | dfa : Steps q r s -> DFA q r s
188 | dfa = byteDFA . map toUTF8
189 |