Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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)
show/hide Instances
(.*.) :: Order -> Order -> OrderSource
Multiplication of Orders. (Corresponds to sequential composition.)
supremum :: [Order] -> OrderSource
The supremum of a (possibly empty) list of Orders.
Call matrices
type Index = IntegerSource
Call matrix indices.
newtype CallMatrix Source
Call matrices. Note the call matrix invariant (callMatrixInvariant).
Constructors
CallMatrix
mat :: Matrix Index Order
show/hide Instances
(>*<) :: Call -> Call -> CallSource

Call combination.

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

callMatrixInvariant :: CallMatrix -> BoolSource
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 :: IndexThe function making the call.
target :: IndexThe function being called.
cm :: CallMatrixThe call matrix describing the call.
show/hide Instances
callInvariant :: Call -> BoolSource
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 Monoidal so that the meta information for different calls can be combined when the calls are combined.
show/hide Instances
Eq meta => Eq (CallGraph meta)
Show meta => Show (CallGraph meta)
callGraphInvariant :: CallGraph meta -> BoolSource
CallGraph invariant.
fromList :: Monoid meta => [(Call, meta)] -> CallGraph metaSource
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 metaSource
Creates an empty call graph.
union :: Monoid meta => CallGraph meta -> CallGraph meta -> CallGraph metaSource
Takes the union of two call graphs.
insert :: Monoid meta => Call -> meta -> CallGraph meta -> CallGraph metaSource
Inserts a call into a call graph.
complete :: Monoid meta => CallGraph meta -> CallGraph metaSource
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 -> StringSource
Displays the recursion behaviour corresponding to a call graph.
Tests
tests :: IO BoolSource
Produced by Haddock version 2.4.2