Safe Haskell | None |
---|---|
Language | Haskell98 |
- type ArgumentIndex = Int
- newtype CallMatrix' a = CallMatrix {
- mat :: Matrix ArgumentIndex a
- type CallMatrix = CallMatrix' Order
- class CallComb a where
- data CallMatrixAug cinfo = CallMatrixAug {
- augCallMatrix :: CallMatrix
- augCallInfo :: cinfo
- noAug :: Monoid cinfo => CallMatrix -> CallMatrixAug cinfo
- newtype CMSet cinfo = CMSet {
- cmSet :: Favorites (CallMatrixAug cinfo)
- insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo
- union :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
- toList :: CMSet cinfo -> [CallMatrixAug cinfo]
- callMatrix :: Size ArgumentIndex -> Gen CallMatrix
- tests :: IO Bool
Documentation
type ArgumentIndex = Int Source
Call matrix indices = function argument indices.
Machine integer Int
is sufficient, since we cannot index more arguments
than we have addresses on our machine.
newtype CallMatrix' a Source
Call matrices.
A call matrix for a call f --> g
has dimensions ar(g) × ar(f)
.
Each column corresponds to one formal argument of caller f
.
Each row corresponds to one argument in the call to g
.
In the presence of dot patterns, a call argument can be related
to several different formal arguments of f
.
See e.g. testsucceedDotPatternTermination.agda
:
data D : Nat -> Set where cz : D zero c1 : forall n -> D n -> D (suc n) c2 : forall n -> D n -> D n f : forall n -> D n -> Nat f .zero cz = zero f .(suc n) (c1 n d) = f n (c2 n d) f n (c2 .n d) = f n d
Call matrices (without guardedness) are
-1 -1 n < suc n and n < c1 n d ? = c2 n d <= c1 n d = -1 n <= n and n < c2 n d ? -1 d < c2 n d
Here is a part of the original documentation for call matrices (kept for historical reasons):
This datatype encodes information about a single recursive
function application. The columns of the call matrix stand for
source
function arguments (patterns). The rows of the matrix stand for
target
function arguments. Element (i, j)
in the matrix should
be computed as follows:
CallMatrix | |
|
Functor CallMatrix' Source | |
Foldable CallMatrix' Source | |
Traversable CallMatrix' Source | |
Arbitrary CallMatrix Source | |
Pretty CallMatrix Source | |
CallComb CallMatrix Source | Call matrix multiplication.
Note the reversed order of multiplication:
The matrix Preconditions:
Postcondition:
|
Eq a => Eq (CallMatrix' a) Source | |
Ord a => Ord (CallMatrix' a) Source | |
(Show a, HasZero a) => Show (CallMatrix' a) Source | |
(CoArbitrary a, HasZero a) => CoArbitrary (CallMatrix' a) Source | |
PartialOrd a => PartialOrd (CallMatrix' a) Source | |
NotWorse (CallMatrix' Order) Source | |
HasZero a => Diagonal (CallMatrix' a) a Source |
type CallMatrix = CallMatrix' Order Source
Call matrix multiplication and call combination.
CallComb CallMatrix Source | Call matrix multiplication.
Note the reversed order of multiplication:
The matrix Preconditions:
Postcondition:
|
Monoid cinfo => CallComb (CMSet cinfo) Source | Call matrix set product is the Cartesian product. |
Monoid cinfo => CallComb (CallMatrixAug cinfo) Source | Augmented call matrix multiplication. |
Call matrix augmented with path information.
data CallMatrixAug cinfo Source
Call matrix augmented with path information.
CallMatrixAug | |
|
Eq cinfo => Eq (CallMatrixAug cinfo) Source | |
Show cinfo => Show (CallMatrixAug cinfo) Source | |
CoArbitrary cinfo => CoArbitrary (CallMatrixAug cinfo) Source | |
Arbitrary cinfo => Arbitrary (CallMatrixAug cinfo) Source | |
PartialOrd (CallMatrixAug cinfo) Source | |
Pretty cinfo => Pretty (CallMatrixAug cinfo) Source | |
NotWorse (CallMatrixAug cinfo) Source | |
Monoid cinfo => CallComb (CallMatrixAug cinfo) Source | Augmented call matrix multiplication. |
Diagonal (CallMatrixAug cinfo) Order Source | |
Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source |
noAug :: Monoid cinfo => CallMatrix -> CallMatrixAug cinfo Source
Non-augmented call matrix.
Sets of incomparable call matrices augmented with path information.
Sets of incomparable call matrices augmented with path information.
Use overloaded null
, empty
, singleton
, mappend
.
CMSet | |
|
Show cinfo => Show (CMSet cinfo) Source | |
Monoid (CMSet cinfo) Source | |
CoArbitrary cinfo => CoArbitrary (CMSet cinfo) Source | |
Arbitrary cinfo => Arbitrary (CMSet cinfo) Source | |
Null (CMSet cinfo) Source | |
Pretty cinfo => Pretty (CMSet cinfo) Source | |
Monoid cinfo => CallComb (CMSet cinfo) Source | Call matrix set product is the Cartesian product. |
Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source |
insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo Source
Insert into a call matrix set.
toList :: CMSet cinfo -> [CallMatrixAug cinfo] Source
Convert into a list of augmented call matrices.
Printing
Generators and tests
CallMatrix
callMatrix :: Size ArgumentIndex -> Gen CallMatrix Source
Generates a call matrix of the given size.