{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE ImplicitParams #-}
module Agda.Termination.CallGraph
(
Node
, Call, mkCall, mkCall', source, target, callMatrixSet
, (>*<)
, CallGraph(..)
, targetNodes
, fromList
, toList
, union
, insert
, complete, completionStep
) 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
type Node = Int
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
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' :: 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
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)
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
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
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
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
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
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
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
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)
= (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
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
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
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
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)
]