{-# 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 :: GInfo c a -> Bool
isReducible GInfo c a
fi = (Node -> Bool) -> [Node] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Gr Node () -> Node -> Bool
forall a b. Gr a b -> Node -> Bool
isReducibleWithStart Gr Node ()
g) [Node]
vs
  where
    g :: Gr Node ()
g  = GInfo c a -> Gr Node ()
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> Gr Node ()
convertToGraph GInfo c a
fi
    vs :: [Node]
vs = {- trace (showDot $ fglToDotGeneric g show (const "") id) -} Gr Node () -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes Gr Node ()
g

isReducibleWithStart :: Gr a b -> Node -> Bool
isReducibleWithStart :: Gr a b -> Node -> Bool
isReducibleWithStart Gr a b
g Node
x = (Edge -> Bool) -> [Edge] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([(Node, [Node])] -> Edge -> Bool
isBackEdge [(Node, [Node])]
domList) [Edge]
rEdges
  where
    dfsTree :: Tree Node
dfsTree              = [Tree Node] -> Tree Node
forall a. [a] -> a
head ([Tree Node] -> Tree Node) -> [Tree Node] -> Tree Node
forall a b. (a -> b) -> a -> b
$ [Node] -> Gr a b -> [Tree Node]
forall (gr :: * -> * -> *) a b.
Graph gr =>
[Node] -> gr a b -> [Tree Node]
dff [Node
x] Gr a b
g --head because only care about nodes reachable from 'start node'?
    rEdges :: [Edge]
rEdges               = [ Edge
e | e :: Edge
e@(Node
a,Node
b) <- Gr a b -> [Edge]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Edge]
edges Gr a b
g, Node -> Node -> Tree Node -> Bool
isDescendant Node
a Node
b Tree Node
dfsTree]
    domList :: [(Node, [Node])]
domList              = Gr a b -> Node -> [(Node, [Node])]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [(Node, [Node])]
dom Gr a b
g Node
x



convertToGraph :: (F.TaggedC c a) => F.GInfo c a -> Gr Int ()
convertToGraph :: GInfo c a -> Gr Node ()
convertToGraph GInfo c a
fi = [Edge] -> [LEdge ()] -> Gr Node ()
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [Edge]
vs [LEdge ()]
es
  where
    subCs :: [c a]
subCs        = HashMap SubcId (c a) -> [c a]
forall k v. HashMap k v -> [v]
M.elems (GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi)
    es :: [LEdge ()]
es           = Edge -> LEdge ()
forall a b. (a, b) -> (a, b, ())
lUEdge (Edge -> LEdge ()) -> [Edge] -> [LEdge ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c a -> [Edge]) -> [c a] -> [Edge]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((KVar -> Node) -> BindEnv -> c a -> [Edge]
forall (c :: * -> *) a.
TaggedC c a =>
(KVar -> Node) -> BindEnv -> c a -> [Edge]
subcEdges' KVar -> Node
kvI (BindEnv -> c a -> [Edge]) -> BindEnv -> c a -> [Edge]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs GInfo c a
fi) [c a]
subCs
    ks :: [KVar]
ks           = HashMap KVar (WfC a) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys (GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws GInfo c a
fi)
    kiM :: HashMap KVar Node
kiM          = [(KVar, Node)] -> HashMap KVar Node
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(KVar, Node)] -> HashMap KVar Node)
-> [(KVar, Node)] -> HashMap KVar Node
forall a b. (a -> b) -> a -> b
$ [KVar] -> [Node] -> [(KVar, Node)]
forall a b. [a] -> [b] -> [(a, b)]
zip [KVar]
ks [Node
0..]
    kvI :: KVar -> Node
kvI KVar
k        = String -> KVar -> HashMap KVar Node -> Node
forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
safeLookup (String
"convertToGraph: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ KVar -> String
forall a. Show a => a -> String
show KVar
k) KVar
k HashMap KVar Node
kiM
    vs :: [Edge]
vs           = Node -> Edge
forall b. b -> (b, b)
lNode (Node -> Edge) -> (KVar -> Node) -> KVar -> Edge
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Node
kvI (KVar -> Edge) -> [KVar] -> [Edge]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap KVar (WfC a) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys (GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws GInfo c a
fi)
    lNode :: b -> (b, b)
lNode b
i      = (b
i, b
i)
    lUEdge :: (a, b) -> (a, b, ())
lUEdge (a
i,b
j) = (a
i, b
j, ())

isDescendant :: Node -> Node -> T.Tree Node -> Bool
isDescendant :: Node -> Node -> Tree Node -> Bool
isDescendant Node
x Node
y (T.Node Node
z [Tree Node]
f) | Node
z Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
y    = [Tree Node]
f [Tree Node] -> Node -> Bool
`contains` Node
x
                              | Node
z Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
x    = Bool
False
                              | Bool
otherwise = (Tree Node -> Bool) -> [Tree Node] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Node -> Node -> Tree Node -> Bool
isDescendant Node
x Node
y) [Tree Node]
f

contains :: [T.Tree Node] -> Node -> Bool
contains :: [Tree Node] -> Node -> Bool
contains [Tree Node]
t Node
x = Node
x Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Tree Node -> [Node]) -> [Tree Node] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Tree Node -> [Node]
forall a. Tree a -> [a]
T.flatten [Tree Node]
t

isBackEdge :: [(Node, [Node])] -> Edge -> Bool
isBackEdge :: [(Node, [Node])] -> Edge -> Bool
isBackEdge [(Node, [Node])]
t (Node
u,Node
v) = Node
v Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node]
xs
  where
    (Just [Node]
xs) = Node -> [(Node, [Node])] -> Maybe [Node]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Node
u [(Node, [Node])]
t

subcEdges' :: (F.TaggedC c a) => (F.KVar -> Node) -> F.BindEnv -> c a -> [(Node, Node)]
subcEdges' :: (KVar -> Node) -> BindEnv -> c a -> [Edge]
subcEdges' KVar -> Node
kvI BindEnv
be c a
c = [(KVar -> Node
kvI KVar
k1, KVar -> Node
kvI KVar
k2) | KVar
k1 <- BindEnv -> c a -> [KVar]
forall (c :: * -> *) a. TaggedC c a => BindEnv -> c a -> [KVar]
V.envKVars BindEnv
be c a
c
                                        , KVar
k2 <- Expr -> [KVar]
forall t. Visitable t => t -> [KVar]
V.kvars (Expr -> [KVar]) -> Expr -> [KVar]
forall a b. (a -> b) -> a -> b
$ c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs c a
c]