1 module SaturnS
    2 
    3 ( saturnS
    4 , saturnSpublic
    5 )
    6 
    7 -- checks whether a given grammar
    8 -- is forward saturated under reduction
    9 -- in the system   S x y z   <->   x z (y z)
   10 
   11 -- i. e. each state that produces a redex
   12 -- must also produce its contractum (and back)
   13 
   14 
   15 -- this implementation is ugly ugly ugly
   16 -- w.r.t. the rest of the system
   17 -- the reduction rule of S is hardwired
   18 -- as are the names of the constructors (S and @)
   19 
   20 where
   21 
   22 import Trace
   23 
   24 import Set
   25 import FiniteMap
   26 
   27 import Stuff
   28 import Options
   29 
   30 import TA
   31 import FAtypes
   32 import Ids
   33 
   34 import FAmin
   35 import FAuseful
   36 
   37 import FAcon
   38 
   39 import FAneg
   40 import FAintersect
   41 import FAunion
   42 
   43 -- import Reuse
   44 
   45 sons :: TNFA Int -> Int -> [(Int, Int)]
   46 sons (TNFA cons all starts moves) p =
   47     let
   48         ts = lookupWithDefaultFM moves (error "CForwardS.sons.ts") p
   49         lrs =  [ (l, r) 
   50                 | t <- setToList ts
   51                 , tconname (stcon t) == "@"
   52                 , let [l, r] = stargs t
   53                 ]
   54     in
   55         lrs
   56 
   57 
   58 
   59 leaves :: TNFA Int -> Int -> [()]
   60 leaves (TNFA cons all starts moves) p =
   61     let
   62         ts = lookupWithDefaultFM moves (error "CForwardS.leaves.ts") p
   63         lrs =  [ () 
   64                 | t <- setToList ts
   65                 , tconname (stcon t) == "S"
   66                 ]
   67     in
   68         lrs
   69 
   70 
   71 
   72 stackit txyzs = addListToFM_C unionSet emptyFM 
   73         [ (xyz, unitSet t) | (t, xyz) <- txyzs ]
   74 
   75 
   76 
   77 saturnS :: Opts -> TNFA Int -> TNFA Int
   78 -- look for all matches of S x y z (successively)
   79 -- add new states from that to x z (y z) 
   80 saturnS opts a @ (TNFA cons all starts moves) =
   81     let 
   82 
   83         redexquads =   [ (t0, (x, y, z))
   84                 | t0 <- setToList all
   85                 , (t1, z) <- sons a t0
   86                 , (t2, y) <- sons a t1
   87                 , (t3, x) <- sons a t2
   88                 , ()     <- leaves a t3       -- this looks for S
   89                 ]
   90 
   91         redexes = stackit redexquads
   92 
   93 
   94         contraquads = [ (t0, (ll, rl, rr))
   95                 | t0 <- setToList all
   96                 , (l, r) <- sons a t0
   97                 , (ll, lr) <- sons a l
   98                 , (rl, rr) <- sons a r
   99                 , lr == rr      -- these are the two z's
  100                 ]
  101 
  102         contras = stackit contraquads
  103 
  104         purgeFM = filterFM (\ k e -> not (isEmptySet e))
  105 
  106 
  107         nof = purgeFM $ addListToFM_C minusSet redexes (fmToList contras)
  108         nob = purgeFM $ addListToFM_C minusSet contras (fmToList redexes)
  109         
  110         nofs = (keysFM nof)
  111         nobs = (keysFM nob)
  112 
  113         -- this is a bit ugly
  114         -- need to find the complete id information for the constructors
  115         -- we hope they are there
  116         ap = head [ con | con <- setToList cons, tconname con == "@" ]
  117         s  = head [ con | con <- setToList cons, tconname con == "S" ]
  118 
  119 
  120         -- next free state
  121         next = 1 + maximum (setToList all)
  122 
  123 
  124         mksterm' c args = unitSet (mksterm c args)
  125 
  126         mkredex (x, y, z) = listToFM
  127                 [ (next + 0, mksterm' ap [next + 3, z])
  128                 , (next + 1, mksterm' s [])
  129                 , (next + 2, mksterm' ap [next + 1, x])
  130                 , (next + 3, mksterm' ap [next + 2, y])
  131                 ]
  132 
  133         mkcontra (x, y, z) = listToFM
  134                 [ (next + 0, mksterm' ap [next + 1, next + 2])
  135                 , (next + 1, mksterm' ap [x, z])
  136                 , (next + 2, mksterm' ap [y, z])
  137                 ]
  138 
  139         nofx = [ ("no contractum for:"
  140                 , unitSet next
  141                  , plusFM_C (error "SaturnS.nofs") moves (mkredex xyz)
  142                  )
  143                 | xyz <- nofs ]
  144 
  145         nobx = [ ("no redex for:" 
  146                 , unitSet next
  147                 , plusFM_C (error "SaturnS.nobs") moves (mkcontra xyz)
  148                 )
  149                 | xyz <- nobs ]
  150 
  151         okeh = [ ("everything closed", starts, emptyFM) ]
  152         
  153         (msg, starts', moves') = head (nofx ++ nobx ++ okeh)
  154 
  155     in
  156 
  157         trace ("redexes: " ++ show redexes) $
  158         trace ("contras: " ++ show contras) $
  159 
  160         trace ("redexes w/o contra: = " ++ show nofs) $
  161         trace ("contras w/o redex : = " ++ show nobs) $
  162 
  163         trace ("SaturnS : " ++ msg) $
  164 
  165         TNFA cons (all `unionSet` mkSet (keysFM moves')) starts' moves'
  166 
  167 
  168 
  169 
  170 
  171 
  172 saturnSpublic :: Opts -> [ TNFA Int ] -> TNFA Int
  173 
  174 saturnSpublic opts args =
  175     if length args /= 1 
  176     then error "saturnSpublic.args"
  177     else 
  178         let [arg1] = args
  179         in  saturnS opts arg1
  180 
  181 
  182