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