{- | 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.
  ([NamesPerClause]
perClauses, [Set QName]
nss) <- [(NamesPerClause, Set QName)] -> ([NamesPerClause], [Set QName])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(NamesPerClause, Set QName)] -> ([NamesPerClause], [Set QName]))
-> TCMT IO [(NamesPerClause, Set QName)]
-> TCMT IO ([NamesPerClause], [Set QName])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO (NamesPerClause, Set QName))
-> [QName] -> TCMT IO [(NamesPerClause, 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 (NamesPerClause, 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

  VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"rec.graph" VerboseLevel
60 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [(QName, QName, [QName])] -> VerboseKey
forall a. Show a => a -> VerboseKey
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 NamesPerClause
clMap = (NamesPerClause -> NamesPerClause -> NamesPerClause)
-> [(QName, NamesPerClause)] -> Map QName NamesPerClause
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith NamesPerClause -> NamesPerClause -> NamesPerClause
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(QName, NamesPerClause)] -> Map QName NamesPerClause)
-> [(QName, NamesPerClause)] -> Map QName NamesPerClause
forall a b. (a -> b) -> a -> b
$ [QName] -> [NamesPerClause] -> [(QName, NamesPerClause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [QName]
names [NamesPerClause]
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 :: NamesPerClause
perClause  = NamesPerClause
-> QName -> Map QName NamesPerClause -> NamesPerClause
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault NamesPerClause
forall a. HasCallStack => a
__IMPOSSIBLE__ QName
x Map QName NamesPerClause
clMap
      -- A clause is recursive if its calls overlap with its scc.
      let recClause :: VerboseLevel -> Bool
recClause VerboseLevel
i = Set QName -> Bool
overlap (Set QName -> Bool) -> Set QName -> Bool
forall a b. (a -> b) -> a -> b
$ Set QName -> VerboseLevel -> NamesPerClause -> Set QName
forall a. a -> VerboseLevel -> IntMap a -> a
IntMap.findWithDefault Set QName
forall a. HasCallStack => a
__IMPOSSIBLE__ VerboseLevel
i NamesPerClause
perClause
      (VerboseLevel -> Bool) -> QName -> TCMT IO ()
markRecursive VerboseLevel -> 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 :: (VerboseLevel -> Bool) -> QName -> TCMT IO ()
markRecursive VerboseLevel -> 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    = (VerboseLevel -> Clause -> Clause)
-> [VerboseLevel] -> [Clause] -> [Clause]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ VerboseLevel
i Clause
cl -> Clause
cl { clauseRecursive :: Maybe Bool
clauseRecursive = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (VerboseLevel -> Bool
f VerboseLevel
i) }) [VerboseLevel
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 (NamesPerClause, 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
  (NamesPerClause
perClause, Set QName
ns2) <- case Definition -> Defn
theDef Definition
def of
    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls } -> do
      [(VerboseLevel, Set QName)]
perClause <- do
        [(VerboseLevel, Clause)]
-> ((VerboseLevel, Clause) -> TCMT IO (VerboseLevel, Set QName))
-> TCMT IO [(VerboseLevel, Set QName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([VerboseLevel] -> [Clause] -> [(VerboseLevel, Clause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
0..] [Clause]
cls) (((VerboseLevel, Clause) -> TCMT IO (VerboseLevel, Set QName))
 -> TCMT IO [(VerboseLevel, Set QName)])
-> ((VerboseLevel, Clause) -> TCMT IO (VerboseLevel, Set QName))
-> TCMT IO [(VerboseLevel, Set QName)]
forall a b. (a -> b) -> a -> b
$ \ (VerboseLevel
i, Clause
cl) ->
          (VerboseLevel
i,) (Set QName -> (VerboseLevel, Set QName))
-> TCM (Set QName) -> TCMT IO (VerboseLevel, 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
      (NamesPerClause, Set QName) -> TCMT IO (NamesPerClause, Set QName)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(VerboseLevel, Set QName)] -> NamesPerClause
forall a. [(VerboseLevel, a)] -> IntMap a
IntMap.fromList [(VerboseLevel, 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
$ ((VerboseLevel, Set QName) -> Set QName)
-> [(VerboseLevel, Set QName)] -> [Set QName]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel, Set QName) -> Set QName
forall a b. (a, b) -> b
snd [(VerboseLevel, Set QName)]
perClause)
    Defn
_ -> (NamesPerClause, Set QName) -> TCMT IO (NamesPerClause, Set QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (NamesPerClause
forall a. Monoid a => a
mempty, Set QName
forall a. Monoid a => a
mempty)

  VerboseKey -> VerboseLevel -> [VerboseKey] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"rec.graph" VerboseLevel
20
    [ VerboseKey
"recDef " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
name
    , VerboseKey
"  names in the type: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Set QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Set QName
ns1
    , VerboseKey
"  names in the def:  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Set QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Set QName
ns2
    ]
  (NamesPerClause, Set QName) -> TCMT IO (NamesPerClause, Set QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (NamesPerClause
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 :: (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 VerboseLevel
x) = (MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> Maybe MetaVariable -> Maybe MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> MetaStore -> Maybe MetaVariable
forall a. VerboseLevel -> IntMap a -> Maybe a
IntMap.lookup VerboseLevel
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 VerboseKey]
_ 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