Agda-2.5.4.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

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

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, ?cutoff :: CutOff) => 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

Instances
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 #

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 #

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 #

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 #

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 #

targetNodes :: CallGraph cinfo -> Set Node Source #

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

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

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

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 #