1 module CBackwardS
    2 
    3 ( cbackwardS
    4 , cbackwardSpublic
    5 )
    6 
    7 -- checks whether a given grammar
    8 -- is backward closed under reduction
    9 -- in the system   S x y z   ->   x z (y z)
   10 
   11 -- this implementation is ugly ugly ugly
   12 -- w.r.t. the rest of the system
   13 -- the reduction rule of S is hardwired
   14 -- as are the names of the constructors (S and @)
   15 
   16 where
   17 
   18 import Trace
   19 
   20 import Set
   21 import FiniteMap
   22 
   23 import Stuff
   24 import Options
   25 
   26 import TA
   27 import FAtypes
   28 import Ids
   29 
   30 import FAmin
   31 import FAuseful
   32 
   33 import FAneg
   34 import FAintersect
   35 import FAunion
   36 
   37 -- import Reuse
   38 
   39 sons :: TNFA Int -> Int -> [(Int, Int)]
   40 sons (TNFA cons all starts moves) p =
   41     let
   42         ts = lookupWithDefaultFM moves (error "CBackwardS.sons.ts") p
   43         lrs =  [ (l, r) 
   44                 | t <- setToList ts
   45                 , tconname (stcon t) == "@"
   46                 , let [l, r] = stargs t
   47                 ]
   48     in
   49         lrs
   50 
   51 
   52 
   53 leaves :: TNFA Int -> Int -> [()]
   54 leaves (TNFA cons all starts moves) p =
   55     let
   56         ts = lookupWithDefaultFM moves (error "CBackwardS.leaves.ts") p
   57         lrs =  [ () 
   58                 | t <- setToList ts
   59                 , tconname (stcon t) == "S"
   60                 ]
   61     in
   62         lrs
   63 
   64 
   65 
   66 cbackwardS :: Opts -> TNFA Int -> TNFA Int
   67 -- look back all matches of S x y z (successively)
   68 -- add new states from that to x z (y z) 
   69 cbackwardS opts a @ (TNFA cons all starts moves) =
   70     let 
   71 
   72         quads = [ (t, (ll, rl, rr))
   73                 | t <- setToList all
   74                 , (l, r) <- sons a t
   75                 , (ll, lr) <- sons a l
   76                 , (rl, rr) <- sons a r
   77                 , lr == rr      -- these are the two z's
   78                 ]
   79 
   80 
   81         -- next free state
   82         next = 1 + maximum (setToList all)
   83 
   84 
   85         -- this is a bit ugly
   86         -- need to find the complete id information for the constructors
   87         -- we hope they are there
   88         ap = head [ con | con <- setToList cons, tconname con == "@" ]
   89         s  = head [ con | con <- setToList cons, tconname con == "S" ]
   90         
   91 
   92         -- try to bypass complicate constructions.
   93         -- catch cases like this:
   94         -- X -> T X + something, Redex -> X S
   95         -- by looking up where (x z), (y z), (x z(y z))        
   96         -- may go in the current automaton 
   97         -- hoping it's deterministic
   98 
   99         imoves = invert moves
  100 
  101         ifn' t nxt =  
  102             case setToList (lookupset imoves t) of
  103                 [c] -> (c, t) -- state is already there, and unique
  104                 _ -> (nxt, t) -- not there, or not unique
  105 
  106 
  107         ifap x y nxt = ifn' (mksterm ap [x, y]) nxt
  108         ifs      nxt = ifn' (mksterm s  [    ]) nxt
  109 
  110         -- generate new states per quad
  111         newsts (t, (x, y, z)) = 
  112             let thes   @ (s  , ms  ) = ifs        (next + 0)
  113                 thesx  @ (sx , msx ) = ifap  s   x (next + 1)
  114                 thesxy @ (sxy, msxy) = ifap  sx  y (next + 2)
  115                 ( c, msxyz)        = ifap  sxy z (next + 3)
  116             in
  117                 if c == t 
  118                 then []
  119                 else
  120                 [ (t       , msxyz)
  121                 , thesxy
  122                 , thesx
  123                 , thes
  124                 ]
  125 
  126 
  127 
  128         -- generate new moves for automaton
  129 
  130         red txyz @ (t, xyz) = TNFA cons all' starts moves'
  131             where
  132                 moves' = moves `mergeFM` 
  133                         listToFM [ (a, unitSet t) | (a, t) <- newsts txyz ]
  134                 all'= all `unionSet` mkSet (keysFM moves')
  135 
  136 
  137         -- compute differences: a with redex replaced \\ original a
  138         -- hack: first negate the input automaton a
  139         -- then intersect with rewritten automaton
  140 
  141         opts' = addToFM opts "trace" "on"
  142         na = negTNFA opts' a
  143 
  144         diff txyz @ (t, (x, y, z)) = 
  145             let        
  146                 r = red txyz 
  147                 m =   if r == a 
  148                         then trace "\n*** shortcut ***" 
  149                                 emptyTNFA 
  150                         else trace "\n*** longcut ***" 
  151                                 usefulTNFA opts $ intersectTNFA opts r na
  152                 msg = "checking for contractum " ++ show txyz ++ ": "
  153                         ++ show m ++ "\n"
  154             in
  155                 ( chose opts "tracecbackward" (trace msg) id )
  156                 m
  157 
  158 
  159         diffs = foldr (unionTNFA opts) emptyTNFA 
  160                 [ diff txyz | txyz <- quads ]
  161 
  162     in
  163 
  164         chose opts "tracecbackward" 
  165         (trace (   
  166                    "\ncbackward a: " ++ show a ++ "\n"
  167 --           ++ "\ncbackward na: " ++ show na ++ "\n" 
  168         ))
  169         id $
  170 
  171 
  172         diffs
  173 
  174 
  175 
  176 
  177 
  178 
  179 cbackwardSpublic :: Opts -> [ TNFA Int ] -> TNFA Int
  180 
  181 cbackwardSpublic opts args =
  182     if length args /= 1 
  183     then error "cbackwardSpublic.args"
  184     else 
  185         let [arg1] = args
  186         in  cbackwardS opts arg1
  187 
  188 
  189