| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Termination.CallGraph
Contents
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, ?cutoff :: CutOff) => 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
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.
callMatrixSet :: Call cinfo -> CMSet cinfo 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
| |
Instances
| Null (CallGraph cinfo) Source # |
|
| Pretty cinfo => Pretty (CallGraph cinfo) Source # | Displays the recursion behaviour corresponding to a call graph. |
| Monoid (CallGraph cinfo) Source # | |
| Semigroup (CallGraph cinfo) Source # | |
| Show cinfo => Show (CallGraph cinfo) Source # | |
| Collection (Call cinfo) (CallGraph cinfo) Source # | |
| 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 cscs. 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.