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
cyclic :: [(QName, [QName])] -> Bool
cyclic g = or [ True | CyclicSCC _ <- stronglyConnComp g' ]
where g' = map (\ (n, ns) -> ((), n, ns)) g
recDef :: [QName] -> QName -> TCM [QName]
recDef names name = do
def <- getConstInfo name
case theDef def of
Function{ funClauses = cls } -> anyDefs names cls
_ -> return []
anyDefs :: GetDefs a => [QName] -> a -> TCM [QName]
anyDefs names a = do
st <- getMetaStore
let lookup x = case mvInstantiation <$> Map.lookup x st of
Just (InstV _ v) -> Just v
_ -> Nothing
emb d = if d `elem` names then [d] else []
return $ getDefs' lookup emb a