Safe Haskell	None
Language	Haskell2010

Agda.Termination.CallGraph

Contents

Calls
Call graphs

Description

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

Synopsis

type Node = Int
type Call cinfo = Edge Node (CMSet cinfo)
mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo
mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo
source :: Edge n e -> n
target :: Edge n e -> n
callMatrixSet :: Call cinfo -> CMSet cinfo
(>*<) :: CallComb a => a -> a -> a
newtype CallGraph cinfo = CallGraph {
- theCallGraph :: Graph Node (CMSet cinfo)
}
targetNodes :: CallGraph cinfo -> Set Node
fromList :: Collection el coll => [el] -> coll
toList :: CallGraph cinfo -> [Call cinfo]
union :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
insert :: Node -> Node -> CallMatrix -> cinfo -> CallGraph cinfo -> CallGraph cinfo
complete :: (?cutoff :: CutOff, Monoid cinfo) => CallGraph cinfo -> CallGraph cinfo
completionStep :: (?cutoff :: CutOff, Monoid cinfo) => CallGraph cinfo -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)

Calls

type Node = Int Source #

Call graph nodes.

Machine integer Int is sufficient, since we cannot index more than we have addresses on our machine.

type Call cinfo = Edge Node (CMSet cinfo) Source #

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.

mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo Source #

Make a call with a single matrix.

mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo Source #

Make a call with empty cinfo.

source :: Edge n e -> n Source #

Outgoing node.

target :: Edge n e -> n Source #

Incoming node.

callMatrixSet :: Call cinfo -> CMSet cinfo Source #

(>*<) :: CallComb a => a -> a -> a Source #

Call graphs

newtype CallGraph cinfo Source #

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

Constructors

CallGraph
Fields theCallGraph :: Graph Node (CMSet cinfo)

Instances

Instances details

Pretty cinfo => Pretty (CallGraph cinfo) Source #	Displays the recursion behaviour corresponding to a call graph.
Instance details Defined in Agda.Termination.CallGraph Methods pretty :: CallGraph cinfo -> Doc Source # prettyPrec :: Int -> CallGraph cinfo -> Doc Source # prettyList :: [CallGraph cinfo] -> Doc Source #
Null (CallGraph cinfo) Source #	`null` checks whether the call graph is completely disconnected.
Instance details Defined in Agda.Termination.CallGraph Methods empty :: CallGraph cinfo Source # null :: CallGraph cinfo -> Bool Source #
Monoid (CallGraph cinfo) Source #
Instance details Defined in Agda.Termination.CallGraph Methods mempty :: CallGraph cinfo mappend :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo mconcat :: [CallGraph cinfo] -> CallGraph cinfo
Semigroup (CallGraph cinfo) Source #	`CallGraph` is a monoid under `union`.
Instance details Defined in Agda.Termination.CallGraph Methods (<>) :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo # sconcat :: NonEmpty (CallGraph cinfo) -> CallGraph cinfo stimes :: Integral b => b -> CallGraph cinfo -> CallGraph cinfo
Show cinfo => Show (CallGraph cinfo) Source #
Instance details Defined in Agda.Termination.CallGraph Methods showsPrec :: Int -> CallGraph cinfo -> ShowS show :: CallGraph cinfo -> String showList :: [CallGraph cinfo] -> ShowS
Collection (Call cinfo) (CallGraph cinfo) Source #
Instance details Defined in Agda.Termination.CallGraph Methods fromList :: [Call cinfo] -> CallGraph cinfo Source #
Singleton (Call cinfo) (CallGraph cinfo) Source #
Instance details Defined in Agda.Termination.CallGraph Methods singleton :: Call cinfo -> CallGraph cinfo Source #

targetNodes :: CallGraph cinfo -> Set Node Source #

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

fromList :: Collection el coll => [el] -> coll Source #

toList :: CallGraph cinfo -> [Call cinfo] Source #

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

union :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo Source #

Takes the union of two call graphs.

insert :: Node -> Node -> CallMatrix -> cinfo -> CallGraph cinfo -> CallGraph cinfo Source #

Inserts a call into a call graph.

complete :: (?cutoff :: CutOff, Monoid cinfo) => CallGraph cinfo -> CallGraph cinfo Source #

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.

completionStep :: (?cutoff :: CutOff, Monoid cinfo) => CallGraph cinfo -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo) Source #