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