0 | module TyRE.Parser.GroupThompson
  1 |
  2 | import Data.List
  3 | import Data.List1
  4 | import Data.SortedSet
  5 |
  6 | import TyRE.Core
  7 |
  8 | %default total
  9 |
 10 | public export
 11 | record NextStates where
 12 |   constructor MkNextStates
 13 |   condition : CharCond
 14 |   isSat : List (Maybe Nat)
 15 |
 16 | public export
 17 | record GroupSM where
 18 |   constructor MkGroupSM
 19 |   initStates : List (Maybe Nat)
 20 |   statesWithNext : List (Nat, NextStates)
 21 |   max : Nat
 22 |
 23 | filterNothing : List (Maybe Nat) -> List (Maybe Nat)
 24 | filterNothing xs = filter (/= Nothing) xs
 25 |
 26 | replaceEndInInit : List (Maybe Nat) -> List (Maybe Nat) -> List (Maybe Nat)
 27 | replaceEndInInit xs mks =
 28 |   case (find (== Nothing) xs) of
 29 |     Nothing => xs
 30 |     Just _ => mks ++ (filterNothing xs)
 31 |
 32 | replaceEndInNext : List (Nat, NextStates) -> List (Maybe Nat)
 33 |                 -> List (Nat, NextStates)
 34 | replaceEndInNext [] mks = []
 35 | replaceEndInNext ((n, (MkNextStates condition isSat)) :: xs) mks = 
 36 |   (n, (MkNextStates condition (replaceEndInInit isSat mks))) :: (replaceEndInNext xs mks)
 37 |
 38 | groupStates : Nat -> TyRE a -> GroupSM
 39 | groupStates n (MatchChar cond) = 
 40 |   MkGroupSM [Just n] [(n, MkNextStates cond [Nothing])] (n+1)
 41 | groupStates n (Group re) = groupStates n re
 42 | groupStates n Empty =  MkGroupSM [Nothing] [] n
 43 | groupStates n (re1 <*> re2) = 
 44 |   let (MkGroupSM init1 sWN1 n1) := groupStates n re1
 45 |       (MkGroupSM init2 sWN2 n2) := groupStates n1 re2
 46 |   in MkGroupSM  (replaceEndInInit init1 init2)
 47 |                 ((replaceEndInNext sWN1 init2)  ++ sWN2)  
 48 |                 n2
 49 | groupStates n (re1 <|> re2) =
 50 |   let (MkGroupSM init1 sWN1 n1) := groupStates n re1
 51 |       (MkGroupSM init2 sWN2 n2) := groupStates n1 re2
 52 |   in MkGroupSM (init1 ++ init2) (sWN1 ++ sWN2) n2
 53 | groupStates n (Rep re) = 
 54 |   let (MkGroupSM init sWN n') := groupStates n re
 55 |   in MkGroupSM (Nothing :: init) (replaceEndInNext sWN (Nothing :: init)) n'
 56 | groupStates n (Conv re f) = groupStates n re
 57 |
 58 | eq : List (Maybe Nat) -> List (Maybe Nat) -> Bool
 59 | eq mks mjs = (Data.SortedSet.fromList mks) == (fromList mjs)
 60 |
 61 | min : GroupSM -> GroupSM
 62 | min (MkGroupSM initStates statesWithNext max) =
 63 |   let (initStates', statesWithNext') := go (length statesWithNext) (initStates, statesWithNext)
 64 |   in MkGroupSM initStates' statesWithNext' max where
 65 |   go : Nat -> (List (Maybe Nat), List (Nat, NextStates)) -> (List (Maybe Nat), List (Nat, NextStates))
 66 |   go 0 xs = xs
 67 |   go (S k) (init, xs) = 
 68 |     let mappings := getMappings (group xs)
 69 |     in if (length mappings == 0) then (init, xs) else go k (squash mappings (init, xs)) where
 70 |     group : List (Nat, NextStates) -> List (List1 (Nat, NextStates))
 71 |     group xs = groupBy stateEq xs where
 72 |       stateEq : (Nat, NextStates) -> (Nat, NextStates) -> Bool
 73 |       stateEq (_, (MkNextStates cond  isSat )) 
 74 |               (_, (MkNextStates cond' isSat')) =
 75 |                 cond == cond' && (eq isSat isSat')
 76 |     getMappings : List (List1 (Nat, NextStates)) -> List (Nat, Nat)
 77 |     getMappings [] = []
 78 |     getMappings (((nh, _) ::: xs) :: ys) = (map (\case (x, _) => (nh, x)) xs) ++ getMappings ys
 79 |     applyFilter : (Nat, Nat) -> List (Maybe Nat) -> List (Maybe Nat)
 80 |     applyFilter (n, n1) xs = 
 81 |       case (find (== Just n1) xs) of
 82 |         Nothing => xs
 83 |         (Just y) => (Just n) :: filter (\x => not (x == Just n || x == Just n1)) xs
 84 |     squash : List (Nat, Nat) -> (List (Maybe Nat), List (Nat, NextStates)) -> (List (Maybe Nat), List (Nat, NextStates))
 85 |     squash [] x = x
 86 |     squash ((n, n1) :: xs) (init, ys) = 
 87 |       squash xs 
 88 |             ( filter (\x => x /= (Just n1)) init
 89 |             , applyMap ys) where
 90 |             applyMap : List (Nat, NextStates) -> List (Nat, NextStates)
 91 |             applyMap [] = []
 92 |             applyMap ((n', y) :: xs) = 
 93 |               if (n' == n1) then applyMap xs
 94 |               else  ( n'
 95 |                     , MkNextStates  y.condition 
 96 |                                     (applyFilter (n, n1) y.isSat)) :: applyMap xs
 97 |
 98 | public export
 99 | groupSM : TyRE a -> GroupSM
100 | groupSM re = min (groupStates 0 re)