{-# LANGUAGE CPP                   #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE RecordWildCards       #-}

module Language.Fixpoint.Graph.Deps (
       -- * Remove Constraints that don't affect Targets
         slice

       -- * Predicate describing Targets
       , isTarget

      -- * Eliminatable KVars
      , Elims (..)
      , elimVars
      , elimDeps

      -- * Compute Raw Dependencies
      , kvEdges

      -- * Partition
      , decompose

      -- * Debug
      , graphStatistics
      ) where

import           Prelude hiding (init)
import           Data.Maybe                       (mapMaybe, fromMaybe)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup                   (Semigroup (..))
#endif

import           Data.Tree (flatten)
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Utils.Files
import           Language.Fixpoint.Types.Config
import qualified Language.Fixpoint.Types.Visitor      as V
import           Language.Fixpoint.Types.PrettyPrint
import qualified Language.Fixpoint.Types              as F
import           Language.Fixpoint.Graph.Types
import           Language.Fixpoint.Graph.Reducible  (isReducible)
import           Language.Fixpoint.Graph.Indexed

import           Control.Monad             (when)
import qualified Data.HashSet                         as S
import qualified Data.List                            as L
import qualified Data.HashMap.Strict                  as M
import qualified Data.Graph                           as G
import           Data.Function (on)
import           Data.Hashable
import           Text.PrettyPrint.HughesPJ.Compat
import           Debug.Trace (trace)

--------------------------------------------------------------------------------
-- | Compute constraints that transitively affect target constraints,
--   and delete everything else from F.SInfo a
--------------------------------------------------------------------------------
slice :: (F.TaggedC c a) => Config -> F.GInfo c a -> F.GInfo c a
--------------------------------------------------------------------------------
slice :: Config -> GInfo c a -> GInfo c a
slice Config
cfg GInfo c a
fi 
  | Config -> Bool
noslice Config
cfg 
  = GInfo c a
fi 
  | Bool
otherwise
  = GInfo c a
fi { cm :: HashMap SubcId (c a)
F.cm = HashMap SubcId (c a)
cm'
       , ws :: HashMap KVar (WfC a)
F.ws = HashMap KVar (WfC a)
ws' }
  where
     cm' :: HashMap SubcId (c a)
cm' = (SubcId -> c a -> Bool)
-> HashMap SubcId (c a) -> HashMap SubcId (c a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey SubcId -> c a -> Bool
forall p. SubcId -> p -> Bool
inC (GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi)
     ws' :: HashMap KVar (WfC a)
ws' = (KVar -> WfC a -> Bool)
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey KVar -> WfC a -> Bool
forall p. KVar -> p -> Bool
inW (GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws GInfo c a
fi)
     ks :: HashSet KVar
ks  = GInfo c a -> Slice -> HashSet KVar
forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> Slice -> HashSet KVar
sliceKVars GInfo c a
fi Slice
sl
     is :: HashSet SubcId
is  = [SubcId] -> HashSet SubcId
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (Slice -> [SubcId]
slKVarCs Slice
sl [SubcId] -> [SubcId] -> [SubcId]
forall a. [a] -> [a] -> [a]
++ Slice -> [SubcId]
slConcCs Slice
sl)
     sl :: Slice
sl  = GInfo c a -> Slice
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> Slice
mkSlice GInfo c a
fi
     inC :: SubcId -> p -> Bool
inC SubcId
i p
_ = SubcId -> HashSet SubcId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member SubcId
i HashSet SubcId
is
     inW :: KVar -> p -> Bool
inW KVar
k p
_ = KVar -> HashSet KVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member KVar
k HashSet KVar
ks

sliceKVars :: (F.TaggedC c a) => F.GInfo c a -> Slice -> S.HashSet F.KVar
sliceKVars :: GInfo c a -> Slice -> HashSet KVar
sliceKVars GInfo c a
fi Slice
sl = [KVar] -> HashSet KVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([KVar] -> HashSet KVar) -> [KVar] -> HashSet KVar
forall a b. (a -> b) -> a -> b
$ (c a -> [KVar]) -> [c a] -> [KVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BindEnv -> c a -> [KVar]
forall (c :: * -> *) a. TaggedC c a => BindEnv -> c a -> [KVar]
subcKVars BindEnv
be) [c a]
cs
  where
    cs :: [c a]
cs           = CMap (c a) -> SubcId -> c a
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap (c a)
cm (SubcId -> c a) -> [SubcId] -> [c a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Slice -> [SubcId]
slKVarCs Slice
sl [SubcId] -> [SubcId] -> [SubcId]
forall a. [a] -> [a] -> [a]
++ Slice -> [SubcId]
slConcCs Slice
sl
    be :: BindEnv
be           = GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs GInfo c a
fi
    cm :: CMap (c a)
cm           = GInfo c a -> CMap (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi

subcKVars :: (F.TaggedC c a) => F.BindEnv -> c a -> [F.KVar]
subcKVars :: BindEnv -> c a -> [KVar]
subcKVars BindEnv
be c a
c = BindEnv -> c a -> [KVar]
forall (c :: * -> *) a. TaggedC c a => BindEnv -> c a -> [KVar]
V.envKVars BindEnv
be c a
c [KVar] -> [KVar] -> [KVar]
forall a. [a] -> [a] -> [a]
++ c a -> [KVar]
forall (c :: * -> *) a. TaggedC c a => c a -> [KVar]
V.rhsKVars c a
c

--------------------------------------------------------------------------------
mkSlice :: (F.TaggedC c a) => F.GInfo c a -> Slice
--------------------------------------------------------------------------------
mkSlice :: GInfo c a -> Slice
mkSlice GInfo c a
fi        = HashMap SubcId (c a)
-> Graph
-> [DepEdge]
-> (Vertex -> SubcId)
-> (SubcId -> Vertex)
-> Slice
forall (c :: * -> *) a.
TaggedC c a =>
HashMap SubcId (c a)
-> Graph
-> [DepEdge]
-> (Vertex -> SubcId)
-> (SubcId -> Vertex)
-> Slice
mkSlice_ (GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi) Graph
g' [DepEdge]
es Vertex -> SubcId
v2i SubcId -> Vertex
i2v
  where
    g' :: Graph
g'            = Graph -> Graph
G.transposeG Graph
g  -- "inverse" of g (reverse the dep-edges)
    (Graph
g, Vertex -> DepEdge
vf, SubcId -> Maybe Vertex
cf)   = [DepEdge] -> (Graph, Vertex -> DepEdge, SubcId -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
G.graphFromEdges [DepEdge]
es
    es :: [DepEdge]
es            = CGraph -> [DepEdge]
gEdges (CGraph -> [DepEdge]) -> CGraph -> [DepEdge]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> CGraph
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> CGraph
cGraph GInfo c a
fi
    v2i :: Vertex -> SubcId
v2i           = DepEdge -> SubcId
forall a b c. (a, b, c) -> a
fst3 (DepEdge -> SubcId) -> (Vertex -> DepEdge) -> Vertex -> SubcId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vertex -> DepEdge
vf
    i2v :: SubcId -> Vertex
i2v SubcId
i         = Vertex -> Maybe Vertex -> Vertex
forall a. a -> Maybe a -> a
fromMaybe (SubcId -> Vertex
forall a a. Show a => a -> a
errU SubcId
i) (Maybe Vertex -> Vertex) -> Maybe Vertex -> Vertex
forall a b. (a -> b) -> a -> b
$ SubcId -> Maybe Vertex
cf SubcId
i
    errU :: a -> a
errU a
i        = String -> a
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"graphSlice: Unknown constraint " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

mkSlice_ :: F.TaggedC c a
         => M.HashMap F.SubcId (c a)
         -> G.Graph
         -> [DepEdge]
         -> (G.Vertex -> F.SubcId)
         -> (F.SubcId -> G.Vertex)
         -> Slice
mkSlice_ :: HashMap SubcId (c a)
-> Graph
-> [DepEdge]
-> (Vertex -> SubcId)
-> (SubcId -> Vertex)
-> Slice
mkSlice_ HashMap SubcId (c a)
cm Graph
g' [DepEdge]
es Vertex -> SubcId
v2i SubcId -> Vertex
i2v = Slice :: [SubcId] -> [SubcId] -> [DepEdge] -> Slice
Slice { slKVarCs :: [SubcId]
slKVarCs = [SubcId]
kvarCs
                                  , slConcCs :: [SubcId]
slConcCs = [SubcId]
concCs
                                  , slEdges :: [DepEdge]
slEdges  = [SubcId] -> [DepEdge] -> [DepEdge]
sliceEdges [SubcId]
kvarCs [DepEdge]
es
                                  }
  where
    -- n                  = length kvarCs
    concCs :: [SubcId]
concCs             = [ SubcId
i | (SubcId
i, c a
c) <- HashMap SubcId (c a) -> [(SubcId, c a)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId (c a)
cm, c a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget c a
c ]
    kvarCs :: [SubcId]
kvarCs             = Vertex -> SubcId
v2i (Vertex -> SubcId) -> [Vertex] -> [SubcId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Vertex]
reachVs
    rootVs :: [Vertex]
rootVs             = SubcId -> Vertex
i2v (SubcId -> Vertex) -> [SubcId] -> [Vertex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SubcId]
concCs
    reachVs :: [Vertex]
reachVs            = (Tree Vertex -> [Vertex]) -> [Tree Vertex] -> [Vertex]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Tree Vertex -> [Vertex]
forall a. Tree a -> [a]
flatten ([Tree Vertex] -> [Vertex]) -> [Tree Vertex] -> [Vertex]
forall a b. (a -> b) -> a -> b
$ Graph -> [Vertex] -> [Tree Vertex]
G.dfs Graph
g' [Vertex]
rootVs

sliceEdges :: [F.SubcId] -> [DepEdge] -> [DepEdge]
sliceEdges :: [SubcId] -> [DepEdge] -> [DepEdge]
sliceEdges [SubcId]
is [DepEdge]
es = [ (SubcId
i, SubcId
i, (SubcId -> Bool) -> [SubcId] -> [SubcId]
forall a. (a -> Bool) -> [a] -> [a]
filter SubcId -> Bool
inSlice [SubcId]
js) | (SubcId
i, SubcId
_, [SubcId]
js) <- [DepEdge]
es, SubcId -> Bool
inSlice SubcId
i ]
  where
    inSlice :: SubcId -> Bool
inSlice SubcId
i    = SubcId -> HashMap SubcId () -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member SubcId
i HashMap SubcId ()
im
    im :: HashMap SubcId ()
im           = [(SubcId, ())] -> HashMap SubcId ()
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(SubcId, ())] -> HashMap SubcId ())
-> [(SubcId, ())] -> HashMap SubcId ()
forall a b. (a -> b) -> a -> b
$ (, ()) (SubcId -> (SubcId, ())) -> [SubcId] -> [(SubcId, ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SubcId]
is

-- | DO NOT DELETE!
-- sliceCSucc :: Slice -> CSucc
-- sliceCSucc sl = \i -> M.lookupDefault [] i im
  -- where
    -- im        = M.fromList [(i, is) | (i,_,is) <- slEdges sl]

--------------------------------------------------------------------------------
isTarget :: (F.TaggedC c a) => c a -> Bool
--------------------------------------------------------------------------------
isTarget :: c a -> Bool
isTarget c a
c   = c a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
V.isConcC c a
c Bool -> Bool -> Bool
&& c a -> Bool
isNonTriv c a
c
  where
   isNonTriv :: c a -> Bool
isNonTriv = Bool -> Bool
not (Bool -> Bool) -> (c a -> Bool) -> c a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Expr -> Bool
F.isTautoPred (Expr -> Bool) -> (c a -> Expr) -> c a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs


--------------------------------------------------------------------------------
-- | Constraint Graph ----------------------------------------------------------
--------------------------------------------------------------------------------
cGraph :: (F.TaggedC c a) => F.GInfo c a -> CGraph
---------------------------------------------------------------------------
cGraph :: GInfo c a -> CGraph
cGraph GInfo c a
fi = CGraph :: [DepEdge] -> CMap Vertex -> CMap [SubcId] -> Vertex -> CGraph
CGraph { gEdges :: [DepEdge]
gEdges = [DepEdge]
es
                   , gRanks :: CMap Vertex
gRanks = CMap Vertex
outRs
                   , gSucc :: CMap [SubcId]
gSucc  = CMap [SubcId]
next
                   , gSccs :: Vertex
gSccs  = [[Vertex]] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [[Vertex]]
sccs }
  where
    es :: [DepEdge]
es             = [(SubcId
i, SubcId
i, [SubcId] -> SubcId -> CMap [SubcId] -> [SubcId]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] SubcId
i CMap [SubcId]
next) | SubcId
i <- HashMap SubcId (c a) -> [SubcId]
forall k v. HashMap k v -> [k]
M.keys (HashMap SubcId (c a) -> [SubcId])
-> HashMap SubcId (c a) -> [SubcId]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi]
    next :: CMap [SubcId]
next           = GInfo c a -> CMap [SubcId]
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> CMap [SubcId]
kvSucc GInfo c a
fi
    (Graph
g, Vertex -> DepEdge
vf, SubcId -> Maybe Vertex
_)     = [DepEdge] -> (Graph, Vertex -> DepEdge, SubcId -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
G.graphFromEdges [DepEdge]
es
    (CMap Vertex
outRs, [[Vertex]]
sccs)  = Graph -> (Vertex -> DepEdge) -> (CMap Vertex, [[Vertex]])
graphRanks Graph
g Vertex -> DepEdge
vf

--------------------------------------------------------------------------------
-- | Ranks from Graph ----------------------------------------------------------
--------------------------------------------------------------------------------
graphRanks :: G.Graph -> (G.Vertex -> DepEdge) -> (CMap Int, [[G.Vertex]])
---------------------------------------------------------------------------
graphRanks :: Graph -> (Vertex -> DepEdge) -> (CMap Vertex, [[Vertex]])
graphRanks Graph
g Vertex -> DepEdge
vf = ([(SubcId, Vertex)] -> CMap Vertex
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(SubcId, Vertex)]
irs, [[Vertex]]
sccs)
  where
    irs :: [(SubcId, Vertex)]
irs        = [(Vertex -> SubcId
v2i Vertex
v, Vertex
r) | (Vertex
r, [Vertex]
vs) <- [(Vertex, [Vertex])]
rvss, Vertex
v <- [Vertex]
vs ]
    rvss :: [(Vertex, [Vertex])]
rvss       = [Vertex] -> [[Vertex]] -> [(Vertex, [Vertex])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Vertex
0..] [[Vertex]]
sccs
    sccs :: [[Vertex]]
sccs       = [[Vertex]] -> [[Vertex]]
forall a. [a] -> [a]
L.reverse ([[Vertex]] -> [[Vertex]]) -> [[Vertex]] -> [[Vertex]]
forall a b. (a -> b) -> a -> b
$ (Tree Vertex -> [Vertex]) -> [Tree Vertex] -> [[Vertex]]
forall a b. (a -> b) -> [a] -> [b]
map Tree Vertex -> [Vertex]
forall a. Tree a -> [a]
flatten ([Tree Vertex] -> [[Vertex]]) -> [Tree Vertex] -> [[Vertex]]
forall a b. (a -> b) -> a -> b
$ Graph -> [Tree Vertex]
G.scc Graph
g
    v2i :: Vertex -> SubcId
v2i        = DepEdge -> SubcId
forall a b c. (a, b, c) -> a
fst3 (DepEdge -> SubcId) -> (Vertex -> DepEdge) -> Vertex -> SubcId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vertex -> DepEdge
vf

--------------------------------------------------------------------------------
-- | Dependencies --------------------------------------------------------------
--------------------------------------------------------------------------------
kvSucc :: (F.TaggedC c a) => F.GInfo c a -> CMap [F.SubcId]
--------------------------------------------------------------------------------
kvSucc :: GInfo c a -> CMap [SubcId]
kvSucc GInfo c a
fi = CMap (c a) -> KVRead -> CMap [SubcId]
forall (c :: * -> *) a.
TaggedC c a =>
CMap (c a) -> KVRead -> CMap [SubcId]
succs CMap (c a)
cm KVRead
rdBy
  where
    rdBy :: KVRead
rdBy  = GInfo c a -> KVRead
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> KVRead
kvReadBy GInfo c a
fi
    cm :: CMap (c a)
cm    = GInfo c a -> CMap (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm     GInfo c a
fi

succs :: (F.TaggedC c a) => CMap (c a) -> KVRead -> CMap [F.SubcId]
succs :: CMap (c a) -> KVRead -> CMap [SubcId]
succs CMap (c a)
cm KVRead
rdBy = ([SubcId] -> [SubcId]
forall a. Ord a => [a] -> [a]
sortNub ([SubcId] -> [SubcId]) -> (c a -> [SubcId]) -> c a -> [SubcId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar -> [SubcId]) -> [KVar] -> [SubcId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap KVar -> [SubcId]
kvReads ([KVar] -> [SubcId]) -> (c a -> [KVar]) -> c a -> [SubcId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> [KVar]
kvWrites) (c a -> [SubcId]) -> CMap (c a) -> CMap [SubcId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CMap (c a)
cm
  where
    kvReads :: KVar -> [SubcId]
kvReads KVar
k = [SubcId] -> KVar -> KVRead -> [SubcId]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KVRead
rdBy
    kvWrites :: c a -> [KVar]
kvWrites  = Expr -> [KVar]
forall t. Visitable t => t -> [KVar]
V.kvars (Expr -> [KVar]) -> (c a -> Expr) -> c a -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs

--------------------------------------------------------------------------------
kvWriteBy :: (F.TaggedC c a) => CMap (c a) -> F.SubcId -> [F.KVar]
--------------------------------------------------------------------------------
kvWriteBy :: CMap (c a) -> SubcId -> [KVar]
kvWriteBy CMap (c a)
cm = Expr -> [KVar]
forall t. Visitable t => t -> [KVar]
V.kvars (Expr -> [KVar]) -> (SubcId -> Expr) -> SubcId -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs (c a -> Expr) -> (SubcId -> c a) -> SubcId -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CMap (c a) -> SubcId -> c a
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap (c a)
cm

--------------------------------------------------------------------------------
kvReadBy :: (F.TaggedC c a) => F.GInfo c a -> KVRead
--------------------------------------------------------------------------------
kvReadBy :: GInfo c a -> KVRead
kvReadBy GInfo c a
fi = [(KVar, SubcId)] -> KVRead
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (KVar
k, SubcId
i) | (SubcId
i, c a
ci) <- HashMap SubcId (c a) -> [(SubcId, c a)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId (c a)
cm
                             , KVar
k       <- BindEnv -> c a -> [KVar]
forall (c :: * -> *) a. TaggedC c a => BindEnv -> c a -> [KVar]
V.envKVars BindEnv
bs c a
ci]
  where
    cm :: HashMap SubcId (c a)
cm      = GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi
    bs :: BindEnv
bs      = GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs GInfo c a
fi

--------------------------------------------------------------------------------
decompose :: (F.TaggedC c a) => F.GInfo c a -> KVComps
--------------------------------------------------------------------------------
decompose :: GInfo c a -> KVComps
decompose = (GInfo c a -> [(CVertex, CVertex, [CVertex])])
-> GInfo c a -> KVComps
forall c a b. Ord c => (a -> [(b, c, [c])]) -> a -> [[b]]
componentsWith (KVGraph -> [(CVertex, CVertex, [CVertex])]
kvgEdges (KVGraph -> [(CVertex, CVertex, [CVertex])])
-> (GInfo c a -> KVGraph)
-> GInfo c a
-> [(CVertex, CVertex, [CVertex])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> KVGraph
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> KVGraph
kvGraph)

--------------------------------------------------------------------------------
kvGraph :: (F.TaggedC c a) => F.GInfo c a -> KVGraph
--------------------------------------------------------------------------------
kvGraph :: GInfo c a -> KVGraph
kvGraph = [CEdge] -> KVGraph
edgeGraph ([CEdge] -> KVGraph)
-> (GInfo c a -> [CEdge]) -> GInfo c a -> KVGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> [CEdge]
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> [CEdge]
kvEdges

edgeGraph :: [CEdge] -> KVGraph
edgeGraph :: [CEdge] -> KVGraph
edgeGraph [CEdge]
es = [(CVertex, CVertex, [CVertex])] -> KVGraph
KVGraph [(CVertex
v, CVertex
v, [CVertex]
vs) | (CVertex
v, [CVertex]
vs) <- [CEdge] -> [(CVertex, [CVertex])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
groupList [CEdge]
es ]

-- need to plumb list of ebinds
kvEdges :: (F.TaggedC c a) => F.GInfo c a -> [CEdge]
kvEdges :: GInfo c a -> [CEdge]
kvEdges GInfo c a
fi = [CEdge]
selfes [CEdge] -> [CEdge] -> [CEdge]
forall a. [a] -> [a] -> [a]
++ (c a -> [CEdge]) -> [c a] -> [CEdge]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BindEnv -> c a -> [CEdge]
forall (c :: * -> *) a. TaggedC c a => BindEnv -> c a -> [CEdge]
subcEdges BindEnv
bs) [c a]
cs [CEdge] -> [CEdge] -> [CEdge]
forall a. [a] -> [a] -> [a]
++ (c a -> [CEdge]) -> [c a] -> [CEdge]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Vertex] -> BindEnv -> c a -> [CEdge]
forall (c :: * -> *) a.
TaggedC c a =>
[Vertex] -> BindEnv -> c a -> [CEdge]
ebindEdges [Vertex]
ebs BindEnv
bs) [c a]
cs
  where
    bs :: BindEnv
bs     = GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs GInfo c a
fi
    ebs :: [Vertex]
ebs    = GInfo c a -> [Vertex]
forall (c :: * -> *) a. GInfo c a -> [Vertex]
F.ebinds GInfo c a
fi
    cs :: [c a]
cs     = 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)
    ks :: [KVar]
ks     = GInfo c a -> [KVar]
forall (c :: * -> *) a. GInfo c a -> [KVar]
fiKVars GInfo c a
fi
    selfes :: [CEdge]
selfes =  [(SubcId -> CVertex
Cstr SubcId
i , SubcId -> CVertex
Cstr  SubcId
i) | c a
c <- [c a]
cs, let i :: SubcId
i = c a -> SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
F.subcId c a
c]
           [CEdge] -> [CEdge] -> [CEdge]
forall a. [a] -> [a] -> [a]
++ [(KVar -> CVertex
KVar KVar
k , KVar -> CVertex
DKVar KVar
k) | KVar
k <- [KVar]
ks]
           [CEdge] -> [CEdge] -> [CEdge]
forall a. [a] -> [a] -> [a]
++ [(KVar -> CVertex
DKVar KVar
k, KVar -> CVertex
DKVar KVar
k) | KVar
k <- [KVar]
ks]

fiKVars :: F.GInfo c a -> [F.KVar]
fiKVars :: GInfo c a -> [KVar]
fiKVars = HashMap KVar (WfC a) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys (HashMap KVar (WfC a) -> [KVar])
-> (GInfo c a -> HashMap KVar (WfC a)) -> GInfo c a -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws

ebindEdges :: (F.TaggedC c a) => [F.BindId] -> F.BindEnv -> c a -> [CEdge]
ebindEdges :: [Vertex] -> BindEnv -> c a -> [CEdge]
ebindEdges [Vertex]
ebs BindEnv
bs c a
c =  [(Symbol -> CVertex
EBind Symbol
k, SubcId -> CVertex
Cstr SubcId
i ) | Symbol
k  <- [Symbol] -> BindEnv -> c a -> [Symbol]
forall (c :: * -> *) a (t :: * -> *).
(TaggedC c a, Foldable t) =>
t Symbol -> BindEnv -> c a -> [Symbol]
envEbinds [Symbol]
xs BindEnv
bs c a
c ]
                    [CEdge] -> [CEdge] -> [CEdge]
forall a. [a] -> [a] -> [a]
++ [(SubcId -> CVertex
Cstr SubcId
i, Symbol -> CVertex
EBind Symbol
k') | Symbol
k' <- [Symbol] -> c a -> [Symbol]
forall (t :: * -> *) (c :: * -> *) a.
(Foldable t, TaggedC c a) =>
t Symbol -> c a -> [Symbol]
rhsEbinds [Symbol]
xs c a
c ]
  where
    i :: SubcId
i          = c a -> SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
F.subcId c a
c
    xs :: [Symbol]
xs         = (Symbol, SortedReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SortedReft) -> Symbol)
-> (Vertex -> (Symbol, SortedReft)) -> Vertex -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vertex -> BindEnv -> (Symbol, SortedReft))
-> BindEnv -> Vertex -> (Symbol, SortedReft)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Vertex -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv BindEnv
bs (Vertex -> Symbol) -> [Vertex] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Vertex]
ebs

envEbinds :: (F.TaggedC c a, Foldable t) =>
             t F.Symbol -> F.BindEnv -> c a -> [F.Symbol]
envEbinds :: t Symbol -> BindEnv -> c a -> [Symbol]
envEbinds t Symbol
xs BindEnv
be c a
c = [ Symbol
x | Symbol
x <- [Symbol]
envBinds , Symbol
x Symbol -> t Symbol -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Symbol
xs ]
  where envBinds :: [Symbol]
envBinds = (Symbol, SortedReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SortedReft) -> Symbol)
-> [(Symbol, SortedReft)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BindEnv -> c a -> [(Symbol, SortedReft)]
forall (c :: * -> *) a.
TaggedC c a =>
BindEnv -> c a -> [(Symbol, SortedReft)]
F.clhs BindEnv
be c a
c
rhsEbinds :: (Foldable t, F.TaggedC c a) =>
             t F.Symbol -> c a -> [F.Symbol]
rhsEbinds :: t Symbol -> c a -> [Symbol]
rhsEbinds t Symbol
xs c a
c = [ Symbol
x | Symbol
x <- Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms (c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs c a
c) , Symbol
x Symbol -> t Symbol -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Symbol
xs ]

subcEdges :: (F.TaggedC c a) => F.BindEnv -> c a -> [CEdge]
subcEdges :: BindEnv -> c a -> [CEdge]
subcEdges BindEnv
bs c a
c =  [(KVar -> CVertex
KVar KVar
k, SubcId -> CVertex
Cstr SubcId
i ) | KVar
k  <- BindEnv -> c a -> [KVar]
forall (c :: * -> *) a. TaggedC c a => BindEnv -> c a -> [KVar]
V.envKVars BindEnv
bs c a
c]
               [CEdge] -> [CEdge] -> [CEdge]
forall a. [a] -> [a] -> [a]
++ [(SubcId -> CVertex
Cstr SubcId
i, KVar -> CVertex
KVar KVar
k') | KVar
k' <- c a -> [KVar]
forall (c :: * -> *) a. TaggedC c a => c a -> [KVar]
V.rhsKVars c a
c ]
  where
    i :: SubcId
i          = c a -> SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
F.subcId c a
c

--------------------------------------------------------------------------------
-- | Eliminated Dependencies
--------------------------------------------------------------------------------
elimDeps :: (F.TaggedC c a) => F.GInfo c a -> [CEdge] -> S.HashSet F.KVar -> S.HashSet F.Symbol -> CDeps
elimDeps :: GInfo c a -> [CEdge] -> HashSet KVar -> HashSet Symbol -> CDeps
elimDeps GInfo c a
si [CEdge]
es HashSet KVar
nonKutVs HashSet Symbol
ebs = GInfo c a -> [CEdge] -> CDeps
forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> CDeps
graphDeps GInfo c a
si [CEdge]
es'
  where
    es' :: [CEdge]
es'                 = [CEdge] -> HashSet KVar -> HashSet Symbol -> [CEdge]
graphElim [CEdge]
es HashSet KVar
nonKutVs HashSet Symbol
ebs
    _msg :: String
_msg                = String
"graphElim: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Vertex -> String
forall a. Show a => a -> String
show ([CEdge] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [CEdge]
es')

{- | `graphElim` "eliminates" a kvar k by replacing every "path"

          ki -> ci -> k -> c

      with an edge

          ki ------------> c
-}
graphElim :: [CEdge] -> S.HashSet F.KVar -> S.HashSet F.Symbol -> [CEdge]
graphElim :: [CEdge] -> HashSet KVar -> HashSet Symbol -> [CEdge]
graphElim [CEdge]
es HashSet KVar
ks HashSet Symbol
_ebs = IKVGraph -> [CEdge]
ikvgEdges (IKVGraph -> [CEdge]) -> IKVGraph -> [CEdge]
forall a b. (a -> b) -> a -> b
$ -- elimEs (S.map EBind ebs) $
                                  HashSet CVertex -> IKVGraph -> IKVGraph
elimKs ((KVar -> CVertex) -> HashSet KVar -> HashSet CVertex
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map KVar -> CVertex
KVar HashSet KVar
ks)   (IKVGraph -> IKVGraph) -> IKVGraph -> IKVGraph
forall a b. (a -> b) -> a -> b
$ [CEdge] -> IKVGraph
edgesIkvg [CEdge]
es
  where
    elimKs :: HashSet CVertex -> IKVGraph -> IKVGraph
elimKs      = (IKVGraph -> HashSet CVertex -> IKVGraph)
-> HashSet CVertex -> IKVGraph -> IKVGraph
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((IKVGraph -> CVertex -> IKVGraph)
-> IKVGraph -> HashSet CVertex -> IKVGraph
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl' IKVGraph -> CVertex -> IKVGraph
elimK)
    _elimEs :: HashSet CVertex -> IKVGraph -> IKVGraph
_elimEs      = (IKVGraph -> HashSet CVertex -> IKVGraph)
-> HashSet CVertex -> IKVGraph -> IKVGraph
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((IKVGraph -> CVertex -> IKVGraph)
-> IKVGraph -> HashSet CVertex -> IKVGraph
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl' IKVGraph -> CVertex -> IKVGraph
elimE)

elimE  :: IKVGraph -> CVertex -> IKVGraph
elimE :: IKVGraph -> CVertex -> IKVGraph
elimE IKVGraph
g CVertex
e = IKVGraph
g IKVGraph -> [CVertex] -> IKVGraph
`delNodes` (CVertex
e CVertex -> [CVertex] -> [CVertex]
forall a. a -> [a] -> [a]
: [CVertex]
cs)
  where cs :: [CVertex]
cs = IKVGraph -> CVertex -> [CVertex]
getPreds IKVGraph
g CVertex
e

elimK  :: IKVGraph -> CVertex -> IKVGraph
elimK :: IKVGraph -> CVertex -> IKVGraph
elimK IKVGraph
g CVertex
kV   = (IKVGraph
g IKVGraph -> [CEdge] -> IKVGraph
`addLinks` [CEdge]
es') IKVGraph -> [CVertex] -> IKVGraph
`delNodes` (CVertex
kV CVertex -> [CVertex] -> [CVertex]
forall a. a -> [a] -> [a]
: [CVertex]
cis)
  where
   es' :: [CEdge]
es'      = [(CVertex
ki, CVertex
c) | CVertex
ki <- (CVertex -> Bool) -> [CVertex] -> [CVertex]
forall a. (a -> Bool) -> [a] -> [a]
filter CVertex -> Bool
unC [CVertex]
kis, c :: CVertex
c@(Cstr SubcId
_) <- [CVertex]
cs]
   cs :: [CVertex]
cs       = IKVGraph -> CVertex -> [CVertex]
getSuccs IKVGraph
g CVertex
kV
   cis :: [CVertex]
cis      = IKVGraph -> CVertex -> [CVertex]
getPreds IKVGraph
g CVertex
kV
   kis :: [CVertex]
kis      = (CVertex -> [CVertex]) -> [CVertex] -> [CVertex]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (IKVGraph -> CVertex -> [CVertex]
getPreds IKVGraph
g) [CVertex]
cis
   unC :: CVertex -> Bool
unC (Cstr SubcId
_) = Bool
False
   unC CVertex
_        = Bool
True

--------------------------------------------------------------------------------
-- | Generic Dependencies ------------------------------------------------------
--------------------------------------------------------------------------------
data Elims a
  = Deps { Elims a -> HashSet a
depCuts    :: !(S.HashSet a)
         , Elims a -> HashSet a
depNonCuts :: !(S.HashSet a)
         }
    deriving (Vertex -> Elims a -> String -> String
[Elims a] -> String -> String
Elims a -> String
(Vertex -> Elims a -> String -> String)
-> (Elims a -> String)
-> ([Elims a] -> String -> String)
-> Show (Elims a)
forall a. Show a => Vertex -> Elims a -> String -> String
forall a. Show a => [Elims a] -> String -> String
forall a. Show a => Elims a -> String
forall a.
(Vertex -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Elims a] -> String -> String
$cshowList :: forall a. Show a => [Elims a] -> String -> String
show :: Elims a -> String
$cshow :: forall a. Show a => Elims a -> String
showsPrec :: Vertex -> Elims a -> String -> String
$cshowsPrec :: forall a. Show a => Vertex -> Elims a -> String -> String
Show)

instance PPrint (Elims a) where
  pprintTidy :: Tidy -> Elims a -> Doc
pprintTidy Tidy
_ Elims a
d = Doc
"#Cuts ="    Doc -> Doc -> Doc
<+> HashSet a -> Doc
forall a. HashSet a -> Doc
ppSize (Elims a -> HashSet a
forall a. Elims a -> HashSet a
depCuts Elims a
d) Doc -> Doc -> Doc
<+>
                   Doc
"#NonCuts =" Doc -> Doc -> Doc
<+> HashSet a -> Doc
forall a. HashSet a -> Doc
ppSize (Elims a -> HashSet a
forall a. Elims a -> HashSet a
depNonCuts Elims a
d)
    where
      ppSize :: HashSet a -> Doc
ppSize     = Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint (Vertex -> Doc) -> (HashSet a -> Vertex) -> HashSet a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet a -> Vertex
forall a. HashSet a -> Vertex
S.size

instance (Eq a, Hashable a) => Semigroup (Elims a) where
  Deps HashSet a
d1 HashSet a
n1 <> :: Elims a -> Elims a -> Elims a
<> Deps HashSet a
d2 HashSet a
n2 = HashSet a -> HashSet a -> Elims a
forall a. HashSet a -> HashSet a -> Elims a
Deps (HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet a
d1 HashSet a
d2) (HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet a
n1 HashSet a
n2)

instance (Eq a, Hashable a) => Monoid (Elims a) where
  mempty :: Elims a
mempty  = HashSet a -> HashSet a -> Elims a
forall a. HashSet a -> HashSet a -> Elims a
Deps HashSet a
forall a. HashSet a
S.empty HashSet a
forall a. HashSet a
S.empty
  mappend :: Elims a -> Elims a -> Elims a
mappend = Elims a -> Elims a -> Elims a
forall a. Semigroup a => a -> a -> a
(<>)

dCut, dNonCut :: (Hashable a) => a -> Elims a
dNonCut :: a -> Elims a
dNonCut a
v = HashSet a -> HashSet a -> Elims a
forall a. HashSet a -> HashSet a -> Elims a
Deps HashSet a
forall a. HashSet a
S.empty (a -> HashSet a
forall a. Hashable a => a -> HashSet a
S.singleton a
v)
dCut :: a -> Elims a
dCut    a
v = HashSet a -> HashSet a -> Elims a
forall a. HashSet a -> HashSet a -> Elims a
Deps (a -> HashSet a
forall a. Hashable a => a -> HashSet a
S.singleton a
v) HashSet a
forall a. HashSet a
S.empty

--------------------------------------------------------------------------------
-- | Compute Dependencies and Cuts ---------------------------------------------
--------------------------------------------------------------------------------
elimVars :: (F.TaggedC c a) => Config -> F.GInfo c a -> ([CEdge], Elims F.KVar)
--------------------------------------------------------------------------------
elimVars :: Config -> GInfo c a -> ([CEdge], Elims KVar)
elimVars Config
cfg GInfo c a
si = ([CEdge]
es, Elims KVar
ds)
  where
    ds :: Elims KVar
ds          = Config -> GInfo c a -> [CEdge] -> Elims KVar
forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> [CEdge] -> Elims KVar
edgeDeps Config
cfg GInfo c a
si [CEdge]
es
    es :: [CEdge]
es          = GInfo c a -> [CEdge]
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> [CEdge]
kvEdges GInfo c a
si

removeKutEdges ::  S.HashSet F.KVar -> [CEdge] -> [CEdge]
removeKutEdges :: HashSet KVar -> [CEdge] -> [CEdge]
removeKutEdges HashSet KVar
ks = (CEdge -> Bool) -> [CEdge] -> [CEdge]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CEdge -> Bool) -> CEdge -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVertex -> Bool
isKut (CVertex -> Bool) -> (CEdge -> CVertex) -> CEdge -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CEdge -> CVertex
forall a b. (a, b) -> b
snd)
  where
    cutVs :: HashSet CVertex
cutVs         = (KVar -> CVertex) -> HashSet KVar -> HashSet CVertex
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map KVar -> CVertex
KVar HashSet KVar
ks
    isKut :: CVertex -> Bool
isKut         = (CVertex -> HashSet CVertex -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet CVertex
cutVs)

cutVars :: (F.TaggedC c a) => Config -> F.GInfo c a -> S.HashSet F.KVar
cutVars :: Config -> GInfo c a -> HashSet KVar
cutVars Config
cfg GInfo c a
si
  | Config -> Bool
autoKuts Config
cfg = HashSet KVar
forall a. HashSet a
S.empty
  | Bool
otherwise    = Kuts -> HashSet KVar
F.ksVars (Kuts -> HashSet KVar)
-> (GInfo c a -> Kuts) -> GInfo c a -> HashSet KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> Kuts
forall (c :: * -> *) a. GInfo c a -> Kuts
F.kuts (GInfo c a -> HashSet KVar) -> GInfo c a -> HashSet KVar
forall a b. (a -> b) -> a -> b
$ GInfo c a
si

forceKuts :: (Hashable a, Eq a) => S.HashSet a -> Elims a  -> Elims a
forceKuts :: HashSet a -> Elims a -> Elims a
forceKuts HashSet a
xs (Deps HashSet a
cs HashSet a
ns) = HashSet a -> HashSet a -> Elims a
forall a. HashSet a -> HashSet a -> Elims a
Deps (HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet a
cs HashSet a
xs) (HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet a
ns HashSet a
xs)

edgeDeps :: (F.TaggedC c a) => Config -> F.GInfo c a -> [CEdge] -> Elims F.KVar
edgeDeps :: Config -> GInfo c a -> [CEdge] -> Elims KVar
edgeDeps Config
cfg GInfo c a
si  = HashSet KVar -> Elims KVar -> Elims KVar
forall a. (Hashable a, Eq a) => HashSet a -> Elims a -> Elims a
forceKuts HashSet KVar
ks
                 (Elims KVar -> Elims KVar)
-> ([CEdge] -> Elims KVar) -> [CEdge] -> Elims KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> [CEdge] -> Elims KVar
edgeDeps' Config
cfg
                 ([CEdge] -> Elims KVar)
-> ([CEdge] -> [CEdge]) -> [CEdge] -> Elims KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet KVar -> [CEdge] -> [CEdge]
removeKutEdges HashSet KVar
ks
                 ([CEdge] -> [CEdge]) -> ([CEdge] -> [CEdge]) -> [CEdge] -> [CEdge]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CEdge -> Bool) -> [CEdge] -> [CEdge]
forall a. (a -> Bool) -> [a] -> [a]
filter CEdge -> Bool
isRealEdge
  where
    ks :: HashSet KVar
ks           = HashSet KVar
givenKs HashSet KVar -> HashSet KVar -> HashSet KVar
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet KVar
nlKs
    givenKs :: HashSet KVar
givenKs      = Config -> GInfo c a -> HashSet KVar
forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> HashSet KVar
cutVars Config
cfg    GInfo c a
si
    nlKs :: HashSet KVar
nlKs
      | Config -> Bool
nonLinCuts Config
cfg = GInfo c a -> HashSet KVar
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> HashSet KVar
nonLinearKVars GInfo c a
si
      | Bool
otherwise      = HashSet KVar
forall a. Monoid a => a
mempty

edgeDeps' :: Config -> [CEdge] -> Elims F.KVar
edgeDeps' :: Config -> [CEdge] -> Elims KVar
edgeDeps' Config
cfg [CEdge]
es = HashSet KVar -> HashSet KVar -> Elims KVar
forall a. HashSet a -> HashSet a -> Elims a
Deps (HashSet CVertex -> HashSet KVar
takeK HashSet CVertex
cs) (HashSet CVertex -> HashSet KVar
takeK HashSet CVertex
ns)
  where
    Deps HashSet CVertex
cs HashSet CVertex
ns   = Config
-> (CVertex -> Bool)
-> Cutter CVertex
-> [(CVertex, CVertex, [CVertex])]
-> Elims CVertex
forall a.
Cutable a =>
Config -> (a -> Bool) -> Cutter a -> [(a, a, [a])] -> Elims a
gElims Config
cfg CVertex -> Bool
kF Cutter CVertex
cutF [(CVertex, CVertex, [CVertex])]
g
    g :: [(CVertex, CVertex, [CVertex])]
g            = KVGraph -> [(CVertex, CVertex, [CVertex])]
kvgEdges    ([CEdge] -> KVGraph
edgeGraph [CEdge]
es)
    cutF :: Cutter CVertex
cutF         = EdgeRank -> Cutter CVertex
edgeRankCut ([CEdge] -> EdgeRank
edgeRank [CEdge]
es)
    takeK :: HashSet CVertex -> HashSet KVar
takeK        = (CVertex -> Maybe KVar) -> HashSet CVertex -> HashSet KVar
forall b a.
(Hashable b, Eq b) =>
(a -> Maybe b) -> HashSet a -> HashSet b
sMapMaybe CVertex -> Maybe KVar
tx
    tx :: CVertex -> Maybe KVar
tx (KVar KVar
z)  = KVar -> Maybe KVar
forall a. a -> Maybe a
Just KVar
z
    tx CVertex
_         = Maybe KVar
forall a. Maybe a
Nothing
    kF :: CVertex -> Bool
kF (KVar KVar
_)  = Bool
True
    kF CVertex
_         = Bool
False

sMapMaybe :: (Hashable b, Eq b) => (a -> Maybe b) -> S.HashSet a -> S.HashSet b
sMapMaybe :: (a -> Maybe b) -> HashSet a -> HashSet b
sMapMaybe a -> Maybe b
f = [b] -> HashSet b
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([b] -> HashSet b) -> (HashSet a -> [b]) -> HashSet a -> HashSet b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe b) -> [a] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe a -> Maybe b
f ([a] -> [b]) -> (HashSet a -> [a]) -> HashSet a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet a -> [a]
forall a. HashSet a -> [a]
S.toList

--------------------------------------------------------------------------------
type EdgeRank = M.HashMap F.KVar Integer
--------------------------------------------------------------------------------
edgeRank :: [CEdge] -> EdgeRank
edgeRank :: [CEdge] -> EdgeRank
edgeRank [CEdge]
es = [SubcId] -> SubcId
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([SubcId] -> SubcId)
-> ([SubcId] -> [SubcId]) -> [SubcId] -> SubcId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubcId
n SubcId -> [SubcId] -> [SubcId]
forall a. a -> [a] -> [a]
:) ([SubcId] -> SubcId) -> KVRead -> EdgeRank
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KVRead
kiM
  where
    n :: SubcId
n       = SubcId
1 SubcId -> SubcId -> SubcId
forall a. Num a => a -> a -> a
+ [SubcId] -> SubcId
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ SubcId
i | (Cstr SubcId
i, CVertex
_)     <- [CEdge]
es ]
    kiM :: KVRead
kiM     = [(KVar, SubcId)] -> KVRead
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (KVar
k, SubcId
i) | (KVar KVar
k, Cstr SubcId
i) <- [CEdge]
es ]

edgeRankCut :: EdgeRank -> Cutter CVertex
edgeRankCut :: EdgeRank -> Cutter CVertex
edgeRankCut EdgeRank
km [(CVertex, CVertex, [CVertex])]
vs = case [KVar]
ks of
                      []  -> Maybe (CVertex, [(CVertex, CVertex, [CVertex])])
forall a. Maybe a
Nothing
                      KVar
k:[KVar]
_ -> (CVertex, [(CVertex, CVertex, [CVertex])])
-> Maybe (CVertex, [(CVertex, CVertex, [CVertex])])
forall a. a -> Maybe a
Just (KVar -> CVertex
KVar KVar
k, [(CVertex, CVertex, [CVertex])
x | x :: (CVertex, CVertex, [CVertex])
x@(CVertex
u,CVertex
_,[CVertex]
_) <- [(CVertex, CVertex, [CVertex])]
vs, CVertex
u CVertex -> CVertex -> Bool
forall a. Eq a => a -> a -> Bool
/= KVar -> CVertex
KVar KVar
k])
  where
    ks :: [KVar]
ks            = [KVar] -> [KVar]
orderBy [KVar
k | (KVar KVar
k, CVertex
_ ,[CVertex]
_) <- [(CVertex, CVertex, [CVertex])]
vs]
    rank :: KVar -> SubcId
rank          = (EdgeRank
km EdgeRank -> KVar -> SubcId
forall k v.
(Eq k, Hashable k, ?callStack::CallStack) =>
HashMap k v -> k -> v
M.!)
    orderBy :: [KVar] -> [KVar]
orderBy       = (KVar -> KVar -> Ordering) -> [KVar] -> [KVar]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (SubcId -> SubcId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SubcId -> SubcId -> Ordering)
-> (KVar -> SubcId) -> KVar -> KVar -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` KVar -> SubcId
rank)

--------------------------------------------------------------------------------
type Cutter a = [(a, a, [a])] -> Maybe (a, [(a, a, [a])])
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
type Cutable a = (Eq a, Ord a, Hashable a, Show a)
--------------------------------------------------------------------------------
gElims :: (Cutable a) => Config -> (a -> Bool) -> Cutter a -> [(a, a, [a])] -> Elims a
--------------------------------------------------------------------------------
gElims :: Config -> (a -> Bool) -> Cutter a -> [(a, a, [a])] -> Elims a
gElims Config
cfg a -> Bool
kF Cutter a
cutF [(a, a, [a])]
g = Config -> (a -> Bool) -> [(a, a, [a])] -> Elims a -> Elims a
forall a.
Cutable a =>
Config -> (a -> Bool) -> [(a, a, [a])] -> Elims a -> Elims a
boundElims Config
cfg a -> Bool
kF [(a, a, [a])]
g (Elims a -> Elims a) -> Elims a -> Elims a
forall a b. (a -> b) -> a -> b
$ Cutter a -> [(a, a, [a])] -> Elims a
forall a. Cutable a => Cutter a -> [(a, a, [a])] -> Elims a
sccElims Cutter a
cutF [(a, a, [a])]
g

--------------------------------------------------------------------------------
-- | `sccElims` returns an `Elims` that renders the dependency graph acyclic
--    by picking _at least one_ kvar from each non-trivial SCC in the graph
--------------------------------------------------------------------------------

sccElims :: (Cutable a) => Cutter a -> [(a, a, [a])] -> Elims a
sccElims :: Cutter a -> [(a, a, [a])] -> Elims a
sccElims Cutter a
f = Cutter a -> [SCC (a, a, [a])] -> Elims a
forall a. Cutable a => Cutter a -> [SCC (a, a, [a])] -> Elims a
sccsToDeps Cutter a
f ([SCC (a, a, [a])] -> Elims a)
-> ([(a, a, [a])] -> [SCC (a, a, [a])]) -> [(a, a, [a])] -> Elims a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, a, [a])] -> [SCC (a, a, [a])]
forall key node.
Ord key =>
[(node, key, [key])] -> [SCC (node, key, [key])]
G.stronglyConnCompR

sccsToDeps :: (Cutable a) => Cutter a -> [G.SCC (a, a, [a])] -> Elims a
sccsToDeps :: Cutter a -> [SCC (a, a, [a])] -> Elims a
sccsToDeps Cutter a
f [SCC (a, a, [a])]
xs = [Elims a] -> Elims a
forall a. Monoid a => [a] -> a
mconcat ([Elims a] -> Elims a) -> [Elims a] -> Elims a
forall a b. (a -> b) -> a -> b
$ Cutter a -> SCC (a, a, [a]) -> Elims a
forall a. Cutable a => Cutter a -> SCC (a, a, [a]) -> Elims a
sccDep Cutter a
f (SCC (a, a, [a]) -> Elims a) -> [SCC (a, a, [a])] -> [Elims a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SCC (a, a, [a])]
xs

sccDep :: (Cutable a) =>  Cutter a -> G.SCC (a, a, [a]) -> Elims a
sccDep :: Cutter a -> SCC (a, a, [a]) -> Elims a
sccDep Cutter a
_ (G.AcyclicSCC (a
v,a
_,[a]
_)) = a -> Elims a
forall a. Hashable a => a -> Elims a
dNonCut a
v
sccDep Cutter a
f (G.CyclicSCC [(a, a, [a])]
vs)      = Cutter a -> [(a, a, [a])] -> Elims a
forall a. Cutable a => Cutter a -> [(a, a, [a])] -> Elims a
cycleDep Cutter a
f [(a, a, [a])]
vs

cycleDep :: (Cutable a) => Cutter a -> [(a, a, [a])] -> Elims a
cycleDep :: Cutter a -> [(a, a, [a])] -> Elims a
cycleDep Cutter a
_ [] = Elims a
forall a. Monoid a => a
mempty
cycleDep Cutter a
f [(a, a, [a])]
vs = Cutter a -> Maybe (a, [(a, a, [a])]) -> Elims a
forall a.
Cutable a =>
Cutter a -> Maybe (a, [(a, a, [a])]) -> Elims a
addCut Cutter a
f (Cutter a
f [(a, a, [a])]
vs)

addCut :: (Cutable a) => Cutter a -> Maybe (a, [(a, a, [a])]) -> Elims a
addCut :: Cutter a -> Maybe (a, [(a, a, [a])]) -> Elims a
addCut Cutter a
_ Maybe (a, [(a, a, [a])])
Nothing         = Elims a
forall a. Monoid a => a
mempty
addCut Cutter a
f (Just (a
v, [(a, a, [a])]
vs')) = [Elims a] -> Elims a
forall a. Monoid a => [a] -> a
mconcat ([Elims a] -> Elims a) -> [Elims a] -> Elims a
forall a b. (a -> b) -> a -> b
$ a -> Elims a
forall a. Hashable a => a -> Elims a
dCut a
v Elims a -> [Elims a] -> [Elims a]
forall a. a -> [a] -> [a]
: (Cutter a -> SCC (a, a, [a]) -> Elims a
forall a. Cutable a => Cutter a -> SCC (a, a, [a]) -> Elims a
sccDep Cutter a
f (SCC (a, a, [a]) -> Elims a) -> [SCC (a, a, [a])] -> [Elims a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SCC (a, a, [a])]
sccs)
  where
    sccs :: [SCC (a, a, [a])]
sccs                 = [(a, a, [a])] -> [SCC (a, a, [a])]
forall key node.
Ord key =>
[(node, key, [key])] -> [SCC (node, key, [key])]
G.stronglyConnCompR [(a, a, [a])]
vs'


--------------------------------------------------------------------------------
-- | `boundElims` extends the input `Elims` by adding kuts that ensure that
--   the *maximum distance* between an eliminated KVar and a cut KVar is
--   *upper bounded* by a given threshold.
--------------------------------------------------------------------------------
boundElims :: (Cutable a) => Config -> (a -> Bool) -> [(a, a, [a])] -> Elims a -> Elims a
--------------------------------------------------------------------------------
boundElims :: Config -> (a -> Bool) -> [(a, a, [a])] -> Elims a -> Elims a
boundElims Config
cfg a -> Bool
isK [(a, a, [a])]
es Elims a
ds = Elims a -> (Vertex -> Elims a) -> Maybe Vertex -> Elims a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Elims a
ds ((a -> Bool) -> [(a, a, [a])] -> Elims a -> Vertex -> Elims a
forall a.
Cutable a =>
(a -> Bool) -> [(a, a, [a])] -> Elims a -> Vertex -> Elims a
bElims a -> Bool
isK [(a, a, [a])]
es Elims a
ds) (Config -> Maybe Vertex
elimBound Config
cfg)

bElims :: (Cutable a) => (a -> Bool) -> [(a, a, [a])] -> Elims a -> Int -> Elims a
bElims :: (a -> Bool) -> [(a, a, [a])] -> Elims a -> Vertex -> Elims a
bElims a -> Bool
isK [(a, a, [a])]
es Elims a
ds Vertex
dMax   = HashSet a -> Elims a -> Elims a
forall a. (Hashable a, Eq a) => HashSet a -> Elims a -> Elims a
forceKuts HashSet a
kS' Elims a
ds
  where
    (HashMap a (Vertex, HashSet a)
_ , HashSet a
kS')           = ((HashMap a (Vertex, HashSet a), HashSet a)
 -> a -> (HashMap a (Vertex, HashSet a), HashSet a))
-> (HashMap a (Vertex, HashSet a), HashSet a)
-> [a]
-> (HashMap a (Vertex, HashSet a), HashSet a)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (HashMap a (Vertex, HashSet a), HashSet a)
-> a -> (HashMap a (Vertex, HashSet a), HashSet a)
step (HashMap a (Vertex, HashSet a)
forall k v. HashMap k v
M.empty, Elims a -> HashSet a
forall a. Elims a -> HashSet a
depCuts Elims a
ds) [a]
vs
    vs :: [a]
vs                  = Elims a -> [(a, a, [a])] -> [a]
forall a. Cutable a => Elims a -> [(a, a, [a])] -> [a]
topoSort Elims a
ds [(a, a, [a])]
es
    predM :: HashMap a [a]
predM               = [(a, a, [a])] -> HashMap a [a]
forall a. Cutable a => [(a, a, [a])] -> HashMap a [a]
invertEdges [(a, a, [a])]
es
    addK :: a -> HashSet a -> HashSet a
addK a
v HashSet a
ks
      | a -> Bool
isK a
v           = a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert a
v HashSet a
ks
      | Bool
otherwise       = HashSet a
ks

    zero :: (Vertex, HashSet a)
zero                = (Vertex
0, HashSet a
forall a. HashSet a
S.empty)

    step :: (HashMap a (Vertex, HashSet a), HashSet a)
-> a -> (HashMap a (Vertex, HashSet a), HashSet a)
step (HashMap a (Vertex, HashSet a)
dM, HashSet a
kS) a
v
      | a
v a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet a
kS = (a
-> (Vertex, HashSet a)
-> HashMap a (Vertex, HashSet a)
-> HashMap a (Vertex, HashSet a)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
v (Vertex, HashSet a)
forall a. (Vertex, HashSet a)
zero  HashMap a (Vertex, HashSet a)
dM,        HashSet a
kS)
      | Vertex
vDist Vertex -> Vertex -> Bool
forall a. Ord a => a -> a -> Bool
< Vertex
dMax    = (a
-> (Vertex, HashSet a)
-> HashMap a (Vertex, HashSet a)
-> HashMap a (Vertex, HashSet a)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
v (Vertex, HashSet a)
dv    HashMap a (Vertex, HashSet a)
dM,        HashSet a
kS)
      | Bool
otherwise       = (a
-> (Vertex, HashSet a)
-> HashMap a (Vertex, HashSet a)
-> HashMap a (Vertex, HashSet a)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
v (Vertex, HashSet a)
forall a. (Vertex, HashSet a)
zero  HashMap a (Vertex, HashSet a)
dM, a -> HashSet a -> HashSet a
addK a
v HashSet a
kS)
      where
        dv :: (Vertex, HashSet a)
dv              = String -> (Vertex, HashSet a) -> (Vertex, HashSet a)
forall a. String -> a -> a
trace String
msg (Vertex, HashSet a)
dv_
        msg :: String
msg             = a -> String
forall a. Show a => a -> String
show a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" DIST =" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Vertex -> String
forall a. Show a => a -> String
show Vertex
vDist String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" SIZE = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Vertex -> String
forall a. Show a => a -> String
show Vertex
vSize
        dv_ :: (Vertex, HashSet a)
dv_@(Vertex
vDist, HashSet a
s)  = HashMap a [a]
-> a -> HashMap a (Vertex, HashSet a) -> (Vertex, HashSet a)
forall a.
Cutable a =>
HashMap a [a]
-> a -> HashMap a (Vertex, HashSet a) -> (Vertex, HashSet a)
distV HashMap a [a]
predM a
v HashMap a (Vertex, HashSet a)
dM
        vSize :: Vertex
vSize           = HashSet a -> Vertex
forall a. HashSet a -> Vertex
S.size HashSet a
s

distV :: (Cutable a) => M.HashMap a [a] -> a -> M.HashMap a (Int, S.HashSet a) -> (Int, S.HashSet a)
distV :: HashMap a [a]
-> a -> HashMap a (Vertex, HashSet a) -> (Vertex, HashSet a)
distV HashMap a [a]
predM a
v HashMap a (Vertex, HashSet a)
dM = (Vertex
d, HashSet a
s)
  where
    d :: Vertex
d            = Vertex
1 Vertex -> Vertex -> Vertex
forall a. Num a => a -> a -> a
+ Vertex -> [Vertex] -> Vertex
forall a. Ord a => a -> [a] -> a
maximumDef Vertex
0 ((Vertex, HashSet a) -> Vertex
forall a b. (a, b) -> a
fst ((Vertex, HashSet a) -> Vertex)
-> (a -> (Vertex, HashSet a)) -> a -> Vertex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (Vertex, HashSet a)
du (a -> Vertex) -> [a] -> [Vertex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
us)
    s :: HashSet a
s            = a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert a
v ([HashSet a] -> HashSet a
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions ((Vertex, HashSet a) -> HashSet a
forall a b. (a, b) -> b
snd ((Vertex, HashSet a) -> HashSet a)
-> (a -> (Vertex, HashSet a)) -> a -> HashSet a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (Vertex, HashSet a)
du (a -> HashSet a) -> [a] -> [HashSet a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
us))
    du :: a -> (Vertex, HashSet a)
du a
u         = (Vertex, HashSet a)
-> Maybe (Vertex, HashSet a) -> (Vertex, HashSet a)
forall a. a -> Maybe a -> a
fromMaybe (a -> (Vertex, HashSet a)
forall a a. Show a => a -> a
oops a
u) (Maybe (Vertex, HashSet a) -> (Vertex, HashSet a))
-> Maybe (Vertex, HashSet a) -> (Vertex, HashSet a)
forall a b. (a -> b) -> a -> b
$ a -> HashMap a (Vertex, HashSet a) -> Maybe (Vertex, HashSet a)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup a
u HashMap a (Vertex, HashSet a)
dM
    us :: [a]
us           = [a] -> a -> HashMap a [a] -> [a]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] a
v HashMap a [a]
predM
    oops :: a -> a
oops a
u       = String -> a
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"dist: don't have dist for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
u String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" when checking " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v

topoSort :: (Cutable a) => Elims a -> [(a, a, [a])] -> [a]
topoSort :: Elims a -> [(a, a, [a])] -> [a]
topoSort Elims a
ds = [SCC a] -> [a]
forall a. [SCC a] -> [a]
G.flattenSCCs ([SCC a] -> [a])
-> ([(a, a, [a])] -> [SCC a]) -> [(a, a, [a])] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SCC a] -> [SCC a]
forall a. [a] -> [a]
reverse ([SCC a] -> [SCC a])
-> ([(a, a, [a])] -> [SCC a]) -> [(a, a, [a])] -> [SCC a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, a, [a])] -> [SCC a]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
G.stronglyConnComp ([(a, a, [a])] -> [SCC a])
-> ([(a, a, [a])] -> [(a, a, [a])]) -> [(a, a, [a])] -> [SCC a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elims a -> [(a, a, [a])] -> [(a, a, [a])]
forall a. Cutable a => Elims a -> [(a, a, [a])] -> [(a, a, [a])]
ripKuts Elims a
ds

ripKuts :: (Cutable a) => Elims a -> [(a, a, [a])] -> [(a, a, [a])]
ripKuts :: Elims a -> [(a, a, [a])] -> [(a, a, [a])]
ripKuts Elims a
ds [(a, a, [a])]
es = [ (a
u, a
x, [a] -> [a]
notKuts [a]
vs) | (a
u, a
x, [a]
vs) <- [(a, a, [a])]
es ]
  where
    notKuts :: [a] -> [a]
notKuts   = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet a
ks))
    ks :: HashSet a
ks        = Elims a -> HashSet a
forall a. Elims a -> HashSet a
depCuts Elims a
ds

invertEdges :: (Cutable a) => [(a, a, [a])] -> M.HashMap a [a]
invertEdges :: [(a, a, [a])] -> HashMap a [a]
invertEdges [(a, a, [a])]
es = [(a, a)] -> HashMap a [a]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (a
v, a
u) | (a
u, a
_, [a]
vs) <- [(a, a, [a])]
es, a
v <- [a]
vs ]

maximumDef :: (Ord a) => a -> [a] -> a
maximumDef :: a -> [a] -> a
maximumDef a
d [] = a
d
maximumDef a
_ [a]
xs = [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [a]
xs


---------------------------------------------------------------------------
graphDeps :: F.TaggedC c a => F.GInfo c a -> [CEdge] -> CDeps
---------------------------------------------------------------------------
graphDeps :: GInfo c a -> [CEdge] -> CDeps
graphDeps GInfo c a
fi [CEdge]
cs = CDs :: CMap [SubcId] -> CMap [KVar] -> CMap Rank -> Vertex -> CDeps
CDs { cSucc :: CMap [SubcId]
cSucc   = CGraph -> CMap [SubcId]
gSucc CGraph
cg
                      , cPrev :: CMap [KVar]
cPrev   = CMap [KVar]
cPrevM
                      , cNumScc :: Vertex
cNumScc = CGraph -> Vertex
gSccs CGraph
cg
                      , cRank :: CMap Rank
cRank   = [(SubcId, Rank)] -> CMap Rank
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(SubcId
i, SubcId -> Rank
rf SubcId
i) | SubcId
i <- [SubcId]
is ]
                      }
  where
    rf :: SubcId -> Rank
rf          = CMap (c a) -> CMap Vertex -> CMap Vertex -> SubcId -> Rank
forall (c :: * -> *) a.
TaggedC c a =>
CMap (c a) -> CMap Vertex -> CMap Vertex -> SubcId -> Rank
rankF (GInfo c a -> CMap (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi) CMap Vertex
outRs CMap Vertex
inRs
    inRs :: CMap Vertex
inRs        = GInfo c a -> [DepEdge] -> CMap Vertex -> CMap Vertex
forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [DepEdge] -> CMap Vertex -> CMap Vertex
inRanks GInfo c a
fi [DepEdge]
es CMap Vertex
outRs
    outRs :: CMap Vertex
outRs       = CGraph -> CMap Vertex
gRanks CGraph
cg
    es :: [DepEdge]
es          = CGraph -> [DepEdge]
gEdges CGraph
cg
    cg :: CGraph
cg          = [CEdge] -> CGraph
cGraphCE [CEdge]
cs
    is :: [SubcId]
is          = [SubcId
i | (Cstr SubcId
i, CVertex
_) <- [CEdge]
cs]
    cPrevM :: CMap [KVar]
cPrevM      = [KVar] -> [KVar]
forall a. Ord a => [a] -> [a]
sortNub ([KVar] -> [KVar]) -> CMap [KVar] -> CMap [KVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubcId, KVar)] -> CMap [KVar]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (SubcId
i, KVar
k) | (KVar KVar
k, Cstr SubcId
i) <- [CEdge]
cs ]

--TODO merge these with cGraph and kvSucc
cGraphCE :: [CEdge] -> CGraph
cGraphCE :: [CEdge] -> CGraph
cGraphCE [CEdge]
cs = CGraph :: [DepEdge] -> CMap Vertex -> CMap [SubcId] -> Vertex -> CGraph
CGraph { gEdges :: [DepEdge]
gEdges = [DepEdge]
es
                     , gRanks :: CMap Vertex
gRanks = CMap Vertex
outRs
                     , gSucc :: CMap [SubcId]
gSucc  = CMap [SubcId]
next
                     , gSccs :: Vertex
gSccs  = [[Vertex]] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [[Vertex]]
sccs }
  where
    es :: [DepEdge]
es             = [(SubcId
i, SubcId
i, [SubcId] -> SubcId -> CMap [SubcId] -> [SubcId]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] SubcId
i CMap [SubcId]
next) | (Cstr SubcId
i, CVertex
_) <- [CEdge]
cs]
    next :: CMap [SubcId]
next           = [CEdge] -> CMap [SubcId]
cSuccM [CEdge]
cs
    (Graph
g, Vertex -> DepEdge
vf, SubcId -> Maybe Vertex
_)     = [DepEdge] -> (Graph, Vertex -> DepEdge, SubcId -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
G.graphFromEdges [DepEdge]
es
    (CMap Vertex
outRs, [[Vertex]]
sccs)  = Graph -> (Vertex -> DepEdge) -> (CMap Vertex, [[Vertex]])
graphRanks Graph
g Vertex -> DepEdge
vf

cSuccM      :: [CEdge] -> CMap [F.SubcId]
cSuccM :: [CEdge] -> CMap [SubcId]
cSuccM [CEdge]
es    = ([SubcId] -> [SubcId]
forall a. Ord a => [a] -> [a]
sortNub ([SubcId] -> [SubcId])
-> ([KVar] -> [SubcId]) -> [KVar] -> [SubcId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar -> [SubcId]) -> [KVar] -> [SubcId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap KVar -> [SubcId]
kRdBy) ([KVar] -> [SubcId]) -> CMap [KVar] -> CMap [SubcId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CMap [KVar]
iWrites
  where
    kRdBy :: KVar -> [SubcId]
kRdBy KVar
k  = [SubcId] -> KVar -> KVRead -> [SubcId]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KVRead
kReads
    iWrites :: CMap [KVar]
iWrites  = [(SubcId, KVar)] -> CMap [KVar]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (SubcId
i, KVar
k) | (Cstr SubcId
i, KVar KVar
k) <- [CEdge]
es ]
    kReads :: KVRead
kReads   = [(KVar, SubcId)] -> KVRead
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (KVar
k, SubcId
j) | (KVar KVar
k, Cstr SubcId
j) <- [CEdge]
es ]

rankF ::  F.TaggedC c a => CMap (c a) -> CMap Int -> CMap Int -> F.SubcId -> Rank
rankF :: CMap (c a) -> CMap Vertex -> CMap Vertex -> SubcId -> Rank
rankF CMap (c a)
cm CMap Vertex
outR CMap Vertex
inR = \SubcId
i -> Vertex -> Vertex -> [Vertex] -> Rank
Rank (SubcId -> Vertex
outScc SubcId
i) (SubcId -> Vertex
inScc SubcId
i) (SubcId -> [Vertex]
tag SubcId
i)
  where
    outScc :: SubcId -> Vertex
outScc        = CMap Vertex -> SubcId -> Vertex
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
outR
    inScc :: SubcId -> Vertex
inScc         = CMap Vertex -> SubcId -> Vertex
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
inR
    tag :: SubcId -> [Vertex]
tag           = c a -> [Vertex]
forall (c :: * -> *) a. TaggedC c a => c a -> [Vertex]
F.stag (c a -> [Vertex]) -> (SubcId -> c a) -> SubcId -> [Vertex]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CMap (c a) -> SubcId -> c a
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap (c a)
cm

---------------------------------------------------------------------------
inRanks ::  F.TaggedC c a => F.GInfo c a -> [DepEdge] -> CMap Int -> CMap Int
---------------------------------------------------------------------------
inRanks :: GInfo c a -> [DepEdge] -> CMap Vertex -> CMap Vertex
inRanks GInfo c a
fi [DepEdge]
es CMap Vertex
outR
  | Kuts
ks Kuts -> Kuts -> Bool
forall a. Eq a => a -> a -> Bool
== Kuts
forall a. Monoid a => a
mempty      = CMap Vertex
outR
  | Bool
otherwise         = (CMap Vertex, [[Vertex]]) -> CMap Vertex
forall a b. (a, b) -> a
fst ((CMap Vertex, [[Vertex]]) -> CMap Vertex)
-> (CMap Vertex, [[Vertex]]) -> CMap Vertex
forall a b. (a -> b) -> a -> b
$ Graph -> (Vertex -> DepEdge) -> (CMap Vertex, [[Vertex]])
graphRanks Graph
g' Vertex -> DepEdge
vf'
  where
    ks :: Kuts
ks                = GInfo c a -> Kuts
forall (c :: * -> *) a. GInfo c a -> Kuts
F.kuts GInfo c a
fi
    cm :: HashMap SubcId (c a)
cm                = GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi
    (Graph
g', Vertex -> DepEdge
vf', SubcId -> Maybe Vertex
_)      = [DepEdge] -> (Graph, Vertex -> DepEdge, SubcId -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
G.graphFromEdges [DepEdge]
es'
    es' :: [DepEdge]
es'               = [(SubcId
i, SubcId
i, (SubcId -> Bool) -> [SubcId] -> [SubcId]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (SubcId -> Bool) -> SubcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubcId -> SubcId -> Bool
isCut SubcId
i) [SubcId]
js) | (SubcId
i,SubcId
_,[SubcId]
js) <- [DepEdge]
es ]
    isCut :: SubcId -> SubcId -> Bool
isCut SubcId
i SubcId
j         = SubcId -> HashSet SubcId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member SubcId
i HashSet SubcId
cutCIds Bool -> Bool -> Bool
&& SubcId -> SubcId -> Bool
isEqOutRank SubcId
i SubcId
j
    isEqOutRank :: SubcId -> SubcId -> Bool
isEqOutRank SubcId
i SubcId
j   = CMap Vertex -> SubcId -> Vertex
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
outR SubcId
i Vertex -> Vertex -> Bool
forall a. Eq a => a -> a -> Bool
== CMap Vertex -> SubcId -> Vertex
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
outR SubcId
j
    cutCIds :: HashSet SubcId
cutCIds           = [SubcId] -> HashSet SubcId
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [SubcId
i | SubcId
i <- HashMap SubcId (c a) -> [SubcId]
forall k v. HashMap k v -> [k]
M.keys HashMap SubcId (c a)
cm, SubcId -> Bool
isKutWrite SubcId
i ]
    isKutWrite :: SubcId -> Bool
isKutWrite        = (KVar -> Bool) -> [KVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (KVar -> Kuts -> Bool
`F.ksMember` Kuts
ks) ([KVar] -> Bool) -> (SubcId -> [KVar]) -> SubcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap SubcId (c a) -> SubcId -> [KVar]
forall (c :: * -> *) a.
TaggedC c a =>
CMap (c a) -> SubcId -> [KVar]
kvWriteBy HashMap SubcId (c a)
cm

--------------------------------------------------------------------------------
graphStatistics :: F.TaggedC c a => Config -> F.GInfo c a -> IO ()
--------------------------------------------------------------------------------
graphStatistics :: Config -> GInfo c a -> IO ()
graphStatistics Config
cfg GInfo c a
si = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
elimStats Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  -- writeGraph f  (kvGraph si)
  String -> [CEdge] -> IO ()
writeEdges String
f [CEdge]
es'
  String -> String -> IO ()
appendFile String
f (String -> IO ()) -> (Stats -> String) -> Stats -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DocTable -> String
forall a. PPrint a => a -> String
ppc (DocTable -> String) -> (Stats -> DocTable) -> Stats -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stats -> DocTable
forall a. PTable a => a -> DocTable
ptable (Stats -> IO ()) -> Stats -> IO ()
forall a b. (a -> b) -> a -> b
$ Config -> GInfo c a -> Stats
forall (c :: * -> *) a. TaggedC c a => Config -> GInfo c a -> Stats
graphStats Config
cfg GInfo c a
si
  where
    f :: String
f        = Ext -> Config -> String
queryFile Ext
Dot Config
cfg
    es' :: [CEdge]
es'      = HashSet KVar -> [CEdge] -> [CEdge]
removeKutEdges (Elims KVar -> HashSet KVar
forall a. Elims a -> HashSet a
depCuts Elims KVar
ds) [CEdge]
es
    ([CEdge]
es, Elims KVar
ds) = Config -> GInfo c a -> ([CEdge], Elims KVar)
forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> ([CEdge], Elims KVar)
elimVars Config
cfg GInfo c a
si
    ppc :: a -> String
ppc a
d    = Doc -> String
forall a. PPrint a => a -> String
showpp (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [Doc
" ", Doc
" ", Doc
"/*", a -> Doc
forall a. PPrint a => a -> Doc
pprint a
d, Doc
"*/"]

data Stats = Stats {
    Stats -> Vertex
stNumKVCuts   :: !Int   -- ^ number of kvars whose removal makes deps acyclic
  , Stats -> Vertex
stNumKVNonLin :: !Int   -- ^ number of kvars that appear >= 2 in some LHS
  , Stats -> Vertex
stNumKVTotal  :: !Int   -- ^ number of kvars
  , Stats -> Bool
stIsReducible :: !Bool  -- ^ is dep-graph reducible
  , Stats -> HashSet KVar
stSetKVNonLin :: !(S.HashSet F.KVar) -- ^ set of non-linear kvars
  }

instance PTable Stats where
  ptable :: Stats -> DocTable
ptable (Stats {Bool
Vertex
HashSet KVar
stSetKVNonLin :: HashSet KVar
stIsReducible :: Bool
stNumKVTotal :: Vertex
stNumKVNonLin :: Vertex
stNumKVCuts :: Vertex
stSetKVNonLin :: Stats -> HashSet KVar
stIsReducible :: Stats -> Bool
stNumKVTotal :: Stats -> Vertex
stNumKVNonLin :: Stats -> Vertex
stNumKVCuts :: Stats -> Vertex
..})  = [(Doc, Doc)] -> DocTable
DocTable [
      (Doc
"# KVars [Cut]"    , Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
stNumKVCuts)
    , (Doc
"# KVars [NonLin]" , Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
stNumKVNonLin)
    , (Doc
"# KVars [All]"    , Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
stNumKVTotal)
    , (Doc
"# Reducible"      , Bool -> Doc
forall a. PPrint a => a -> Doc
pprint Bool
stIsReducible)
    , (Doc
"KVars NonLin"     , HashSet KVar -> Doc
forall a. PPrint a => a -> Doc
pprint HashSet KVar
stSetKVNonLin)
    ]

graphStats :: F.TaggedC c a => Config -> F.GInfo c a -> Stats
graphStats :: Config -> GInfo c a -> Stats
graphStats Config
cfg GInfo c a
si = Stats :: Vertex -> Vertex -> Vertex -> Bool -> HashSet KVar -> Stats
Stats {
    stNumKVCuts :: Vertex
stNumKVCuts   = HashSet KVar -> Vertex
forall a. HashSet a -> Vertex
S.size (Elims KVar -> HashSet KVar
forall a. Elims a -> HashSet a
depCuts Elims KVar
d)
  , stNumKVNonLin :: Vertex
stNumKVNonLin = HashSet KVar -> Vertex
forall a. HashSet a -> Vertex
S.size  HashSet KVar
nlks
  , stNumKVTotal :: Vertex
stNumKVTotal  = HashSet KVar -> Vertex
forall a. HashSet a -> Vertex
S.size (Elims KVar -> HashSet KVar
forall a. Elims a -> HashSet a
depCuts Elims KVar
d) Vertex -> Vertex -> Vertex
forall a. Num a => a -> a -> a
+ HashSet KVar -> Vertex
forall a. HashSet a -> Vertex
S.size (Elims KVar -> HashSet KVar
forall a. Elims a -> HashSet a
depNonCuts Elims KVar
d)
  , stIsReducible :: Bool
stIsReducible = GInfo c a -> Bool
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> Bool
isReducible GInfo c a
si
  , stSetKVNonLin :: HashSet KVar
stSetKVNonLin = HashSet KVar
nlks
  }
  where
    nlks :: HashSet KVar
nlks          = GInfo c a -> HashSet KVar
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> HashSet KVar
nonLinearKVars GInfo c a
si
    d :: Elims KVar
d             = ([CEdge], Elims KVar) -> Elims KVar
forall a b. (a, b) -> b
snd (([CEdge], Elims KVar) -> Elims KVar)
-> ([CEdge], Elims KVar) -> Elims KVar
forall a b. (a -> b) -> a -> b
$ Config -> GInfo c a -> ([CEdge], Elims KVar)
forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> ([CEdge], Elims KVar)
elimVars Config
cfg GInfo c a
si

--------------------------------------------------------------------------------
nonLinearKVars :: (F.TaggedC c a) => F.GInfo c a -> S.HashSet F.KVar
--------------------------------------------------------------------------------
nonLinearKVars :: GInfo c a -> HashSet KVar
nonLinearKVars GInfo c a
fi = [HashSet KVar] -> HashSet KVar
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions ([HashSet KVar] -> HashSet KVar) -> [HashSet KVar] -> HashSet KVar
forall a b. (a -> b) -> a -> b
$ BindEnv -> c a -> HashSet KVar
forall (c :: * -> *) a.
TaggedC c a =>
BindEnv -> c a -> HashSet KVar
nlKVarsC BindEnv
bs (c a -> HashSet KVar) -> [c a] -> [HashSet KVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [c a]
cs
  where
    bs :: BindEnv
bs            = GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs GInfo c a
fi
    cs :: [c a]
cs            = 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)

nlKVarsC :: (F.TaggedC c a) => F.BindEnv -> c a -> S.HashSet F.KVar
nlKVarsC :: BindEnv -> c a -> HashSet KVar
nlKVarsC BindEnv
bs c a
c = [KVar] -> HashSet KVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ KVar
k |  (KVar
k, Vertex
n) <- BindEnv -> c a -> [(KVar, Vertex)]
forall (c :: * -> *) a.
TaggedC c a =>
BindEnv -> c a -> [(KVar, Vertex)]
V.envKVarsN BindEnv
bs c a
c, Vertex
n Vertex -> Vertex -> Bool
forall a. Ord a => a -> a -> Bool
>= Vertex
2]