{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}
module Agda.Termination.CallGraph
(
Node
, Call, mkCall, mkCall', source, target, callMatrixSet
, (>*<)
, CallGraph(..)
, targetNodes
, fromList
, toList
, union
, insert
, complete, completionStep
) where
import Prelude hiding (null)
import qualified Data.List as List
import Data.Semigroup
import Data.Set (Set)
import Agda.Termination.CallMatrix (CallMatrix, CallMatrixAug(..), CMSet(..), CallComb(..))
import qualified Agda.Termination.CallMatrix as CMSet
import Agda.Termination.CutOff
import Agda.Termination.SparseMatrix as Matrix
import Agda.Utils.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.Monad
import Agda.Utils.Null
import Agda.Utils.PartialOrd
import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Singleton
import Agda.Utils.Tuple
type Node = Int
type Call cinfo = Edge 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 $ singleton $ CallMatrixAug m cinfo
mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo
mkCall' s t m = mkCall s t m mempty
newtype CallGraph cinfo = CallGraph { theCallGraph :: Graph Node (CMSet cinfo) }
deriving (Show)
targetNodes :: CallGraph cinfo -> Set Node
targetNodes = Graph.targetNodes . theCallGraph
toList :: CallGraph cinfo -> [Call cinfo]
toList = Graph.edges . theCallGraph
fromList :: [Call cinfo] -> CallGraph cinfo
fromList = CallGraph . Graph.fromEdgesWith CMSet.union
instance Null (CallGraph cinfo) where
empty = CallGraph Graph.empty
null = List.all (null . label) . toList
union :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
union (CallGraph cs1) (CallGraph cs2) = CallGraph $
Graph.unionWith CMSet.union cs1 cs2
instance Semigroup (CallGraph cinfo) where
(<>) = union
instance Monoid (CallGraph cinfo) where
mempty = empty
mappend = (<>)
insert :: 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 n) => CombineNewOld (Graph n 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 null (callMatrixSet e) then empty else align 20 $
[ ("Source:", text $ show $ source e)
, ("Target:", text $ show $ target e)
, ("Matrix:", pretty $ callMatrixSet e)
]