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 | 0 Step1 : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
 46 | Step1 q r s = (1 sk : R1 q (s q)) -> R1 q (Index r)
 47 |
 48 | export %inline
 49 | toState : Index r -> Step1 q r s
 50 | toState v = \(_ # t) => v # t
 51 |
 52 | public export
 53 | data Transition :
 54 |      (n : Nat)
 55 |   -> (q : Type)
 56 |   -> (r : Bits32)
 57 |   -> (s : Type -> Type)
 58 |   -> Type where
 59 |   Keep   : Transition n q r s
 60 |   Done   : Step1 q r s -> Transition n q r s
 61 |   DoneBS : Step1 q r s -> Transition n q r s
 62 |   Move   : Fin (S n) -> Step1 q r s -> Transition n q r s
 63 |   MoveE  : Fin (S n) -> Transition n q r s
 64 |   Bottom : Transition n q r s
 65 |
 66 | ||| An array of arrays describing a lexer's state machine.
 67 | public export
 68 | 0 ByteStep : Nat -> (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
 69 | ByteStep n q r s = IArray 256 (Transition n q r s)
 70 |
 71 | ||| An array of arrays describing a lexer's state machine.
 72 | public export
 73 | 0 Stepper : Nat -> (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
 74 | Stepper n q r s = IArray (S n) (ByteStep n q r s)
 75 |
 76 | ||| A discrete finite automaton (DFA) encoded as
 77 | ||| an array of state transitions plus an array
 78 | ||| describing the terminal token states.
 79 | public export
 80 | record DFA q r s where
 81 |   constructor L
 82 |   ||| Number of non-zero states in the automaton.
 83 |   states : Nat
 84 |
 85 |   ||| State transitions matrix.
 86 |   |||
 87 |   ||| If `cur` is the current state (encoded as a `Fin (S states)`
 88 |   ||| and `b` is the current input byte, the next state is determined
 89 |   ||| by `next[cur][b]` (in pseudo C-syntax).
 90 |   next   : Stepper states q r s
 91 |
 92 | --------------------------------------------------------------------------------
 93 | -- Lexer Generator
 94 | --------------------------------------------------------------------------------
 95 |
 96 | public export
 97 | data Step : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type where
 98 |   Go  : Step1 q r s -> Step q r s
 99 |   Rd  : Step1 q r s -> Step q r s
100 |
101 | public export
102 | 0 Steps : (q : Type) -> (r : Bits32) -> (s : Type -> Type) -> Type
103 | Steps q r s = TokenMap (Step q r s)
104 |
105 | emptyRow : ByteStep n q r s
106 | emptyRow = fill _ Bottom
107 |
108 | emptyDFA : DFA q r s
109 | emptyDFA = L 0 (fill _ emptyRow)
110 |
111 | -- Extracts the terminal state of a node
112 | -- `Left` : This is a final node with no more state transitions
113 | -- `Right`: This node has additional state transitions
114 | terminals : SortedMap Nat a -> Node -> Maybe (Nat, Either a a)
115 | terminals m (N n (t::_) []) = ((n,) . Left) <$> lookup t m
116 | terminals m (N n (t::_) _)  = ((n,) . Right) <$> lookup t m
117 | terminals _ _               = Nothing
118 |
119 | nonFinal : SortedMap Nat (Either a a) -> Node -> Maybe Node
120 | nonFinal m n =
121 |   case lookup n.pos m of
122 |     Just (Left _) => Nothing
123 |     _             => Just n
124 |
125 | index : {n : _} -> List (Nat,Node) -> SortedMap Nat (Fin (S n))
126 | index ns = SM.fromList $ mapMaybe (\(x,n) => (n.pos,) <$> tryNatToFin x) ns
127 |
128 | node :
129 |      SortedMap Nat (Either (Step q r s) (Step q r s))
130 |   -> (index : SortedMap Nat (Fin (S n)))
131 |   -> (node  : (Nat,Node))
132 |   -> (Nat, ByteStep n q r s)
133 | node terms index (ix, N me _ out) =
134 |   (ix, fromPairs _ Bottom $ mapMaybe pair (out >>= transitions))
135 |   where
136 |     pair : (Bits8,Nat) -> Maybe (Nat, Transition n q r s)
137 |     pair (b,tgt) =
138 |       case lookup tgt terms of
139 |         Nothing        => case tgt == me of
140 |           True  => Just (cast b, Keep)
141 |           False => ((cast b,) . MoveE) <$> lookup tgt index
142 |         Just (Left $ Go f)  => Just (cast b, Done f)
143 |         Just (Left $ Rd f)  => Just (cast b, DoneBS f)
144 |         Just (Right $ Go f) => case tgt == me of
145 |           True  => Just (cast b, Keep)
146 |           False => ((cast b,) . (`Move` f)) <$> lookup tgt index
147 |         Just (Right $ Rd 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 |