module Agda.Termination.CallGraph
(
Node
, Call, mkCall, mkCall', source, target, callMatrixSet
, (>*<)
, CallGraph(..)
, targetNodes
, fromList
, toList
, empty
, null
, union
, insert
, complete, completionStep
, Agda.Termination.CallGraph.tests
) where
import Prelude hiding (null)
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Data.Function
import qualified Data.List as List
import Data.Map (Map, (!))
import qualified Data.Map as Map
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (Traversable)
import qualified Data.Traversable as Trav
import Agda.Termination.CallMatrix (CallMatrix, callMatrix, CallMatrixAug(..), CMSet(..), CallComb(..))
import qualified Agda.Termination.CallMatrix as CMSet
import Agda.Termination.CutOff
import Agda.Termination.Order
import Agda.Termination.SparseMatrix as Matrix hiding (tests)
import Agda.Termination.Semiring (HasZero(..), Semiring)
import qualified Agda.Termination.Semiring as Semiring
import Agda.Utils.Favorites (Favorites(Favorites))
import qualified Agda.Utils.Favorites as Fav
import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Edge(..),Graph(..))
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Function
import Agda.Utils.List hiding (tests)
import Agda.Utils.Map
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.PartialOrd
import Agda.Utils.Pretty hiding (empty)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.QuickCheck hiding (label)
import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
type Node = Int
type Call cinfo = Edge Node Node (CMSet cinfo)
callMatrixSet :: Call cinfo -> CMSet cinfo
callMatrixSet = label
mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo
mkCall s t m cinfo = Edge s t $ CMSet.singleton $ CallMatrixAug m cinfo
mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo
mkCall' s t m = mkCall s t m mempty
instance Monoid cinfo => CallComb (Call cinfo) where
c1 >*< c2 | g == g' = Edge f h (label c1 >*< label c2)
where f = source c2
g = target c2
g' = source c1
h = target c1
c1 >*< c2 = __IMPOSSIBLE__
newtype CallGraph cinfo = CallGraph { theCallGraph :: Graph Node Node (CMSet cinfo) }
deriving (Show)
targetNodes :: CallGraph cinfo -> Set Node
targetNodes = Graph.targetNodes . theCallGraph
toList :: CallGraph cinfo -> [Call cinfo]
toList = Graph.edges . theCallGraph
fromList :: Monoid cinfo => [Call cinfo] -> CallGraph cinfo
fromList = CallGraph . Graph.fromListWith CMSet.union
empty :: CallGraph cinfo
empty = CallGraph Graph.empty
null :: CallGraph cinfo -> Bool
null = List.all (CMSet.null . label) . toList
union :: Monoid cinfo
=> CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
union (CallGraph cs1) (CallGraph cs2) = CallGraph $
Graph.unionWith CMSet.union cs1 cs2
instance Monoid cinfo => Monoid (CallGraph cinfo) where
mempty = empty
mappend = union
insert :: Monoid cinfo
=> Node -> Node -> CallMatrix -> cinfo
-> CallGraph cinfo -> CallGraph cinfo
insert s t cm cinfo = CallGraph . Graph.insertEdgeWith CMSet.union e . theCallGraph
where e = mkCall s t cm cinfo
type CombineNewOldT a = a -> a -> (a, a)
class CombineNewOld a where
combineNewOld :: CombineNewOldT a
instance PartialOrd a => CombineNewOld (Favorites a) where
combineNewOld new old = (new', Fav.unionCompared (new', old'))
where (new', old') = Fav.compareFavorites new old
deriving instance CombineNewOld (CMSet cinfo)
instance (Monoid a, CombineNewOld a, Ord s, Ord t) => CombineNewOld (Graph s t a) where
combineNewOld new old = Graph.unzip $ Graph.unionWith comb new' old'
where
new' = (,mempty) <$> new
old' = (mempty,) <$> old
comb (new1,old1) (new2,old2)
= mapFst (new2 `mappend`) $ combineNewOld new1 old2
combineNewOldCallGraph :: (Monoid cinfo, ?cutoff :: CutOff) => CombineNewOldT (CallGraph cinfo)
combineNewOldCallGraph (CallGraph new) (CallGraph old) = CallGraph -*- CallGraph $ combineNewOld comb old
where comb = Graph.composeWith (>*<) CMSet.union new old
complete :: (?cutoff :: CutOff) => Monoid cinfo => CallGraph cinfo -> CallGraph cinfo
complete cs = repeatWhile (mapFst (not . null) . completionStep cs) cs
completionStep :: (?cutoff :: CutOff) => Monoid cinfo =>
CallGraph cinfo -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
completionStep gOrig gThis = combineNewOldCallGraph gOrig gThis
instance Pretty cinfo => Pretty (CallGraph cinfo) where
pretty = vcat . map prettyCall . toList
where
prettyCall e = if CMSet.null (callMatrixSet e) then P.empty else align 20 $
[ ("Source:", text $ show $ source e)
, ("Target:", text $ show $ target e)
, ("Matrix:", pretty $ callMatrixSet e)
]
callGraph :: (Monoid cinfo, Arbitrary cinfo) => Gen (CallGraph cinfo)
callGraph = do
indices <- fmap List.nub arbitrary
n <- natural
let noMatrices | List.null indices = 0
| otherwise = n `min` 3
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 })
mkCall s t m <$> arbitrary
tests :: IO Bool
tests = runTests "Agda.Termination.CallGraph" []
where ?cutoff = DontCutOff