{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE ImplicitParams             #-}

-- | Call graphs and related concepts, more or less as defined in
--     \"A Predicative Analysis of Structural Recursion\" by
--     Andreas Abel and Thorsten Altenkirch.

-- Originally copied from Agda1 sources.

module Agda.Termination.CallGraph
  ( -- * Calls
    Node
  , Call, source, target, callMatrixSet
  , mkCall, mkCall' -- exported for the sake of testing, otherwise we use 'insert'
  , (>*<)
    -- * Call graphs
  , CallGraph(..)
  , loops
  , targetNodes
  , fromList
  , toList
  , union
  , insert
  , complete, completionStep
  -- , strengthenLoopDiagonals -- bad heuristics, see https://github.com/agda/agda/pull/8184#issuecomment-3487147737
  -- , prettyBehaviour
  ) where

import Prelude hiding (null)

import Data.List qualified as List
import Data.Set (Set)

import Agda.Syntax.Common.Pretty

import Agda.Termination.CallMatrix (CallMatrix, CallMatrixAug(..), CMSet(..), CallComb(..)) -- , mapCMSet, mapCallMatrixAug, mapCallMatrix)
import Agda.Termination.CallMatrix qualified as CMSet
import Agda.Termination.CutOff
-- import Agda.Termination.Order        ( makeIncreaseInfinite )
-- import Agda.Termination.SparseMatrix ( mapDiagonalNonZeros )

import Agda.Utils.Favorites (Favorites)
import Agda.Utils.Favorites qualified as Fav
import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Edge(..),Graph(..))
import Agda.Utils.Graph.AdjacencyMap.Unidirectional qualified as Graph

import Agda.Utils.Function

import Agda.Utils.Null
import Agda.Utils.PartialOrd
import Agda.Utils.Singleton
import Agda.Utils.Tuple

------------------------------------------------------------------------
-- Calls

-- | Call graph nodes.
--
--   Machine integer 'Int' is sufficient, since we cannot index more than
--   we have addresses on our machine.

type Node = Int

-- | Calls are edges in the call graph.
--   It can be labelled with several call matrices if there
--   are several pathes from one function to another.

type Call cinfo = Edge Node (CMSet cinfo)

callMatrixSet :: Call cinfo -> CMSet cinfo
callMatrixSet :: forall cinfo. Call cinfo -> CMSet cinfo
callMatrixSet = Edge Node (CMSet cinfo) -> CMSet cinfo
forall n e. Edge n e -> e
label

-- | Make a call with a single matrix.
mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo
mkCall :: forall cinfo. Node -> Node -> CallMatrix -> cinfo -> Call cinfo
mkCall Node
s Node
t CallMatrix
m cinfo
cinfo = Node -> Node -> CMSet cinfo -> Edge Node (CMSet cinfo)
forall n e. n -> n -> e -> Edge n e
Edge Node
s Node
t (CMSet cinfo -> Edge Node (CMSet cinfo))
-> CMSet cinfo -> Edge Node (CMSet cinfo)
forall a b. (a -> b) -> a -> b
$ CallMatrixAug cinfo -> CMSet cinfo
forall el coll. Singleton el coll => el -> coll
singleton (CallMatrixAug cinfo -> CMSet cinfo)
-> CallMatrixAug cinfo -> CMSet cinfo
forall a b. (a -> b) -> a -> b
$ CallMatrix -> cinfo -> CallMatrixAug cinfo
forall cinfo. CallMatrix -> cinfo -> CallMatrixAug cinfo
CallMatrixAug CallMatrix
m cinfo
cinfo

-- @mkCall'@ is only used in our Internal tests.
-- | Make a call with empty @cinfo@.
mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo
mkCall' :: forall cinfo.
Monoid cinfo =>
Node -> Node -> CallMatrix -> Call cinfo
mkCall' Node
s Node
t CallMatrix
m = Node -> Node -> CallMatrix -> cinfo -> Call cinfo
forall cinfo. Node -> Node -> CallMatrix -> cinfo -> Call cinfo
mkCall Node
s Node
t CallMatrix
m cinfo
forall a. Monoid a => a
mempty

------------------------------------------------------------------------
-- Call graphs

-- | A call graph is a set of calls. Every call also has some
-- associated meta information, which should be 'Monoid'al so that the
-- meta information for different calls can be combined when the calls
-- are combined.

newtype CallGraph cinfo = CallGraph { forall cinfo. CallGraph cinfo -> Graph Node (CMSet cinfo)
theCallGraph :: Graph Node (CMSet cinfo) }
  deriving (Node -> CallGraph cinfo -> ShowS
[CallGraph cinfo] -> ShowS
CallGraph cinfo -> String
(Node -> CallGraph cinfo -> ShowS)
-> (CallGraph cinfo -> String)
-> ([CallGraph cinfo] -> ShowS)
-> Show (CallGraph cinfo)
forall cinfo. Show cinfo => Node -> CallGraph cinfo -> ShowS
forall cinfo. Show cinfo => [CallGraph cinfo] -> ShowS
forall cinfo. Show cinfo => CallGraph cinfo -> String
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall cinfo. Show cinfo => Node -> CallGraph cinfo -> ShowS
showsPrec :: Node -> CallGraph cinfo -> ShowS
$cshow :: forall cinfo. Show cinfo => CallGraph cinfo -> String
show :: CallGraph cinfo -> String
$cshowList :: forall cinfo. Show cinfo => [CallGraph cinfo] -> ShowS
showList :: [CallGraph cinfo] -> ShowS
Show)

mapCallGraph :: (Graph Node (CMSet cinfo) -> Graph Node (CMSet cinfo)) -> CallGraph cinfo -> CallGraph cinfo
mapCallGraph :: forall cinfo.
(Graph Node (CMSet cinfo) -> Graph Node (CMSet cinfo))
-> CallGraph cinfo -> CallGraph cinfo
mapCallGraph Graph Node (CMSet cinfo) -> Graph Node (CMSet cinfo)
f (CallGraph Graph Node (CMSet cinfo)
g) = Graph Node (CMSet cinfo) -> CallGraph cinfo
forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph (Graph Node (CMSet cinfo) -> Graph Node (CMSet cinfo)
f Graph Node (CMSet cinfo)
g)

-- | Returns all nodes with self-loops.

loops :: CallGraph cinfo -> [(Node, CMSet cinfo)]
loops :: forall cinfo. CallGraph cinfo -> [(Node, CMSet cinfo)]
loops = Graph Node (CMSet cinfo) -> [(Node, CMSet cinfo)]
forall n e. Ord n => Graph n e -> [(n, e)]
Graph.loops (Graph Node (CMSet cinfo) -> [(Node, CMSet cinfo)])
-> (CallGraph cinfo -> Graph Node (CMSet cinfo))
-> CallGraph cinfo
-> [(Node, CMSet cinfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> Graph Node (CMSet cinfo)
forall cinfo. CallGraph cinfo -> Graph Node (CMSet cinfo)
theCallGraph

-- | Returns all the nodes with incoming edges.  Somewhat expensive. @O(e)@.

targetNodes :: CallGraph cinfo -> Set Node
targetNodes :: forall cinfo. CallGraph cinfo -> Set Node
targetNodes = Graph Node (CMSet cinfo) -> Set Node
forall n e. Ord n => Graph n e -> Set n
Graph.targetNodes (Graph Node (CMSet cinfo) -> Set Node)
-> (CallGraph cinfo -> Graph Node (CMSet cinfo))
-> CallGraph cinfo
-> Set Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> Graph Node (CMSet cinfo)
forall cinfo. CallGraph cinfo -> Graph Node (CMSet cinfo)
theCallGraph

-- | Converts a call graph to a list of calls with associated meta
--   information.

toList :: CallGraph cinfo -> [Call cinfo]
toList :: forall cinfo. CallGraph cinfo -> [Call cinfo]
toList = Graph Node (CMSet cinfo) -> [Edge Node (CMSet cinfo)]
forall n e. Graph n e -> [Edge n e]
Graph.edges (Graph Node (CMSet cinfo) -> [Edge Node (CMSet cinfo)])
-> (CallGraph cinfo -> Graph Node (CMSet cinfo))
-> CallGraph cinfo
-> [Edge Node (CMSet cinfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> Graph Node (CMSet cinfo)
forall cinfo. CallGraph cinfo -> Graph Node (CMSet cinfo)
theCallGraph

-- | Converts a list of calls with associated meta information to a
--   call graph.

fromListCG :: [Call cinfo] -> CallGraph cinfo
fromListCG :: forall cinfo. [Call cinfo] -> CallGraph cinfo
fromListCG = Graph Node (CMSet cinfo) -> CallGraph cinfo
forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph (Graph Node (CMSet cinfo) -> CallGraph cinfo)
-> ([Call cinfo] -> Graph Node (CMSet cinfo))
-> [Call cinfo]
-> CallGraph cinfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CMSet cinfo -> CMSet cinfo -> CMSet cinfo)
-> [Call cinfo] -> Graph Node (CMSet cinfo)
forall n e. Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
Graph.fromEdgesWith CMSet cinfo -> CMSet cinfo -> CMSet cinfo
forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
CMSet.union

-- | 'null' checks whether the call graph is completely disconnected.
instance Null (CallGraph cinfo) where
  empty :: CallGraph cinfo
empty = Graph Node (CMSet cinfo) -> CallGraph cinfo
forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph Graph Node (CMSet cinfo)
forall n e. Graph n e
Graph.empty
  null :: CallGraph cinfo -> Bool
null  = (Edge Node (CMSet cinfo) -> Bool)
-> [Edge Node (CMSet cinfo)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.all (CMSet cinfo -> Bool
forall a. Null a => a -> Bool
null (CMSet cinfo -> Bool)
-> (Edge Node (CMSet cinfo) -> CMSet cinfo)
-> Edge Node (CMSet cinfo)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge Node (CMSet cinfo) -> CMSet cinfo
forall n e. Edge n e -> e
label) ([Edge Node (CMSet cinfo)] -> Bool)
-> (CallGraph cinfo -> [Edge Node (CMSet cinfo)])
-> CallGraph cinfo
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> [Edge Node (CMSet cinfo)]
forall cinfo. CallGraph cinfo -> [Call cinfo]
toList

-- | Takes the union of two call graphs.

union :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
union :: forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
union (CallGraph Graph Node (CMSet cinfo)
cs1) (CallGraph Graph Node (CMSet cinfo)
cs2) = Graph Node (CMSet cinfo) -> CallGraph cinfo
forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph (Graph Node (CMSet cinfo) -> CallGraph cinfo)
-> Graph Node (CMSet cinfo) -> CallGraph cinfo
forall a b. (a -> b) -> a -> b
$
  (CMSet cinfo -> CMSet cinfo -> CMSet cinfo)
-> Graph Node (CMSet cinfo)
-> Graph Node (CMSet cinfo)
-> Graph Node (CMSet cinfo)
forall n e.
Ord n =>
(e -> e -> e) -> Graph n e -> Graph n e -> Graph n e
Graph.unionWith CMSet cinfo -> CMSet cinfo -> CMSet cinfo
forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
CMSet.union Graph Node (CMSet cinfo)
cs1 Graph Node (CMSet cinfo)
cs2

-- | 'CallGraph' is a monoid under 'union'.

instance Semigroup (CallGraph cinfo) where
  <> :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
(<>) = CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
union

instance Monoid (CallGraph cinfo) where
  mempty :: CallGraph cinfo
mempty  = CallGraph cinfo
forall a. Null a => a
empty
  mappend :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
mappend = CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
forall a. Semigroup a => a -> a -> a
(<>)

instance Singleton (Call cinfo) (CallGraph cinfo) where
  singleton :: Call cinfo -> CallGraph cinfo
singleton = [Call cinfo] -> CallGraph cinfo
forall el coll. Collection el coll => [el] -> coll
fromList ([Call cinfo] -> CallGraph cinfo)
-> (Call cinfo -> [Call cinfo]) -> Call cinfo -> CallGraph cinfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Call cinfo -> [Call cinfo]
forall el coll. Singleton el coll => el -> coll
singleton

instance Collection (Call cinfo) (CallGraph cinfo) where
  fromList :: [Call cinfo] -> CallGraph cinfo
fromList = [Call cinfo] -> CallGraph cinfo
forall cinfo. [Call cinfo] -> CallGraph cinfo
fromListCG

-- | Inserts a call into a call graph.

insert :: Node -> Node -> CallMatrix -> cinfo
       -> CallGraph cinfo -> CallGraph cinfo
insert :: forall cinfo.
Node
-> Node
-> CallMatrix
-> cinfo
-> CallGraph cinfo
-> CallGraph cinfo
insert Node
s Node
t CallMatrix
cm cinfo
cinfo = Graph Node (CMSet cinfo) -> CallGraph cinfo
forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph (Graph Node (CMSet cinfo) -> CallGraph cinfo)
-> (CallGraph cinfo -> Graph Node (CMSet cinfo))
-> CallGraph cinfo
-> CallGraph cinfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CMSet cinfo -> CMSet cinfo -> CMSet cinfo)
-> Edge Node (CMSet cinfo)
-> Graph Node (CMSet cinfo)
-> Graph Node (CMSet cinfo)
forall n e.
Ord n =>
(e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
Graph.insertEdgeWith CMSet cinfo -> CMSet cinfo -> CMSet cinfo
forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
CMSet.union Edge Node (CMSet cinfo)
e (Graph Node (CMSet cinfo) -> Graph Node (CMSet cinfo))
-> (CallGraph cinfo -> Graph Node (CMSet cinfo))
-> CallGraph cinfo
-> Graph Node (CMSet cinfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> Graph Node (CMSet cinfo)
forall cinfo. CallGraph cinfo -> Graph Node (CMSet cinfo)
theCallGraph
  where e :: Edge Node (CMSet cinfo)
e = Node -> Node -> CallMatrix -> cinfo -> Edge Node (CMSet cinfo)
forall cinfo. Node -> Node -> CallMatrix -> cinfo -> Call cinfo
mkCall Node
s Node
t CallMatrix
cm cinfo
cinfo


-- * Combination of a new thing with an old thing
--   returning a really new things and updated old things.

type CombineNewOldT a = a -> a -> (a, a)

class CombineNewOld a where
  combineNewOld :: CombineNewOldT a

instance PartialOrd a => CombineNewOld (Favorites a) where
  combineNewOld :: CombineNewOldT (Favorites a)
combineNewOld Favorites a
new Favorites a
old = (Favorites a
new', (Favorites a, Favorites a) -> Favorites a
forall a. (Favorites a, Favorites a) -> Favorites a
Fav.unionCompared (Favorites a
new', Favorites a
old'))
    where (Favorites a
new', Favorites a
old') = CombineNewOldT (Favorites a)
forall a. PartialOrd a => CombineNewOldT (Favorites a)
Fav.compareFavorites Favorites a
new Favorites a
old

deriving instance CombineNewOld (CMSet cinfo)

instance (Monoid a, CombineNewOld a, Ord n) => CombineNewOld (Graph n a) where
  combineNewOld :: CombineNewOldT (Graph n a)
combineNewOld Graph n a
new Graph n a
old = Graph n (a, a) -> (Graph n a, Graph n a)
forall n e e'. Graph n (e, e') -> (Graph n e, Graph n e')
Graph.unzip (Graph n (a, a) -> (Graph n a, Graph n a))
-> Graph n (a, a) -> (Graph n a, Graph n a)
forall a b. (a -> b) -> a -> b
$ ((a, a) -> (a, a) -> (a, a))
-> Graph n (a, a) -> Graph n (a, a) -> Graph n (a, a)
forall n e.
Ord n =>
(e -> e -> e) -> Graph n e -> Graph n e -> Graph n e
Graph.unionWith (a, a) -> (a, a) -> (a, a)
forall {c} {b}.
(Monoid c, CombineNewOld c) =>
(c, b) -> (c, c) -> (c, c)
comb Graph n (a, a)
new' Graph n (a, a)
old'
    where
      new' :: Graph n (a, a)
new' = (,a
forall a. Monoid a => a
mempty) (a -> (a, a)) -> Graph n a -> Graph n (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n a
new
      old' :: Graph n (a, a)
old' = (a
forall a. Monoid a => a
mempty,) (a -> (a, a)) -> Graph n a -> Graph n (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n a
old
      comb :: (c, b) -> (c, c) -> (c, c)
comb (c
new1,b
old1) (c
new2,c
old2)  -- TODO: ensure old1 is null
        = (c -> c) -> (c, c) -> (c, c)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (c
new2 c -> c -> c
forall a. Monoid a => a -> a -> a
`mappend`) ((c, c) -> (c, c)) -> (c, c) -> (c, c)
forall a b. (a -> b) -> a -> b
$ CombineNewOldT c
forall a. CombineNewOld a => CombineNewOldT a
combineNewOld c
new1 c
old2
        -- -- | old1 == mempty = first (new2 `mappend`) $ combineNewOld new1 old2
        -- -- | otherwise      = __IMPOSSIBLE__

      -- Filter unlabelled edges from the resulting new graph.
      -- filt = Graph.filterEdges (not . null)

-- | Call graph combination.
--
--   Application of '>*<' to all pairs @(c1,c2)@
--   for which @'source' c1 = 'target' c2@.)

-- GHC supports implicit-parameter constraints in instance declarations
-- only from 7.4.  To maintain compatibility with 7.2, we skip this instance:
-- Andreas, 2025-10-29, not allowed in GHC 9.12:
-- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/implicit_parameters.html#implicit-parameter-type-constraints
-- KEEP:
-- instance (Monoid cinfo, ?cutoff :: CutOff) => CombineNewOld (CallGraph cinfo) where
--   combineNewOld (CallGraph new) (CallGraph old) = CallGraph *** CallGraph $ combineNewOld comb old
--     -- combined calls:
--     where comb = Graph.composeWith (>*<) CMSet.union new old

-- Non-overloaded version:
combineNewOldCallGraph :: forall cinfo. (Monoid cinfo, ?cutoff :: CutOff) => CombineNewOldT (CallGraph cinfo)
combineNewOldCallGraph :: forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CombineNewOldT (CallGraph cinfo)
combineNewOldCallGraph (CallGraph Graph Node (CMSet cinfo)
new) (CallGraph Graph Node (CMSet cinfo)
old) = Graph Node (CMSet cinfo) -> CallGraph cinfo
forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph (Graph Node (CMSet cinfo) -> CallGraph cinfo)
-> (Graph Node (CMSet cinfo) -> CallGraph cinfo)
-> (Graph Node (CMSet cinfo), Graph Node (CMSet cinfo))
-> (CallGraph cinfo, CallGraph cinfo)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Graph Node (CMSet cinfo) -> CallGraph cinfo
forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph ((Graph Node (CMSet cinfo), Graph Node (CMSet cinfo))
 -> (CallGraph cinfo, CallGraph cinfo))
-> (Graph Node (CMSet cinfo), Graph Node (CMSet cinfo))
-> (CallGraph cinfo, CallGraph cinfo)
forall a b. (a -> b) -> a -> b
$ CombineNewOldT (Graph Node (CMSet cinfo))
forall a. CombineNewOld a => CombineNewOldT a
combineNewOld Graph Node (CMSet cinfo)
comb Graph Node (CMSet cinfo)
old
    -- combined calls:
    where
      comb :: Graph Node (CMSet cinfo)
      comb :: Graph Node (CMSet cinfo)
comb = -- strengthenLoopDiagonals' $ -- bad heuristics, see https://github.com/agda/agda/pull/8184#issuecomment-3487147737
        (CMSet cinfo -> CMSet cinfo -> CMSet cinfo)
-> (CMSet cinfo -> CMSet cinfo -> CMSet cinfo)
-> Graph Node (CMSet cinfo)
-> Graph Node (CMSet cinfo)
-> Graph Node (CMSet cinfo)
forall c d e n.
Ord n =>
(c -> d -> e)
-> (e -> e -> e) -> Graph n c -> Graph n d -> Graph n e
Graph.composeWith CMSet cinfo -> CMSet cinfo -> CMSet cinfo
forall a. (CallComb a, ?cutoff::CutOff) => a -> a -> a
(>*<) CMSet cinfo -> CMSet cinfo -> CMSet cinfo
forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
CMSet.union Graph Node (CMSet cinfo)
new Graph Node (CMSet cinfo)
old

-- Andreas, 2025-11-04
-- bad heuristics, see https://github.com/agda/agda/pull/8184#issuecomment-3487147737
-- -- | Any increase in the diagonal of a loop can be strengthened to infinite increase
-- --   since we can iterate loops indefinitely.
-- strengthenLoopDiagonals' :: Graph Node (CMSet cinfo) -> Graph Node (CMSet cinfo)
-- strengthenLoopDiagonals' =
--   Graph.mapLoops $ mapCMSet $ fmap $ mapCallMatrixAug $ mapCallMatrix $
--     mapDiagonalNonZeros makeIncreaseInfinite

-- -- | Any increase in the diagonal of a loop can be strengthened to infinite increase
-- --   since we can iterate loops indefinitely.
-- strengthenLoopDiagonals :: CallGraph cinfo -> CallGraph cinfo
-- strengthenLoopDiagonals = mapCallGraph $ strengthenLoopDiagonals'

-- | Call graph comparison.
--   A graph @cs'@ is ``worse'' than @cs@ if it has a new edge (call)
--   or a call got worse, which means that one of its elements
--   that was better or equal to 'Le' moved a step towards 'Un'.
--
--   A call graph is complete if combining it with itself does not make it
--   any worse.  This is sound because of monotonicity:  By combining a graph
--   with itself, it can only get worse, but if it does not get worse after
--   one such step, it gets never any worse.

-- | @'complete' cs@ completes the call graph @cs@. A call graph is
-- complete if it contains all indirect calls; if @f -> g@ and @g ->
-- h@ are present in the graph, then @f -> h@ should also be present.

complete :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> CallGraph cinfo
complete :: forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CallGraph cinfo -> CallGraph cinfo
complete CallGraph cinfo
cs = (CallGraph cinfo -> (Bool, CallGraph cinfo))
-> CallGraph cinfo -> CallGraph cinfo
forall a. (a -> (Bool, a)) -> a -> a
repeatWhile ((CallGraph cinfo -> Bool)
-> (CallGraph cinfo, CallGraph cinfo) -> (Bool, CallGraph cinfo)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Bool -> Bool
not (Bool -> Bool)
-> (CallGraph cinfo -> Bool) -> CallGraph cinfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> Bool
forall a. Null a => a -> Bool
null) ((CallGraph cinfo, CallGraph cinfo) -> (Bool, CallGraph cinfo))
-> (CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo))
-> CallGraph cinfo
-> (Bool, CallGraph cinfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo
-> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CombineNewOldT (CallGraph cinfo)
completionStep CallGraph cinfo
cs) CallGraph cinfo
cs

completionStep :: (Monoid cinfo, ?cutoff :: CutOff)
  => CallGraph cinfo
       -- ^ The original call graph.
  -> CallGraph cinfo
       -- ^ The current completion.
  -> (CallGraph cinfo, CallGraph cinfo)
completionStep :: forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CombineNewOldT (CallGraph cinfo)
completionStep CallGraph cinfo
gOrig CallGraph cinfo
gThis = CombineNewOldT (CallGraph cinfo)
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CombineNewOldT (CallGraph cinfo)
combineNewOldCallGraph CallGraph cinfo
gOrig CallGraph cinfo
gThis

------------------------------------------------------------------------
-- * Printing
------------------------------------------------------------------------

-- | Displays the recursion behaviour corresponding to a call graph.

instance Pretty cinfo => Pretty (CallGraph cinfo) where
  pretty :: CallGraph cinfo -> Doc
pretty = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc)
-> (CallGraph cinfo -> [Doc]) -> CallGraph cinfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Call cinfo -> Doc) -> [Call cinfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Call cinfo -> Doc
forall {cinfo}. Pretty cinfo => Call cinfo -> Doc
prettyCall ([Call cinfo] -> [Doc])
-> (CallGraph cinfo -> [Call cinfo]) -> CallGraph cinfo -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> [Call cinfo]
forall cinfo. CallGraph cinfo -> [Call cinfo]
toList
    where
    prettyCall :: Call cinfo -> Doc
prettyCall Call cinfo
e = if CMSet cinfo -> Bool
forall a. Null a => a -> Bool
null (Call cinfo -> CMSet cinfo
forall cinfo. Call cinfo -> CMSet cinfo
callMatrixSet Call cinfo
e) then Doc
forall a. Null a => a
empty else Node -> [(String, Doc)] -> Doc
align Node
20 ([(String, Doc)] -> Doc) -> [(String, Doc)] -> Doc
forall a b. (a -> b) -> a -> b
$
      [ (String
"Source:",    String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Node -> String
forall a. Show a => a -> String
show (Node -> String) -> Node -> String
forall a b. (a -> b) -> a -> b
$ Call cinfo -> Node
forall n e. Edge n e -> n
source Call cinfo
e)
      , (String
"Target:",    String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Node -> String
forall a. Show a => a -> String
show (Node -> String) -> Node -> String
forall a b. (a -> b) -> a -> b
$ Call cinfo -> Node
forall n e. Edge n e -> n
target Call cinfo
e)
      , (String
"Matrix:",    CMSet cinfo -> Doc
forall a. Pretty a => a -> Doc
pretty (CMSet cinfo -> Doc) -> CMSet cinfo -> Doc
forall a b. (a -> b) -> a -> b
$ Call cinfo -> CMSet cinfo
forall cinfo. Call cinfo -> CMSet cinfo
callMatrixSet Call cinfo
e)
      ]

-- -- | Displays the recursion behaviour corresponding to a call graph.

-- prettyBehaviour :: Show cinfo => CallGraph cinfo -> Doc
-- prettyBehaviour = vcat . map prettyCall . filter toSelf . toList
--   where
--   toSelf c = source c == target c

--   prettyCall e = vcat $ map text
--     [ "Function:  " ++ show (source e)
-- --    , "Behaviour: " ++ show (diagonal $ mat $ cm c)  -- TODO
-- --    , "Meta info: " ++ show cinfo
--     ]