{-# 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, 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
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.Syntax.Common.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 = 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 = forall n e. n -> n -> e -> Edge n e
Edge Node
s Node
t forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ 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 = forall cinfo. Node -> Node -> CallMatrix -> cinfo -> Call cinfo
mkCall Node
s Node
t CallMatrix
m 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
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 = forall n e. Ord n => Graph n e -> Set n
Graph.targetNodes forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall n e. Graph n e -> [Edge n e]
Graph.edges forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
Graph.fromEdgesWith 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 = forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph forall n e. Graph n e
Graph.empty
  null :: CallGraph cinfo -> Bool
null  = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.all (forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Edge n e -> e
label) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph forall a b. (a -> b) -> a -> b
$
  forall n e.
Ord n =>
(e -> e -> e) -> Graph n e -> Graph n e -> Graph n e
Graph.unionWith 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
(<>) = forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
union

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

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

instance Collection (Call cinfo) (CallGraph cinfo) where
  fromList :: [Call cinfo] -> CallGraph cinfo
fromList = 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 = forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e.
Ord n =>
(e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
Graph.insertEdgeWith forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
CMSet.union Call cinfo
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall cinfo. CallGraph cinfo -> Graph Node (CMSet cinfo)
theCallGraph
  where e :: Call cinfo
e = 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', forall a. (Favorites a, Favorites a) -> Favorites a
Fav.unionCompared (Favorites a
new', Favorites a
old'))
    where (Favorites a
new', Favorites a
old') = 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 = forall n e e'. Graph n (e, e') -> (Graph n e, Graph n e')
Graph.unzip forall a b. (a -> b) -> a -> b
$ forall n e.
Ord n =>
(e -> e -> e) -> Graph n e -> Graph n e -> Graph n e
Graph.unionWith 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' = (,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n a
new
      old' :: Graph n (a, a)
old' = (forall a. Monoid a => a
mempty,) 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
        = forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (b
new2 forall a. Monoid a => a -> a -> a
`mappend`) forall a b. (a -> b) -> a -> 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) = forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- forall cinfo. Graph Node (CMSet cinfo) -> CallGraph cinfo
CallGraph forall a b. (a -> b) -> a -> b
$ 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 = forall n c d e.
Ord n =>
(c -> d -> e)
-> (e -> e -> e) -> Graph n c -> Graph n d -> Graph n e
Graph.composeWith forall a. (CallComb a, ?cutoff::CutOff) => a -> a -> a
(>*<) 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 = forall a. (a -> (Bool, a)) -> a -> a
repeatWhile (forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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 = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {cinfo}. Pretty cinfo => Call cinfo -> Doc
prettyCall forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall cinfo. CallGraph cinfo -> [Call cinfo]
toList
    where
    prettyCall :: Call cinfo -> Doc
prettyCall Call cinfo
e = if forall a. Null a => a -> Bool
null (forall cinfo. Call cinfo -> CMSet cinfo
callMatrixSet Call cinfo
e) then forall a. Null a => a
empty else Node -> [(String, Doc)] -> Doc
align Node
20 forall a b. (a -> b) -> a -> b
$
      [ (String
"Source:",    forall a. String -> Doc a
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall n e. Edge n e -> n
source Call cinfo
e)
      , (String
"Target:",    forall a. String -> Doc a
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall n e. Edge n e -> n
target Call cinfo
e)
      , (String
"Matrix:",    forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ 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
--     ]