{- Checking for recursion: - We detect truly (co)recursive definitions by computing the dependency graph and checking for cycles. - This is inexpensive and let us skip the termination check when there's no (co)recursion Original contribution by Andrea Vezzosi (sanzhiyan). This implementation by Andreas. -} module Agda.Termination.RecCheck ( recursive , anyDefs ) where import Control.Applicative import Data.Graph import Data.List (nub) import qualified Data.Map as Map import Agda.Syntax.Internal import Agda.Syntax.Internal.Defs import Agda.TypeChecking.Monad recursive :: [QName] -> TCM Bool recursive names = do graph <- zip names <\$> mapM (\ d -> nub <\$> recDef names d) names reportSLn "rec.graph" 20 \$ show graph return \$ cyclic graph -- | A graph is cyclic if it has any strongly connected component. cyclic :: [(QName, [QName])] -> Bool cyclic g = or [ True | CyclicSCC _ <- stronglyConnComp g' ] where g' = map (\ (n, ns) -> ((), n, ns)) g -- | @recDef names name@ returns all definitions from @names@ -- that are used in the body of @name@. recDef :: [QName] -> QName -> TCM [QName] recDef names name = do -- Retrieve definition def <- getConstInfo name case theDef def of Function{ funClauses = cls } -> anyDefs names cls _ -> return [] -- | @anysDef names a@ returns all definitions from @names@ -- that are used in @a@. anyDefs :: GetDefs a => [QName] -> a -> TCM [QName] anyDefs names a = do -- Prepare function to lookup metas outside of TCM st <- getMetaStore let lookup x = case mvInstantiation <\$> Map.lookup x st of Just (InstV _ v) -> Just v -- TODO: ignoring the lambdas might be bad? _ -> Nothing -- we collect only those used definitions that are in @names@ emb d = if d `elem` names then [d] else [] -- get all the Defs that are in names return \$ getDefs' lookup emb a