module Language.Fixpoint.Partition (
CPart (..)
, partition, partition', partitionN
, MCInfo (..)
, mcInfo
, graphStatistics
, GDeps (..)
, deps
, elimSolGraph
) where
import GHC.Conc (getNumProcessors)
import Control.Monad (when, forM_)
import Language.Fixpoint.Misc
import Language.Fixpoint.Utils.Files
import Language.Fixpoint.Types.Config
import Language.Fixpoint.Types.PrettyPrint
import qualified Language.Fixpoint.Types.Visitor as V
import qualified Language.Fixpoint.Solver.Solution as So
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Types.Graphs
import qualified Data.HashMap.Strict as M
import qualified Data.Graph as G
import qualified Data.Tree as T
import Data.Function (on)
import Data.Maybe (mapMaybe, fromMaybe)
import Data.Hashable
import Text.PrettyPrint.HughesPJ
import Data.List (sortBy)
import qualified Data.HashSet as S
import Data.Graph.Inductive
data CPart a = CPart { pws :: M.HashMap F.KVar (F.WfC a)
, pcm :: M.HashMap Integer (F.SubC a)
, cFileName :: FilePath
}
instance Monoid (CPart a) where
mempty = CPart mempty mempty mempty
mappend l r = CPart { pws = pws l `mappend` pws r
, pcm = pcm l `mappend` pcm r
, cFileName = cFileName l
}
data MCInfo = MCInfo { mcCores :: Int
, mcMinPartSize :: Int
, mcMaxPartSize :: Int
} deriving (Show)
mcInfo :: Config -> IO MCInfo
mcInfo c = do
np <- getNumProcessors
let nc = fromMaybe np (cores c)
return MCInfo { mcCores = nc
, mcMinPartSize = minPartSize c
, mcMaxPartSize = maxPartSize c
}
partition :: (F.Fixpoint a) => Config -> F.FInfo a -> IO (F.Result (Integer, a))
partition cfg fi
= do dumpPartitions cfg fis
writeGraph f g
return mempty
where
f = queryFile Dot cfg
(g, fis) = partition' Nothing fi
partition' :: Maybe MCInfo
-> F.FInfo a -> (KVGraph, [F.FInfo a])
partition' mn fi = case mn of
Nothing -> (g, fis mkPartition id)
Just mi -> (g, partitionN mi fi $ fis mkPartition' finfoToCpart)
where
g = kvGraph fi
css = decompose g
fis partF ctor = applyNonNull [ctor fi] (pbc partF) css
pbc partF = partitionByConstraints partF fi
partitionN :: MCInfo
-> F.FInfo a
-> [CPart a]
-> [F.FInfo a]
partitionN mi fi cp
| cpartSize (finfoToCpart fi) <= minThresh = [fi]
| otherwise = map (cpartToFinfo fi) $ toNParts sortedParts
where
toNParts p
| isDone p = p
| otherwise = toNParts $ insertSorted firstTwo rest
where (firstTwo, rest) = unionFirstTwo p
isDone [] = True
isDone [_] = True
isDone fi'@(a:b:_) = length fi' <= prts
&& (cpartSize a >= minThresh
|| cpartSize a + cpartSize b >= maxThresh)
sortedParts = sortBy sortPredicate cp
unionFirstTwo (a:b:xs) = (a `mappend` b, xs)
unionFirstTwo _ = errorstar "Partition.partitionN.unionFirstTwo called on bad arguments"
sortPredicate lhs rhs
| cpartSize lhs < cpartSize rhs = GT
| cpartSize lhs > cpartSize rhs = LT
| otherwise = EQ
insertSorted a [] = [a]
insertSorted a (x:xs) = if sortPredicate a x == LT
then x : insertSorted a xs
else a : x : xs
prts = mcCores mi
minThresh = mcMinPartSize mi
maxThresh = mcMaxPartSize mi
cpartSize :: CPart a -> Int
cpartSize c = (M.size . pcm) c + (length . pws) c
cpartToFinfo :: F.FInfo a -> CPart a -> F.FInfo a
cpartToFinfo fi p = fi { F.cm = pcm p
, F.ws = pws p
, F.fileName = cFileName p
}
finfoToCpart :: F.FInfo a -> CPart a
finfoToCpart fi = CPart { pcm = F.cm fi
, pws = F.ws fi
, cFileName = F.fileName fi
}
dumpPartitions :: (F.Fixpoint a) => Config -> [F.FInfo a] -> IO ()
dumpPartitions cfg fis =
forM_ (zip [0..] fis) $ \(i, fi) ->
writeFile (partFile fi i) (render $ F.toFixpoint cfg fi)
partFile :: F.FInfo a -> Int -> FilePath
partFile fi j = extFileName (Part j) (F.fileName fi)
type PartitionCtor a b = F.FInfo a
-> M.HashMap Int [(Integer, F.SubC a)]
-> M.HashMap Int [(F.KVar, F.WfC a)]
-> Int
-> b
partitionByConstraints :: PartitionCtor a b
-> F.FInfo a
-> KVComps
-> ListNE b
partitionByConstraints f fi kvss = f fi icM iwM <$> js
where
js = fst <$> jkvs
gc = groupFun cM
gk = groupFun kM
iwM = groupMap (gk . fst) (M.toList (F.ws fi))
icM = groupMap (gc . fst) (M.toList (F.cm fi))
jkvs = zip [1..] kvss
kvI = [ (x, j) | (j, kvs) <- jkvs, x <- kvs ]
kM = M.fromList [ (k, i) | (KVar k, i) <- kvI ]
cM = M.fromList [ (c, i) | (Cstr c, i) <- kvI ]
mkPartition fi icM iwM j
= fi { F.cm = M.fromList $ M.lookupDefault [] j icM
, F.ws = M.fromList $ M.lookupDefault [] j iwM
, F.fileName = partFile fi j
}
mkPartition' fi icM iwM j
= CPart { pcm = M.fromList $ M.lookupDefault [] j icM
, pws = M.fromList $ M.lookupDefault [] j iwM
, cFileName = partFile fi j
}
groupFun :: (Show k, Eq k, Hashable k) => M.HashMap k Int -> k -> Int
groupFun m k = safeLookup ("groupFun: " ++ show k) k m
decompose :: KVGraph -> KVComps
decompose kg = map (fst3 . f) <$> vss
where
(g,f,_) = G.graphFromEdges kg
vss = T.flatten <$> G.components g
kvGraph :: (F.TaggedC c a) => F.GInfo c a -> KVGraph
kvGraph = edgeGraph . kvEdges
edgeGraph :: [CEdge] -> KVGraph
edgeGraph es = [(v,v,vs) | (v, vs) <- groupList es ]
kvEdges :: (F.TaggedC c a) => F.GInfo c a -> [CEdge]
kvEdges fi = selfes ++ concatMap (subcEdges bs) cs
where
bs = F.bs fi
cs = M.elems (F.cm fi)
ks = fiKVars fi
selfes = [(Cstr i, Cstr i) | c <- cs, let i = F.subcId c]
++ [(KVar k, DKVar k) | k <- ks]
++ [(DKVar k, DKVar k) | k <- ks]
fiKVars :: F.GInfo c a -> [F.KVar]
fiKVars = M.keys . F.ws
subcEdges :: (F.TaggedC c a) => F.BindEnv -> c a -> [CEdge]
subcEdges bs c = [(KVar k, Cstr i ) | k <- V.envKVars bs c]
++ [(Cstr i, KVar k') | k' <- V.rhsKVars c ]
where
i = F.subcId c
data GDeps a
= Deps { depCuts :: !(S.HashSet a)
, depNonCuts :: !(S.HashSet a)
}
deriving (Show)
instance (Eq a, Hashable a) => Monoid (GDeps a) where
mempty = Deps S.empty S.empty
mappend (Deps d1 n1) (Deps d2 n2) = Deps (S.union d1 d2) (S.union n1 n2)
dCut, dNonCut :: (Hashable a) => a -> GDeps a
dNonCut v = Deps S.empty (S.singleton v)
dCut v = Deps (S.singleton v) S.empty
deps :: (F.TaggedC c a) => F.GInfo c a -> GDeps F.KVar
deps si = Deps (takeK cs) (takeK ns)
where
Deps cs ns = gDeps cutF (edgeGraph es)
es = kvEdges si
cutF = edgeRankCut (edgeRank es)
takeK = sMapMaybe tx
tx (KVar z) = Just z
tx _ = Nothing
sMapMaybe :: (Hashable b, Eq b) => (a -> Maybe b) -> S.HashSet a -> S.HashSet b
sMapMaybe f = S.fromList . mapMaybe f . S.toList
type EdgeRank = M.HashMap F.KVar Integer
edgeRank :: [CEdge] -> EdgeRank
edgeRank es = minimum . (n :) <$> kiM
where
n = 1 + maximum [ i | (Cstr i, _) <- es ]
kiM = group [ (k, i) | (KVar k, Cstr i) <- es ]
edgeRankCut :: EdgeRank -> Cutter CVertex
edgeRankCut km vs = case ks of
[] -> Nothing
k:_ -> Just (KVar k, [x | x@(u,_,_) <- vs, u /= KVar k])
where
ks = orderBy [k | (KVar k, _ ,_) <- vs]
rank = (km M.!)
orderBy = sortBy (compare `on` rank)
type Cutter a = [(a, a, [a])] -> Maybe (a, [(a, a, [a])])
type Cutable a = (Eq a, Ord a, Hashable a, Show a)
gDeps :: (Cutable a) => Cutter a -> [(a, a, [a])] -> GDeps a
gDeps f g = sccsToDeps f (G.stronglyConnCompR g)
sccsToDeps :: (Cutable a) => Cutter a -> [G.SCC (a, a, [a])] -> GDeps a
sccsToDeps f xs = mconcat $ sccDep f <$> xs
sccDep :: (Cutable a) => Cutter a -> G.SCC (a, a, [a]) -> GDeps a
sccDep _ (G.AcyclicSCC (v,_,_)) = dNonCut v
sccDep f (G.CyclicSCC vs) = cycleDep f vs
cycleDep :: (Cutable a) => Cutter a -> [(a,a,[a])] -> GDeps a
cycleDep _ [] = mempty
cycleDep f vs = addCut f (f vs)
addCut _ Nothing = mempty
addCut f (Just (v, vs')) = mconcat $ dCut v : (sccDep f <$> sccs)
where
sccs = G.stronglyConnCompR vs'
isReducible :: F.SInfo a -> Bool
isReducible fi = all (isReducibleWithStart g) vs
where
g = convertToGraph fi
vs = nodes g
isReducibleWithStart :: Gr a b -> Node -> Bool
isReducibleWithStart g x = all (isBackEdge domList) rEdges
where
dfsTree = head $ dff [x] g
rEdges = [e | e@(a,b) <- edges g, isDescendant a b dfsTree]
domList = dom g x
convertToGraph :: F.SInfo a -> Gr Int ()
convertToGraph fi = mkGraph vs es
where
subCs = M.elems (F.cm fi)
es = lUEdge <$> concatMap (subcEdges' kvI $ F.bs fi) subCs
ks = M.keys (F.ws fi)
kiM = M.fromList $ zip ks [0..]
kvI k = safeLookup ("convertToGraph: " ++ show k) k kiM
vs = lNode . kvI <$> M.keys (F.ws fi)
lNode i = (i, i)
lUEdge (i,j) = (i, j, ())
isDescendant :: Node -> Node -> T.Tree Node -> Bool
isDescendant x y (T.Node z f) | z == y = f `contains` x
| z == x = False
| otherwise = any (isDescendant x y) f
contains :: [T.Tree Node] -> Node -> Bool
contains t x = x `elem` concatMap T.flatten t
isBackEdge :: [(Node, [Node])] -> Edge -> Bool
isBackEdge t (u,v) = v `elem` xs
where
(Just xs) = lookup u t
subcEdges' :: (F.KVar -> Node) -> F.BindEnv -> F.SimpC a -> [(Node, Node)]
subcEdges' kvI be c = [(kvI k1, kvI k2) | k1 <- V.envKVars be c
, k2 <- V.kvars $ F.crhs c]
graphStatistics :: Config -> F.SInfo a -> IO ()
graphStatistics cfg si = when (elimStats cfg) $ do
writeGraph f (kvGraph si)
appendFile f . ppc . ptable $ graphStats si
where
f = queryFile Dot cfg
ppc d = showpp $ vcat [" ", " ", "/*", pprint d, "*/"]
data Stats = Stats {
stNumKVCuts :: !Int
, stNumKVNonLin :: !Int
, stNumKVTotal :: !Int
, stIsReducible :: !Bool
, stSetKVNonLin :: S.HashSet F.KVar
}
instance PTable Stats where
ptable (Stats {..}) = DocTable [
("# KVars [Cut]" , pprint stNumKVCuts)
, ("# KVars [NonLin]" , pprint stNumKVNonLin)
, ("# KVars [All]" , pprint stNumKVTotal)
, ("# Reducible" , pprint stIsReducible)
, ("KVars NonLin" , pprint stSetKVNonLin)
]
graphStats :: F.SInfo a -> Stats
graphStats si = Stats {
stNumKVCuts = S.size (depCuts d)
, stNumKVNonLin = S.size nlks
, stNumKVTotal = S.size (depCuts d) + S.size (depNonCuts d)
, stIsReducible = isReducible si
, stSetKVNonLin = nlks
}
where
nlks = nlKVars si
d = deps si
nlKVars :: (F.TaggedC c a) => F.GInfo c a -> S.HashSet F.KVar
nlKVars fi = S.unions $ nlKVarsC bs <$> cs
where
bs = F.bs fi
cs = M.elems (F.cm fi)
nlKVarsC :: (F.TaggedC c a) => F.BindEnv -> c a -> S.HashSet F.KVar
nlKVarsC bs c = S.fromList [ k | (k, n) <- V.envKVarsN bs c, n >= 2]
elimSolGraph :: Config -> F.Solution -> IO ()
elimSolGraph cfg s = writeGraph f (So.solutionGraph s)
where
f = queryFile Dot cfg