1{-# LANGUAGE CPP #-} 2{-# LANGUAGE ImplicitParams #-} 3 4-- | Call graphs and related concepts, more or less as defined in 5-- \"A Predicative Analysis of Structural Recursion\" by 6-- Andreas Abel and Thorsten Altenkirch. 7 8-- Originally copied from Agda1 sources. 9 10module Agda.Termination.CallGraph 11 ( -- * Calls 12 Node 13 , Call, mkCall, mkCall', source, target, callMatrixSet 14 , (>*<) 15 -- * Call graphs 16 , CallGraph(..) 17 , targetNodes 18 , fromList 19 , toList 20 , union 21 , insert 22 , complete, completionStep 23 -- , prettyBehaviour 24 ) where 25 26import Prelude hiding (null) 27 28import qualified Data.List as List 29#if __GLASGOW_HASKELL__ < 804 30import Data.Semigroup 31#endif 32import Data.Set (Set) 33 34import Agda.Termination.CallMatrix (CallMatrix, CallMatrixAug(..), CMSet(..), CallComb(..)) 35import qualified Agda.Termination.CallMatrix as CMSet 36import Agda.Termination.CutOff 37 38import Agda.Utils.Favorites (Favorites) 39import qualified Agda.Utils.Favorites as Fav 40import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Edge(..),Graph(..)) 41import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph 42 43import Agda.Utils.Function 44 45import Agda.Utils.Null 46import Agda.Utils.PartialOrd 47import Agda.Utils.Pretty 48import Agda.Utils.Singleton 49import Agda.Utils.Tuple 50 51------------------------------------------------------------------------ 52-- Calls 53 54-- | Call graph nodes. 55-- 56-- Machine integer 'Int' is sufficient, since we cannot index more than 57-- we have addresses on our machine. 58 59type Node = Int 60 61-- | Calls are edges in the call graph. 62-- It can be labelled with several call matrices if there 63-- are several pathes from one function to another. 64 65type Call cinfo = Edge Node (CMSet cinfo) 66 67callMatrixSet :: Call cinfo -> CMSet cinfo 68callMatrixSet = label 69 70-- | Make a call with a single matrix. 71mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo 72mkCall s t m cinfo = Edge s t $ singleton $ CallMatrixAug m cinfo 73 74-- | Make a call with empty @cinfo@. 75mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo 76mkCall' s t m = mkCall s t m mempty 77 78------------------------------------------------------------------------ 79-- Call graphs 80 81-- | A call graph is a set of calls. Every call also has some 82-- associated meta information, which should be 'Monoid'al so that the 83-- meta information for different calls can be combined when the calls 84-- are combined. 85 86newtype CallGraph cinfo = CallGraph { theCallGraph :: Graph Node (CMSet cinfo) } 87 deriving (Show) 88 89 90-- | Returns all the nodes with incoming edges. Somewhat expensive. @O(e)@. 91 92targetNodes :: CallGraph cinfo -> Set Node 93targetNodes = Graph.targetNodes . theCallGraph 94 95-- | Converts a call graph to a list of calls with associated meta 96-- information. 97 98toList :: CallGraph cinfo -> [Call cinfo] 99toList = Graph.edges . theCallGraph 100 101-- | Converts a list of calls with associated meta information to a 102-- call graph. 103 104fromListCG :: [Call cinfo] -> CallGraph cinfo 105fromListCG = CallGraph . Graph.fromEdgesWith CMSet.union 106 107-- | 'null' checks whether the call graph is completely disconnected. 108instance Null (CallGraph cinfo) where 109 empty = CallGraph Graph.empty 110 null = List.all (null . label) . toList 111 112-- | Takes the union of two call graphs. 113 114union :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo 115union (CallGraph cs1) (CallGraph cs2) = CallGraph $ 116 Graph.unionWith CMSet.union cs1 cs2 117 118-- | 'CallGraph' is a monoid under 'union'. 119 120instance Semigroup (CallGraph cinfo) where 121 (<>) = union 122 123instance Monoid (CallGraph cinfo) where 124 mempty = empty 125 mappend = (<>) 126 127instance Singleton (Call cinfo) (CallGraph cinfo) where 128 singleton = fromList . singleton 129 130instance Collection (Call cinfo) (CallGraph cinfo) where 131 fromList = fromListCG 132 133-- | Inserts a call into a call graph. 134 135insert :: Node -> Node -> CallMatrix -> cinfo 136 -> CallGraph cinfo -> CallGraph cinfo 137insert s t cm cinfo = CallGraph . Graph.insertEdgeWith CMSet.union e . theCallGraph 138 where e = mkCall s t cm cinfo 139 140 141-- * Combination of a new thing with an old thing 142-- returning a really new things and updated old things. 143 144type CombineNewOldT a = a -> a -> (a, a) 145 146class CombineNewOld a where 147 combineNewOld :: CombineNewOldT a 148 149instance PartialOrd a => CombineNewOld (Favorites a) where 150 combineNewOld new old = (new', Fav.unionCompared (new', old')) 151 where (new', old') = Fav.compareFavorites new old 152 153deriving instance CombineNewOld (CMSet cinfo) 154 155instance (Monoid a, CombineNewOld a, Ord n) => CombineNewOld (Graph n a) where 156 combineNewOld new old = Graph.unzip $ Graph.unionWith comb new' old' 157 where 158 new' = (,mempty) <$> new 159 old' = (mempty,) <$> old 160 comb (new1,old1) (new2,old2) -- TODO: ensure old1 is null 161 = mapFst (new2 `mappend`) $ combineNewOld new1 old2 162 -- -- | old1 == mempty = mapFst (new2 `mappend`) $ combineNewOld new1 old2 163 -- -- | otherwise = __IMPOSSIBLE__ 164 165 -- Filter unlabelled edges from the resulting new graph. 166 -- filt = Graph.filterEdges (not . null) 167 168-- | Call graph combination. 169-- 170-- Application of '>*<' to all pairs @(c1,c2)@ 171-- for which @'source' c1 = 'target' c2@.) 172 173-- GHC supports implicit-parameter constraints in instance declarations 174-- only from 7.4. To maintain compatibility with 7.2, we skip this instance: 175-- KEEP: 176-- instance (Monoid cinfo, ?cutoff :: CutOff) => CombineNewOld (CallGraph cinfo) where 177-- combineNewOld (CallGraph new) (CallGraph old) = CallGraph -*- CallGraph $ combineNewOld comb old 178-- -- combined calls: 179-- where comb = Graph.composeWith (>*<) CMSet.union new old 180 181-- Non-overloaded version: 182combineNewOldCallGraph :: (Monoid cinfo, ?cutoff :: CutOff) => CombineNewOldT (CallGraph cinfo) 183combineNewOldCallGraph (CallGraph new) (CallGraph old) = CallGraph -*- CallGraph $ combineNewOld comb old 184 -- combined calls: 185 where comb = Graph.composeWith (>*<) CMSet.union new old 186 187-- | Call graph comparison. 188-- A graph @cs'@ is ``worse'' than @cs@ if it has a new edge (call) 189-- or a call got worse, which means that one of its elements 190-- that was better or equal to 'Le' moved a step towards 'Un'. 191-- 192-- A call graph is complete if combining it with itself does not make it 193-- any worse. This is sound because of monotonicity: By combining a graph 194-- with itself, it can only get worse, but if it does not get worse after 195-- one such step, it gets never any worse. 196 197-- | @'complete' cs@ completes the call graph @cs@. A call graph is 198-- complete if it contains all indirect calls; if @f -> g@ and @g -> 199-- h@ are present in the graph, then @f -> h@ should also be present. 200 201complete :: (?cutoff :: CutOff) => Monoid cinfo => CallGraph cinfo -> CallGraph cinfo 202complete cs = repeatWhile (mapFst (not . null) . completionStep cs) cs 203 204completionStep :: (?cutoff :: CutOff) => Monoid cinfo => 205 CallGraph cinfo -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo) 206completionStep gOrig gThis = combineNewOldCallGraph gOrig gThis 207 208------------------------------------------------------------------------ 209-- * Printing 210------------------------------------------------------------------------ 211 212-- | Displays the recursion behaviour corresponding to a call graph. 213 214instance Pretty cinfo => Pretty (CallGraph cinfo) where 215 pretty = vcat . map prettyCall . toList 216 where 217 prettyCall e = if null (callMatrixSet e) then empty else align 20 $ 218 [ ("Source:", text $ show $ source e) 219 , ("Target:", text $ show $ target e) 220 , ("Matrix:", pretty $ callMatrixSet e) 221 ] 222 223-- -- | Displays the recursion behaviour corresponding to a call graph. 224 225-- prettyBehaviour :: Show cinfo => CallGraph cinfo -> Doc 226-- prettyBehaviour = vcat . map prettyCall . filter toSelf . toList 227-- where 228-- toSelf c = source c == target c 229 230-- prettyCall e = vcat $ map text 231-- [ "Function: " ++ show (source e) 232-- -- , "Behaviour: " ++ show (diagonal $ mat $ cm c) -- TODO 233-- -- , "Meta info: " ++ show cinfo 234-- ] 235