summaryrefslogtreecommitdiff
path: root/src/full/Agda/Termination/CallGraph.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Termination/CallGraph.hs')
-rw-r--r--src/full/Agda/Termination/CallGraph.hs39
1 files changed, 16 insertions, 23 deletions
diff --git a/src/full/Agda/Termination/CallGraph.hs b/src/full/Agda/Termination/CallGraph.hs
index 635ea95..4bd5c65 100644
--- a/src/full/Agda/Termination/CallGraph.hs
+++ b/src/full/Agda/Termination/CallGraph.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
-- | Call graphs and related concepts, more or less as defined in
-- \"A Predicative Analysis of Structural Recursion\" by
@@ -23,8 +22,6 @@ module Agda.Termination.CallGraph
, targetNodes
, fromList
, toList
- , empty
- , null
, union
, insert
, complete, completionStep
@@ -65,10 +62,11 @@ import Agda.Utils.List hiding (tests)
import Agda.Utils.Map
import Agda.Utils.Maybe
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.PartialOrd
-import Agda.Utils.Pretty hiding (empty)
-import qualified Agda.Utils.Pretty as P
+import Agda.Utils.Pretty
import Agda.Utils.QuickCheck hiding (label)
+import Agda.Utils.Singleton
import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
@@ -96,7 +94,7 @@ callMatrixSet = label
-- | Make a call with a single matrix.
mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo
-mkCall s t m cinfo = Edge s t $ CMSet.singleton $ CallMatrixAug m cinfo
+mkCall s t m cinfo = Edge s t $ singleton $ CallMatrixAug m cinfo
-- | Make a call with empty @cinfo@.
mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo
@@ -145,15 +143,10 @@ toList = Graph.edges . theCallGraph
fromList :: Monoid cinfo => [Call cinfo] -> CallGraph cinfo
fromList = CallGraph . Graph.fromListWith CMSet.union
--- | Creates an empty call graph.
-
-empty :: CallGraph cinfo
-empty = CallGraph Graph.empty
-
--- | Check whether the call graph is completely disconnected.
-
-null :: CallGraph cinfo -> Bool
-null = List.all (CMSet.null . label) . toList
+-- | 'null' checks whether the call graph is completely disconnected.
+instance Null (CallGraph cinfo) where
+ empty = CallGraph Graph.empty
+ null = List.all (null . label) . toList
-- | Takes the union of two call graphs.
@@ -202,7 +195,7 @@ instance (Monoid a, CombineNewOld a, Ord s, Ord t) => CombineNewOld (Graph s t a
-- -- | otherwise = __IMPOSSIBLE__
-- Filter unlabelled edges from the resulting new graph.
- -- filt = Graph.filterEdges (not . CMSet.null)
+ -- filt = Graph.filterEdges (not . null)
-- | Call graph combination.
--
@@ -263,7 +256,7 @@ completionStep gOrig gThis = combineNewOldCallGraph gOrig gThis
instance Pretty cinfo => Pretty (CallGraph cinfo) where
pretty = vcat . map prettyCall . toList
where
- prettyCall e = if CMSet.null (callMatrixSet e) then P.empty else align 20 $
+ prettyCall e = if null (callMatrixSet e) then empty else align 20 $
[ ("Source:", text $ show $ source e)
, ("Target:", text $ show $ target e)
, ("Matrix:", pretty $ callMatrixSet e)