{-# LANGUAGE CPP                   #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# 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)
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 :: forall (c :: * -> *) a.
TaggedC c a =>
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' = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey forall {p}. SubcId -> p -> Bool
inC (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi)
     ws' :: HashMap KVar (WfC a)
ws' = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey forall {p}. KVar -> p -> Bool
inW (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws GInfo c a
fi)
     ks :: HashSet KVar
ks  = forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> Slice -> HashSet KVar
sliceKVars GInfo c a
fi Slice
sl
     is :: HashSet SubcId
is  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (Slice -> [SubcId]
slKVarCs Slice
sl forall a. [a] -> [a] -> [a]
++ Slice -> [SubcId]
slConcCs Slice
sl)
     sl :: Slice
sl  = forall (c :: * -> *) a. TaggedC c a => GInfo c a -> Slice
mkSlice GInfo c a
fi
     inC :: SubcId -> p -> Bool
inC SubcId
i p
_ = 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
_ = 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 :: forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> Slice -> HashSet KVar
sliceKVars GInfo c a
fi Slice
sl = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (c :: * -> *) a. TaggedC c a => BindEnv a -> c a -> [KVar]
subcKVars BindEnv a
be) [c a]
cs
  where
    cs :: [c a]
cs           = forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap HashMap SubcId (c a)
cm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Slice -> [SubcId]
slKVarCs Slice
sl forall a. [a] -> [a] -> [a]
++ Slice -> [SubcId]
slConcCs Slice
sl
    be :: BindEnv a
be           = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs GInfo c a
fi
    cm :: HashMap SubcId (c a)
cm           = forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi

subcKVars :: (F.TaggedC c a) => F.BindEnv a -> c a -> [F.KVar]
subcKVars :: forall (c :: * -> *) a. TaggedC c a => BindEnv a -> c a -> [KVar]
subcKVars BindEnv a
be c a
c = forall (c :: * -> *) a. TaggedC c a => BindEnv a -> c a -> [KVar]
V.envKVars BindEnv a
be c a
c forall a. [a] -> [a] -> [a]
++ 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 :: forall (c :: * -> *) a. TaggedC c a => GInfo c a -> Slice
mkSlice GInfo c a
fi        = forall (c :: * -> *) a.
TaggedC c a =>
HashMap SubcId (c a)
-> Graph
-> [DepEdge]
-> (Vertex -> SubcId)
-> (SubcId -> Vertex)
-> Slice
mkSlice_ (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)   = 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 forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. TaggedC c a => GInfo c a -> CGraph
cGraph GInfo c a
fi
    v2i :: Vertex -> SubcId
v2i           = forall a b c. (a, b, c) -> a
fst3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vertex -> DepEdge
vf
    i2v :: SubcId -> Vertex
i2v SubcId
i         = forall a. a -> Maybe a -> a
fromMaybe (forall {a} {a}. Show a => a -> a
errU SubcId
i) forall a b. (a -> b) -> a -> b
$ SubcId -> Maybe Vertex
cf SubcId
i
    errU :: a -> a
errU a
i        = forall a. (?callStack::CallStack) => [Char] -> a
errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"graphSlice: Unknown constraint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
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_ :: forall (c :: * -> *) a.
TaggedC c a =>
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 { 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) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId (c a)
cm, forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget c a
c ]
    kvarCs :: [SubcId]
kvarCs             = Vertex -> SubcId
v2i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Vertex]
reachVs
    rootVs :: [Vertex]
rootVs             = SubcId -> Vertex
i2v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SubcId]
concCs
    reachVs :: [Vertex]
reachVs            = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. Tree a -> [a]
flatten forall a b. (a -> b) -> a -> b
$ Graph -> [Vertex] -> Forest 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, 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    = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member SubcId
i HashMap SubcId ()
im
    im :: HashMap SubcId ()
im           = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ (, ()) 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 :: forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget c a
c   = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Expr -> Bool
F.isTautoPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs


--------------------------------------------------------------------------------
-- | Constraint Graph ----------------------------------------------------------
--------------------------------------------------------------------------------
cGraph :: (F.TaggedC c a) => F.GInfo c a -> CGraph
---------------------------------------------------------------------------
cGraph :: forall (c :: * -> *) a. TaggedC c a => GInfo c a -> CGraph
cGraph GInfo c a
fi = CGraph { gEdges :: [DepEdge]
gEdges = [DepEdge]
es
                   , gRanks :: CMap Vertex
gRanks = CMap Vertex
outRs
                   , gSucc :: CMap [SubcId]
gSucc  = CMap [SubcId]
next
                   , gSccs :: Vertex
gSccs  = forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [[Vertex]]
sccs }
  where
    es :: [DepEdge]
es             = [(SubcId
i, SubcId
i, forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] SubcId
i CMap [SubcId]
next) | SubcId
i <- forall k v. HashMap k v -> [k]
M.keys forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi]
    next :: CMap [SubcId]
next           = forall (c :: * -> *) a. TaggedC c a => GInfo c a -> CMap [SubcId]
kvSucc GInfo c a
fi
    (Graph
g, Vertex -> DepEdge
vf, 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 ----------------------------------------------------------
--
-- Yields the strongly conected components and a map of constraint ids to
-- an index identifying the strongly connected component to which it belongs.
-- The scc indices correspond with a topological ordering of the sccs.
--------------------------------------------------------------------------------
graphRanks :: G.Graph -> (G.Vertex -> DepEdge) -> (CMap Int, [[G.Vertex]])
---------------------------------------------------------------------------
graphRanks :: Graph -> (Vertex -> DepEdge) -> (CMap Vertex, [[Vertex]])
graphRanks Graph
g Vertex -> DepEdge
vf = (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       = forall a b. [a] -> [b] -> [(a, b)]
zip [Vertex
0..] [[Vertex]]
sccs
    sccs :: [[Vertex]]
sccs       = forall a. [a] -> [a]
L.reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Tree a -> [a]
flatten forall a b. (a -> b) -> a -> b
$ Graph -> Forest Vertex
G.scc Graph
g
    v2i :: Vertex -> SubcId
v2i        = forall a b c. (a, b, c) -> a
fst3 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 :: forall (c :: * -> *) a. TaggedC c a => GInfo c a -> CMap [SubcId]
kvSucc GInfo c a
fi = forall (c :: * -> *) a.
TaggedC c a =>
CMap (c a) -> KVRead -> CMap [SubcId]
succs HashMap SubcId (c a)
cm KVRead
rdBy
  where
    rdBy :: KVRead
rdBy  = forall (c :: * -> *) a. TaggedC c a => GInfo c a -> KVRead
kvReadBy GInfo c a
fi
    cm :: HashMap SubcId (c a)
cm    = 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 :: forall (c :: * -> *) a.
TaggedC c a =>
CMap (c a) -> KVRead -> CMap [SubcId]
succs CMap (c a)
cm KVRead
rdBy = forall a. Ord a => [a] -> [a]
sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap KVar -> [SubcId]
kvReads forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> [KVar]
kvWrites forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CMap (c a)
cm
  where
    kvReads :: KVar -> [SubcId]
kvReads KVar
k = 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]
V.kvarsExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs

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

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

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

--------------------------------------------------------------------------------
kvGraph :: (F.TaggedC c a) => F.GInfo c a -> KVGraph
--------------------------------------------------------------------------------
kvGraph :: forall (c :: * -> *) a. TaggedC c a => GInfo c a -> KVGraph
kvGraph = [CEdge] -> KVGraph
edgeGraph forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) <- forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
groupList [CEdge]
es ]

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

ebindEdges :: (F.TaggedC c a) => [F.BindId] -> F.BindEnv a -> c a -> [CEdge]
ebindEdges :: forall (c :: * -> *) a.
TaggedC c a =>
[Vertex] -> BindEnv a -> c a -> [CEdge]
ebindEdges [Vertex]
ebs BindEnv a
bs c a
c =  [(Symbol -> CVertex
EBind Symbol
k, SubcId -> CVertex
Cstr SubcId
i ) | Symbol
k  <- forall (c :: * -> *) a (t :: * -> *).
(TaggedC c a, Foldable t) =>
t Symbol -> BindEnv a -> c a -> [Symbol]
envEbinds [Symbol]
xs BindEnv a
bs c a
c ]
                    forall a. [a] -> [a] -> [a]
++ [(SubcId -> CVertex
Cstr SubcId
i, Symbol -> CVertex
EBind Symbol
k') | Symbol
k' <- forall (t :: * -> *) (c :: * -> *) a.
(Foldable t, TaggedC c a) =>
t Symbol -> c a -> [Symbol]
rhsEbinds [Symbol]
xs c a
c ]
  where
    i :: SubcId
i          = forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
F.subcId c a
c
    xs :: [Symbol]
xs         = forall a b c. (a, b, c) -> a
fst3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Vertex -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv BindEnv a
bs 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 a -> c a -> [F.Symbol]
envEbinds :: forall (c :: * -> *) a (t :: * -> *).
(TaggedC c a, Foldable t) =>
t Symbol -> BindEnv a -> c a -> [Symbol]
envEbinds t Symbol
xs BindEnv a
be c a
c = [ Symbol
x | Symbol
x <- [Symbol]
envBinds , Symbol
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Symbol
xs ]
  where envBinds :: [Symbol]
envBinds = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a.
TaggedC c a =>
BindEnv a -> c a -> [(Symbol, SortedReft)]
F.clhs BindEnv a
be c a
c
rhsEbinds :: (Foldable t, F.TaggedC c a) =>
             t F.Symbol -> c a -> [F.Symbol]
rhsEbinds :: forall (t :: * -> *) (c :: * -> *) a.
(Foldable t, TaggedC c a) =>
t Symbol -> c a -> [Symbol]
rhsEbinds t Symbol
xs c a
c = [ Symbol
x | Symbol
x <- forall a. Subable a => a -> [Symbol]
F.syms (forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs c a
c) , Symbol
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Symbol
xs ]

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

--------------------------------------------------------------------------------
-- | Eliminated Dependencies
--------------------------------------------------------------------------------
{-# SCC elimDeps #-}
elimDeps :: (F.TaggedC c a) => F.GInfo c a -> [CEdge] -> S.HashSet F.KVar -> S.HashSet F.Symbol -> CDeps
elimDeps :: forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> HashSet KVar -> HashSet Symbol -> CDeps
elimDeps GInfo c a
si [CEdge]
es HashSet KVar
nonKutVs HashSet Symbol
ebs = 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 :: [Char]
_msg                = [Char]
"graphElim: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (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 forall a b. (a -> b) -> a -> b
$ -- elimEs (S.map EBind ebs) $
                                  HashSet CVertex -> IKVGraph -> IKVGraph
elimKs (forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map KVar -> CVertex
KVar HashSet KVar
ks)   forall a b. (a -> b) -> a -> b
$ [CEdge] -> IKVGraph
edgesIkvg [CEdge]
es
  where
    elimKs :: HashSet CVertex -> IKVGraph -> IKVGraph
elimKs      = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl' IKVGraph -> CVertex -> IKVGraph
elimK)
    _elimEs :: HashSet CVertex -> IKVGraph -> IKVGraph
_elimEs      = forall a b c. (a -> b -> c) -> b -> a -> c
flip (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 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 forall a. a -> [a] -> [a]
: [CVertex]
cis)
  where
   es' :: [CEdge]
es'      = [(CVertex
ki, CVertex
c) | CVertex
ki <- 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      = 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 { forall a. Elims a -> HashSet a
depCuts    :: !(S.HashSet a)
         , forall a. Elims a -> HashSet a
depNonCuts :: !(S.HashSet a)
         }
    deriving (Vertex -> Elims a -> ShowS
forall a. Show a => Vertex -> Elims a -> ShowS
forall a. Show a => [Elims a] -> ShowS
forall a. Show a => Elims a -> [Char]
forall a.
(Vertex -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Elims a] -> ShowS
$cshowList :: forall a. Show a => [Elims a] -> ShowS
show :: Elims a -> [Char]
$cshow :: forall a. Show a => Elims a -> [Char]
showsPrec :: Vertex -> Elims a -> ShowS
$cshowsPrec :: forall a. Show a => Vertex -> Elims a -> ShowS
Show)

instance PPrint (Elims a) where
  pprintTidy :: Tidy -> Elims a -> Doc
pprintTidy Tidy
_ Elims a
d = Doc
"#Cuts ="    Doc -> Doc -> Doc
<+> forall {a}. HashSet a -> Doc
ppSize (forall a. Elims a -> HashSet a
depCuts Elims a
d) Doc -> Doc -> Doc
<+>
                   Doc
"#NonCuts =" Doc -> Doc -> Doc
<+> forall {a}. HashSet a -> Doc
ppSize (forall a. Elims a -> HashSet a
depNonCuts Elims a
d)
    where
      ppSize :: HashSet a -> Doc
ppSize     = forall a. PPrint a => a -> Doc
pprint forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. HashSet a -> HashSet a -> Elims a
Deps (forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet a
d1 HashSet a
d2) (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  = forall a. HashSet a -> HashSet a -> Elims a
Deps forall a. HashSet a
S.empty forall a. HashSet a
S.empty
  mappend :: Elims a -> Elims a -> Elims a
mappend = forall a. Semigroup a => a -> a -> a
(<>)

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

--------------------------------------------------------------------------------
-- | Compute Dependencies and Cuts ---------------------------------------------
--------------------------------------------------------------------------------
{-# SCC elimVars #-}
elimVars :: (F.TaggedC c a) => Config -> F.GInfo c a -> ([CEdge], Elims F.KVar)
--------------------------------------------------------------------------------
elimVars :: forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> ([CEdge], Elims KVar)
elimVars Config
cfg GInfo c a
si = ([CEdge]
es, Elims KVar
ds)
  where
    ds :: Elims KVar
ds          = 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          = 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 = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVertex -> Bool
isKut forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
  where
    cutVs :: HashSet CVertex
cutVs         = 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         = (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 :: forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> HashSet KVar
cutVars Config
cfg GInfo c a
si
  | Config -> Bool
autoKuts Config
cfg = forall a. HashSet a
S.empty
  | Bool
otherwise    = Kuts -> HashSet KVar
F.ksVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> Kuts
F.kuts forall a b. (a -> b) -> a -> b
$ GInfo c a
si

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

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

edgeDeps' :: Config -> [CEdge] -> Elims F.KVar
edgeDeps' :: Config -> [CEdge] -> Elims KVar
edgeDeps' Config
cfg [CEdge]
es = 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   = 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        = 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)  = forall a. a -> Maybe a
Just KVar
z
    tx CVertex
_         = 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 :: forall b a.
(Hashable b, Eq b) =>
(a -> Maybe b) -> HashSet a -> HashSet b
sMapMaybe a -> Maybe b
f = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe a -> Maybe b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> [a]
S.toList

--------------------------------------------------------------------------------
type EdgeRank = M.HashMap F.KVar Integer
--------------------------------------------------------------------------------
edgeRank :: [CEdge] -> EdgeRank
edgeRank :: [CEdge] -> EdgeRank
edgeRank [CEdge]
es = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubcId
n forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KVRead
kiM
  where
    n :: SubcId
n       = SubcId
1 forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ SubcId
i | (Cstr SubcId
i, CVertex
_)     <- [CEdge]
es ]
    kiM :: KVRead
kiM     = 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
                      []  -> forall a. Maybe a
Nothing
                      KVar
k:[KVar]
_ -> 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 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 forall k v.
(Eq k, Hashable k, ?callStack::CallStack) =>
HashMap k v -> k -> v
M.!)
    orderBy :: [KVar] -> [KVar]
orderBy       = forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (forall a. Ord a => a -> a -> Ordering
compare 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 :: forall a.
Cutable a =>
Config -> (a -> Bool) -> Cutter a -> [(a, a, [a])] -> Elims a
gElims Config
cfg a -> Bool
kF Cutter a
cutF [(a, a, [a])]
g = forall a.
Cutable a =>
Config -> (a -> Bool) -> [(a, a, [a])] -> Elims a -> Elims a
boundElims Config
cfg a -> Bool
kF [(a, a, [a])]
g forall a b. (a -> b) -> a -> b
$ 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 :: forall a. Cutable a => Cutter a -> [(a, a, [a])] -> Elims a
sccElims Cutter a
f = forall a. Cutable a => Cutter a -> [SCC (a, a, [a])] -> Elims a
sccsToDeps Cutter a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. Cutable a => Cutter a -> [SCC (a, a, [a])] -> Elims a
sccsToDeps Cutter a
f [SCC (a, a, [a])]
xs = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a. Cutable a => Cutter a -> SCC (a, a, [a]) -> Elims a
sccDep Cutter a
f 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 :: forall a. Cutable a => Cutter a -> SCC (a, a, [a]) -> Elims a
sccDep Cutter a
_ (G.AcyclicSCC (a
v,a
_,[a]
_)) = forall a. Hashable a => a -> Elims a
dNonCut a
v
sccDep Cutter a
f (G.CyclicSCC [(a, a, [a])]
vs)      = 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 :: forall a. Cutable a => Cutter a -> [(a, a, [a])] -> Elims a
cycleDep Cutter a
_ [] = forall a. Monoid a => a
mempty
cycleDep Cutter a
f [(a, a, [a])]
vs = 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 :: forall a.
Cutable a =>
Cutter a -> Maybe (a, [(a, a, [a])]) -> Elims a
addCut Cutter a
_ Maybe (a, [(a, a, [a])])
Nothing         = forall a. Monoid a => a
mempty
addCut Cutter a
f (Just (a
v, [(a, a, [a])]
vs')) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a. Hashable a => a -> Elims a
dCut a
v forall a. a -> [a] -> [a]
: (forall a. Cutable a => Cutter a -> SCC (a, a, [a]) -> Elims a
sccDep Cutter a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SCC (a, a, [a])]
sccs)
  where
    sccs :: [SCC (a, a, [a])]
sccs                 = 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 :: forall a.
Cutable a =>
Config -> (a -> Bool) -> [(a, a, [a])] -> Elims a -> Elims a
boundElims Config
cfg a -> Bool
isK [(a, a, [a])]
es Elims a
ds = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Elims a
ds (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 :: 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 Vertex
dMax   = 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')           = 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 (forall k v. HashMap k v
M.empty, forall a. Elims a -> HashSet a
depCuts Elims a
ds) [a]
vs
    vs :: [a]
vs                  = forall a. Cutable a => Elims a -> [(a, a, [a])] -> [a]
topoSort Elims a
ds [(a, a, [a])]
es
    predM :: HashMap a [a]
predM               = 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           = 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, 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 forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet a
kS = (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
v forall {a}. (Vertex, HashSet a)
zero  HashMap a (Vertex, HashSet a)
dM,        HashSet a
kS)
      | Vertex
vDist forall a. Ord a => a -> a -> Bool
< Vertex
dMax    = (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       = (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
v 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              = forall a. [Char] -> a -> a
trace [Char]
msg (Vertex, HashSet a)
dv_
        msg :: [Char]
msg             = forall a. Show a => a -> [Char]
show a
v forall a. [a] -> [a] -> [a]
++ [Char]
" DIST =" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Vertex
vDist forall a. [a] -> [a] -> [a]
++ [Char]
" SIZE = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Vertex
vSize
        dv_ :: (Vertex, HashSet a)
dv_@(Vertex
vDist, HashSet a
s)  = 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           = 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 :: 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 = (Vertex
d, HashSet a
s)
  where
    d :: Vertex
d            = Vertex
1 forall a. Num a => a -> a -> a
+ forall a. Ord a => a -> [a] -> a
maximumDef Vertex
0 (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (Vertex, HashSet a)
du forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
us)
    s :: HashSet a
s            = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert a
v (forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (Vertex, HashSet a)
du forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
us))
    du :: a -> (Vertex, HashSet a)
du a
u         = forall a. a -> Maybe a -> a
fromMaybe (forall {a} {a}. Show a => a -> a
oops a
u) forall a b. (a -> b) -> a -> b
$ 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           = 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       = forall a. (?callStack::CallStack) => [Char] -> a
errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"dist: don't have dist for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
u forall a. [a] -> [a] -> [a]
++ [Char]
" when checking " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
v

topoSort :: (Cutable a) => Elims a -> [(a, a, [a])] -> [a]
topoSort :: forall a. Cutable a => Elims a -> [(a, a, [a])] -> [a]
topoSort Elims a
ds = forall a. [SCC a] -> [a]
G.flattenSCCs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall key node. Ord key => [(node, key, [key])] -> [SCC node]
G.stronglyConnComp forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. Cutable a => 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   = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet a
ks))
    ks :: HashSet a
ks        = forall a. Elims a -> HashSet a
depCuts Elims a
ds

invertEdges :: (Cutable a) => [(a, a, [a])] -> M.HashMap a [a]
invertEdges :: forall a. Cutable a => [(a, a, [a])] -> HashMap a [a]
invertEdges [(a, a, [a])]
es = 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 :: forall a. Ord a => a -> [a] -> a
maximumDef a
d [] = a
d
maximumDef a
_ [a]
xs = 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 :: forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> CDeps
graphDeps GInfo c a
fi [CEdge]
cs = 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   = 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          = forall (c :: * -> *) a.
TaggedC c a =>
CMap (c a) -> CMap Vertex -> CMap Vertex -> SubcId -> Rank
rankF (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        = 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      = forall a. Ord a => [a] -> [a]
sortNub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 ]

-- | Converts dependencies between constraints and kvars, to dependencies between
-- constraints.
--
-- TODO merge these with cGraph and kvSucc
cGraphCE :: [CEdge] -> CGraph
cGraphCE :: [CEdge] -> CGraph
cGraphCE [CEdge]
cs = CGraph { gEdges :: [DepEdge]
gEdges = [DepEdge]
es
                     , gRanks :: CMap Vertex
gRanks = CMap Vertex
outRs
                     , gSucc :: CMap [SubcId]
gSucc  = CMap [SubcId]
next
                     , gSccs :: Vertex
gSccs  = forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [[Vertex]]
sccs }
  where
    es :: [DepEdge]
es             = [(SubcId
i, SubcId
i, 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
_)     = 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

-- | Converts dependencies between constraints and kvars to
-- dependencies between constraints.
--
-- The returned map tells for each coonstraint writing a kvar
-- which constraints are reading the kvar.
cSuccM      :: [CEdge] -> CMap [F.SubcId]
cSuccM :: [CEdge] -> CMap [SubcId]
cSuccM [CEdge]
es    = forall a. Ord a => [a] -> [a]
sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap KVar -> [SubcId]
kRdBy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CMap [KVar]
iWrites
  where
    kRdBy :: KVar -> [SubcId]
kRdBy KVar
k  = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KVRead
kReads
    iWrites :: CMap [KVar]
iWrites  = 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   = 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 :: forall (c :: * -> *) a.
TaggedC c a =>
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        = forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
outR
    inScc :: SubcId -> Vertex
inScc         = forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
inR
    tag :: SubcId -> [Vertex]
tag           = forall (c :: * -> *) a. TaggedC c a => c a -> [Vertex]
F.stag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap (c a)
cm

---------------------------------------------------------------------------
-- | Removes the kut vars from the graph, and recomputes the SCC indices.
inRanks ::  F.TaggedC c a => F.GInfo c a -> [DepEdge] -> CMap Int -> CMap Int
---------------------------------------------------------------------------
inRanks :: forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [DepEdge] -> CMap Vertex -> CMap Vertex
inRanks GInfo c a
fi [DepEdge]
es CMap Vertex
outR
  | Kuts
ks forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty      = CMap Vertex
outR
  | Bool
otherwise         = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Graph -> (Vertex -> DepEdge) -> (CMap Vertex, [[Vertex]])
graphRanks Graph
g' Vertex -> DepEdge
vf'
  where
    ks :: Kuts
ks                = forall (c :: * -> *) a. GInfo c a -> Kuts
F.kuts GInfo c a
fi
    cm :: HashMap SubcId (c a)
cm                = forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo c a
fi
    (Graph
g', Vertex -> DepEdge
vf', 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, forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not 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         = 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   = forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
outR SubcId
i forall a. Eq a => a -> a -> Bool
== forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Vertex
outR SubcId
j
    cutCIds :: HashSet SubcId
cutCIds           = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [SubcId
i | SubcId
i <- forall k v. HashMap k v -> [k]
M.keys HashMap SubcId (c a)
cm, SubcId -> Bool
isKutWrite SubcId
i ]
    isKutWrite :: SubcId -> Bool
isKutWrite        = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (KVar -> Kuts -> Bool
`F.ksMember` Kuts
ks) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (c :: * -> *) a. TaggedC c a => Config -> GInfo c a -> IO ()
graphStatistics Config
cfg GInfo c a
si = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
elimStats Config
cfg) forall a b. (a -> b) -> a -> b
$ do
  -- writeGraph f  (kvGraph si)
  [Char] -> [CEdge] -> IO ()
writeEdges [Char]
f [CEdge]
es'
  [Char] -> [Char] -> IO ()
appendFile [Char]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. PPrint a => a -> [Char]
ppc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PTable a => a -> DocTable
ptable forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. TaggedC c a => Config -> GInfo c a -> Stats
graphStats Config
cfg GInfo c a
si
  where
    f :: [Char]
f        = Ext -> Config -> [Char]
queryFile Ext
Dot Config
cfg
    es' :: [CEdge]
es'      = HashSet KVar -> [CEdge] -> [CEdge]
removeKutEdges (forall a. Elims a -> HashSet a
depCuts Elims KVar
ds) [CEdge]
es
    ([CEdge]
es, Elims KVar
ds) = forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> ([CEdge], Elims KVar)
elimVars Config
cfg GInfo c a
si
    ppc :: a -> [Char]
ppc a
d    = forall {a}. PPrint a => a -> [Char]
showpp forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [Doc
" ", Doc
" ", 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]"    , forall a. PPrint a => a -> Doc
pprint Vertex
stNumKVCuts)
    , (Doc
"# KVars [NonLin]" , forall a. PPrint a => a -> Doc
pprint Vertex
stNumKVNonLin)
    , (Doc
"# KVars [All]"    , forall a. PPrint a => a -> Doc
pprint Vertex
stNumKVTotal)
    , (Doc
"# Reducible"      , forall a. PPrint a => a -> Doc
pprint Bool
stIsReducible)
    , (Doc
"KVars NonLin"     , forall a. PPrint a => a -> Doc
pprint HashSet KVar
stSetKVNonLin)
    ]

graphStats :: F.TaggedC c a => Config -> F.GInfo c a -> Stats
graphStats :: forall (c :: * -> *) a. TaggedC c a => Config -> GInfo c a -> Stats
graphStats Config
cfg GInfo c a
si = Stats {
    stNumKVCuts :: Vertex
stNumKVCuts   = forall a. HashSet a -> Vertex
S.size (forall a. Elims a -> HashSet a
depCuts Elims KVar
d)
  , stNumKVNonLin :: Vertex
stNumKVNonLin = forall a. HashSet a -> Vertex
S.size  HashSet KVar
nlks
  , stNumKVTotal :: Vertex
stNumKVTotal  = forall a. HashSet a -> Vertex
S.size (forall a. Elims a -> HashSet a
depCuts Elims KVar
d) forall a. Num a => a -> a -> a
+ forall a. HashSet a -> Vertex
S.size (forall a. Elims a -> HashSet a
depNonCuts Elims KVar
d)
  , stIsReducible :: Bool
stIsReducible = 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          = forall (c :: * -> *) a. TaggedC c a => GInfo c a -> HashSet KVar
nonLinearKVars GInfo c a
si
    d :: Elims KVar
d             = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ 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 :: forall (c :: * -> *) a. TaggedC c a => GInfo c a -> HashSet KVar
nonLinearKVars GInfo c a
fi = forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a.
TaggedC c a =>
BindEnv a -> c a -> HashSet KVar
nlKVarsC BindEnv a
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [c a]
cs
  where
    bs :: BindEnv a
bs            = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs GInfo c a
fi
    cs :: [c a]
cs            = 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)

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