
  0 | module Text.ILex.Internal.DFA
  1 | 
  2 | import Data.Linear.Traverse1
  3 | import Syntax.T1
  4 | import Text.ILex.Internal.ENFA
  5 | import Text.ILex.Internal.NFA
  6 | import Text.ILex.Internal.Types
  7 | 
  8 | %default total
  9 | 
 10 | parameters {auto st : DFAState s a}
 11 | 
 12 |   covering
 13 |   process : SnocList Edge -> NEdges -> F1 s Edges
 14 | 
 15 |   covering
 16 |   discrete : Nat -> F1' s
 17 |   discrete x = T1.do
 18 |     Nothing <- lookupNode x | Just v => pure ()
 19 |     nn      <- getNNode x
 20 |     ds      <- process [<] nn.out
 21 |     let nde := N nn.pos nn.acc ds
 22 |     insertNode x nde
 23 | 
 24 |   process sx []              = pure (sx <>> [])
 25 |   process sx (NE r ts :: xs) = T1.do
 26 |     case ts of
 27 |       -- oops, there is no possible target for this rule. we can drop it
 28 |       []  => process sx xs
 29 | 
 30 |       -- a single target so this rule is already discrete
 31 |       -- let's keep it and move on
 32 |       [t] => process (sx:<E r t) xs
 33 | 
 34 |       -- a group of targets. let's see if we already have seen these
 35 |       set =>
 36 |         lookupSet set >>= \case
 37 |           -- this is a known group.
 38 |           Just t  => process (sx:<E r t) xs
 39 | 
 40 |           -- a new group. we have work to do
 41 |           Nothing => do
 42 |             t  <- addSet set
 43 |             ns <- traverse1 getNNode set
 44 |             insertNNode t (foldl joinNNode (NN t [] []) ns)
 45 |             discrete t
 46 |             process (sx:<E r t) xs
 47 | 
 48 |   covering
 49 |   nodes : F1' s
 50 |   nodes = keys1 st.ngraph >>= traverse1_ discrete
 51 | 
 52 |   export covering
 53 |   toDFA : TokenMap8 a -> F1 s (List (Nat,Node))
 54 |   toDFA xs = T1.do
 55 |     toNFA xs
 56 |     nodes
 57 |     connectedComponent children 0 st.graph
 58 |     normalizeGraph
 59 |     pairs1 st.graph
 60 |