1 module BackwardS
    2 
    3 ( backwardS
    4 , backwardSpublic
    5 )
    6 
    7 -- implements thomas genet's algorithm
    8 -- for approximating term replacement in a finite automaton
    9 
   10 -- we're looking at the reversed system   x z (y z) -> S x y z
   11 
   12 -- this implementation is ugly ugly ugly
   13 -- w.r.t. the rest of the system
   14 -- the reduction rule of S is hardwired
   15 -- as are the names of the constructors (S and @)
   16 
   17 where
   18 
   19 import Set
   20 import FiniteMap
   21 
   22 import Stuff
   23 import Options
   24 
   25 import TA
   26 import FAtypes
   27 import Ids
   28 
   29 import Reuse
   30 
   31 sons :: TNFA Int -> Int -> [(Int, Int)]
   32 sons (TNFA cons all starts moves) p =
   33     let
   34         ts = lookupWithDefaultFM moves (error "BackwardS.sons.ts") p
   35         lrs =  [ (l, r) 
   36                 | t <- setToList ts
   37                 , tconname (stcon t) == "@"
   38                 , let [l, r] = stargs t
   39                 ]
   40     in
   41         lrs
   42 
   43 
   44 backwardS :: Opts -> TNFA Int -> TNFA Int
   45 -- look for all matches of x z (y z) 
   46 -- add new states from that to S x y z
   47 backwardS opts a @ (TNFA cons all starts moves) =
   48     let 
   49         quads =        [ (t, (ll, rl, rr))
   50                 | t <- setToList all
   51                 , (l, r) <- sons a t
   52                 , (ll, lr) <- sons a l
   53                 , (rl, rr) <- sons a r
   54                 , lr == rr    -- these are the two z's
   55                 ]
   56 
   57         -- next free state
   58         next = 1 + maximum (setToList all)
   59 
   60         -- write new top state numbers to quads
   61         -- warnig: the number 3 depends on the states used in "new" below
   62         iquads = zip [next, next + 3 .. ] quads
   63 
   64         -- this is a bit ugly
   65         -- need to find the complete id information for the constructors
   66         -- we hope they are there
   67         ap = head [ con | con <- setToList cons, tconname con == "@" ]
   68         s  = head [ con | con <- setToList cons, tconname con == "S" ]
   69         
   70         -- generate new states per quad
   71 
   72         movesr = invert moves
   73 
   74         new (i, (t, (x, y, z))) = 
   75                 [ (t    , mksterm ap [i + 0, z] )
   76                 , (i + 0, mksterm ap [i + 1, y] )
   77                 , (i + 1, mksterm ap [i + 2, x] )
   78                 , (i + 2, mksterm s  []         )
   79                 ]
   80 
   81         newsl = [ p | iq <- iquads, p <- new iq ]
   82         news = listToFM [ (a, unitSet t) | (a, t) <- newsl ]
   83         moves' = moves `mergeFM` news
   84         all' = all `unionSet` mkSet (keysFM moves')
   85 
   86         r = TNFA cons all' starts moves'
   87 
   88 
   89         addons = [ a | a <- keysFM news, a >= next ]
   90         r' = reuse opts r addons
   91 
   92         r'' = chose opts "reuse" r' r
   93 
   94     in
   95 
   96         trinfo opts "backwardS" r'' $
   97 
   98         r''
   99 
  100 
  101 
  102 
  103 backwardSpublic :: Opts -> [ TNFA Int ] -> TNFA Int
  104 
  105 backwardSpublic opts args =
  106     if length args /= 1 
  107     then error "backwardSpublic.args"
  108     else 
  109         let [arg1] = args
  110         in  backwardS opts arg1
  111 
  112 
  113 
  114 -- later:
  115 
  116 -- iterate the backwardS operation
  117 -- making the automaton deterministic and minimal
  118 -- before and after each step
  119 -- until process converges
  120 
  121 -- making determin. should ensure that the two z's really "are the same"