{-# OPTIONS_GHC -Wunused-imports #-}
-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all -dno-suppress-type-signatures -ddump-to-file -dno-typeable-binds #-}

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

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

import Mikan.Syntax.Internal
import Mikan.Syntax.Internal.Defs

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.CompiledClause

import Mikan.Utils.List
import Mikan.Utils.Impossible
import Mikan.Utils.StrictFlipEndo

-- | 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 (Set QName -> QName -> TCMT IO (IntMap (Set QName), Set QName)
recDef 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

  reportSDoc "rec.graph" 60 $ vcat
    [ "termination graph:"
    , nest 2 $ vcat $ graph <&> \(QName
a, QName
_, [QName]
c) -> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
prettyTCM [QName]
c
    , "connected components:"
    , nest 2 $ vcat $ sccs <&> \case
      AcyclicSCC QName
x -> TCMT IO Doc
"nonrec" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x
      CyclicSCC [QName]
xs -> TCMT IO Doc
"mutual" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
prettyTCM [QName]
xs
    ]

  -- 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 = ASetter' TCState Defn -> (Defn -> Defn) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) ((Defn -> Defn) -> TCMT IO ()) -> (Defn -> Defn) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \case
  def :: Defn
def@Function{} -> Defn
def
    { funTerminates = Just True
    , funClauses    = map' (\ Clause
cl -> Clause
cl { clauseRecursive = NotRecursive }) $ funClauses def
    , funCompiled   = fmap (mapDone \ CCDone Term
done -> CCDone Term
done{ ccClauseRecursive = NotRecursive }) $ funCompiled 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 = ASetter' TCState Defn -> (Defn -> Defn) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) \case
  def :: Defn
def@Function{} -> Defn
def
    { funClauses    = zipWith' (\ Key
i Clause
cl -> Clause
cl { clauseRecursive = decideRecursive (f i) }) [0..] $ funClauses def
    , funCompiled   = fmap (mapDone \ done :: CCDone Term
done@CCDone{ ccClauseNumber :: forall a. CCDone a -> Key
ccClauseNumber = Key
i } -> CCDone Term
done{ ccClauseRecursive = decideRecursive (f i) }) $ funCompiled def
    }
  Defn
def -> Defn
def

-- | @recDef names name@ returns all definitions from @names@
--   that are used in the type and body of @name@.
recDef :: Set QName -> QName -> TCM (NamesPerClause, Set QName)
recDef :: Set QName -> QName -> TCMT IO (IntMap (Set QName), Set QName)
recDef Set QName
include QName
name = do
  -- Retrieve definition
  def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
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 } -> (((Key, Clause) -> TCMT IO (IntMap (Set QName), Set QName))
 -> [(Key, Clause)] -> TCMT IO (IntMap (Set QName), Set QName))
-> [(Key, Clause)]
-> ((Key, Clause) -> TCMT IO (IntMap (Set QName), Set QName))
-> TCMT IO (IntMap (Set QName), Set QName)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Key, Clause) -> TCMT IO (IntMap (Set QName), Set QName))
-> [(Key, Clause)] -> TCMT IO (IntMap (Set QName), Set QName)
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ([Key] -> [Clause] -> [(Key, Clause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Key
0..] [Clause]
cls) \(Key
i, Clause
cl) -> do
      -- Fix for performance regression in Issue3554: that function is
      -- nonrecursive, but only trivially so *if* we disregard
      -- references to names from the mutual block in the right-hand
      -- sides of generated clauses.
      --
      -- Since generated clauses are not considered for termination
      -- checking, considering them here can only change the result
      -- from "trivially nonrecursive" to "heat", if there are very
      -- large DotPs.
      --
      -- (ReduceNonrecDefP) However, termination checking can depend on
      -- whether we *reduce* DefP clauses from the current SCC.
      -- Therefore, we keep them in the NamesPerClause but not in the
      -- edge set.
      defs <- Set QName -> Clause -> TCM (Set QName)
forall a. GetDefs a => Set QName -> a -> TCM (Set QName)
anyDefs Set QName
include Clause
cl
      pure
        ( IntMap.singleton i defs
        , if hasDefP cl then mempty else defs
        )

    Datatype{ dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
cl } -> do
      ns <- Set QName -> Clause -> TCM (Set QName)
forall a. GetDefs a => Set QName -> a -> TCM (Set QName)
anyDefs Set QName
include Clause
cl
      return (IntMap.singleton 0 ns, ns)

    Record{ Maybe Clause
recClause :: Maybe Clause
recClause :: Defn -> Maybe Clause
recClause, Telescope
recTel :: Telescope
recTel :: Defn -> Telescope
recTel } -> do
      ns1 <- Set QName -> Maybe Clause -> TCM (Set QName)
forall a. GetDefs a => Set QName -> a -> TCM (Set QName)
anyDefs Set QName
include Maybe Clause
recClause
      ns2 <- anyDefs include recTel
      let ns = Set QName
ns1 Set QName -> Set QName -> Set QName
forall a. Monoid a => a -> a -> a
`mappend` Set QName
ns2
      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)

  reportSDoc "rec.graph" 20 $ vcat
    [ "recDef" <+> pretty name
    , "names in the type:" <+> pretty ns1
    , "names in the def: " <+> pretty ns2
    , "names per clause:"
    , vcat $ IntMap.toList perClause <&> \(Key
i, Set QName
x) ->
        Key -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Key -> m Doc -> m Doc
nest Key
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"." TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Key -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Key
i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
colon TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Set QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Set QName -> m Doc
prettyTCM Set QName
x
    ]
  return (perClause, ns1 `mappend` ns2)

{-# INLINE anyDefs #-}
-- | @anysDef names a@ returns all definitions from @names@
--   that are used in @a@.
anyDefs :: GetDefs a => Set QName -> a -> TCM (Set QName)
anyDefs :: forall a. GetDefs a => Set QName -> a -> TCM (Set QName)
anyDefs Set QName
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 = (Set QName -> Set QName) -> Endo (Set QName)
forall a. (a -> a) -> Endo a
Endo \Set QName
s -> if QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
d Set QName
include then QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
d Set QName
s
                                                 else Set QName
s
  -- get all the Defs that are in names
  return $! getDefs lookup emb a `appEndo` mempty
  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__