1 module CForwardS
    2 
    3 ( cforwardS
    4 , cforwardSpublic
    5 )
    6 
    7 -- checks whether a given grammar
    8 -- is forward 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 "CForwardS.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 "CForwardS.leaves.ts") p
   57         lrs =  [ () 
   58                 | t <- setToList ts
   59                 , tconname (stcon t) == "S"
   60                 ]
   61     in
   62         lrs
   63 
   64 
   65 
   66 cforwardS :: Opts -> TNFA Int -> TNFA Int
   67 -- look for all matches of S x y z (successively)
   68 -- add new states from that to x z (y z) 
   69 cforwardS opts a @ (TNFA cons all starts moves) =
   70     let 
   71         quads =        [ (t0, (x, y, z))
   72                 | t0 <- setToList all
   73                 , (t1, z) <- sons a t0
   74                 , (t2, y) <- sons a t1
   75                 , (t3, x) <- sons a t2
   76                 , ()     <- leaves a t3       -- this looks for S
   77                 ]
   78 
   79         -- next free state
   80         next = 1 + maximum (setToList all)
   81 
   82 
   83         -- this is a bit ugly
   84         -- need to find the complete id information for the constructors
   85         -- we hope they are there
   86         ap = head [ con | con <- setToList cons, tconname con == "@" ]
   87         s  = head [ con | con <- setToList cons, tconname con == "S" ]
   88         
   89 
   90         -- try to bypass complicate constructions.
   91         -- catch cases like this:
   92         -- X -> T X + something, Redex -> X S
   93         -- by looking up where (x z), (y z), (x z(y z))        
   94         -- may go in the current automaton 
   95         -- hoping it's deterministic
   96 
   97         imoves = invert moves
   98 
   99         ifn x y nxt = 
  100             let xy = mksterm ap [x, y]
  101             in case setToList (lookupset imoves xy) of
  102                 [c] -> (c, xy)        -- state is already there, and unique
  103                 _ -> (nxt, xy)        -- not there, or not unique
  104 
  105 
  106         -- generate new states per quad
  107         newsts (t, (x, y, z)) = 
  108             let        thexz @ (xz, mxz) = ifn  x  z (next + 0)
  109                 theyz @ (yz, myz) = ifn  y  z (next + 1)
  110                 ( c, mxzyz) = ifn xz yz (next + 2)
  111             in
  112                 if c == t 
  113                 then []
  114                 else
  115                 [ (t       , mxzyz)
  116                 , thexz
  117                 , theyz
  118                 ]
  119 
  120 
  121 
  122         -- generate new moves for automaton
  123 
  124         red txyz @ (t, xyz) = TNFA cons all' starts moves'
  125             where
  126                 moves' = moves `mergeFM` 
  127                         listToFM [ (a, unitSet t) | (a, t) <- newsts txyz ]
  128                 all'= all `unionSet` mkSet (keysFM moves')
  129 
  130 
  131         -- compute differences: a with redex replaced \\ original a
  132         -- hack: first negate the input automaton a
  133         -- then intersect with rewritten automaton
  134 
  135         opts' = addToFM opts "trace" "on"
  136         na = negTNFA opts' a
  137 
  138         diff txyz @ (t, (x, y, z)) = 
  139             let        
  140                 r = red txyz 
  141                 m =   if r == a 
  142                         then trace "\n*** shortcut ***" 
  143                                 emptyTNFA 
  144                         else trace "\n*** longcut ***" 
  145                                 usefulTNFA opts $ intersectTNFA opts r na
  146                 msg = "checking for redex " ++ show txyz ++ ": "
  147                         ++ show m ++ "\n"
  148             in
  149                 ( chose opts "tracecforward" (trace msg) id )
  150                 m
  151 
  152 
  153         diffs = foldr (unionTNFA opts) emptyTNFA 
  154                 [ diff txyz | txyz <- quads ]
  155 
  156     in
  157 
  158         chose opts "tracecforward" 
  159         (trace (   
  160                    "\ncforward a: " ++ show a ++ "\n"
  161 --           ++ "\ncforward na: " ++ show na ++ "\n" 
  162         ))
  163         id $
  164 
  165 
  166         diffs
  167 
  168 
  169 
  170 
  171 
  172 
  173 cforwardSpublic :: Opts -> [ TNFA Int ] -> TNFA Int
  174 
  175 cforwardSpublic opts args =
  176     if length args /= 1 
  177     then error "cforwardSpublic.args"
  178     else 
  179         let [arg1] = args
  180         in  cforwardS opts arg1
  181 
  182 
  183