{-# OPTIONS_GHC -Wunused-imports #-}

{- | 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
    ( MutualNames
    , recursive
    , anyDefs
    )
 where

import Control.Monad (forM)
import Data.Foldable
import Data.Graph
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import qualified Data.Map.Strict as MapS
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.Syntax.Internal
import Agda.Syntax.Internal.Defs
import Agda.Syntax.Common.Pretty  (prettyShow)

import Agda.TypeChecking.Monad

import Agda.Utils.Impossible

-- | The mutual block we are checking.
--
--   The functions are numbered according to their order of appearance
--   in this set.

type MutualNames = Set QName

-- | 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 :: Set QName -> TCM [MutualNames]
recursive :: Set QName -> TCM [Set QName]
recursive Set QName
names = do
  let names' :: [QName]
names' = Set QName -> [QName]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set QName
names
  -- For each function, get names per clause and total.
  (perClauses, 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((QName -> Bool) -> QName -> TCMT IO (IntMap (Set QName), Set QName)
recDef (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
names)) [QName]
names'
  -- Create graph suitable for stronglyConnComp.
  -- Nodes are identical to node keys.
  let 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   = [(QName, QName, [QName])] -> [SCC QName]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [(QName, QName, [QName])]
graph
  let 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   = (SCC QName -> Maybe (Set QName)) -> [SCC QName] -> [Set QName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case CyclicSCC [QName]
xs -> Set QName -> Maybe (Set QName)
forall a. a -> Maybe a
Just ([QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList [QName]
xs)
                               SCC QName
_            -> Maybe (Set QName)
forall a. Maybe a
Nothing)
                 [SCC QName]
sccs

  reportSLn "rec.graph" 60 $ show graph

  -- Mark all non-recursive functions and their clauses as such.
  mapM_ markNonRecursive nonRec

  -- Mark individual clauses of recursive functions:
  --------------------------------------------------
  -- Map names to clause numbers to sets of mentioned names.
  let 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.
  forM_ recs $ \ Set 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) -> Set 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) Set QName
scc
    -- Walk through members of SCC.
    Set QName -> (QName -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set 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.
  return 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 = Just True
   , funClauses    = map (\ Clause
cl -> Clause
cl { clauseRecursive = Just False }) $ funClauses def
   }
  def :: Defn
def@Record{} -> Defn
def
   { recTerminates = Just True
   }
  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    = zipWith (\ Key
i Clause
cl -> Clause
cl { clauseRecursive = Just (f i) }) [0..] $ funClauses 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
  def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name

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

  -- Get names in body
  (perClause, ns2) <- case theDef def of

    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls } -> do
      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
      return (IntMap.fromList perClause, mconcat $ map snd perClause)

    Record{ Telescope
recTel :: Telescope
recTel :: Defn -> Telescope
recTel } -> do
      ns <- (QName -> Bool) -> Telescope -> TCM (Set QName)
forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
anyDefs QName -> Bool
include Telescope
recTel
      return (IntMap.singleton 0 ns, ns)

    Defn
_ -> (IntMap (Set QName), Set QName)
-> TCMT IO (IntMap (Set QName), Set QName)
forall a. a -> TCMT IO a
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)

  reportS "rec.graph" 20
    [ "recDef " ++ prettyShow name
    , "  names in the type: " ++ prettyShow ns1
    , "  names in the def:  " ++ prettyShow ns2
    ]
  return (perClause, ns1 `mappend` 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
  st <- Lens' TCState (Map MetaId MetaVariable)
-> TCMT IO (Map MetaId MetaVariable)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map MetaId MetaVariable -> f (Map MetaId MetaVariable))
-> TCState -> f TCState
Lens' TCState (Map MetaId MetaVariable)
stSolvedMetaStore
  let lookup MetaId
x = MetaInstantiation -> Term
inst (MetaInstantiation -> Term)
-> (MetaVariable -> MetaInstantiation) -> MetaVariable -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> Term) -> Maybe MetaVariable -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> Map MetaId MetaVariable -> Maybe MetaVariable
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
x Map MetaId MetaVariable
st
      -- we collect only those used definitions that are in @names@
      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
  return $ getDefs' lookup emb a
  where
  -- TODO: Is it bad to ignore the lambdas?
  inst :: MetaInstantiation -> Term
inst (InstV Instantiation
i)                      = Instantiation -> Term
instBody Instantiation
i
  inst OpenMeta{}                     = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
  inst BlockedConst{}                 = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
  inst PostponedTypeCheckingProblem{} = Term
forall a. HasCallStack => a
__IMPOSSIBLE__