content: {-# LANGUAGE ConstraintKinds   #-}
  {-# LANGUAGE OverloadedStrings #-}
  
  -- | This module a test for whether the constraint dependencies form a
  --   reducible graph.
  
  module Language.Fixpoint.Graph.Reducible ( isReducible ) where
  
  import qualified Data.Tree                            as T
  import qualified Data.HashMap.Strict                  as M
  import           Data.Graph.Inductive
  
  import           Language.Fixpoint.Misc         -- hiding (group)
  import qualified Language.Fixpoint.Types.Visitor      as V
  import qualified Language.Fixpoint.Types              as F
  
  
  --------------------------------------------------------------------------------
  isReducible :: (F.TaggedC c a) => F.GInfo c a -> Bool
  --------------------------------------------------------------------------------
  isReducible fi = all (isReducibleWithStart g) vs
    where
      g  = convertToGraph fi
      vs = {- trace (showDot $ fglToDotGeneric g show (const "") id) -} nodes g
  
  isReducibleWithStart :: Gr a b -> Node -> Bool
  isReducibleWithStart g x = all (isBackEdge domList) rEdges
    where
      dfsTree              = head $ dff [x] g --head because only care about nodes reachable from 'start node'?
      rEdges               = [ e | e@(a,b) <- edges g, isDescendant a b dfsTree]
      domList              = dom g x
  
  
  
  convertToGraph :: (F.TaggedC c a) => F.GInfo c a -> Gr Int ()
  convertToGraph fi = mkGraph vs es
    where
      subCs        = M.elems (F.cm fi)
      es           = lUEdge <$> concatMap (subcEdges' kvI $ F.bs fi) subCs
      ks           = M.keys (F.ws fi)
      kiM          = M.fromList $ zip ks [0..]
      kvI k        = safeLookup ("convertToGraph: " ++ show k) k kiM
      vs           = lNode . kvI <$> M.keys (F.ws fi)
      lNode i      = (i, i)
      lUEdge (i,j) = (i, j, ())
  
  isDescendant :: Node -> Node -> T.Tree Node -> Bool
  isDescendant x y (T.Node z f) | z == y    = f `contains` x
                                | z == x    = False
                                | otherwise = any (isDescendant x y) f
  
  contains :: [T.Tree Node] -> Node -> Bool
  contains t x = x `elem` concatMap T.flatten t
  
  isBackEdge :: [(Node, [Node])] -> Edge -> Bool
  isBackEdge t (u,v) = case lookup u t of
    Just xs -> v `elem` xs
    -- REVIEW: Would False work instead of error?
    Nothing -> error "Unable to lookup back edge"
  
  
  subcEdges' :: (F.TaggedC c a) => (F.KVar -> Node) -> F.BindEnv a -> c a -> [(Node, Node)]
  subcEdges' kvI be c = [(kvI k1, kvI k2) | k1 <- V.envKVars be c
                                          , k2 <- V.kvarsExpr $ F.crhs c]
  