| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Termination.CallGraph

Contents

Structural orderings
Call matrices
Calls
Call graphs
Tests

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

data Order

= Lt
| Le
| Unknown
| Mat (Matrix Integer Order)

(.*.) :: Order -> Order -> Order
supremum :: [Order] -> Order
type Index = Integer

newtype CallMatrix = CallMatrix {

mat :: Matrix Index Order

}

(>*<) :: Call -> Call -> Call
callMatrixInvariant :: CallMatrix -> Bool

data Call = Call {

source :: Index
target :: Index
cm :: CallMatrix

}

callInvariant :: Call -> Bool
data CallGraph meta
callGraphInvariant :: CallGraph meta -> Bool
fromList :: Monoid meta => [(Call, meta)] -> CallGraph meta
toList :: CallGraph meta -> [(Call, meta)]
empty :: CallGraph meta
union :: Monoid meta => CallGraph meta -> CallGraph meta -> CallGraph meta
insert :: Monoid meta => Call -> meta -> CallGraph meta -> CallGraph meta
complete :: Monoid meta => CallGraph meta -> CallGraph meta
showBehaviour :: Show meta => CallGraph meta -> String
tests :: IO Bool

Structural orderings

data Order | Source

The order called R in the paper referred to above. Note that ``Unknown` `<=` `Le` `<=` `Lt``. See `Call` for more information. TODO: document orders which are call-matrices themselves.
Constructors

Lt |
Le |
Unknown |
Mat (Matrix Integer Order) |

Instances

Eq Order
Ord Order
Show Order
Arbitrary Order
CoArbitrary Order

(.*.) :: Order -> Order -> Order | Source

Multiplication of `Order`s. (Corresponds to sequential composition.)

supremum :: [Order] -> Order | Source

The supremum of a (possibly empty) list of `Order`s.
Call matrices

type Index = Integer | Source

Call matrix indices.

newtype CallMatrix | Source

Call matrices. Note the call matrix invariant (`callMatrixInvariant`).
Constructors

CallMatrix |

mat :: Matrix Index Order |

Instances

Eq CallMatrix
Ord CallMatrix
Show CallMatrix
Arbitrary CallMatrix
CoArbitrary CallMatrix

(>*<) :: Call -> Call -> Call | Source

`Call` combination. Precondition: see `<*>`; furthermore the `source` of the first argument should be equal to the `target` of the second one.

callMatrixInvariant :: CallMatrix -> Bool | Source

In a call matrix at most one element per row may be different from `Unknown`.
Calls

data Call | Source

This datatype encodes information about a single recursive function application. The columns of the call matrix stand for `source` function arguments (patterns); the first argument has index 0, the second 1, and so on. The rows of the matrix stand for `target` function arguments. Element `(i, j)` in the matrix should be computed as follows:

- `Lt` (less than) if the `j`-th argument to the `target` function is structurally strictly smaller than the `i`-th pattern.
- `Le` (less than or equal) if the `j`-th argument to the `target` function is structurally smaller than the `i`-th pattern.
- `Unknown` otherwise.

The structural ordering used is defined in the paper referred to above.

Constructors

Call |

source :: Index | The function making the call.
target :: Index | The function being called.
cm :: CallMatrix | The call matrix describing the call.

Instances

Eq Call
Ord Call
Show Call
Arbitrary Call
CoArbitrary Call

callInvariant :: Call -> Bool | Source

`Call` invariant.
Call graphs

data CallGraph meta | 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.
Instances

Eq meta => Eq (CallGraph meta)
Show meta => Show (CallGraph meta)

callGraphInvariant :: CallGraph meta -> Bool | Source

`CallGraph` invariant.

fromList :: Monoid meta => [(Call, meta)] -> CallGraph meta | Source

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

toList :: CallGraph meta -> [(Call, meta)] | Source

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

empty :: CallGraph meta | Source

Creates an empty call graph.

union :: Monoid meta => CallGraph meta -> CallGraph meta -> CallGraph meta | Source

Takes the union of two call graphs.

insert :: Monoid meta => Call -> meta -> CallGraph meta -> CallGraph meta | Source

Inserts a call into a call graph.

complete :: Monoid meta => CallGraph meta -> CallGraph meta | Source

``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.

showBehaviour :: Show meta => CallGraph meta -> String | Source

Displays the recursion behaviour corresponding to a call graph.
Tests

tests :: IO Bool | Source

Produced by Haddock version 2.4.2