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

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 `Monoid`al 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 Source # mappend :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo Source # mconcat :: [CallGraph cinfo] -> CallGraph cinfo Source #
Semigroup (CallGraph cinfo) Source # | `CallGraph` is a monoid under `union`.
Instance details Defined in Agda.Termination.CallGraph Methods (<>) :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo Source # sconcat :: NonEmpty (CallGraph cinfo) -> CallGraph cinfo Source # stimes :: Integral b => b -> CallGraph cinfo -> CallGraph cinfo Source #
Show cinfo => Show (CallGraph cinfo) Source # |
Instance details Defined in Agda.Termination.CallGraph Methods showsPrec :: Int -> CallGraph cinfo -> ShowS Source # show :: CallGraph cinfo -> String Source # showList :: [CallGraph cinfo] -> ShowS Source #
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 #