    {-# LANGUAGE CPP #-}

    {- 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 qualified Data.IntMap as IntMap

    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Defs

    import Agda.TypeChecking.Monad

    import Agda.Utils.Pretty (prettyShow)

    #include "undefined.h"
    import Agda.Utils.Impossible

    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 type and body of @name@.
    recDef :: [QName] -> QName -> TCM [QName]
    recDef names name = do
      -- Retrieve definition
      def <- getConstInfo name

      -- Get names in type
      ns1 <- anyDefs names (defType def)

      -- Get names in body
      ns2 <- case theDef def of
        Function{ funClauses = cls } -> anyDefs names cls
        _ -> return []

      reportSLn "rec.graph" 20 $ unlines
        [ "recDef " ++ prettyShow name
        , "  names in the type: " ++ show ns1
        , "  names in the def:  " ++ show ns2
        ]
      return $ ns1 `mappend` ns2

    -- | @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 (MetaId x) = case mvInstantiation <$> IntMap.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