1 -- powerset construction
    2 
    3 module FAdet
    4 
    5 ( bnfa2bdfa
    6 , tnfa2bdfa
    7 , detTNFA
    8 )
    9 
   10 
   11 where
   12 
   13 
   14 
   15 import Set
   16 import FiniteMap
   17 
   18 import Options
   19 
   20 import Stuff
   21 
   22 import TA
   23 import FAtypes
   24 
   25 import FAconv
   26 
   27 import FAcmpct
   28 
   29 pick :: Ord a => FiniteMap (STerm a) (Set a) -> STerm (Set a) -> Set a
   30 -- look up the (set of) predec. of a term (whose comps. are sets)
   31 pick m t =
   32     let args = insts (stargs t) 
   33         ts = mapSet (\ a -> mksterm (stcon t) a) args
   34         ps = ts `bind` lookupset m 
   35     in  ps
   36 
   37 
   38 phull :: Ord a =>
   39         TCons -> FiniteMap (STerm a) (Set a)   -- original map
   40         -> Set (Set a) -> Set (Set a)          -- known/unknown
   41         -> FiniteMap (STerm (Set a)) (Set a)   -- input
   42         -> (Set (Set a), FiniteMap (STerm (Set a)) (Set a))    -- output
   43 
   44 phull tcons m known unknown rels | isEmptySet unknown = (known, rels)
   45 phull tcons m known unknown rels =
   46     let ts =    [ mksterm tc a
   47                 | tc <- setToList tcons, n <- [tconarity tc], n > 0
   48                 , a <- packs n 1 (setToList known) (setToList unknown)
   49                 ]
   50 
   51         ps = [ (t, p) | t <- ts, p <- [pick m t] -- new relations
   52 
   53 -- x-perry-mental: don't generate the sink state {}
   54                         , not (isEmptySet p)
   55 
   56              ]                      
   57 
   58         qs = listToFM ps                  -- new relations as map
   59         gs = mkSet [ g | (t, g) <- ps ]               -- new sets
   60         ks = known `unionSet` unknown   -- they are no longer unknown
   61         ns = gs `minusSet` ks           -- these are brand new
   62         rs = plusFM_C (error "phull") rels qs  -- should not clash
   63     in  phull tcons m ks ns rs
   64 
   65 
   66 
   67 {-# SPECIALIZE bnfa2bdfa' :: Opts -> BNFA Int -> BDFA (Set Int) #-}
   68 bnfa2bdfa' :: Ord a => Opts -> BNFA a -> BDFA (Set a)
   69 bnfa2bdfa' opts (BNFA cons all starts moves) =
   70     let ps =    [ ( mksterm tc []
   71                   , g
   72                   )
   73                 | tc <- setToList cons, tconarity tc == 0
   74 
   75                 , g <- [lookupset moves (mksterm tc [])] 
   76 
   77 -- x-perry-mental: don't generate sink state {}
   78                 , not (isEmptySet g)
   79 
   80                 ]
   81         qs = listToFM ps                  -- start relations
   82         gs = mkSet [ g | (t, g) <- ps ]               -- start sets
   83         (ks, rs) = phull cons moves emptySet gs qs     -- find hull
   84         fs = filterSet (\ s -> not (isEmptySet (s `intersectSet` starts))) ks
   85     in  BDFA cons ks fs rs
   86 
   87 ------------------------------------------------------------------------
   88 
   89 bnfa2bdfa :: (Show a, Ord a) => Opts -> BNFA a -> BDFA Int
   90 bnfa2bdfa opts = cmpctBDFA opts . bnfa2bdfa' opts
   91 
   92 tnfa2bdfa :: (Show a, Ord a) => Opts -> TNFA a -> BDFA Int
   93 tnfa2bdfa opts = bnfa2bdfa opts . tnfa2bnfa opts
   94 
   95 
   96 detTNFA :: Opts -> TNFA Int -> TNFA Int
   97 detTNFA opts = bdfa2tnfa opts . tnfa2bdfa opts
   98 
   99