| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Termination
Synopsis
- traceTerm :: String -> a -> a
- traceTermM :: Monad m => String -> m ()
- traceProg :: String -> a -> a
- traceProgM :: Monad m => String -> m ()
- cutoff :: Int
- type Matrix a = Matrix Int a
- empty :: Matrix a
- data Order
- orderMat :: Matrix Order -> Order
- decr :: (?cutoff :: Int) => Int -> Order
- abstract :: Order -> Order
- absCM :: Matrix Order -> Matrix Order
- ordRing :: (?cutoff :: Int) => Semiring Order
- comp :: (?cutoff :: Int) => Order -> Order -> Order
- maxO :: (?cutoff :: Int) => Order -> Order -> Order
- minO :: (?cutoff :: Int) => Order -> Order -> Order
- minM :: (?cutoff :: Int) => Matrix Order -> Matrix Order -> Matrix Order
- maxL :: (?cutoff :: Int) => [Order] -> Order
- minL :: (?cutoff :: Int) => [Order] -> Order
- collapse :: (?cutoff :: Int) => Matrix Order -> Order
- type Vector a = [a]
- type NaiveMatrix a = [Vector a]
- ssum :: Semiring a -> Vector a -> a
- vadd :: Semiring a -> Vector a -> Vector a -> Vector a
- scalarProdukt :: Semiring a -> Vector a -> Vector a -> a
- madd :: Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
- transp :: NaiveMatrix a -> NaiveMatrix a
- mmul :: Show a => Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
- diag :: NaiveMatrix a -> Vector a
- elems :: NaiveMatrix a -> Vector a
- sameSize :: Matrix a -> Matrix a -> Bool
- composable :: Matrix a -> Matrix a -> Bool
- compareArgs :: (?cutoff :: Int) => TSO Name -> [Pattern] -> [Expr] -> Arity -> Matrix Order
- compareExpr :: (?cutoff :: Int) => TSO Name -> Expr -> Pattern -> Order
- compareExpr' :: (?cutoff :: Int) => TSO Name -> Expr -> Pattern -> Order
- conView :: (Expr, [Expr]) -> (Expr, [Expr])
- compareVar :: (?cutoff :: Int) => TSO Name -> Name -> Pattern -> Order
- type Index = Name
- data Call = Call {}
- type CallMatrix = Matrix Order
- subsumes :: Matrix Order -> Matrix Order -> Bool
- leq :: Order -> Order -> Bool
- progress :: Matrix Order -> Matrix Order -> Bool
- decrToward0 :: Order -> Order -> Bool
- newtype CallPath = CallPath {
- getCallPath :: [Name]
- emptyCP :: CallPath
- mkCP :: Name -> Name -> CallPath
- mulCP :: CallPath -> CallPath -> CallPath
- compatibleCP :: CallPath -> CallPath -> Bool
- type CompCall = (CallPath, CallMatrix)
- mulCC :: (?cutoff :: Int) => CompCall -> CompCall -> CompCall
- subsumesCC :: CompCall -> CompCall -> Bool
- progressCC :: CompCall -> CompCall -> Bool
- type CMSet = [CompCall]
- cmRing :: (?cutoff :: Int) => Semiring CMSet
- type Progress = Writer Any
- type ProgressH = Writer (Any, Any)
- firstHalf :: (Any, Any)
- secondHalf :: (Any, Any)
- addCMh :: CompCall -> CMSet -> ProgressH CMSet
- addCM' :: CompCall -> CMSet -> Progress CMSet
- unionCMSet' :: CMSet -> CMSet -> Progress CMSet
- addCM :: CompCall -> CMSet -> CMSet
- unionCMSet :: CMSet -> CMSet -> CMSet
- mulCMSet :: (?cutoff :: Int) => CMSet -> CMSet -> CMSet
- type CallGraph = NaiveMatrix CMSet
- stepCG :: (?cutoff :: Int) => CallGraph -> Progress CallGraph
- complCGraph :: (?cutoff :: Int) => CallGraph -> CallGraph
- checkAll :: (?cutoff :: Int) => CallGraph -> Bool
- checkIdem :: (?cutoff :: Int) => CallMatrix -> Bool
- makeCG :: [Name] -> [Call] -> CallGraph
- isDecr :: Order -> Bool
- terminationCheck :: MonadAssert m => [Fun] -> m ()
- terminationCheckFuns :: (?cutoff :: Int) => [Fun] -> [(Name, Bool)]
- sizeChangeTermination :: (?cutoff :: Int) => [Name] -> [Call] -> [(Name, Bool)]
- collectCGFunDecl :: (?cutoff :: Int) => [(Name, Arity)] -> [Fun] -> [Call]
- tsoCase :: TSO Name -> Expr -> [Clause] -> TSO Name
- tsoBind :: TSO Name -> TBind -> TSO Name
- collectCallsExpr :: (?cutoff :: Int) => [(Name, Arity)] -> Name -> [Pattern] -> Expr -> [Call]
Documentation
traceTermM :: Monad m => String -> m () Source #
traceProgM :: Monad m => String -> m () Source #
type NaiveMatrix a = [Vector a] Source #
madd :: Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a Source #
transp :: NaiveMatrix a -> NaiveMatrix a Source #
mmul :: Show a => Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a Source #
diag :: NaiveMatrix a -> Vector a Source #
elems :: NaiveMatrix a -> Vector a Source #
compareArgs :: (?cutoff :: Int) => TSO Name -> [Pattern] -> [Expr] -> Arity -> Matrix Order Source #
type CallMatrix = Matrix Order Source #
Constructors
| CallPath | |
Fields
| |
type CompCall = (CallPath, CallMatrix) Source #
secondHalf :: (Any, Any) Source #
type CallGraph = NaiveMatrix CMSet Source #
terminationCheck :: MonadAssert m => [Fun] -> m () Source #