{-|
  Description : Generate mu-rules.
  Copyright   : (c) Paul Govereau and Jean-Baptiste Tristan 2010
  License     : All Rights Reserved
  Maintainer  : Paul Govereau <govereau@cs.harvard.edu>

  This module generates a mu-node for variable modified within a loop.
-}
module MD.Mu ( mkmu ) where
import Data.List

import MD.Syntax.GDSA
import MD.Structural
import MD.Rewrite

mkmu :: Structure GBlock -> IO [RR]
mkmu s = return $ findRules 1 s

findRules :: Int -> Structure GBlock -> [RR]
findRules n s = case s of
  Empty         -> []
  Single b      -> rules b
  Sequence l    -> concatMap (findRules n) l
  If cs x y     -> concatMap rules cs ++ findRules n x ++ findRules n y
  IfN c xs      -> rules c ++ concatMap (findRules n) xs
  WhileLoop c b -> let cr = rules c
                       rr = findRules (n+1) b
                   in mu n (cr ++ rr) c

-------------------------------------------------------------------------------
-- The current implementation is different from the description in the paper.
-- To handle nested loops, we perform symbolic evaluation in order to
-- generate the inductive rules for each variable. This is a short-cut that
-- we plan to remove in future versions.

mu :: Int -> [RR] -> GBlock -> [RR]
mu ndx rr c = condterm : initial ++ inductive ++ mus
 where
   [entry,body] = sort (pre' c)     -- may not be right?
   vars = map fst3 (phis c)
   sub0 = map (find_sub entry) (phis c)
   subn = map (find_sub body)  (phis c)
   find_sub n (_,_,l) =
       case find (\(m,_) -> n == m) l of
         Nothing    -> error "no sub 0"
         Just (_,t) -> t
   --
   rx = map (\v -> RR v (Atom $ Var $ P v)) vars
   ry = map (\v -> RR v (Atom $ Var $ N v)) vars
   --
   (cn',tl,fl) = cond c          -- CHECK LABELS
   cn = simplify [] (rr++ry) cn'
   --
   rhs = map f subn
   f t = simplify [] (rr++rx) t
   --
   initial = map (\(v,z) -> RR (Z v) z) $ zip vars sub0
   inductive = map (\(v,x) -> RR (N v) x) $ zip vars rhs
   condvar   = Ident ('&':show ndx)
   condterm  = RR (N condvar) cn
   mus = map (\v -> RR v (Mu ST condvar v)) vars
   --
   fst3 (x,_,_) = x
   thr  (_,_,x) = x

cond :: GBlock -> (Term,Label,Label)
cond b = case control b of
           MBr t1 ty l [(t2,l')] -> (BinOp (Cmp MD.Syntax.GDSA.EQ) "" ty t1 t2, l', l)
           foo -> error (show foo)