    {-# LANGUAGE CPP                        #-}
    {-# 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, mkCall, mkCall', source, target, callMatrixSet
      , (>*<)
        -- * Call graphs
      , CallGraph(..)
      , targetNodes
      , fromList
      , toList
      , union
      , insert
      , complete, completionStep
      -- , prettyBehaviour
      ) where

    import Prelude hiding (null)

    import qualified Data.List as List
    #if __GLASGOW_HASKELL__ < 804
    import Data.Semigroup
    #endif
    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.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.Null
    import Agda.Utils.PartialOrd
    import Agda.Utils.Pretty
    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

    -- | 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
    showList :: [CallGraph cinfo] -> ShowS
    $cshowList :: forall cinfo. Show cinfo => [CallGraph cinfo] -> ShowS
    show :: CallGraph cinfo -> String
    $cshow :: forall cinfo. Show cinfo => CallGraph cinfo -> String
    showsPrec :: Node -> CallGraph cinfo -> ShowS
    $cshowsPrec :: forall cinfo. Show cinfo => Node -> CallGraph cinfo -> ShowS
    Show)

    -- | 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)
    -> ([Edge Node (CMSet cinfo)] -> Graph Node (CMSet cinfo))
    -> [Edge Node (CMSet 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)
    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 {b} {b}.
    (Monoid b, CombineNewOld b) =>
    (b, b) -> (b, b) -> (b, b)
    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 :: (b, b) -> (b, b) -> (b, b)
    comb (b
    new1,b
    old1) (b
    new2,b
    old2)  -- TODO: ensure old1 is null
            = (b -> b) -> (b, b) -> (b, b)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (b
    new2 b -> b -> b
    forall a. Monoid a => a -> a -> a
    `mappend`) ((b, b) -> (b, b)) -> (b, b) -> (b, b)
    forall a b. (a -> b) -> a -> b
    $ CombineNewOldT b
    forall a. CombineNewOld a => CombineNewOldT a
    combineNewOld b
    new1 b
    old2
            -- -- | old1 == mempty = mapFst (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:
    -- 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 :: (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 a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
    -*- 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 = (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 n c d e.
    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

    -- | 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 :: (?cutoff :: CutOff) => Monoid cinfo => CallGraph cinfo -> CallGraph cinfo
    complete :: forall cinfo.
    (?cutoff::CutOff, Monoid cinfo) =>
    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 c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (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.
    (?cutoff::CutOff, Monoid cinfo) =>
    CallGraph cinfo
    -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
    completionStep CallGraph cinfo
    cs) CallGraph cinfo
    cs

    completionStep :: (?cutoff :: CutOff) => Monoid cinfo =>
      CallGraph cinfo -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
    completionStep :: forall cinfo.
    (?cutoff::CutOff, Monoid cinfo) =>
    CallGraph cinfo
    -> CallGraph cinfo -> (CallGraph cinfo, 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
    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
    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
    --     ]