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

isReducibleWithStart :: Gr a b -> Node -> Bool
isReducibleWithStart :: forall a b. Gr a b -> Node -> Bool
isReducibleWithStart Gr a b
g Node
x = 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              = forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ 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) <- 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              = 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 :: forall (c :: * -> *) a. TaggedC c a => GInfo c a -> Gr Node ()
convertToGraph GInfo c a
fi = forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [Edge]
vs [(Node, Node, ())]
es
  where
    subCs :: [c a]
subCs        = forall k v. HashMap k v -> [v]
M.elems (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi)
    es :: [(Node, Node, ())]
es           = forall {a} {b}. (a, b) -> (a, b, ())
lUEdge forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (c :: * -> *) a.
TaggedC c a =>
(KVar -> Node) -> BindEnv a -> c a -> [Edge]
subcEdges' KVar -> Node
kvI forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs GInfo c a
fi) [c a]
subCs
    ks :: [KVar]
ks           = forall k v. HashMap k v -> [k]
M.keys (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws GInfo c a
fi)
    kiM :: HashMap KVar Node
kiM          = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [KVar]
ks [Node
0..]
    kvI :: KVar -> Node
kvI KVar
k        = forall k v.
(HasCallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
safeLookup ([Char]
"convertToGraph: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show KVar
k) KVar
k HashMap KVar Node
kiM
    vs :: [Edge]
vs           = forall {b}. b -> (b, b)
lNode forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Node
kvI forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. HashMap k v -> [k]
M.keys (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 forall a. Eq a => a -> a -> Bool
== Node
y    = [Tree Node]
f [Tree Node] -> Node -> Bool
`contains` Node
x
                              | Node
z forall a. Eq a => a -> a -> Bool
== Node
x    = Bool
False
                              | Bool
otherwise = 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap 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) = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Node
u [(Node, [Node])]
t of
  Just [Node]
xs -> Node
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node]
xs
  -- REVIEW: Would False work instead of error?
  Maybe [Node]
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Unable to lookup back edge"


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