
  0 | module Text.ILex.Internal.NFA
  1 | 
  2 | import Data.Linear.Traverse1
  3 | import Data.Maybe
  4 | import Syntax.T1
  5 | import Text.ILex.Internal.ENFA
  6 | import Text.ILex.Internal.Types
  7 | 
  8 | %default total
  9 | 
 10 | prep : NEdge -> NEdges -> NEdges
 11 | prep x xs = if isEmpty x.rule then xs else x::xs
 12 | 
 13 | split : NEdge -> NEdge -> (NEdge,NEdge,NEdge)
 14 | split x y =
 15 |   let ri := intersection x.rule y.rule
 16 |       ei := NE ri (sunion x.tgts y.tgts)
 17 |       Left rx := difference x.rule ri
 18 |         | Right (a,b) => (NE a x.tgts,ei,NE b x.tgts)
 19 |       Left ry := difference y.rule ri
 20 |         | Right (a,b) => (NE a y.tgts,ei,NE b y.tgts)
 21 |    in case rx < ry of
 22 |         True  => (NE rx x.tgts,ei,NE ry y.tgts)
 23 |         False => (NE ry y.tgts,ei,NE rx x.tgts)
 24 | 
 25 | insertEdge : NEdges -> NEdge -> NEdges
 26 | insertEdge []           x     = if isEmpty x.rule then [] else [x]
 27 | insertEdge es@(y :: ys) x     =
 28 |   case isEmpty x.rule of
 29 |     True  => es
 30 |     False => case x.tgts == y.tgts of
 31 |       False => case overlap x.rule y.rule of
 32 |         False => case x.rule < y.rule of
 33 |           True  => prep x es
 34 |           False => y :: insertEdge ys x
 35 |         True  =>
 36 |           let (ex,ei,ey) := split x y
 37 |            in prep ex . prep ei $ insertEdge ys ey
 38 | 
 39 |       -- They share the same targets. We try and build one large range
 40 |       -- from the two.
 41 |       True  => case overlap x.rule y.rule || adjacent x.rule y.rule of
 42 |         False => case x.rule < y.rule of
 43 |           True  => prep x es
 44 |           False => y :: insertEdge ys x
 45 |         True  => NE (span x.rule y.rule) x.tgts :: ys
 46 | 
 47 | outUnion : NEdges -> NEdges -> NEdges
 48 | outUnion xs ys = foldl insertEdge ys xs
 49 | 
 50 | export
 51 | joinNNode : NNode -> NNode -> NNode
 52 | joinNNode x y = NN x.pos (sunion x.acc y.acc) (outUnion x.out y.out)
 53 | 
 54 | fromEdge : Edge -> NEdge
 55 | fromEdge (E r t) = (NE r [t])
 56 | 
 57 | fromENode : Nat -> ENode -> NNode
 58 | fromENode n x = NN n x.acc $ map fromEdge x.out
 59 | 
 60 | parameters {auto st : DFAState s a}
 61 |   covering
 62 |   eclosure : Nat -> F1 s NNode
 63 |   eclosure x = T1.do
 64 |     Nothing <- lookupNNode x | Just v => pure v
 65 |     n       <- getENode x
 66 |     es      <- traverse1 eclosure n.eps
 67 |     let nn := foldl joinNNode (fromENode x n) es
 68 |     insertNNode x nn
 69 |     pure nn
 70 | 
 71 |   covering
 72 |   closures : F1' s
 73 |   closures = keys1 st.egraph >>= traverse1_  (ignore1 . eclosure)
 74 | 
 75 |   export covering
 76 |   toNFA : TokenMap8 a -> F1' s
 77 |   toNFA xs = T1.do
 78 |     toENFA xs
 79 |     closures
 80 |     connectedComponent nchildren 0 st.ngraph
 81 | 
 82 |   export %inline
 83 |   debugNFA : TokenMap8 a -> F1 s (List (Nat, NNode))
 84 |   debugNFA ts = assert_total (toNFA ts) >> pairs1 st.ngraph
 85 |