Agda.Termination.CallGraph

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

Calls

type Node = Int

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)

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

Make a call with a single matrix.

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

Make a call with empty cinfo.

source :: Edge n e -> n

Outgoing node.

target :: Edge n e -> n

Incoming node.

callMatrixSet :: Call cinfo -> CMSet cinfo

(>*<) :: (CallComb a, ?cutoff :: CutOff) => a -> a -> a

Call graphs

newtype CallGraph cinfo

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

Pretty cinfo => Pretty (CallGraph cinfo)

Displays the recursion behaviour corresponding to a call graph.

Defined in Agda.Termination.CallGraph

Methods

pretty :: CallGraph cinfo -> Doc

prettyPrec :: Int -> CallGraph cinfo -> Doc

prettyList :: [CallGraph cinfo] -> Doc

Null (CallGraph cinfo)

null checks whether the call graph is completely disconnected.

Defined in Agda.Termination.CallGraph

Methods

empty :: CallGraph cinfo

null :: CallGraph cinfo -> Bool

Monoid (CallGraph cinfo)

Defined in Agda.Termination.CallGraph

Methods

mempty :: CallGraph cinfo

mappend :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo

mconcat :: [CallGraph cinfo] -> CallGraph cinfo

Semigroup (CallGraph cinfo)

CallGraph is a monoid under union.

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)

Defined in Agda.Termination.CallGraph

Methods

showsPrec :: Int -> CallGraph cinfo -> ShowS

show :: CallGraph cinfo -> String

showList :: [CallGraph cinfo] -> ShowS

Collection (Call cinfo) (CallGraph cinfo)

Defined in Agda.Termination.CallGraph

Methods

fromList :: [Call cinfo] -> CallGraph cinfo

Singleton (Call cinfo) (CallGraph cinfo)

Defined in Agda.Termination.CallGraph

Methods

singleton :: Call cinfo -> CallGraph cinfo

targetNodes :: CallGraph cinfo -> Set Node

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

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

toList :: CallGraph cinfo -> [Call cinfo]

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

union :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo

Takes the union of two call graphs.

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

Inserts a call into a call graph.

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

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)