    {- | 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.Monad (forM, forM_)
    import Data.Graph
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import qualified Data.Map as Map
    import Data.Maybe
    import Data.Set (Set)
    import qualified Data.Set as Set

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

    import Agda.TypeChecking.Monad

    import Agda.Utils.List    (hasElem)
    import Agda.Utils.Pretty  (prettyShow)

    import Agda.Utils.Impossible

    -- | We compute for each clause the set of potentially recursive names.
    type NamesPerClause = IntMap (Set QName)

    -- | Given a list of formally mutually recursive functions,
    --   check for actual recursive calls in the bodies of these functions.
    --   Returns the actually recursive functions as strongly connected components.
    --
    --   As a side effect, update the 'clauseRecursive' field in the
    --   clauses belonging to the given functions.
    recursive :: [QName] -> TCM [[QName]]
    recursive :: [QName] -> TCM [[QName]]
    recursive [QName]
    names = do
      -- For each function, get names per clause and total.
      ([IntMap (Set QName)]
    perClauses, [Set QName]
    nss) <- [(IntMap (Set QName), Set QName)]
    -> ([IntMap (Set QName)], [Set QName])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(IntMap (Set QName), Set QName)]
     -> ([IntMap (Set QName)], [Set QName]))
    -> TCMT IO [(IntMap (Set QName), Set QName)]
    -> TCMT IO ([IntMap (Set QName)], [Set QName])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCMT IO (IntMap (Set QName), Set QName))
    -> [QName] -> TCMT IO [(IntMap (Set QName), Set QName)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((QName -> Bool) -> QName -> TCMT IO (IntMap (Set QName), Set QName)
    recDef ([QName]
    names [QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    `hasElem`)) [QName]
    names
      -- Create graph suitable for stronglyConnComp.
      -- Nodes are identical to node keys.
      let graph :: [(QName, QName, [QName])]
    graph  = (QName -> Set QName -> (QName, QName, [QName]))
    -> [QName] -> [Set QName] -> [(QName, QName, [QName])]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ QName
    x Set QName
    ns -> (QName
    x, QName
    x, Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    ns)) [QName]
    names [Set QName]
    nss
      let sccs :: [SCC QName]
    sccs   = [(QName, QName, [QName])] -> [SCC QName]
    forall key node. Ord key => [(node, key, [key])] -> [SCC node]
    stronglyConnComp [(QName, QName, [QName])]
    graph
      let nonRec :: [QName]
    nonRec = (SCC QName -> Maybe QName) -> [SCC QName] -> [QName]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (\case{ AcyclicSCC QName
    x -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x ; SCC QName
    _ -> Maybe QName
    forall a. Maybe a
    Nothing}) [SCC QName]
    sccs
      let recs :: [[QName]]
    recs   = (SCC QName -> Maybe [QName]) -> [SCC QName] -> [[QName]]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (\case{ CyclicSCC [QName]
    xs -> [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [QName]
    xs; SCC QName
    _ -> Maybe [QName]
    forall a. Maybe a
    Nothing}) [SCC QName]
    sccs

      [Char] -> Key -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Key -> [Char] -> m ()
    reportSLn [Char]
    "rec.graph" Key
    60 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [(QName, QName, [QName])] -> [Char]
    forall a. Show a => a -> [Char]
    show [(QName, QName, [QName])]
    graph

      -- Mark all non-recursive functions and their clauses as such.
      (QName -> TCMT IO ()) -> [QName] -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> TCMT IO ()
    markNonRecursive [QName]
    nonRec

      -- Mark individual clauses of recursive functions:
      --------------------------------------------------
      -- Map names to clause numbers to sets of mentioned names.
      let clMap :: Map QName (IntMap (Set QName))
    clMap = (IntMap (Set QName) -> IntMap (Set QName) -> IntMap (Set QName))
    -> [(QName, IntMap (Set QName))] -> Map QName (IntMap (Set QName))
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith IntMap (Set QName) -> IntMap (Set QName) -> IntMap (Set QName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(QName, IntMap (Set QName))] -> Map QName (IntMap (Set QName)))
    -> [(QName, IntMap (Set QName))] -> Map QName (IntMap (Set QName))
    forall a b. (a -> b) -> a -> b
    $ [QName] -> [IntMap (Set QName)] -> [(QName, IntMap (Set QName))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [QName]
    names [IntMap (Set QName)]
    perClauses
      -- Walk through SCCs.
      [[QName]] -> ([QName] -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [[QName]]
    recs (([QName] -> TCMT IO ()) -> TCMT IO ())
    -> ([QName] -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ [QName]
    scc -> do
        -- Does a set of names have an overlap with the current scc?
        let overlap :: Set QName -> Bool
    overlap Set QName
    s = (QName -> Bool) -> [QName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set QName
    s) [QName]
    scc
        -- Walk through members of SCC.
        [QName] -> (QName -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [QName]
    scc ((QName -> TCMT IO ()) -> TCMT IO ())
    -> (QName -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    x -> do
          -- Get the NamesPerClause for the current function x.
          let perClause :: IntMap (Set QName)
    perClause  = IntMap (Set QName)
    -> QName -> Map QName (IntMap (Set QName)) -> IntMap (Set QName)
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault IntMap (Set QName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ QName
    x Map QName (IntMap (Set QName))
    clMap
          -- A clause is recursive if its calls overlap with its scc.
          let recClause :: Key -> Bool
    recClause Key
    i = Set QName -> Bool
    overlap (Set QName -> Bool) -> Set QName -> Bool
    forall a b. (a -> b) -> a -> b
    $ Set QName -> Key -> IntMap (Set QName) -> Set QName
    forall a. a -> Key -> IntMap a -> a
    IntMap.findWithDefault Set QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Key
    i IntMap (Set QName)
    perClause
          (Key -> Bool) -> QName -> TCMT IO ()
    markRecursive Key -> Bool
    recClause QName
    x

      -- Return recursive SCCs.
      [[QName]] -> TCM [[QName]]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [[QName]]
    recs

    -- | Mark a function as terminating and all its clauses as non-recursive.
    markNonRecursive :: QName -> TCM ()
    markNonRecursive :: QName -> TCMT IO ()
    markNonRecursive QName
    q = (Signature -> Signature) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCMT IO ())
    -> (Signature -> Signature) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
      def :: Defn
    def@Function{} -> Defn
    def
       { funTerminates :: Maybe Bool
    funTerminates = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
       , funClauses :: [Clause]
    funClauses    = (Clause -> Clause) -> [Clause] -> [Clause]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Clause
    cl -> Clause
    cl { clauseRecursive :: Maybe Bool
    clauseRecursive = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False }) ([Clause] -> [Clause]) -> [Clause] -> [Clause]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Clause]
    funClauses Defn
    def
       }
      Defn
    def -> Defn
    def

    -- | Mark all clauses of a function as recursive or non-recursive.
    markRecursive
      :: (Int -> Bool)  -- ^ Which clauses are recursive?
      -> QName -> TCM ()
    markRecursive :: (Key -> Bool) -> QName -> TCMT IO ()
    markRecursive Key -> Bool
    f QName
    q = (Signature -> Signature) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCMT IO ())
    -> (Signature -> Signature) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
      def :: Defn
    def@Function{} -> Defn
    def
       { funClauses :: [Clause]
    funClauses    = (Key -> Clause -> Clause) -> [Key] -> [Clause] -> [Clause]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Key
    i Clause
    cl -> Clause
    cl { clauseRecursive :: Maybe Bool
    clauseRecursive = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (Key -> Bool
    f Key
    i) }) [Key
    0..] ([Clause] -> [Clause]) -> [Clause] -> [Clause]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Clause]
    funClauses Defn
    def
       }
      Defn
    def -> Defn
    def

    -- | @recDef names name@ returns all definitions from @names@
    --   that are used in the type and body of @name@.
    recDef :: (QName -> Bool) -> QName -> TCM (NamesPerClause, Set QName)
    recDef :: (QName -> Bool) -> QName -> TCMT IO (IntMap (Set QName), Set QName)
    recDef QName -> Bool
    include QName
    name = do
      -- Retrieve definition
      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name

      -- Get names in type
      Set QName
    ns1 <- (QName -> Bool) -> Type -> TCM (Set QName)
    forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
    anyDefs QName -> Bool
    include (Definition -> Type
    defType Definition
    def)

      -- Get names in body
      (IntMap (Set QName)
    perClause, Set QName
    ns2) <- case Definition -> Defn
    theDef Definition
    def of
        Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls } -> do
          [(Key, Set QName)]
    perClause <- do
            [(Key, Clause)]
    -> ((Key, Clause) -> TCMT IO (Key, Set QName))
    -> TCMT IO [(Key, Set QName)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ([Key] -> [Clause] -> [(Key, Clause)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Key
    0..] [Clause]
    cls) (((Key, Clause) -> TCMT IO (Key, Set QName))
     -> TCMT IO [(Key, Set QName)])
    -> ((Key, Clause) -> TCMT IO (Key, Set QName))
    -> TCMT IO [(Key, Set QName)]
    forall a b. (a -> b) -> a -> b
    $ \ (Key
    i, Clause
    cl) ->
              (Key
    i,) (Set QName -> (Key, Set QName))
    -> TCM (Set QName) -> TCMT IO (Key, Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> Bool) -> Clause -> TCM (Set QName)
    forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
    anyDefs QName -> Bool
    include Clause
    cl
          (IntMap (Set QName), Set QName)
    -> TCMT IO (IntMap (Set QName), Set QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Key, Set QName)] -> IntMap (Set QName)
    forall a. [(Key, a)] -> IntMap a
    IntMap.fromList [(Key, Set QName)]
    perClause, [Set QName] -> Set QName
    forall a. Monoid a => [a] -> a
    mconcat ([Set QName] -> Set QName) -> [Set QName] -> Set QName
    forall a b. (a -> b) -> a -> b
    $ ((Key, Set QName) -> Set QName)
    -> [(Key, Set QName)] -> [Set QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (Key, Set QName) -> Set QName
    forall a b. (a, b) -> b
    snd [(Key, Set QName)]
    perClause)
        Defn
    _ -> (IntMap (Set QName), Set QName)
    -> TCMT IO (IntMap (Set QName), Set QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntMap (Set QName)
    forall a. Monoid a => a
    mempty, Set QName
    forall a. Monoid a => a
    mempty)

      [Char] -> Key -> [[Char]] -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Key -> a -> m ()
    reportS [Char]
    "rec.graph" Key
    20
        [ [Char]
    "recDef " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    name
        , [Char]
    "  names in the type: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Set QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Set QName
    ns1
        , [Char]
    "  names in the def:  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Set QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Set QName
    ns2
        ]
      (IntMap (Set QName), Set QName)
    -> TCMT IO (IntMap (Set QName), Set QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntMap (Set QName)
    perClause, Set QName
    ns1 Set QName -> Set QName -> Set QName
    forall a. Monoid a => a -> a -> a
    `mappend` Set QName
    ns2)

    -- | @anysDef names a@ returns all definitions from @names@
    --   that are used in @a@.
    anyDefs :: GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
    anyDefs :: forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
    anyDefs QName -> Bool
    include a
    a = do
      -- Prepare function to lookup metas outside of TCM
      MetaStore
    st <- TCMT IO MetaStore
    forall (m :: * -> *). ReadTCState m => m MetaStore
    getMetaStore
      let lookup :: MetaId -> Maybe Term
    lookup (MetaId Key
    x) = (MetaVariable -> MetaInstantiation
    mvInstantiation (MetaVariable -> MetaInstantiation)
    -> Maybe MetaVariable -> Maybe MetaInstantiation
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Key -> MetaStore -> Maybe MetaVariable
    forall a. Key -> IntMap a -> Maybe a
    IntMap.lookup Key
    x MetaStore
    st) Maybe MetaInstantiation
    -> (MetaInstantiation -> Maybe Term) -> Maybe Term
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            InstV [Arg [Char]]
    _ Term
    v                      -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    v    -- TODO: ignoring the lambdas might be bad?
            MetaInstantiation
    Open                           -> Maybe Term
    forall a. Maybe a
    Nothing
            MetaInstantiation
    OpenInstance                   -> Maybe Term
    forall a. Maybe a
    Nothing
            BlockedConst{}                 -> Maybe Term
    forall a. Maybe a
    Nothing
            PostponedTypeCheckingProblem{} -> Maybe Term
    forall a. Maybe a
    Nothing
          -- we collect only those used definitions that are in @names@
          emb :: QName -> Set QName
    emb QName
    d = if QName -> Bool
    include QName
    d then QName -> Set QName
    forall a. a -> Set a
    Set.singleton QName
    d else Set QName
    forall a. Set a
    Set.empty
      -- get all the Defs that are in names
      Set QName -> TCM (Set QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set QName -> TCM (Set QName)) -> Set QName -> TCM (Set QName)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Maybe Term) -> (QName -> Set QName) -> a -> Set QName
    forall a b.
    (GetDefs a, Monoid b) =>
    (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
    getDefs' MetaId -> Maybe Term
    lookup QName -> Set QName
    emb a
    a