module Agda.Termination.CallGraph
(
Order(Mat), decr
, (.*.)
, supremum, infimum
, decreasing, le, lt, unknown, orderMat
, Index
, CallMatrix(..)
, (>*<)
, callMatrixInvariant
, Call(..)
, callInvariant
, CallGraph
, callGraphInvariant
, fromList
, toList
, empty
, union
, insert
, complete
, prettyBehaviour
, Agda.Termination.CallGraph.tests
) where
import Agda.Utils.QuickCheck
import Agda.Utils.Function
import Agda.Utils.List hiding (tests)
import Agda.Utils.Pretty hiding (empty)
import Agda.Utils.TestHelpers
import Agda.Termination.SparseMatrix as Matrix hiding (tests)
import Agda.Termination.Semiring (HasZero(..),SemiRing,Semiring)
import qualified Agda.Termination.Semiring as Semiring
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map, (!))
import qualified Data.Map as Map
import Data.List hiding (union, insert)
import Data.Monoid
import Data.Array (elems)
import Data.Function
#include "../undefined.h"
import Agda.Utils.Impossible
data Order
= Decr Int | Unknown | Mat (Matrix Integer Order)
deriving (Eq,Ord)
instance Show Order where
show (Decr k) = show ( k)
show Unknown = "."
show (Mat m) = "Mat " ++ show m
instance HasZero Order where
zeroElement = Unknown
decr :: (?cutoff :: Int) => Int -> Order
decr k | k < ?cutoff = Unknown
| k > ?cutoff = Decr (?cutoff + 1)
| otherwise = Decr k
orderMat :: Matrix Integer Order -> Order
orderMat m | Matrix.isEmpty m = Decr 0
| otherwise = case isSingleton m of
Just o -> o
Nothing -> Mat m
isOrder :: (?cutoff :: Int) => Order -> Bool
isOrder (Decr k) = k >= ?cutoff && k <= ?cutoff + 1
isOrder Unknown = True
isOrder (Mat m) = False
prop_decr :: (?cutoff :: Int) => Int -> Bool
prop_decr = isOrder . decr
le :: Order
le = Decr 0
lt :: Order
lt = Decr 1
unknown :: Order
unknown = Unknown
decreasing :: Order -> Bool
decreasing (Decr k) | k > 0 = True
decreasing _ = False
instance Pretty Order where
pretty (Decr 0) = text "="
pretty (Decr k) = text $ show k
pretty Unknown = text "?"
pretty (Mat m) = text "Mat" <+> pretty m
instance Arbitrary Order where
arbitrary = frequency
[(30, return Unknown)
,(70, elements [0,1] >>= return . Decr)
]
instance CoArbitrary Order where
coarbitrary (Decr k) = variant 0
coarbitrary Unknown = variant 1
coarbitrary (Mat m) = variant 2
(.*.) :: (?cutoff :: Int) => Order -> Order -> Order
Unknown .*. _ = Unknown
(Mat m) .*. Unknown = Unknown
(Decr k) .*. Unknown = Unknown
(Decr k) .*. (Decr l) = decr (k + l)
(Decr 0) .*. (Mat m) = Mat m
(Decr k) .*. (Mat m) = (Decr k) .*. (collapse m)
(Mat m1) .*. (Mat m2) = if (okM m1 m2) then
Mat $ mul orderSemiring m1 m2
else
(collapse m1) .*. (collapse m2)
(Mat m) .*. (Decr 0) = Mat m
(Mat m) .*. (Decr k) = (collapse m) .*. (Decr k)
collapse :: (?cutoff :: Int) => Matrix Integer Order -> Order
collapse m = case (toLists (Matrix.transpose m)) of
[] -> __IMPOSSIBLE__
m' -> foldl1 (.*.) $ map (foldl1 maxO) m'
okM :: Matrix Integer Order -> Matrix Integer Order -> Bool
okM m1 m2 = (rows $ size m2) == (cols $ size m1)
supremum :: (?cutoff :: Int) => [Order] -> Order
supremum = foldr maxO Unknown
maxO :: (?cutoff :: Int) => Order -> Order -> Order
maxO o1 o2 = case (o1,o2) of
(Decr k, Decr l) -> Decr (max k l)
(Unknown,_) -> o2
(_,Unknown) -> o1
(Mat m1, Mat m2) -> Mat (Matrix.add maxO m1 m2)
(Mat m,_) -> maxO (collapse m) o2
(_,Mat m) -> maxO o1 (collapse m)
infimum :: (?cutoff :: Int) => [Order] -> Order
infimum (o:l) = foldl minO o l
infimum [] = __IMPOSSIBLE__
minO :: (?cutoff :: Int) => Order -> Order -> Order
minO o1 o2 = case (o1,o2) of
(Unknown,_) -> Unknown
(_,Unknown) -> Unknown
(Decr k, Decr l) -> decr (min k l)
(Mat m1, Mat m2) -> if (size m1 == size m2) then
Mat $ Matrix.intersectWith minO m1 m2
else
minO (collapse m1) (collapse m2)
(Mat m1,_) -> minO (collapse m1) o2
(_,Mat m2) -> minO o1 (collapse m2)
orderSemiring :: (?cutoff :: Int) => Semiring Order
orderSemiring =
Semiring.Semiring { Semiring.add = maxO
, Semiring.mul = (.*.)
, Semiring.zero = Unknown
}
prop_orderSemiring :: (?cutoff :: Int) => Order -> Order -> Order -> Bool
prop_orderSemiring = Semiring.semiringInvariant orderSemiring
type Index = Integer
newtype CallMatrix = CallMatrix { mat :: Matrix Index Order }
deriving (Eq, Ord, Show)
instance Arbitrary CallMatrix where
arbitrary = do
sz <- arbitrary
callMatrix sz
instance CoArbitrary CallMatrix where
coarbitrary (CallMatrix m) = coarbitrary m
prop_Arbitrary_CallMatrix = callMatrixInvariant
callMatrix :: Size Index -> Gen CallMatrix
callMatrix sz = do
m <- matrixUsingRowGen sz rowGen
return $ CallMatrix { mat = m }
where
rowGen :: Index -> Gen [Order]
rowGen 0 = return []
rowGen n = do
x <- arbitrary
i <- choose (0, n 1)
return $ genericReplicate i Unknown ++ [x] ++
genericReplicate (n 1 i) Unknown
prop_callMatrix sz =
forAll (callMatrix sz) $ \cm ->
callMatrixInvariant cm
&&
size (mat cm) == sz
callMatrixInvariant :: CallMatrix -> Bool
callMatrixInvariant cm =
matrixInvariant m &&
all ((<= 1) . length . filter (/= Unknown)) (toLists m)
where m = mat cm
(<*>) :: (?cutoff :: Int) => CallMatrix -> CallMatrix -> CallMatrix
cm1 <*> cm2 =
CallMatrix { mat = mul orderSemiring (mat cm1) (mat cm2) }
prop_cmMul sz =
forAll natural $ \c2 ->
forAll (callMatrix sz) $ \cm1 ->
forAll (callMatrix $ Size { rows = cols sz, cols = c2 }) $ \cm2 ->
callMatrixInvariant (cm1 <*> cm2)
data Call =
Call { source :: Index
, target :: Index
, cm :: CallMatrix
}
deriving (Eq, Ord, Show)
instance Arbitrary Call where
arbitrary = do
[s, t] <- vectorOf 2 arbitrary
cm <- arbitrary
return (Call { source = s, target = t, cm = cm })
instance CoArbitrary Call where
coarbitrary (Call s t cm) =
coarbitrary s . coarbitrary t . coarbitrary cm
prop_Arbitrary_Call :: Call -> Bool
prop_Arbitrary_Call = callInvariant
callInvariant :: Call -> Bool
callInvariant = callMatrixInvariant . cm
(>*<) :: (?cutoff :: Int) => Call -> Call -> Call
c1 >*< c2 =
Call { source = source c2
, target = target c1
, cm = cm c1 <*> cm c2
}
newtype CallGraph meta = CallGraph { cg :: Map Call meta }
deriving (Eq, Show)
callGraphInvariant :: CallGraph meta -> Bool
callGraphInvariant = all (callInvariant . fst) . toList
toList :: CallGraph meta -> [(Call, meta)]
toList = Map.toList . cg
fromList :: Monoid meta => [(Call, meta)] -> CallGraph meta
fromList = CallGraph . Map.fromListWith mappend
empty :: CallGraph meta
empty = CallGraph Map.empty
union :: Monoid meta
=> CallGraph meta -> CallGraph meta -> CallGraph meta
union cs1 cs2 = CallGraph $ (Map.unionWith mappend `on` cg) cs1 cs2
insert :: Monoid meta
=> Call -> meta -> CallGraph meta -> CallGraph meta
insert c m = CallGraph . Map.insertWith mappend c m . cg
callGraph :: (Monoid meta, Arbitrary meta) => Gen (CallGraph meta)
callGraph = do
indices <- fmap nub arbitrary
n <- natural
let noMatrices | null indices = 0
| otherwise = n `min` 3
fmap fromList $ vectorOf noMatrices (matGen indices)
where
matGen indices = do
[s, t] <- vectorOf 2 (elements indices)
[c, r] <- vectorOf 2 (choose (0, 2))
m <- callMatrix (Size { rows = r, cols = c })
callId <- arbitrary
return (Call { source = s, target = t, cm = m }, callId)
prop_callGraph =
forAll (callGraph :: Gen (CallGraph [Integer])) $ \cs ->
callGraphInvariant cs
combine
:: (Monoid meta, ?cutoff :: Int) => CallGraph meta -> CallGraph meta -> CallGraph meta
combine s1 s2 = fromList $
[ (c1 >*< c2, m1 `mappend` m2)
| (c1, m1) <- toList s1, (c2, m2) <- toList s2
, source c1 == target c2
]
complete :: (?cutoff :: Int) => Monoid meta => CallGraph meta -> CallGraph meta
complete cs = complete' safeCS
where
safeCS = ensureCompletePrecondition cs
complete' cs | cs' .==. cs = cs
| otherwise = complete' cs'
where
cs' = cs `union` combine cs safeCS
(.==.) = ((==) `on` (Map.keys . cg))
prop_complete :: (?cutoff :: Int) => Property
prop_complete =
forAll (callGraph :: Gen (CallGraph [Integer])) $ \cs ->
isComplete (complete cs)
isComplete :: (Ord meta, Monoid meta, ?cutoff :: Int) => CallGraph meta -> Bool
isComplete s = all (`Map.member` cg s) combinations
where
calls = toList s
combinations =
[ c2 >*< c1 | (c1, _) <- calls, (c2, _) <- calls
, target c1 == source c2 ]
completePrecondition :: CallGraph meta -> Bool
completePrecondition cs =
all (allEqual . map snd) $
groupOn fst $
concat [ [(source c, cols $ size' c), (target c, rows $ size' c)]
| (c, _) <- toList cs]
where
size' = size . mat . cm
ensureCompletePrecondition
:: Monoid meta => CallGraph meta -> CallGraph meta
ensureCompletePrecondition cs =
CallGraph $ Map.mapKeysWith mappend pad $ cg cs
where
noArgs :: Map Index Integer
noArgs = foldr (\c m -> insert (source c) (cols' c) $
insert (target c) (rows' c) m)
Map.empty
(map fst $ toList cs)
where insert = Map.insertWith max
pad c = c { cm = CallMatrix { mat = padRows $ padCols $ mat $ cm c } }
where
padCols = iterate' ((noArgs ! source c) cols' c)
(addColumn Unknown)
padRows = iterate' ((noArgs ! target c) rows' c)
(addRow Unknown)
cols' = cols . size'
rows' = rows . size'
size' = size . mat . cm
prop_ensureCompletePrecondition =
forAll (callGraph :: Gen (CallGraph [Integer])) $ \cs ->
let cs' = ensureCompletePrecondition cs in
completePrecondition cs'
&&
all callInvariant (map fst $ toList cs')
&&
and [ or [ new .==. old | (old, _) <- toList cs ]
| (new, _) <- toList cs' ]
where
c1 .==. c2 = all (all (uncurry (==)))
((zipZip `on` (toLists . mat . cm)) c1 c2)
zipZip :: [[a]] -> [[b]] -> [[(a, b)]]
zipZip xs ys = map (uncurry zip) $ zip xs ys
instance Show meta => Pretty (CallGraph meta) where
pretty = vcat . map prettyCall . toList
where
prettyCall (c, meta) = align 20
[ ("Source:", text $ show $ source c)
, ("Target:", text $ show $ target c)
, ("Matrix:", pretty (mat $ cm c))
, ("Meta info:", text $ show meta)
]
prettyBehaviour :: Show meta => CallGraph meta -> Doc
prettyBehaviour = vcat . map prettyCall . filter (toSelf . fst) . toList
where
toSelf c = source c == target c
prettyCall (c, meta) = vcat $ map text
[ "Function: " ++ show (source c)
, "Behaviour: " ++ show (elems $ diagonal $ mat $ cm c)
, "Meta info: " ++ show meta
]
tests :: IO Bool
tests = runTests "Agda.Termination.CallGraph"
[ quickCheck' callMatrixInvariant
, quickCheck' prop_decr
, quickCheck' prop_orderSemiring
, quickCheck' prop_Arbitrary_CallMatrix
, quickCheck' prop_callMatrix
, quickCheck' prop_cmMul
, quickCheck' prop_Arbitrary_Call
, quickCheck' prop_callGraph
, quickCheck' prop_complete
, quickCheck' prop_ensureCompletePrecondition
]
where ?cutoff = 2