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

Safe HaskellNone

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

Structural orderings

data Order Source

In the paper referred to above, there is an order R with Unknown <= Le <= Lt.

This is generalized to Unknown <= 'Decr k' where Decr 1 replaces Lt and Decr 0 replaces Le. A negative decrease means an increase. The generalization allows the termination checker to record an increase by 1 which can be compensated by a following decrease by 2 which results in an overall decrease.

However, the termination checker of the paper itself terminates because there are only finitely many different call-matrices. To maintain termination of the terminator we set a cutoff point which determines how high the termination checker can count. This value should be set by a global or file-wise option.

See Call for more information.

TODO: document orders which are call-matrices themselves.

Constructors

Mat (Matrix Integer Order) 

decr :: [cutoff :: Int] => Int -> OrderSource

Smart constructor for Decr k :: Order which cuts off too big values.

Possible values for k: - ?cutoff <= k <= ?cutoff + 1.

increase :: Int -> Order -> OrderSource

Raw increase which does not cut off.

decrease :: Int -> Order -> OrderSource

Raw decrease which does not cut off.

(.*.) :: [cutoff :: Int] => Order -> Order -> OrderSource

Multiplication of Orders. (Corresponds to sequential composition.)

supremum :: [cutoff :: Int] => [Order] -> OrderSource

The supremum of a (possibly empty) list of Orders. More information (i.e., more decrease) is bigger. Unknown is no information, thus, smallest.

infimum :: [cutoff :: Int] => [Order] -> OrderSource

The infimum of a (non empty) list of Orders. Unknown is the least element, thus, dominant.

le :: OrderSource

le, lt, decreasing, unknown: for backwards compatibility, and for external use.

orderMat :: Matrix Integer Order -> OrderSource

Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.

Call matrices

type Index = IntegerSource

Call matrix indices.

newtype CallMatrix Source

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

Constructors

CallMatrix 

Fields

mat :: Matrix Index Order
 

(>*<) :: [cutoff :: Int] => 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 

Fields

source :: Index

The function making the call.

target :: Index

The function being called.

cm :: CallMatrix

The call matrix describing the call.

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.

Instances

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

CallGraph is a monoid under union.

Show meta => Pretty (CallGraph meta)

Displays the recursion behaviour corresponding to a call graph.

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 :: [cutoff :: Int] => 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.

prettyBehaviour :: Show meta => CallGraph meta -> DocSource

Displays the recursion behaviour corresponding to a call graph.

Tests