{-# LANGUAGE ImplicitParams             #-}
{-# LANGUAGE NondecreasingIndentation   #-}

{- Checking for Structural recursion
   Authors: Andreas Abel, Nils Anders Danielsson, Ulf Norell,
              Karl Mehltretter and others
   Created: 2007-05-28
   Source : TypeCheck.Rules.Decl
 -}

module Agda.Termination.TermCheck
    ( termDecl
    , termMutual
    , Result
    ) where

import Prelude hiding ( null )

import Control.Applicative  ( liftA2 )
import Control.Monad        ( (<=<), filterM, forM, forM_, zipWithM )

import Data.Foldable (toList)
import qualified Data.List as List
import Data.Monoid hiding ((<>))
import Data.Set (Set)
import qualified Data.Set as Set

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Internal.Generic
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Translation.InternalToAbstract (NamedClause(..))

import Agda.Termination.CutOff
import Agda.Termination.Monad
import Agda.Termination.CallGraph hiding (toList)
import qualified Agda.Termination.CallGraph as CallGraph
import Agda.Termination.CallMatrix hiding (toList)
import Agda.Termination.Order     as Order
import qualified Agda.Termination.SparseMatrix as Matrix
import Agda.Termination.Termination (endos, idempotent)
import qualified Agda.Termination.Termination  as Term
import Agda.Termination.RecCheck

import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Forcing
import Agda.TypeChecking.Records -- (isRecordConstructor, isInductiveRecord)
import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull, appDefE')
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import qualified Agda.Benchmarking as Benchmark
import Agda.TypeChecking.Monad.Benchmark (billTo, billPureTo)

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad -- (mapM', forM', ifM, or2M, and2M)
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.SmallSet as SmallSet
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible

-- | Call graph with call info for composed calls.

type Calls = CallGraph CallPath

-- | The result of termination checking a module.
--   Must be a 'Monoid' and have 'Singleton'.

type Result = [TerminationError]

-- | Entry point: Termination check a single declaration.
--
--   Precondition: 'envMutualBlock' must be set correctly.

termDecl :: A.Declaration -> TCM Result
termDecl :: Declaration -> TCM Result
termDecl Declaration
d = TCM Result -> TCM Result
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Result -> TCM Result) -> TCM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM Result
termDecl' Declaration
d


-- | Termination check a single declaration
--   (without necessarily ignoring @abstract@).

termDecl' :: A.Declaration -> TCM Result
termDecl' :: Declaration -> TCM Result
termDecl' = \case
    A.Axiom {}            -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Field {}            -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Primitive {}        -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Mutual MutualInfo
i [Declaration]
ds         -> [QName] -> TCM Result
termMutual ([QName] -> TCM Result) -> [QName] -> TCM Result
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [QName]
getNames [Declaration]
ds
    A.Section Range
_ Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds  -> [Declaration] -> TCM Result
forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
termDecls [Declaration]
ds
        -- section structure can be ignored as we are termination checking
        -- definitions lifted to the top-level
    A.Apply {}            -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Import {}           -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Pragma {}           -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Open {}             -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.PatternSynDef {}    -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.UnfoldingDecl{}     -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Generalize {}       -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
        -- open, pattern synonym and generalize defs are just artifacts from the concrete syntax
    A.ScopedDecl ScopeInfo
scope [Declaration]
ds -> {- withScope_ scope $ -} [Declaration] -> TCM Result
forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
termDecls [Declaration]
ds
        -- scope is irrelevant as we are termination checking Syntax.Internal
    A.RecSig{}            -> Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.RecDef DefInfo
_ QName
x UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Type
_ [Declaration]
ds -> [QName] -> TCM Result
termMutual [QName
x] TCM Result -> TCM Result -> TCM Result
forall a. Semigroup a => a -> a -> a
<> [Declaration] -> TCM Result
forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
termDecls [Declaration]
ds
        -- Andreas, 2022-10-23, issue #5823
        -- Also check record types for termination.
        -- They are unfolded during construction of unique inhabitants of eta-records.
    -- These should all be wrapped in mutual blocks:
    A.FunDef{}      -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DataSig{}     -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DataDef{}     -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteDecl{} -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteDef{}  -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteData{} -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    termDecls :: t Declaration -> TCM Result
termDecls t Declaration
ds = t Result -> Result
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (t Result -> Result) -> TCMT IO (t Result) -> TCM Result
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> TCM Result) -> t Declaration -> TCMT IO (t Result)
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) -> t a -> m (t b)
mapM Declaration -> TCM Result
termDecl' t Declaration
ds

    -- The mutual names mentioned in the abstract syntax
    -- for symbols that need to be termination-checked.
    getNames :: [Declaration] -> [QName]
getNames = (Declaration -> [QName]) -> [Declaration] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Declaration -> [QName]
getName
    getName :: Declaration -> [QName]
getName (A.FunDef DefInfo
i QName
x [Clause]
cs)   = [QName
x]
    getName (A.RecDef DefInfo
_ QName
x UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Type
_ [Declaration]
ds)   = QName
x QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
: [Declaration] -> [QName]
getNames [Declaration]
ds
    getName (A.Mutual MutualInfo
_ [Declaration]
ds)             = [Declaration] -> [QName]
getNames [Declaration]
ds
    getName (A.Section Range
_ Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds)      = [Declaration] -> [QName]
getNames [Declaration]
ds
    getName (A.ScopedDecl ScopeInfo
_ [Declaration]
ds)         = [Declaration] -> [QName]
getNames [Declaration]
ds
    getName (A.UnquoteDecl MutualInfo
_ [DefInfo]
_ [QName]
xs Type
_)    = [QName]
xs
    getName (A.UnquoteDef [DefInfo]
_ [QName]
xs Type
_)       = [QName]
xs
    getName Declaration
_                           = []


-- | Entry point: Termination check the current mutual block.

termMutual
  :: [QName]
     -- ^ The function names defined in this block on top-level.
     --   (For error-reporting only.)
  -> TCM Result
termMutual :: [QName] -> TCM Result
termMutual [QName]
names0 = TCMT IO Bool -> TCM Result -> TCM Result -> TCM Result
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optTerminationCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (Result -> TCM Result
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty) (TCM Result -> TCM Result) -> TCM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ {-else-}
 TCM Result -> TCM Result
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Result -> TCM Result) -> TCM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ do

  -- Get set of mutually defined names from the TCM.
  -- This includes local and auxiliary functions introduced
  -- during type-checking.
  mid <- MutualId -> Maybe MutualId -> MutualId
forall a. a -> Maybe a -> a
fromMaybe MutualId
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe MutualId -> MutualId)
-> TCMT IO (Maybe MutualId) -> TCMT IO MutualId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock
  mutualBlock <- lookupMutualBlock mid
  let allNames = (QName -> Bool) -> Set QName -> Set QName
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (QName -> Bool) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool
isAbsurdLambdaName) (Set QName -> Set QName) -> Set QName -> Set QName
forall a b. (a -> b) -> a -> b
$
                 MutualBlock -> Set QName
mutualNames MutualBlock
mutualBlock
      names    = if [QName] -> Bool
forall a. Null a => a -> Bool
null [QName]
names0 then Set QName
allNames else [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList [QName]
names0
      i        = MutualBlock -> MutualInfo
mutualInfo MutualBlock
mutualBlock

  -- We set the range to avoid panics when printing error messages.
  setCurrentRange i $ do

  -- The following debug statement is part of a test case for Issue
  -- #3590.
  reportSLn "term.mutual.id" 40 $
    "Termination checking mutual block " ++ show mid
  reportSLn "term.mutual" 10 $ "Termination checking " ++ prettyShow allNames

  -- NO_TERMINATION_CHECK
  if (Info.mutualTerminationCheck i `elem` [ NoTerminationCheck, Terminating ]) then do
      reportSLn "term.warn.yes" 10 $ "Skipping termination check for " ++ prettyShow names
      forM_ allNames $ \ QName
q -> QName -> Bool -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
q Bool
True -- considered terminating!
      return mempty
  -- NON_TERMINATING
  else if (Info.mutualTerminationCheck i == NonTerminating) then do
      reportSLn "term.warn.yes" 10 $ "Considering as non-terminating: " ++ prettyShow names
      forM_ allNames $ \ QName
q -> QName -> Bool -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
q Bool
False
      return mempty
  else do
    sccs <- do
      -- Andreas, 2016-10-01 issue #2231
      -- Recursivity checker has to see through abstract definitions!
      ignoreAbstractMode $ do
        billTo [Benchmark.Termination, Benchmark.RecCheck] $ recursive allNames
      -- -- Andreas, 2017-03-24, use positivity info to skip non-recursive functions
      -- skip = ignoreAbstractMode $ allM allNames $ \ x -> do
      --   null <$> getMutual x
      -- PROBLEMS with test/Succeed/AbstractCoinduction.agda

    -- Trivially terminating (non-recursive)?
    when (null sccs) $
      reportSLn "term.warn.yes" 10 $ "Trivially terminating: " ++ prettyShow names

    -- Actual termination checking needed: go through SCCs.
    concat <$> do
     forM sccs $ \ Set QName
allNames -> do

     -- Set the mutual names in the termination environment.
     let namesSCC :: Set QName
namesSCC = (QName -> Bool) -> Set QName -> Set QName
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
allNames) Set QName
names
     let setNames :: TerEnv -> TerEnv
setNames TerEnv
e = TerEnv
e
           { terMutual    = allNames
           , terUserNames = namesSCC
           }
         runTerm :: TerM Result -> TCM Result
runTerm TerM Result
cont = TerM Result -> TCM Result
forall a. TerM a -> TCM a
runTerDefault (TerM Result -> TCM Result) -> TerM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ do
           cutoff <- TerM CutOff
terGetCutOff
           reportSLn "term.top" 10 $ "Termination checking " ++ prettyShow namesSCC ++
             " with cutoff=" ++ show cutoff ++ "..."
           terLocal setNames cont

     -- New check currently only makes a difference for copatterns and record types.
     -- Since it is slow, only invoke it if
     -- any of the definitions uses copatterns or is a record type.
     TCMT IO Bool -> TCM Result -> TCM Result -> TCM Result
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Set QName -> (QName -> TCMT IO Bool) -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
anyM Set QName
allNames ((QName -> TCMT IO Bool) -> TCMT IO Bool)
-> (QName -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \ QName
q -> QName -> TCMT IO Bool
forall (m :: * -> *).
(HasConstInfo m, HasBuiltins m) =>
QName -> m Bool
usesCopatterns QName
q TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Maybe RecordData -> Bool
forall a. Maybe a -> Bool
isJust (Maybe RecordData -> Bool)
-> TCMT IO (Maybe RecordData) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
q))
         -- Then: New check, one after another.
         (TerM Result -> TCM Result
runTerm (TerM Result -> TCM Result) -> TerM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ Set QName -> (QName -> TerM Result) -> TerM Result
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' Set QName
allNames ((QName -> TerM Result) -> TerM Result)
-> (QName -> TerM Result) -> TerM Result
forall a b. (a -> b) -> a -> b
$ QName -> TerM Result
termFunction)
         -- Else: Old check, all at once.
         (TerM Result -> TCM Result
runTerm (TerM Result -> TCM Result) -> TerM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ TerM Result
termMutual')

-- | @termMutual'@ checks all names of the current mutual block,
--   henceforth called @allNames@, for termination.
--
--   @allNames@ is taken from 'Internal' syntax, it contains also
--   the definitions created by the type checker (e.g., with-functions).

termMutual' :: TerM Result
termMutual' :: TerM Result
termMutual' = do

  -- collect all recursive calls in the block
  allNames <- TerM (Set QName)
terGetMutual
  let collect = Set QName -> (QName -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' Set QName
allNames QName -> TerM Calls
termDef

  -- first try to termination check ignoring the dot patterns
  calls1 <- collect
  reportCalls "no " calls1

  cutoff <- terGetCutOff
  let ?cutoff = cutoff
  r <- billToTerGraph $ Term.terminates calls1
  r <-
       -- Andrea: 22/04/2020.
       -- With cubical we will always have a clause where the dot
       -- patterns are instead replaced with a variable, so they
       -- cannot be relied on for termination.
       -- See issue #4606 for a counterexample involving HITs.
       --
       -- Without the presence of HITs I conjecture that dot patterns
       -- could be turned into actual splits, because no-confusion
       -- would make the other cases impossible, so I do not disable
       -- this for --without-K entirely.
       ifM (isJust <$> cubicalOption) (return r) {- else -} $
       case r of
         r :: Either CallPath ()
r@Right{} -> Either CallPath () -> TerM (Either CallPath ())
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Either CallPath ()
r
         Left{}    -> do
           -- Try again, but include the dot patterns this time.
           calls2 <- Bool -> TerM Calls -> TerM Calls
forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
True (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ TerM Calls
collect
           reportCalls "" calls2
           billToTerGraph $ Term.terminates calls2

  -- @names@ is taken from the 'Abstract' syntax, so it contains only
  -- the names the user has declared.  This is for error reporting.
  names <- terGetUserNames
  case r of

    Left CallPath
calls -> do
      (QName -> TerM ()) -> Set QName -> TerM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (QName -> Bool -> TerM ()
forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
`setTerminates` Bool
False) Set QName
allNames
      Result -> TerM Result
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> TerM Result) -> Result -> TerM Result
forall a b. (a -> b) -> a -> b
$ TerminationError -> Result
forall el coll. Singleton el coll => el -> coll
singleton (TerminationError -> Result) -> TerminationError -> Result
forall a b. (a -> b) -> a -> b
$ Set QName -> CallPath -> TerminationError
terminationError Set QName
names CallPath
calls

    Right{} -> do
      TCMT IO () -> TerM ()
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.warn.yes" Int
2 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        Set QName -> String
forall a. Pretty a => a -> String
prettyShow (Set QName
names) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does termination check"
      (QName -> TerM ()) -> Set QName -> TerM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (QName -> Bool -> TerM ()
forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
`setTerminates` Bool
True) Set QName
allNames
      Result -> TerM Result
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty

-- | Smart constructor for 'TerminationError'.
--   Removes 'termErrFunctions' that are not mentioned in 'termErrCalls'.
terminationError :: Set QName -> CallPath -> TerminationError
terminationError :: Set QName -> CallPath -> TerminationError
terminationError Set QName
names CallPath
calls = [QName] -> [CallInfo] -> TerminationError
TerminationError [QName]
names' [CallInfo]
calls'
  where
  calls' :: [CallInfo]
calls'    = CallPath -> [CallInfo]
callInfos CallPath
calls
  mentioned :: [QName]
mentioned = (CallInfo -> QName) -> [CallInfo] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map CallInfo -> QName
callInfoTarget [CallInfo]
calls'
  names' :: [QName]
names'    = (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter ([QName] -> QName -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [QName]
mentioned) ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set QName
names

billToTerGraph :: a -> TerM a
billToTerGraph :: forall a. a -> TerM a
billToTerGraph a
a = TCM a -> TerM a
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM a -> TerM a) -> TCM a -> TerM a
forall a b. (a -> b) -> a -> b
$ Account (BenchPhase (TCMT IO)) -> a -> TCM a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> c -> m c
billPureTo [BenchPhase (TCMT IO)
Phase
Benchmark.Termination, BenchPhase (TCMT IO)
Phase
Benchmark.Graph] a
a

-- | @reportCalls@ for debug printing.
--
--   Replays the call graph completion for debugging.

reportCalls :: String -> Calls -> TerM ()
reportCalls :: String -> Calls -> TerM ()
reportCalls String
no Calls
calls = do
  cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff

  -- We work in TCM exclusively.
  liftTCM $ do

    reportS "term.lex" 20
      [ "Calls (" ++ no ++ "dot patterns): " ++ prettyShow calls
      ]

    -- Print the whole completion phase.
    verboseS "term.matrices" 40 $ do
      let header String
s = [String] -> String
unlines
            [ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
'='
            , Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
k Char
'=' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
k' Char
'='
            , Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
'='
            ]
            where n :: Int
n  = Int
70
                  r :: Int
r  = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s
                  k :: Int
k  = Int
r Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
                  k' :: Int
k' = Int
r Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
      let report String
s a
cs = String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.matrices" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text   (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String -> String
header String
s
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ a -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
cs
            ]
          cs0     = Calls
calls
          step Calls
cs = do
            let (Calls
new, Calls
cs') = Calls -> Calls -> (Calls, Calls)
forall cinfo.
(?cutoff::CutOff, Monoid cinfo) =>
CallGraph cinfo
-> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
completionStep Calls
cs0 Calls
cs
            String -> Calls -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, Pretty a) =>
String -> a -> m ()
report String
" New call matrices " Calls
new
            Either () Calls -> TCMT IO (Either () Calls)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either () Calls -> TCMT IO (Either () Calls))
-> Either () Calls -> TCMT IO (Either () Calls)
forall a b. (a -> b) -> a -> b
$ if Calls -> Bool
forall a. Null a => a -> Bool
null Calls
new then () -> Either () Calls
forall a b. a -> Either a b
Left () else Calls -> Either () Calls
forall a b. b -> Either a b
Right Calls
cs'
      report " Initial call matrices " cs0
      trampolineM step cs0

    -- Print the result of completion.
    let calls' = Calls -> Calls
forall cinfo.
(?cutoff::CutOff, Monoid cinfo) =>
CallGraph cinfo -> CallGraph cinfo
CallGraph.complete Calls
calls
        idems = (CallMatrixAug CallPath -> Bool)
-> [CallMatrixAug CallPath] -> [CallMatrixAug CallPath]
forall a. (a -> Bool) -> [a] -> [a]
filter CallMatrixAug CallPath -> Bool
forall cinfo. (?cutoff::CutOff) => CallMatrixAug cinfo -> Bool
idempotent ([CallMatrixAug CallPath] -> [CallMatrixAug CallPath])
-> [CallMatrixAug CallPath] -> [CallMatrixAug CallPath]
forall a b. (a -> b) -> a -> b
$ [Call CallPath] -> [CallMatrixAug CallPath]
forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
endos ([Call CallPath] -> [CallMatrixAug CallPath])
-> [Call CallPath] -> [CallMatrixAug CallPath]
forall a b. (a -> b) -> a -> b
$ Calls -> [Call CallPath]
forall cinfo. CallGraph cinfo -> [Call cinfo]
CallGraph.toList Calls
calls'
    -- TODO
    -- reportSDoc "term.behaviours" 20 $ vcat
    --   [ text $ "Recursion behaviours (" ++ no ++ "dot patterns):"
    --   , nest 2 $ return $ Term.prettyBehaviour calls'
    --   ]
    reportSDoc "term.matrices" 30 $ vcat
      [ text $ "Idempotent call matrices (" ++ no ++ "dot patterns):\n"
      , nest 2 $ vcat $ punctuate "\n" $ map pretty idems
      ]
    -- reportSDoc "term.matrices" 30 $ vcat
    --   [ text $ "Other call matrices (" ++ no ++ "dot patterns):"
    --   , nest 2 $ pretty $ CallGraph.fromList others
    --   ]
    return ()

-- | @termFunction name@ checks @name@ for termination.
-- If it passes the termination check it is marked as "terminates" in the signature.

termFunction :: QName -> TerM Result
termFunction :: QName -> TerM Result
termFunction QName
name = QName -> (Definition -> TerM Result) -> TerM Result
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
name ((Definition -> TerM Result) -> TerM Result)
-> (Definition -> TerM Result) -> TerM Result
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do

  -- Function @name@ is henceforth referred to by its @index@
  -- in the list of @allNames@ of the mutual block.

  allNames <- TerM (Set QName)
terGetMutual
  let index = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ QName -> Set QName -> Maybe Int
forall a. Ord a => a -> Set a -> Maybe Int
Set.lookupIndex QName
name Set QName
allNames

  -- Retrieve the target type of the function to check.
  -- #4256: Don't use typeOfConst (which instantiates type with module params), since termination
  -- checking is running in the empty context, but with the current module unchanged.
  target <- case theDef def of
    -- We are termination-checking a record (calls to record will not be guarding):
    Record{} -> Target -> TerM Target
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Target
TargetRecord
    -- We are termination-checking a definition:
    Defn
_ -> Type -> TerM (Maybe QName)
forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm (Maybe QName)
typeEndsInDef (Definition -> Type
defType Definition
def) TerM (Maybe QName) -> (Maybe QName -> Target) -> TerM Target
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
           Just QName
d  -> QName -> Target
TargetDef QName
d
           Maybe QName
Nothing -> Target
TargetOther
  reportTarget target
  terSetTarget target $ do

    -- Collect the recursive calls in the block which (transitively)
    -- involve @name@,
    -- taking the target of @name@ into account for computing guardedness.

    let collect = (((Set Int, Set Int, Calls)
 -> TerM (Either Calls (Set Int, Set Int, Calls)))
-> (Set Int, Set Int, Calls) -> TerM Calls
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Either b a)) -> a -> m b
`trampolineM` (Int -> Set Int
forall a. a -> Set a
Set.singleton Int
index, Set Int
forall a. Monoid a => a
mempty, Calls
forall a. Monoid a => a
mempty)) (((Set Int, Set Int, Calls)
  -> TerM (Either Calls (Set Int, Set Int, Calls)))
 -> TerM Calls)
-> ((Set Int, Set Int, Calls)
    -> TerM (Either Calls (Set Int, Set Int, Calls)))
-> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ (Set Int
todo, Set Int
done, Calls
calls) -> do
          if Set Int -> Bool
forall a. Null a => a -> Bool
null Set Int
todo then Either Calls (Set Int, Set Int, Calls)
-> TerM (Either Calls (Set Int, Set Int, Calls))
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Calls (Set Int, Set Int, Calls)
 -> TerM (Either Calls (Set Int, Set Int, Calls)))
-> Either Calls (Set Int, Set Int, Calls)
-> TerM (Either Calls (Set Int, Set Int, Calls))
forall a b. (a -> b) -> a -> b
$ Calls -> Either Calls (Set Int, Set Int, Calls)
forall a b. a -> Either a b
Left Calls
calls else do
            -- Extract calls originating from indices in @todo@.
            new <- Set Int -> (Int -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' Set Int
todo ((Int -> TerM Calls) -> TerM Calls)
-> (Int -> TerM Calls) -> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ Int
i ->
              QName -> TerM Calls
termDef (QName -> TerM Calls) -> QName -> TerM Calls
forall a b. (a -> b) -> a -> b
$
              if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Set QName -> Int
forall a. Set a -> Int
Set.size Set QName
allNames
              then QName
forall a. HasCallStack => a
__IMPOSSIBLE__
              else Int -> Set QName -> QName
forall a. Int -> Set a -> a
Set.elemAt Int
i Set QName
allNames
            -- Mark those functions as processed and add the calls to the result.
            let done'  = Set Int
done Set Int -> Set Int -> Set Int
forall a. Monoid a => a -> a -> a
`mappend` Set Int
todo
                calls' = Calls
new  Calls -> Calls -> Calls
forall a. Monoid a => a -> a -> a
`mappend` Calls
calls
            -- Compute the new todo list:
                todo' = Calls -> Set Int
forall cinfo. CallGraph cinfo -> Set Int
CallGraph.targetNodes Calls
new Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Int
done'
            -- Jump the trampoline.
            return $ Right (todo', done', calls')

    -- First try to termination check ignoring the dot patterns
    calls1 <- terSetUseDotPatterns False $ collect
    reportCalls "no " calls1

    r <- do
     cutoff <- terGetCutOff
     let ?cutoff = cutoff
     r <- billToTerGraph $ Term.terminatesFilter (== index) calls1

     -- Andrea: 22/04/2020.
     -- With cubical we will always have a clause where the dot
     -- patterns are instead replaced with a variable, so they
     -- cannot be relied on for termination.
     -- See issue #4606 for a counterexample involving HITs.
     --
     -- Without the presence of HITs I conjecture that dot patterns
     -- could be turned into actual splits, because no-confusion
     -- would make the other cases impossible, so I do not disable
     -- this for --without-K entirely.
     --
     -- Andreas, 2022-03-21: The check for --cubical was missing here.
     ifM (isJust <$> cubicalOption) (return r) {- else -} $ case r of
       Right () -> Either CallPath () -> TerM (Either CallPath ())
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either CallPath () -> TerM (Either CallPath ()))
-> Either CallPath () -> TerM (Either CallPath ())
forall a b. (a -> b) -> a -> b
$ () -> Either CallPath ()
forall a b. b -> Either a b
Right ()
       Left{}   -> do
         -- Try again, but include the dot patterns this time.
         calls2 <- Bool -> TerM Calls -> TerM Calls
forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
True (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ TerM Calls
collect
         reportCalls "" calls2
         billToTerGraph $ Term.terminatesFilter (== index) calls2

    names <- terGetUserNames
    case mapLeft callInfos r of

      Left [CallInfo]
calls -> do
        -- Mark as non-terminating.
        QName -> Bool -> TerM ()
forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
name Bool
False

        -- Functions must be terminating, records types need not...
        case Definition -> Defn
theDef Definition
def of

          -- Records need not terminate, so we just put the error on the debug log.
          Record{} -> do
            String -> Int -> TCMT IO Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.warn.no" Int
10 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
              [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCMT IO Doc
"Record type", 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
"does not termination check.", TCMT IO Doc
"Problematic calls:" ] TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
:
              (CallInfo -> TCMT IO Doc) -> [CallInfo] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc)
-> (CallInfo -> TCMT IO Doc) -> CallInfo -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallInfo -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CallInfo -> m Doc
prettyTCM) ((CallInfo -> Range) -> [CallInfo] -> [CallInfo]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn CallInfo -> Range
forall a. HasRange a => a -> Range
getRange [CallInfo]
calls)
            TerM Result
forall a. Monoid a => a
mempty

          -- Functions must terminate, so we report the error.
          Defn
_ -> do
            let err :: TerminationError
err = [QName] -> [CallInfo] -> TerminationError
TerminationError [QName
name | QName
name QName -> Set QName -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
names] [CallInfo]
calls
            Result -> TerM Result
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> TerM Result) -> Result -> TerM Result
forall a b. (a -> b) -> a -> b
$ TerminationError -> Result
forall el coll. Singleton el coll => el -> coll
singleton TerminationError
err

      Right () -> do
        String -> Int -> String -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.warn.yes" Int
2 (String -> TerM ()) -> String -> TerM ()
forall a b. (a -> b) -> a -> b
$
          QName -> String
forall a. Pretty a => a -> String
prettyShow QName
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does termination check"
        QName -> Bool -> TerM ()
forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
name Bool
True
        Result -> TerM Result
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
   where
     reportTarget :: MonadDebug m => Target -> m ()
     reportTarget :: forall (m :: * -> *). MonadDebug m => Target -> m ()
reportTarget Target
tgt = String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.target" Int
20 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ (String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
       case Target
tgt of
         Target
TargetRecord -> String
"termination checking a record type"
         TargetDef QName
q  -> [String] -> String
unwords [ String
"target type ends in", QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q ]
         Target
TargetOther  -> String
"target type not recognized"

-- | To process the target type.
typeEndsInDef :: MonadTCM tcm => Type -> tcm (Maybe QName)
typeEndsInDef :: forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm (Maybe QName)
typeEndsInDef Type
t = TCM (Maybe QName) -> tcm (Maybe QName)
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe QName) -> tcm (Maybe QName))
-> TCM (Maybe QName) -> tcm (Maybe QName)
forall a b. (a -> b) -> a -> b
$ do
  TelV _ core <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
  case unEl core of
    Def QName
d Elims
vs -> Maybe QName -> TCM (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> TCM (Maybe QName))
-> Maybe QName -> TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d
    Term
_        -> Maybe QName -> TCM (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing

-- | Termination check a definition by pattern matching.
--
--   TODO: Refactor!
--   As this function may be called twice,
--   once disregarding dot patterns,
--   the second time regarding dot patterns,
--   it is better if we separated bare call extraction
--   from computing the change in structural order.
--   Only the latter depends on the choice whether we
--   consider dot patterns or not.
termDef :: QName -> TerM Calls
termDef :: QName -> TerM Calls
termDef QName
name = QName -> TerM Calls -> TerM Calls
forall a. QName -> TerM a -> TerM a
terSetCurrent QName
name (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> TerM Calls) -> TerM Calls
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
name ((Definition -> TerM Calls) -> TerM Calls)
-> (Definition -> TerM Calls) -> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do

 -- Skip calls to record types unless we are checking a record type in the first place.
 let isRecord_ :: Bool
isRecord_ = case Definition -> Defn
theDef Definition
def of { Record{} -> Bool
True; Defn
_ -> Bool
False }
 let notTargetRecord :: TerM Bool
notTargetRecord = TerM Target
terGetTarget TerM Target -> (Target -> Bool) -> TerM Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
       Target
TargetRecord -> Bool
False
       Target
_ -> Bool
True
 TerM Bool -> TerM Calls -> TerM Calls -> TerM Calls
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> TerM Bool
forall a. a -> TerM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
isRecord_ TerM Bool -> TerM Bool -> TerM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` TerM Bool
notTargetRecord) TerM Calls
forall a. Monoid a => a
mempty {-else-} (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do

  -- Retrieve definition
  let t :: Type
t = Definition -> Type
defType Definition
def

  TCMT IO () -> TerM ()
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.def.fun" Int
5 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"termination checking type of" 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
name
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        ]

  Type -> TerM Calls
termType Type
t TerM Calls -> TerM Calls -> TerM Calls
forall a. Monoid a => a -> a -> a
`mappend` do

  TCMT IO () -> TerM ()
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.def.fun" Int
5 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"termination checking body of" 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
name
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        ]

  -- If --without-K, we disregard all arguments (and result)
  -- which are not of data or record type.

  withoutKEnabled <- TCMT IO Bool -> TerM Bool
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
  applyWhen withoutKEnabled (setMasks t) $ do

    -- If the result should be disregarded, set all calls to unguarded.
    applyWhenM terGetMaskResult terUnguarded $ do

      case theDef def of
        Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls  } -> [Clause] -> (Clause -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' [Clause]
cls ((Clause -> TerM Calls) -> TerM Calls)
-> (Clause -> TerM Calls) -> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ Clause
cl -> do
          if NAPs -> Bool
hasDefP (Clause -> NAPs
namedClausePats Clause
cl) -- generated hcomp clause, should be safe.
                                          -- TODO find proper strategy.
            then Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
            else Clause -> TerM Calls
termClause Clause
cl

        -- @record R pars : Set where field tel@
        -- is treated like function @R pars = tel@.
        Record{ Int
recPars :: Int
recPars :: Defn -> Int
recPars, Telescope
recTel :: Telescope
recTel :: Defn -> Telescope
recTel } -> Int -> Telescope -> TerM Calls
termRecTel Int
recPars Telescope
recTel

        Defn
_ -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty

-- | Extract "calls" to the field types from a record constructor telescope.
-- Does not extract from the parameters, but treats these as the "pattern variables"
-- (the lhs of the "function").
termRecTel :: Nat -> Telescope -> TerM Calls
termRecTel :: Int -> Telescope -> TerM Calls
termRecTel Int
npars Telescope
tel = do
  -- Set up the record parameters like function parameters.
  let ([Dom (String, Type)]
pars, [Dom (String, Type)]
fields) = Int
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
npars ([Dom (String, Type)]
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
  [Dom (String, Type)] -> TerM Calls -> TerM Calls
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
[Dom (String, Type)] -> m a -> m a
addContext [Dom (String, Type)]
pars (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do
    ps <- Int -> TerM MaskedDeBruijnPatterns
forall {f :: * -> *}.
MonadTCEnv f =>
Int -> f MaskedDeBruijnPatterns
mkPats Int
npars
    terSetPatterns ps $ terSetSizeDepth pars $ do
      -- Treat the record fields like the body of a function.
      extract $ telFromList fields
  where
  -- create n variable patterns
  mkPats :: Int -> f MaskedDeBruijnPatterns
mkPats Int
n  = (Int -> Name -> Masked DeBruijnPattern)
-> [Int] -> [Name] -> MaskedDeBruijnPatterns
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Name -> Masked DeBruijnPattern
forall {a}. Pretty a => Int -> a -> Masked DeBruijnPattern
mkPat (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) ([Name] -> MaskedDeBruijnPatterns)
-> f [Name] -> f MaskedDeBruijnPatterns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f [Name]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  mkPat :: Int -> a -> Masked DeBruijnPattern
mkPat Int
i a
x = DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ String -> Int -> DBPatVar
DBPatVar (a -> String
forall a. Pretty a => a -> String
prettyShow a
x) Int
i

-- | Collect calls in type signature @f : (x1:A1)...(xn:An) -> B@.
--   It is treated as if there were the additional function clauses.
--   @@
--      f = A1
--      f x1 = A2
--      f x1 x2 = A3
--      ...
--      f x1 ... xn = B
--   @@

termType :: Type -> TerM Calls
termType :: Type -> TerM Calls
termType = TerM Calls -> Type -> TerM Calls
forall a. a -> Type -> a
forall (m :: * -> *) a. Monad m => a -> m a
return TerM Calls
forall a. Monoid a => a
mempty
-- termType = loop 0  -- Andreas, 2019-04-10 deactivate for backwards-compatibility in 2.6.0 #1556
  where
  loop :: Int -> Type -> TerM Calls
loop Int
n Type
t = do
    ps <- Int -> TerM MaskedDeBruijnPatterns
forall {f :: * -> *}.
MonadTCEnv f =>
Int -> f MaskedDeBruijnPatterns
mkPats Int
n
    reportSDoc "term.type" 60 $ vcat
      [ text $ "termType " ++ show n ++ " with " ++ show (length ps) ++ " patterns"
      , nest 2 $ "looking at type " <+> prettyTCM t
      ]
    tel <- getContextTelescope  -- Andreas, 2018-11-15, issue #3394, forgotten initialization of terSizeDepth
    terSetPatterns ps $ terSetSizeDepth tel $ do
      ifNotPiType t {-then-} extract {-else-} $ \ Dom' Term Type
dom Abs Type
absB -> do
        Dom' Term Type -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Dom' Term Type
dom TerM Calls -> TerM Calls -> TerM Calls
forall a. Monoid a => a -> a -> a
`mappend` Dom' Term Type -> Abs Type -> (Type -> TerM Calls) -> TerM Calls
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom' Term Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom' Term Type
dom Abs Type
absB (Int -> Type -> TerM Calls
loop (Int -> Type -> TerM Calls) -> Int -> Type -> TerM Calls
forall a b. (a -> b) -> a -> b
$! Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

  -- create n variable patterns
  mkPats :: Int -> f MaskedDeBruijnPatterns
mkPats Int
n  = (Int -> Name -> Masked DeBruijnPattern)
-> [Int] -> [Name] -> MaskedDeBruijnPatterns
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Name -> Masked DeBruijnPattern
forall {a}. Pretty a => Int -> a -> Masked DeBruijnPattern
mkPat (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) ([Name] -> MaskedDeBruijnPatterns)
-> f [Name] -> f MaskedDeBruijnPatterns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f [Name]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  mkPat :: Int -> a -> Masked DeBruijnPattern
mkPat Int
i a
x = DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ String -> Int -> DBPatVar
DBPatVar (a -> String
forall a. Pretty a => a -> String
prettyShow a
x) Int
i

-- | Mask arguments and result for termination checking
--   according to type of function.
--   Only arguments of types ending in data/record or Size are counted in.
setMasks :: Type -> TerM a -> TerM a
setMasks :: forall a. Type -> TerM a -> TerM a
setMasks Type
t TerM a
cont = do
  (ds, d) <- TCM ([Bool], Bool) -> TerM ([Bool], Bool)
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM ([Bool], Bool) -> TerM ([Bool], Bool))
-> TCM ([Bool], Bool) -> TerM ([Bool], Bool)
forall a b. (a -> b) -> a -> b
$ do
    TelV tel core <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
    -- Check argument types
    ds <- checkArgumentTypes tel
    -- Check result types
    d  <- addContext tel $ isNothing <.> isDataOrRecord . unEl $ core
    when d $
      reportSLn "term.mask" 20 $ "result type is not data or record type, ignoring guardedness for --without-K"
    return (ds, d)
  terSetMaskArgs (ds ++ repeat True) $ terSetMaskResult d $ cont

  where
    checkArgumentTypes :: Telescope -> TCM [Bool]
    checkArgumentTypes :: Telescope -> TCM [Bool]
checkArgumentTypes Telescope
EmptyTel = [Bool] -> TCM [Bool]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    checkArgumentTypes (ExtendTel Dom' Term Type
dom Abs Telescope
atel) = do
      TelV tel2 t <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
dom
      d <- addContext tel2 $
        (isNothing <$> isDataOrRecord (unEl t)) `or2M` (isJust <$> isSizeType t)
      when d $
        reportSDoc "term.mask" 20 $ do
          "argument type "
            <+> prettyTCM t
            <+> " is not data or record type, ignoring structural descent for --without-K"
      underAbstraction dom atel $ \Telescope
tel -> (Bool
dBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) ([Bool] -> [Bool]) -> TCM [Bool] -> TCM [Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> TCM [Bool]
checkArgumentTypes Telescope
tel

-- | Is the current target type among the given ones?

targetElem :: [QName] -> TerM Bool
targetElem :: [QName] -> TerM Bool
targetElem [QName]
ds = TerM Target
terGetTarget TerM Target -> (Target -> Bool) -> TerM Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
  TargetDef QName
d  -> QName
d QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
ds
  Target
TargetRecord -> Bool
False
  Target
TargetOther  -> Bool
False


-- | Convert a term (from a dot pattern) to a DeBruijn pattern.
--
--   The term is first normalized and stripped of all non-coinductive projections.

termToDBP :: Term -> TerM DeBruijnPattern
termToDBP :: Term -> TerM DeBruijnPattern
termToDBP Term
t =
  Term -> TerM DeBruijnPattern
forall a b. TermToPattern a b => a -> TerM b
termToPattern (Term -> TerM DeBruijnPattern) -> TerM Term -> TerM DeBruijnPattern
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do TCM Term -> TerM Term
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
t

-- | Convert a term (from a dot pattern) to a pattern for the purposes of the termination checker.
--
--   @SIZESUC@ is treated as a constructor.

class TermToPattern a b where
  termToPattern :: a -> TerM b

  default termToPattern :: (TermToPattern a' b', Traversable f, a ~ f a', b ~ f b') => a -> TerM b
  termToPattern = (a' -> TerM b') -> f a' -> TerM (f b')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse a' -> TerM b'
forall a b. TermToPattern a b => a -> TerM b
termToPattern

instance TermToPattern a b => TermToPattern [a] [b] where
instance TermToPattern a b => TermToPattern (Arg a) (Arg b) where
instance TermToPattern a b => TermToPattern (Named c a) (Named c b) where

-- OVERLAPPING
-- instance TermToPattern a b => TermToPattern a (Named c b) where
--   termToPattern t = unnamed <$> termToPattern t

instance TermToPattern Term DeBruijnPattern where
  termToPattern :: Term -> TerM DeBruijnPattern
termToPattern Term
t = TCM Term -> TerM Term
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (Term -> TCM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
t) TerM Term -> (Term -> TerM DeBruijnPattern) -> TerM DeBruijnPattern
forall a b. TerM a -> (a -> TerM b) -> TerM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    -- Constructors.
    Con ConHead
c ConInfo
_ Elims
args -> ConHead -> TerM DeBruijnPattern -> TerM DeBruijnPattern
ifDotPatsOrRecord ConHead
c (TerM DeBruijnPattern -> TerM DeBruijnPattern)
-> TerM DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
      ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo (NAPs -> DeBruijnPattern)
-> ([Arg DeBruijnPattern] -> NAPs)
-> [Arg DeBruijnPattern]
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg DeBruijnPattern -> Arg (Named_ DeBruijnPattern))
-> [Arg DeBruijnPattern] -> NAPs
forall a b. (a -> b) -> [a] -> [b]
map ((DeBruijnPattern -> Named_ DeBruijnPattern)
-> Arg DeBruijnPattern -> Arg (Named_ DeBruijnPattern)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Named_ DeBruijnPattern
forall a name. a -> Named name a
unnamed) ([Arg DeBruijnPattern] -> DeBruijnPattern)
-> TerM [Arg DeBruijnPattern] -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TerM [Arg DeBruijnPattern]
forall a b. TermToPattern a b => a -> TerM b
termToPattern ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
args)
    Def QName
s [Apply Arg Term
arg] -> TerM DeBruijnPattern -> TerM DeBruijnPattern
ifDotPats (TerM DeBruijnPattern -> TerM DeBruijnPattern)
-> TerM DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ do
      suc <- TerM (Maybe QName)
terGetSizeSuc
      if Just s == suc then ConP (ConHead s IsData Inductive []) noConPatternInfo . map (fmap unnamed) <$> termToPattern [arg]
       else fallback
    DontCare Term
t  -> Term -> TerM DeBruijnPattern
forall a b. TermToPattern a b => a -> TerM b
termToPattern Term
t -- OR: __IMPOSSIBLE__  -- removed by stripAllProjections
    -- Leaves.
    Var Int
i []    -> DBPatVar -> DeBruijnPattern
forall a. a -> Pattern' a
varP (DBPatVar -> DeBruijnPattern)
-> (Name -> DBPatVar) -> Name -> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Int -> DBPatVar
`DBPatVar` Int
i) (String -> DBPatVar) -> (Name -> String) -> Name -> DBPatVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> DeBruijnPattern) -> TerM Name -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TerM Name
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV Int
i
    Lit Literal
l       -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> TerM DeBruijnPattern)
-> DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Literal -> DeBruijnPattern
forall a. Literal -> Pattern' a
litP Literal
l
    Dummy String
s Elims
_   -> String -> TerM DeBruijnPattern
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s
    Term
t           -> TerM DeBruijnPattern
fallback
    where
    -- Andreas, 2022-06-14, issues #5953 and #4725
    -- Recognize variable and record patterns in dot patterns regardless
    -- of whether dot-pattern termination is on.
    ifDotPats :: TerM DeBruijnPattern -> TerM DeBruijnPattern
ifDotPats           = TerM Bool
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TerM Bool
terGetUseDotPatterns TerM DeBruijnPattern
fallback
    ifDotPatsOrRecord :: ConHead -> TerM DeBruijnPattern -> TerM DeBruijnPattern
ifDotPatsOrRecord ConHead
c = TerM Bool
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> TerM Bool
forall a. a -> TerM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataOrRecord
forall p. DataOrRecord' p
IsData DataOrRecord -> DataOrRecord -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> DataOrRecord
conDataRecord ConHead
c) TerM Bool -> TerM Bool -> TerM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do Bool -> Bool
not (Bool -> Bool) -> TerM Bool -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM Bool
terGetUseDotPatterns) TerM DeBruijnPattern
fallback
    fallback :: TerM DeBruijnPattern
fallback            = DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> TerM DeBruijnPattern)
-> DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Term
t

-- | Masks all non-data/record type patterns if --without-K.
--   See issue #1023.
maskNonDataArgs :: [DeBruijnPattern] -> TerM [Masked DeBruijnPattern]
maskNonDataArgs :: [DeBruijnPattern] -> TerM MaskedDeBruijnPatterns
maskNonDataArgs [DeBruijnPattern]
ps = (DeBruijnPattern -> Bool -> Masked DeBruijnPattern)
-> [DeBruijnPattern] -> [Bool] -> MaskedDeBruijnPatterns
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DeBruijnPattern -> Bool -> Masked DeBruijnPattern
forall {x}. Pattern' x -> Bool -> Masked (Pattern' x)
mask [DeBruijnPattern]
ps ([Bool] -> MaskedDeBruijnPatterns)
-> TerM [Bool] -> TerM MaskedDeBruijnPatterns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM [Bool]
terGetMaskArgs
  where
    mask :: Pattern' x -> Bool -> Masked (Pattern' x)
mask p :: Pattern' x
p@ProjP{} Bool
_ = Bool -> Pattern' x -> Masked (Pattern' x)
forall a. Bool -> a -> Masked a
Masked Bool
False Pattern' x
p
    mask Pattern' x
p         Bool
d = Bool -> Pattern' x -> Masked (Pattern' x)
forall a. Bool -> a -> Masked a
Masked Bool
d     Pattern' x
p

-- | Drop elements of the list which correspond to arguments forced by
-- the constructor with the given QName.
mapForcedArguments :: QName -> [a] -> (IsForced -> a -> Maybe b) -> TerM [b]
mapForcedArguments :: forall a b. QName -> [a] -> (IsForced -> a -> Maybe b) -> TerM [b]
mapForcedArguments QName
c [a]
xs IsForced -> a -> Maybe b
k = do
  forcedArgs <- QName -> TerM [IsForced]
forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
getForcedArgs QName
c
  let go [IsForced]
xs (a
p:[a]
ps) = do
        let (IsForced
f, [IsForced]
xs') = [IsForced] -> (IsForced, [IsForced])
nextIsForced [IsForced]
xs
        case IsForced -> a -> Maybe b
k IsForced
f a
p of
          Just b
b  -> b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[IsForced] -> [a] -> [b]
go [IsForced]
xs' [a]
ps
          Maybe b
Nothing -> [IsForced] -> [a] -> [b]
go [IsForced]
xs' [a]
ps
      go [IsForced]
_ [] = []
  pure $ go forcedArgs xs

-- | Extract recursive calls from one clause.
termClause :: Clause -> TerM Calls
termClause :: Clause -> TerM Calls
termClause Clause
clause = do
  Clause{ clauseTel = tel, namedClausePats = ps, clauseBody = body } <- Clause -> TerM Clause
forall (tcm :: * -> *). MonadTCM tcm => Clause -> tcm Clause
etaExpandClause Clause
clause
  liftTCM $ reportSDoc "term.check.clause" 25 $ vcat
    [ "termClause"
    , nest 2 $ "tel =" <+> prettyTCM tel
    , nest 2 $ "ps  =" <+> do addContext tel $ prettyTCMPatternList ps
    ]
  forM' body $ \ Term
v -> Telescope -> TerM Calls -> TerM Calls
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do
    -- TODO: combine the following two traversals, avoid full normalisation.
    -- Parse dot patterns as patterns as far as possible.
    ps <- (DeBruijnPattern -> TerM DeBruijnPattern) -> NAPs -> TerM NAPs
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM DeBruijnPattern -> TerM DeBruijnPattern
parseDotP NAPs
ps
    -- Blank out coconstructors.
    ps <- preTraversePatternM stripCoCon ps
    -- Mask non-data arguments.
    mdbpats <- maskNonDataArgs $ map namedArg ps
    terSetPatterns mdbpats $ do
      terSetSizeDepth tel $ do
        reportBody v
        extract v

  where
    parseDotP :: DeBruijnPattern -> TerM DeBruijnPattern
parseDotP = \case
      DotP PatternInfo
o Term
t -> Term -> TerM DeBruijnPattern
termToDBP Term
t
      DeBruijnPattern
p        -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
    stripCoCon :: DeBruijnPattern -> TerM DeBruijnPattern
stripCoCon = \case
      ConP (ConHead QName
c DataOrRecord
_ Induction
CoInductive [Arg QName]
_) ConPatternInfo
_ NAPs
_ -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
unusedVar
      DeBruijnPattern
p -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
    reportBody :: Term -> TerM ()
    reportBody :: Term -> TerM ()
reportBody Term
v = String -> Int -> TerM () -> TerM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"term.check.clause" Int
6 (TerM () -> TerM ()) -> TerM () -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
      f       <- TerM QName
terGetCurrent
      pats    <- terGetPatterns
      liftTCM $ reportSDoc "term.check.clause" 6 $ do
        sep [ text ("termination checking clause of")
                <+> prettyTCM f
            , nest 2 $ "lhs:" <+> sep (map prettyTCM pats)
            , nest 2 $ "rhs:" <+> prettyTCM v
            ]


-- | Extract recursive calls from expressions.
class ExtractCalls a where
  extract :: a -> TerM Calls

instance ExtractCalls a => ExtractCalls (Abs a) where
  extract :: Abs a -> TerM Calls
extract (NoAbs String
_ a
a) = a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract a
a
  extract (Abs String
x a
a)   = String -> TerM Calls -> TerM Calls
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
addContext String
x (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ TerM Calls -> TerM Calls
forall a. TerM a -> TerM a
terRaise (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract a
a

instance ExtractCalls a => ExtractCalls (Arg a) where
  extract :: Arg a -> TerM Calls
extract = a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (a -> TerM Calls) -> (Arg a -> a) -> Arg a -> TerM Calls
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

instance ExtractCalls a => ExtractCalls (Dom a) where
  extract :: Dom a -> TerM Calls
extract = a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (a -> TerM Calls) -> (Dom a -> a) -> Dom a -> TerM Calls
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom a -> a
forall t e. Dom' t e -> e
unDom

instance ExtractCalls a => ExtractCalls (Elim' a) where
  extract :: Elim' a -> TerM Calls
extract Proj{}    = Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
  extract (Apply Arg a
a) = a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (a -> TerM Calls) -> a -> TerM Calls
forall a b. (a -> b) -> a -> b
$ Arg a -> a
forall e. Arg e -> e
unArg Arg a
a
  extract (IApply a
x a
y a
a) = (a, (a, a)) -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (a
x,(a
y,a
a)) -- TODO Andrea: conservative

instance ExtractCalls a => ExtractCalls [a] where
  extract :: [a] -> TerM Calls
extract = (a -> TerM Calls) -> [a] -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
(a -> m b) -> t a -> m b
mapM' a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract

instance (ExtractCalls a, ExtractCalls b) => ExtractCalls (a,b) where
  extract :: (a, b) -> TerM Calls
extract (a
a, b
b) = Calls -> Calls -> Calls
forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
CallGraph.union (Calls -> Calls -> Calls) -> TerM Calls -> TerM (Calls -> Calls)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract a
a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract b
b

instance (ExtractCalls a, ExtractCalls b, ExtractCalls c) => ExtractCalls (a,b,c) where
  extract :: (a, b, c) -> TerM Calls
extract (a
a, b
b, c
c) = (a, (b, c)) -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (a
a, (b
b, c
c))

-- | Sorts can contain arbitrary terms of type @Level@,
--   so look for recursive calls also in sorts.
--   Ideally, 'Sort' would not be its own datatype but just
--   a subgrammar of 'Term', then we would not need this boilerplate.

instance ExtractCalls Sort where
  extract :: Sort -> TerM Calls
extract Sort
s = do
    TCMT IO () -> TerM ()
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
      String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.sort" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"extracting calls from sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s
      String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.sort" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"s = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sort -> String
forall a. Show a => a -> String
show Sort
s)
    case Sort
s of
      Inf Univ
_ Integer
_    -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
      Sort
SizeUniv   -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
      Sort
LockUniv   -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
      Sort
LevelUniv  -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
      Sort
IntervalUniv -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
      Univ Univ
_ Level' Term
t       -> TerM Calls -> TerM Calls
forall a. TerM a -> TerM a
terUnguarded (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ Level' Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Level' Term
t  -- no guarded levels
      PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> (Dom' Term Term, Sort, Abs Sort) -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (Dom' Term Term
a, Sort
s1, Abs Sort
s2)
      FunSort Sort
s1 Sort
s2 -> (Sort, Sort) -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (Sort
s1, Sort
s2)
      UnivSort Sort
s -> Sort -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Sort
s
      MetaS MetaId
x Elims
es -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
      DefS QName
d Elims
es  -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
      DummyS{}   -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty

-- | Extract recursive calls from a type.

instance ExtractCalls Type where
  extract :: Type -> TerM Calls
extract (El Sort
s Term
t) = (Sort, Term) -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (Sort
s, Term
t)

instance ExtractCalls a => ExtractCalls (Tele a) where
  extract :: Tele a -> TerM Calls
extract = \case
    Tele a
EmptyTel        -> TerM Calls
forall a. Monoid a => a
mempty
    ExtendTel a
a Abs (Tele a)
tel -> a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract a
a TerM Calls -> TerM Calls -> TerM Calls
forall a. Semigroup a => a -> a -> a
<> Abs (Tele a) -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Abs (Tele a)
tel

-- | Extract recursive calls from a constructor application.

constructor
  :: QName
    -- ^ Constructor name.
  -> Induction
    -- ^ Should the constructor be treated as inductive or coinductive?
  -> [(Arg Term, Bool)]
    -- ^ All the arguments,
    --   and for every argument a boolean which is 'True' iff the
    --   argument should be viewed as preserving guardedness.
  -> TerM Calls
constructor :: QName -> Induction -> [(Arg Term, Bool)] -> TerM Calls
constructor QName
c Induction
ind [(Arg Term, Bool)]
args = do
  cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  forM' args $ \ (Arg Term
arg, Bool
preserves) -> do
    let g' :: Order -> Order
g' = case (Bool
preserves, Induction
ind) of
             (Bool
True,  Induction
Inductive)   -> Order -> Order
forall a. a -> a
id
             (Bool
True,  Induction
CoInductive) -> (Order
Order.lt (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
.*.)
             (Bool
False, Induction
_)           -> Order -> Order -> Order
forall a b. a -> b -> a
const Order
Order.unknown
    (Order -> Order) -> TerM Calls -> TerM Calls
forall a. (Order -> Order) -> TerM a -> TerM a
terModifyGuarded Order -> Order
g' (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ Arg Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Arg Term
arg

-- | Handles function applications @g es@.

function :: QName -> Elims -> TerM Calls
function :: QName -> Elims -> TerM Calls
function QName
g Elims
es0 = do

    f       <- TerM QName
terGetCurrent
    names   <- terGetMutual
    guarded <- terGetGuarded

    -- let gArgs = Def g es0
    liftTCM $ reportSDoc "term.function" 30 $
      "termination checking function call " <+> prettyTCM (Def g es0)

    -- First, look for calls in the arguments of the call gArgs.

    -- If the function is a projection but not for a coinductive record,
    -- then preserve guardedness for its principal argument.
    isProj <- isProjectionButNotCoinductive g
    let unguards = Order -> [Order]
forall a. a -> [a]
repeat Order
Order.unknown
    let guards = Bool -> ([Order] -> [Order]) -> [Order] -> [Order]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
isProj (Order
guarded Order -> [Order] -> [Order]
forall a. a -> [a] -> [a]
:) [Order]
unguards
    -- Collect calls in the arguments of this call.
    let args = (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall t. [Elim' t] -> [Arg t]
argsFromElims Elims
es0
    calls <- forM' (zip guards args) $ \ (Order
guard, Term
a) -> do
      Order -> TerM Calls -> TerM Calls
forall a. Order -> TerM a -> TerM a
terSetGuarded Order
guard (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Term
a

    -- Then, consider call gArgs itself.

    liftTCM $ reportSDoc "term.found.call" 20 $
      sep [ "found call from" <+> prettyTCM f
          , nest 2 $ "to" <+> prettyTCM g
          ]

    -- insert this call into the call list
    case Set.lookupIndex g names of

       -- call leads outside the mutual block and can be ignored
       Maybe Int
Nothing   -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
calls

       -- call is to one of the mutally recursive functions/record
       Just Int
gInd -> do
         cutoff <- TerM CutOff
terGetCutOff
         let ?cutoff = cutoff

         -- Andreas, 2017-02-14, issue #2458:
         -- If we have inlined with-functions, we could be illtyped,
         -- hence, do not reduce anything.
         -- Andreas, 2017-06-20 issue #2613:
         -- We still need to reduce constructors, even when with-inlining happened.
         es <- -- ifM terGetHaveInlinedWith (return es0) {-else-} $
           liftTCM $ forM es0 $
             -- 2017-09-09, re issue #2732
             -- The eta-contraction that was here does not seem necessary to make structural order
             -- comparison not having to worry about eta.
             -- Maybe we thought an eta redex could come from a meta instantiation.
             -- However, eta-contraction is already performed by instantiateFull.
             -- See test/Succeed/Issue2732-termination.agda.
             traverse reduceCon <=< instantiateFull

           -- 2017-05-16, issue #2403: Argument normalization is too expensive,
           -- even if we only expand non-recursive functions.
           -- Argument normalization TURNED OFF.
           -- liftTCM $ billTo [Benchmark.Termination, Benchmark.Reduce] $ do
           --  -- Andreas, 2017-01-13, issue #2403, normalize arguments for the structural ordering.
           --  -- Andreas, 2017-03-25, issue #2495, restrict this to non-recursive functions
           --  -- otherwise, the termination checking may run forever.
           --  reportSLn "term.reduce" 90 $ "normalizing call arguments"
           --  modifyAllowedReductions (List.\\ [UnconfirmedReductions,RecursiveReductions]) $
           --    forM es0 $ \ e -> do
           --      reportSDoc "term.reduce" 95 $ "normalizing " <+> prettyTCM e
           --      etaContract =<< normalise e

         -- Compute the call matrix.

         -- Andreas, 2014-03-26 only 6% of termination time for library test
         -- spent on call matrix generation
         (nrows, ncols, matrix) <- billTo [Benchmark.Termination, Benchmark.Compare] $
           compareArgs es

         -- Andreas, 2022-03-21, #5823:
         -- If we are "calling" a record type we are guarded unless the origin
         -- of the termination analysis is itself a record.
         -- This is because we usually do not "unfold" record types into their
         -- field telescope.  We only do so when trying to construct the
         -- unique inhabitant of record type (singleton analysis).
         -- In the latter case, a call to a record type is not guarding.
         guarded' <- isRecord g >>= \case
           Just{} -> TerM Target
terGetTarget TerM Target -> (Target -> TerM Order) -> TerM Order
forall a b. TerM a -> (a -> TerM b) -> TerM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
             Target
TargetRecord
               -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
guarded
             Target
_ -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Order
guarded (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
.*. Order
Order.lt)
                    -- guarding when we call a record and not termination checking a record
           Maybe RecordData
Nothing
             -- only a delayed definition can be guarded
             | Order -> Bool
Order.decreasing Order
guarded
               -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le
             | Bool
otherwise
               -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
guarded
         liftTCM $ reportSLn "term.guardedness" 20 $
           "composing with guardedness " ++ prettyShow guarded ++
           " counting as " ++ prettyShow guarded'
         let matrix' = (?cutoff::CutOff) => Order -> [[Order]] -> [[Order]]
Order -> [[Order]] -> [[Order]]
composeGuardedness Order
guarded' [[Order]]
matrix

         -- Andreas, 2013-04-26 FORBIDDINGLY expensive!
         -- This PrettyTCM QName cost 50% of the termination time for std-lib!!
         -- gPretty <-liftTCM $ billTo [Benchmark.Termination, Benchmark.Level] $
         --   render <$> prettyTCM g

         -- Andreas, 2013-05-19 as pointed out by Andrea Vezzosi,
         -- printing the call eagerly is forbiddingly expensive.
         -- So we build a closure such that we can print the call
         -- whenever we really need to.
         -- This saves 30s (12%) on the std-lib!
         -- Andreas, 2015-01-21 Issue 1410: Go to the module where g is defined
         -- otherwise its free variables with be prepended to the call
         -- in the error message.
         doc <- liftTCM $ withCurrentModule (qnameModule g) $ buildClosure $
           Def g $ List.dropWhileEnd ((Inserted ==) . getOrigin) es0
           -- Andreas, 2018-07-22, issue #3136
           -- Dropping only inserted arguments at the end, since
           -- dropping arguments in the middle might make the printer crash.
           -- Def g $ filter ((/= Inserted) . getOrigin) es0
           -- Andreas, 2017-01-05, issue #2376
           -- Remove arguments inserted by etaExpandClause.

         let src  = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ QName -> Set QName -> Maybe Int
forall a. Ord a => a -> Set a -> Maybe Int
Set.lookupIndex QName
f Set QName
names
             tgt  = Int
gInd
             cm   = Int -> Int -> [[Order]] -> CallMatrix
makeCM Int
ncols Int
nrows [[Order]]
matrix'
             info = DList CallInfo -> CallPath
CallPath (DList CallInfo -> CallPath) -> DList CallInfo -> CallPath
forall a b. (a -> b) -> a -> b
$ CallInfo -> DList CallInfo
forall el coll. Singleton el coll => el -> coll
singleton (CallInfo -> DList CallInfo) -> CallInfo -> DList CallInfo
forall a b. (a -> b) -> a -> b
$
                    CallInfo
                      { callInfoTarget :: QName
callInfoTarget = QName
g
                      , callInfoCall :: Closure Term
callInfoCall   = Closure Term
doc
                      }
         verboseS "term.kept.call" 5 $ do
           pats <- terGetPatterns
           reportSDoc "term.kept.call" 5 $ vcat
             [ "kept call from" <+> text (prettyShow f) <+> hsep (map prettyTCM pats)
             , nest 2 $ "to" <+> text (prettyShow g) <+>
                         hsep (map (parens . prettyTCM) args)
             , nest 2 $ "call matrix (with guardedness): "
             , nest 2 $ pretty cm
             ]
         return $ CallGraph.insert src tgt cm info calls

  where
    -- We have to reduce constructors in case they're reexported.
    -- Andreas, Issue 1530: constructors have to be reduced deep inside terms,
    -- thus, we need to use traverseTermM.
    reduceCon :: Term -> TCM Term
    reduceCon :: Term -> TCM Term
reduceCon = (Term -> TCM Term) -> Term -> TCM Term
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
traverseTermM ((Term -> TCM Term) -> Term -> TCM Term)
-> (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ \case
      Con ConHead
c ConInfo
ci Elims
vs -> (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
vs) (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci [])  -- make sure we don't reduce the arguments
      Term
t -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t


-- | Try to get rid of a function call targeting the current SCC
--   using a non-recursive clause.
--
--   This can help copattern definitions of dependent records.
tryReduceNonRecursiveClause
  :: QName                 -- ^ Function
  -> Elims                 -- ^ Arguments
  -> (Term -> TerM Calls)  -- ^ Continue here if we managed to reduce.
  -> TerM Calls            -- ^ Otherwise, continue here.
  -> TerM Calls
tryReduceNonRecursiveClause :: QName -> Elims -> (Term -> TerM Calls) -> TerM Calls -> TerM Calls
tryReduceNonRecursiveClause QName
g Elims
es Term -> TerM Calls
continue TerM Calls
fallback = do
  -- Andreas, 2020-02-06, re: issue #906
  let v0 :: Term
v0 = QName -> Elims -> Term
Def QName
g Elims
es
  String -> Int -> TCMT IO Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.reduce" Int
40 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Trying to reduce away call: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v0

  -- First, make sure the function is in the current SCC.
  TerM Bool -> TerM Calls -> TerM Calls -> TerM Calls
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> Set QName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem QName
g (Set QName -> Bool) -> TerM (Set QName) -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM (Set QName)
terGetMutual) TerM Calls
fallback {-else-} (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do
  String -> Int -> String -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.reduce" Int
40 (String -> TerM ()) -> String -> TerM ()
forall a b. (a -> b) -> a -> b
$ String
"This call is in the current SCC!"

  -- Then, collect its non-recursive clauses.
  cls <- TCM [Clause] -> TerM [Clause]
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [Clause] -> TerM [Clause]) -> TCM [Clause] -> TerM [Clause]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [Clause]
getNonRecursiveClauses QName
g
  reportSLn "term.reduce" 40 $ unwords [ "Function has", show (length cls), "non-recursive exact clauses"]
  reportSDoc "term.reduce" 80 $ vcat $ map (prettyTCM . NamedClause g True) cls
  reportSLn  "term.reduce" 80 . ("allowed reductions = " ++) . show . SmallSet.elems
    =<< asksTC envAllowedReductions

  -- Finally, try to reduce with the non-recursive clauses (and no rewrite rules).
  r <- liftTCM $ modifyAllowedReductions (SmallSet.delete UnconfirmedReductions) $
    runReduceM $ appDefE' g v0 cls [] (map notReduced es)
  case r of
    NoReduction{}    -> TerM Calls
fallback
    YesReduction Simplification
_ Term
v -> do
      String -> Int -> TCMT IO Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.reduce" Int
30 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"Termination checker: Successfully reduced away call:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v0
        ]
      String -> Int -> TerM () -> TerM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"term.reduce" Int
5 (TerM () -> TerM ()) -> TerM () -> TerM ()
forall a b. (a -> b) -> a -> b
$ String -> TerM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"termination-checker-reduced-nonrecursive-call"
      Term -> TerM Calls
continue Term
v

getNonRecursiveClauses :: QName -> TCM [Clause]
getNonRecursiveClauses :: QName -> TCM [Clause]
getNonRecursiveClauses QName
q =
  (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Bool -> Bool -> Bool)
-> (Clause -> Bool) -> (Clause -> Bool) -> Clause -> Bool
forall a b c.
(a -> b -> c) -> (Clause -> a) -> (Clause -> b) -> Clause -> c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) Clause -> Bool
nonrec Clause -> Bool
exact) ([Clause] -> [Clause])
-> (Definition -> [Clause]) -> Definition -> [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> [Clause]
defClauses (Definition -> [Clause]) -> TCMT IO Definition -> TCM [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  where
  nonrec :: Clause -> Bool
nonrec = Bool -> (Bool -> Bool) -> Maybe Bool -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Bool -> Bool
not (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseRecursive
  exact :: Clause -> Bool
exact  = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseExact

-- | Extract recursive calls from a term.

instance ExtractCalls Term where
  extract :: Term -> TerM Calls
extract Term
t = do
    String -> Int -> TCMT IO Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.check.term" Int
50 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO Doc
"looking for calls in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t

    -- Instantiate top-level MetaVar.
    Term -> TerM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
t TerM Term -> (Term -> TerM Calls) -> TerM Calls
forall a b. TerM a -> (a -> TerM b) -> TerM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

      -- Constructed value.
      Con ConHead{conName :: ConHead -> QName
conName = QName
c, conDataRecord :: ConHead -> DataOrRecord
conDataRecord = DataOrRecord
dataOrRec} ConInfo
_ Elims
es -> do
        let args :: [Arg Term]
args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        -- A constructor preserves the guardedness of all its arguments.
        -- Andreas, 2022-09-19, issue #6108:
        -- A higher constructor does not.  So check if there is an @IApply@ amoung @es@.
        let argsg :: [(Arg Term, Bool)]
argsg = [Arg Term] -> [Bool] -> [(Arg Term, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Arg Term]
args ([Bool] -> [(Arg Term, Bool)]) -> [Bool] -> [(Arg Term, Bool)]
forall a b. (a -> b) -> a -> b
$ Bool -> [Bool]
forall a. a -> [a]
repeat (Bool -> [Bool]) -> Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ (Elim -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim -> Bool
forall a. Elim' a -> Bool
isProperApplyElim Elims
es

        -- If we encounter a coinductive record constructor
        -- in a type mutual with the current target
        -- then we count it as guarding.
        let inductive :: TerM Induction
inductive   = Induction -> TerM Induction
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive    -- not guarding, but preserving
            coinductive :: TerM Induction
coinductive = Induction -> TerM Induction
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
CoInductive  -- guarding
        -- ♯ is guarding
        ind <- TerM Bool -> TerM Induction -> TerM Induction -> TerM Induction
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe QName -> Bool) -> TerM (Maybe QName) -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM (Maybe QName)
terGetSharp) TerM Induction
coinductive (TerM Induction -> TerM Induction)
-> TerM Induction -> TerM Induction
forall a b. (a -> b) -> a -> b
$ {-else-} do
          -- data constructors are not guarding
          if DataOrRecord
dataOrRec DataOrRecord -> DataOrRecord -> Bool
forall a. Eq a => a -> a -> Bool
== DataOrRecord
forall p. DataOrRecord' p
IsData then TerM Induction
inductive else do
          -- abstract constructors are not guarding
          TerM (Maybe (QName, RecordData))
-> TerM Induction
-> ((QName, RecordData) -> TerM Induction)
-> TerM Induction
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> TerM (Maybe (QName, RecordData))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
c) TerM Induction
inductive (((QName, RecordData) -> TerM Induction) -> TerM Induction)
-> ((QName, RecordData) -> TerM Induction) -> TerM Induction
forall a b. (a -> b) -> a -> b
$ \ (QName
q, RecordData
def) -> do
            String -> Int -> String -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.check.term" Int
50 (String -> TerM ()) -> String -> TerM ()
forall a b. (a -> b) -> a -> b
$ String
"constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has record type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q
            -- inductive record constructors are not guarding
            if RecordData -> Maybe Induction
_recInduction RecordData
def Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive then TerM Induction
inductive else do
            -- coinductive constructors unrelated to the mutually
            -- constructed inhabitants of coinductive types are not guarding
            TerM Bool -> TerM Induction -> TerM Induction -> TerM Induction
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([QName] -> TerM Bool
targetElem ([QName] -> TerM Bool)
-> (Maybe [QName] -> [QName]) -> Maybe [QName] -> TerM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName] -> Maybe [QName] -> [QName]
forall a. a -> Maybe a -> a
fromMaybe [QName]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [QName] -> TerM Bool) -> Maybe [QName] -> TerM Bool
forall a b. (a -> b) -> a -> b
$ RecordData -> Maybe [QName]
_recMutual RecordData
def)
               {-then-} TerM Induction
coinductive
               {-else-} TerM Induction
inductive
        constructor c ind argsg

      -- Function, data, or record type.
      Def QName
g Elims
es -> QName -> Elims -> (Term -> TerM Calls) -> TerM Calls -> TerM Calls
tryReduceNonRecursiveClause QName
g Elims
es Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> TerM Calls
function QName
g Elims
es

      -- Abstraction. Preserves guardedness.
      Lam ArgInfo
h Abs Term
b -> Abs Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Abs Term
b

      -- Neutral term. Destroys guardedness.
      Var Int
i Elims
es -> TerM Calls -> TerM Calls
forall a. TerM a -> TerM a
terUnguarded (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ Elims -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Elims
es

      -- Dependent function space.
      Pi Dom' Term Type
a (Abs String
x Type
b) ->
        Calls -> Calls -> Calls
forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
CallGraph.union (Calls -> Calls -> Calls) -> TerM Calls -> TerM (Calls -> Calls)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        Dom' Term Type -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Dom' Term Type
a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> do
          a <- Dom' Term Type -> TerM (Dom' Term Type)
forall (tcm :: * -> *).
MonadTCM tcm =>
Dom' Term Type -> tcm (Dom' Term Type)
maskSizeLt Dom' Term Type
a  -- OR: just do not add a to the context!
          addContext (x, a) $ terRaise $ extract b

      -- Non-dependent function space.
      Pi Dom' Term Type
a (NoAbs String
_ Type
b) ->
        Calls -> Calls -> Calls
forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
CallGraph.union (Calls -> Calls -> Calls) -> TerM Calls -> TerM (Calls -> Calls)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Type -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Dom' Term Type
a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Type
b

      -- Literal.
      Lit Literal
l -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty

      -- Sort.
      Sort Sort
s -> Sort -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Sort
s

      -- Unsolved metas are not considered termination problems, there
      -- will be a warning for them anyway.
      MetaV MetaId
x Elims
args -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty

      -- Erased and not-yet-erased proof.
      DontCare Term
t -> Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Term
t

      -- Level.
      Level Level' Term
l -> -- billTo [Benchmark.Termination, Benchmark.Level] $ do
        -- Andreas, 2014-03-26 Benchmark discontinued, < 0.3% spent on levels.
        Level' Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Level' Term
l

      -- Dummy.
      Dummy{} -> Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty

-- | Extract recursive calls from level expressions.

instance ExtractCalls Level where
  extract :: Level' Term -> TerM Calls
extract (Max Integer
n [PlusLevel' Term]
as) = [PlusLevel' Term] -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract [PlusLevel' Term]
as

instance ExtractCalls PlusLevel where
  extract :: PlusLevel' Term -> TerM Calls
extract (Plus Integer
n Term
l) = Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Term
l

-- | Rewrite type @tel -> Size< u@ to @tel -> Size@.
maskSizeLt :: MonadTCM tcm => Dom Type -> tcm (Dom Type)
maskSizeLt :: forall (tcm :: * -> *).
MonadTCM tcm =>
Dom' Term Type -> tcm (Dom' Term Type)
maskSizeLt !Dom' Term Type
dom = TCM (Dom' Term Type) -> tcm (Dom' Term Type)
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Dom' Term Type) -> tcm (Dom' Term Type))
-> TCM (Dom' Term Type) -> tcm (Dom' Term Type)
forall a b. (a -> b) -> a -> b
$ do
  let a :: Type
a = Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
dom
  (msize, msizelt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  case (msize, msizelt) of
    (Maybe QName
_ , Maybe QName
Nothing) -> Dom' Term Type -> TCM (Dom' Term Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Dom' Term Type
dom
    (Maybe QName
Nothing, Maybe QName
_)  -> TCM (Dom' Term Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Just QName
size, Just QName
sizelt) -> do
      TelV tel c <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
      case a of
        El Sort
s (Def QName
d [Elim
v]) | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt -> Dom' Term Type -> TCM (Dom' Term Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom' Term Type -> TCM (Dom' Term Type))
-> Dom' Term Type -> TCM (Dom' Term Type)
forall a b. (a -> b) -> a -> b
$
          Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
size []) Type -> Dom' Term Type -> Dom' Term Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom' Term Type
dom
        Type
_ -> Dom' Term Type -> TCM (Dom' Term Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Dom' Term Type
dom

{- | @compareArgs es@

     Compare the list of de Bruijn patterns (=parameters) @pats@
     with a list of arguments @es@ and create a call maxtrix
     with |es| rows and |pats| columns.

     The guardedness is the number of projection patterns in @pats@
     minus the number of projections in @es@.
 -}
compareArgs :: [Elim] -> TerM (Int, Int, [[Order]])
compareArgs :: Elims -> TerM (Int, Int, [[Order]])
compareArgs Elims
es = do
  pats <- TerM MaskedDeBruijnPatterns
terGetPatterns
  liftTCM $ reportSDoc "term.compareArgs" 90 $ vcat
    [ text $ "comparing " ++ show (length es) ++ " args to " ++ show (length pats) ++ " patterns"
    ]
  -- apats <- annotatePatsWithUseSizeLt pats
  -- reportSDoc "term.compare" 20 $
  --   "annotated patterns = " <+> sep (map prettyTCM apats)
  -- matrix <- forM es $ \ e -> forM apats $ \ (b, p) -> terSetUseSizeLt b $ compareElim e p
  matrix <- withUsableVars pats $ forM es $ \ Elim
e -> MaskedDeBruijnPatterns
-> (Masked DeBruijnPattern -> TerM Order) -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM MaskedDeBruijnPatterns
pats ((Masked DeBruijnPattern -> TerM Order) -> TerM [Order])
-> (Masked DeBruijnPattern -> TerM Order) -> TerM [Order]
forall a b. (a -> b) -> a -> b
$ \ Masked DeBruijnPattern
p -> Elim -> Masked DeBruijnPattern -> TerM Order
compareElim Elim
e Masked DeBruijnPattern
p

  -- Count the number of coinductive projection(pattern)s in caller and callee.
  -- Only recursive coinductive projections are eligible (Issue 1209).
  projsCaller <- length <$> do
    filterM (isCoinductiveProjection True) $ mapMaybe (fmap (headAmbQ . snd) . isProjP . getMasked) pats
  projsCallee <- length <$> do
    filterM (isCoinductiveProjection True) $ mapMaybe (fmap snd . isProjElim) es
  cutoff <- terGetCutOff
  let ?cutoff = cutoff
  useGuardedness <- liftTCM guardednessOption
  let guardedness =
        if Bool
useGuardedness
        then (?cutoff::CutOff) => Bool -> Int -> Order
Bool -> Int -> Order
decr Bool
True (Int -> Order) -> Int -> Order
forall a b. (a -> b) -> a -> b
$ Int
projsCaller Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
projsCallee
        else Order
Order.le
  liftTCM $ reportSDoc "term.guardedness" 30 $ sep
    [ "compareArgs:"
    , nest 2 $ text $ "projsCaller = " ++ prettyShow projsCaller
    , nest 2 $ text $ "projsCallee = " ++ prettyShow projsCallee
    , nest 2 $ text $ "guardedness of call: " ++ prettyShow guardedness
    ]
  return $ addGuardedness guardedness (size es, size pats, matrix)

-- | Traverse patterns from left to right.
--   When we come to a projection pattern,
--   switch usage of SIZELT constraints:
--   on, if coinductive,
--   off, if inductive.
--
--   UNUSED
--annotatePatsWithUseSizeLt :: [DeBruijnPattern] -> TerM [(Bool,DeBruijnPattern)]
--annotatePatsWithUseSizeLt = loop where
--  loop [] = return []
--  loop (p@(ProjP _ q) : pats) = ((False,p) :) <$> do projUseSizeLt q $ loop pats
--  loop (p : pats) = (\ b ps -> (b,p) : ps) <$> terGetUseSizeLt <*> loop pats


-- | @compareElim e dbpat@

compareElim :: Elim -> Masked DeBruijnPattern -> TerM Order
compareElim :: Elim -> Masked DeBruijnPattern -> TerM Order
compareElim Elim
e Masked DeBruijnPattern
p = do
  TCMT IO () -> TerM ()
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
    String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.compare" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"compareElim"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"e = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elim
e
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"p = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Masked DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Masked DeBruijnPattern -> m Doc
prettyTCM Masked DeBruijnPattern
p
      ]
    String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"term.compare" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"e = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Elim -> String
forall a. Show a => a -> String
show Elim
e
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"p = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Masked DeBruijnPattern -> String
forall a. Show a => a -> String
show Masked DeBruijnPattern
p
      ]
  case (Elim
e, Masked DeBruijnPattern -> DeBruijnPattern
forall a. Masked a -> a
getMasked Masked DeBruijnPattern
p) of
    (Proj ProjOrigin
_ QName
d, ProjP ProjOrigin
_ QName
d') -> do
      d  <- QName -> TerM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d
      d' <- getOriginalProjection d'
      o  <- compareProj d d'
      reportSDoc "term.compare" 30 $ sep
        [ text $ "comparing callee projection " ++ prettyShow d
        , text $ "against caller projection " ++ prettyShow d'
        , text $ "yields order " ++ prettyShow o
        ]
      return o
    (Proj{}, DeBruijnPattern
_)            -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
    (Apply{}, ProjP{})     -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
    (Apply Arg Term
arg, DeBruijnPattern
_)         -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg) Masked DeBruijnPattern
p
    -- TODO Andrea: making sense?
    (IApply{}, ProjP{})  -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
    (IApply Term
_ Term
_ Term
arg, DeBruijnPattern
_)    -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm Term
arg Masked DeBruijnPattern
p

-- | In dependent records, the types of later fields may depend on the
--   values of earlier fields.  Thus when defining an inhabitant of a
--   dependent record type such as Σ by copattern matching,
--   a recursive call eliminated by an earlier projection (proj₁) might
--   occur in the definition at a later projection (proj₂).
--   Thus, earlier projections are considered "smaller" when
--   comparing copattern spines.  This is an ok approximation
--   of the actual dependency order.
--   See issues 906, 942.
compareProj :: MonadTCM tcm => QName -> QName -> tcm Order
compareProj :: forall (tcm :: * -> *). MonadTCM tcm => QName -> QName -> tcm Order
compareProj QName
d QName
d'
  | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' = Order -> tcm Order
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le
  | Bool
otherwise = TCM Order -> tcm Order
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Order -> tcm Order) -> TCM Order -> tcm Order
forall a b. (a -> b) -> a -> b
$ do
      -- different projections
      mr  <- QName -> TCM (Maybe QName)
getRecordOfField QName
d
      mr' <- getRecordOfField d'
      case (mr, mr') of
        (Just QName
r, Just QName
r') | QName
r QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
r' -> do
          -- of same record
          def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
          case def of
            Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } -> do
              fs <- [QName] -> TCMT IO [QName]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([QName] -> TCMT IO [QName]) -> [QName] -> TCMT IO [QName]
forall a b. (a -> b) -> a -> b
$ (Dom QName -> QName) -> [Dom QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> QName
forall t e. Dom' t e -> e
unDom [Dom QName]
fs
              case (List.find (d ==) fs, List.find (d' ==) fs) of
                (Just QName
i, Just QName
i')
                  -- earlier field is smaller
                  | QName
i QName -> QName -> Bool
forall a. Ord a => a -> a -> Bool
< QName
i'    -> Order -> TCM Order
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.lt
                  | QName
i QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
i'   -> do
                     __IMPOSSIBLE__
                  | Bool
otherwise -> Order -> TCM Order
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
                (Maybe QName, Maybe QName)
_ -> TCM Order
forall a. HasCallStack => a
__IMPOSSIBLE__
            Defn
_ -> TCM Order
forall a. HasCallStack => a
__IMPOSSIBLE__
        (Maybe QName, Maybe QName)
_ -> Order -> TCM Order
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown

-- | 'makeCM' turns the result of 'compareArgs' into a proper call matrix
makeCM :: Int -> Int -> [[Order]] -> CallMatrix
makeCM :: Int -> Int -> [[Order]] -> CallMatrix
makeCM Int
ncols Int
nrows [[Order]]
matrix = Matrix Int Order -> CallMatrix
forall a. Matrix Int a -> CallMatrix' a
CallMatrix (Matrix Int Order -> CallMatrix) -> Matrix Int Order -> CallMatrix
forall a b. (a -> b) -> a -> b
$
  Size Int -> [[Order]] -> Matrix Int Order
forall i b.
(Ord i, Num i, Enum i, HasZero b) =>
Size i -> [[b]] -> Matrix i b
Matrix.fromLists (Int -> Int -> Size Int
forall i. i -> i -> Size i
Matrix.Size Int
nrows Int
ncols) [[Order]]
matrix

-- | 'addGuardedness' adds guardedness flag in the upper left corner
-- (0,0).
addGuardedness :: Order -> (Int, Int, [[Order]]) -> (Int, Int, [[Order]])
addGuardedness :: Order -> (Int, Int, [[Order]]) -> (Int, Int, [[Order]])
addGuardedness Order
o (Int
nrows, Int
ncols, [[Order]]
m) =
  (Int
nrows Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
ncols Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1,
   (Order
o Order -> [Order] -> [Order]
forall a. a -> [a] -> [a]
: Int -> Order -> [Order]
forall a. Int -> a -> [a]
replicate Int
ncols Order
Order.unknown) [Order] -> [[Order]] -> [[Order]]
forall a. a -> [a] -> [a]
: ([Order] -> [Order]) -> [[Order]] -> [[Order]]
forall a b. (a -> b) -> [a] -> [b]
map (Order
Order.unknown Order -> [Order] -> [Order]
forall a. a -> [a] -> [a]
:) [[Order]]
m)

-- | Compose something with the upper-left corner of a call matrix
composeGuardedness :: (?cutoff :: CutOff) => Order -> [[Order]] -> [[Order]]
composeGuardedness :: (?cutoff::CutOff) => Order -> [[Order]] -> [[Order]]
composeGuardedness Order
o ((Order
corner : [Order]
row) : [[Order]]
rows) = ((Order
o (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
.*. Order
corner) Order -> [Order] -> [Order]
forall a. a -> [a] -> [a]
: [Order]
row) [Order] -> [[Order]] -> [[Order]]
forall a. a -> [a] -> [a]
: [[Order]]
rows
composeGuardedness Order
_ [[Order]]
_ = [[Order]]
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Stripping off a record constructor is not counted as decrease, in
--   contrast to a data constructor.
--   A record constructor increases/decreases by 0, a data constructor by 1.
offsetFromConstructor :: HasConstInfo tcm => QName -> tcm Int
offsetFromConstructor :: forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
offsetFromConstructor QName
c =
  tcm Bool -> tcm Int -> tcm Int -> tcm Int
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> tcm Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c) (Int -> tcm Int
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0) (Int -> tcm Int
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1)

--UNUSED Liang-Ting 2019-07-16
---- | Compute the proper subpatterns of a 'DeBruijnPattern'.
--subPatterns :: DeBruijnPattern -> [DeBruijnPattern]
--subPatterns = foldPattern $ \case
--  ConP _ _ ps -> map namedArg ps
--  DefP _ _ ps -> map namedArg ps -- TODO check semantics
--  VarP _ _    -> mempty
--  LitP _      -> mempty
--  DotP _ _    -> mempty
--  ProjP _ _   -> mempty
--  IApplyP{}   -> mempty


compareTerm :: Term -> Masked DeBruijnPattern -> TerM Order
compareTerm :: Term -> Masked DeBruijnPattern -> TerM Order
compareTerm Term
t Masked DeBruijnPattern
p = do
--   reportSDoc "term.compare" 25 $
--     " comparing term " <+> prettyTCM t <+>
--     " to pattern " <+> prettyTCM p
  t <- TCM Term -> TerM Term
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
t
  o <- compareTerm' t p
  liftTCM $ reportSDoc "term.compare" 25 $
    " comparing term " <+> prettyTCM t <+>
    " to pattern " <+> prettyTCM p <+>
    text (" results in " ++ prettyShow o)
  return o


-- | Remove all non-coinductive projections from an algebraic term
--   (not going under binders).
--   Also, remove 'DontCare's.
--
class StripAllProjections a where
  stripAllProjections :: a -> TCM a

instance StripAllProjections a => StripAllProjections (Arg a) where
  stripAllProjections :: Arg a -> TCM (Arg a)
stripAllProjections = (a -> TCMT IO a) -> Arg a -> TCM (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse a -> TCMT IO a
forall a. StripAllProjections a => a -> TCM a
stripAllProjections

instance StripAllProjections Elims where
  stripAllProjections :: Elims -> TCM Elims
stripAllProjections Elims
es =
    case Elims
es of
      []             -> Elims -> TCM Elims
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      (Apply Arg Term
a : Elims
es) -> do
        (:) (Elim -> Elims -> Elims)
-> TCMT IO Elim -> TCMT IO (Elims -> Elims)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> TCMT IO (Arg Term) -> TCMT IO Elim
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> TCMT IO (Arg Term)
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Arg Term
a) TCMT IO (Elims -> Elims) -> TCM Elims -> TCM Elims
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
es
      (IApply Term
x Term
y Term
a : Elims
es) -> do
        -- TODO Andrea: are we doind extra work?
        (:) (Elim -> Elims -> Elims)
-> TCMT IO Elim -> TCMT IO (Elims -> Elims)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply (Term -> Term -> Term -> Elim)
-> TCM Term -> TCMT IO (Term -> Term -> Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
x
                        TCMT IO (Term -> Term -> Elim)
-> TCM Term -> TCMT IO (Term -> Elim)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
y
                        TCMT IO (Term -> Elim) -> TCM Term -> TCMT IO Elim
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
a)
            TCMT IO (Elims -> Elims) -> TCM Elims -> TCM Elims
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
es
      (Proj ProjOrigin
o QName
p  : Elims
es) -> do
        isP <- QName -> TCMT IO Bool
forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive QName
p
        applyUnless isP (Proj o p :) <$> stripAllProjections es

instance StripAllProjections Args where
  stripAllProjections :: [Arg Term] -> TCM [Arg Term]
stripAllProjections = (Arg Term -> TCMT IO (Arg Term)) -> [Arg Term] -> TCM [Arg Term]
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 Arg Term -> TCMT IO (Arg Term)
forall a. StripAllProjections a => a -> TCM a
stripAllProjections

instance StripAllProjections Term where
  stripAllProjections :: Term -> TCM Term
stripAllProjections Term
t = do
    case Term
t of
      Var Int
i Elims
es   -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> TCM Elims -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
es
      Con ConHead
c ConInfo
ci Elims
ts -> do
        -- Andreas, 2019-02-23, re #2613.  This is apparently not necessary:
        -- c <- fromRightM (\ err -> return c) $ getConForm (conName c)
        ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> TCM Elims -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
ts
      Def QName
d Elims
es   -> QName -> Elims -> Term
Def QName
d (Elims -> Term) -> TCM Elims -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
es
      DontCare Term
t -> Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
t
      Term
_ -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

-- | Normalize outermost constructor name in a pattern.

reduceConPattern :: DeBruijnPattern -> TCM DeBruijnPattern
reduceConPattern :: DeBruijnPattern -> TCM DeBruijnPattern
reduceConPattern = \case
  ConP ConHead
c ConPatternInfo
i NAPs
ps -> (SigError -> TCMT IO ConHead)
-> TCMT IO (Either SigError ConHead) -> TCMT IO ConHead
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m (Either a b) -> m b
fromRightM (\ SigError
err -> ConHead -> TCMT IO ConHead
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c) (QName -> TCMT IO (Either SigError ConHead)
getConForm (ConHead -> QName
conName ConHead
c)) TCMT IO ConHead
-> (ConHead -> DeBruijnPattern) -> TCM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ ConHead
c' ->
    ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c' ConPatternInfo
i NAPs
ps
  DeBruijnPattern
p -> DeBruijnPattern -> TCM DeBruijnPattern
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p

-- | @compareTerm' t dbpat@

compareTerm' :: Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' :: Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
v mp :: Masked DeBruijnPattern
mp@(Masked Bool
m DeBruijnPattern
p) = do
  suc  <- TerM (Maybe QName)
terGetSizeSuc
  cutoff <- terGetCutOff
  let ?cutoff = cutoff
  v <- liftTCM (instantiate v)
  p <- liftTCM $ reduceConPattern p
  case (v, p) of

    -- Andreas, 2013-11-20 do not drop projections,
    -- in any case not coinductive ones!:
    (Var Int
i Elims
es, DeBruijnPattern
_) | Just{} <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
      Int -> Masked DeBruijnPattern -> TerM Order
compareVar Int
i Masked DeBruijnPattern
mp

    (DontCare Term
t, DeBruijnPattern
_) ->
      Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
t Masked DeBruijnPattern
mp

    -- Andreas, 2014-09-22, issue 1281:
    -- For metas, termination checking should be optimistic.
    -- If there is any instance of the meta making termination
    -- checking succeed, then we should not fail.
    -- Thus, we assume the meta will be instantiated with the
    -- deepest variable in @p@.
    -- For sized types, the depth is maximally
    -- the number of SIZELT hypotheses one can have in a context.
    (MetaV{}, DeBruijnPattern
p) -> (?cutoff::CutOff) => Bool -> Int -> Order
Bool -> Int -> Order
Order.decr Bool
True (Int -> Order) -> (Int -> Int) -> Int -> Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (if Bool
m then Int
0 else DeBruijnPattern -> Int
forall a. Pattern' a -> Int
patternDepth DeBruijnPattern
p) (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
pred (Int -> Order) -> TerM Int -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
       (TerEnv -> Int) -> TerM Int
forall a. (TerEnv -> a) -> TerM a
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Int
_terSizeDepth

    -- Successor on both sides cancel each other.
    -- We ignore the mask for sizes.
    (Def QName
s [Apply Arg Term
t], ConP ConHead
s' ConPatternInfo
_ [Arg (Named_ DeBruijnPattern)
p]) | QName
s QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
s' Bool -> Bool -> Bool
&& QName -> Maybe QName
forall a. a -> Maybe a
Just QName
s Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
suc ->
      Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) (DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p)

    -- Register also size increase.
    (Def QName
s [Apply Arg Term
t], DeBruijnPattern
p) | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
s Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
suc ->
      -- Andreas, 2012-10-19 do not cut off here
      Int -> Order -> Order
increase Int
1 (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) Masked DeBruijnPattern
mp

    -- In all cases that do not concern sizes,
    -- we cannot continue if pattern is masked.

    (Term, DeBruijnPattern)
_ | Bool
m -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown

    (Lit Literal
l, LitP PatternInfo
_ Literal
l')
      | Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'     -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le
      | Bool
otherwise   -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown

    (Lit Literal
l, DeBruijnPattern
_) -> do
      v <- TCM Term -> TerM Term
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v
      case v of
        Lit{}       -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
        Term
v           -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
v Masked DeBruijnPattern
mp

    -- Andreas, 2011-04-19 give subterm priority over matrix order

    (Con{}, ConP ConHead
c ConPatternInfo
_ NAPs
ps) | (Arg (Named_ DeBruijnPattern) -> Bool) -> NAPs -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
Term -> DeBruijnPattern -> Bool
isSubTerm Term
v (DeBruijnPattern -> Bool)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps ->
      (?cutoff::CutOff) => Bool -> Int -> Order
Bool -> Int -> Order
decr Bool
True (Int -> Order) -> TerM Int -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TerM Int
forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
offsetFromConstructor (ConHead -> QName
conName ConHead
c)

    (Con ConHead
c ConInfo
_ Elims
es, ConP ConHead
c' ConPatternInfo
_ NAPs
ps) | ConHead -> QName
conName ConHead
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c'->
      let ts :: [Arg Term]
ts = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es in
      [Arg Term] -> NAPs -> TerM Order
compareConArgs [Arg Term]
ts NAPs
ps

    (Con ConHead
_ ConInfo
_ [], DeBruijnPattern
_) -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le

    -- new case for counting constructors / projections
    -- register also increase
    (Con ConHead
c ConInfo
_ Elims
es, DeBruijnPattern
_) -> do
      let ts :: [Arg Term]
ts = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      Int -> Order -> Order
increase (Int -> Order -> Order) -> TerM Int -> TerM (Order -> Order)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TerM Int
forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
offsetFromConstructor (ConHead -> QName
conName ConHead
c)
               TerM (Order -> Order) -> TerM Order -> TerM Order
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((?cutoff::CutOff) => [Order] -> Order
[Order] -> Order
infimum ([Order] -> Order) -> TerM [Order] -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Term -> TerM Order) -> [Arg Term] -> TerM [Order]
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 (\ Arg Term
t -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) Masked DeBruijnPattern
mp) [Arg Term]
ts)

    (Term
t, DeBruijnPattern
p) -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Order -> TerM Order) -> Order -> TerM Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
Term -> DeBruijnPattern -> Order
subTerm Term
t DeBruijnPattern
p

-- | @subTerm@ computes a size difference (Order)
subTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPattern -> Order
subTerm :: (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
subTerm Term
t DeBruijnPattern
p = if Term -> DeBruijnPattern -> Bool
equal Term
t DeBruijnPattern
p then Order
Order.le else (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
Term -> DeBruijnPattern -> Order
properSubTerm Term
t DeBruijnPattern
p
  where
    equal :: Term -> DeBruijnPattern -> Bool
equal (Con ConHead
c ConInfo
_ Elims
es) (ConP ConHead
c' ConPatternInfo
_ NAPs
ps) =
      let ts :: [Arg Term]
ts = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es in
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (ConHead -> QName
conName ConHead
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c')
          Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NAPs -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
ps)
          Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: (Arg Term -> Arg (Named_ DeBruijnPattern) -> Bool)
-> [Arg Term] -> NAPs -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg Term
t Arg (Named_ DeBruijnPattern)
p -> Term -> DeBruijnPattern -> Bool
equal (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p)) [Arg Term]
ts NAPs
ps
    equal (Var Int
i []) (VarP PatternInfo
_ DBPatVar
x) = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== DBPatVar -> Int
dbPatVarIndex DBPatVar
x
    equal (Lit Literal
l)    (LitP PatternInfo
_ Literal
l') = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
    -- Terms.
    -- Checking for identity here is very fragile.
    -- However, we cannot do much more, as we are not allowed to normalize t.
    -- (It might diverge, and we are just in the process of termination checking.)
    equal Term
t         (DotP PatternInfo
_ Term
t') = Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
t'
    equal Term
_ DeBruijnPattern
_ = Bool
False

    properSubTerm :: Term -> DeBruijnPattern -> Order
properSubTerm Term
t (ConP ConHead
_ ConPatternInfo
_ NAPs
ps) =
      Bool -> Order -> Order
setUsability Bool
True (Order -> Order) -> Order -> Order
forall a b. (a -> b) -> a -> b
$ Int -> Order -> Order
decrease Int
1 (Order -> Order) -> Order -> Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => [Order] -> Order
[Order] -> Order
supremum ([Order] -> Order) -> [Order] -> Order
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ DeBruijnPattern) -> Order) -> NAPs -> [Order]
forall a b. (a -> b) -> [a] -> [b]
map ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
Term -> DeBruijnPattern -> Order
subTerm Term
t (DeBruijnPattern -> Order)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps
    properSubTerm Term
_ DeBruijnPattern
_ = Order
Order.unknown

isSubTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPattern -> Bool
isSubTerm :: (?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
isSubTerm Term
t DeBruijnPattern
p = Order -> Bool
nonIncreasing (Order -> Bool) -> Order -> Bool
forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
Term -> DeBruijnPattern -> Order
subTerm Term
t DeBruijnPattern
p

compareConArgs :: Args -> [NamedArg DeBruijnPattern] -> TerM Order
compareConArgs :: [Arg Term] -> NAPs -> TerM Order
compareConArgs [Arg Term]
ts NAPs
ps = do
  cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  case compare (length ts) (length ps) of

    -- We may assume |ps| >= |ts|, otherwise c ps would be of functional type
    -- which is impossible.
    Ordering
GT -> TerM Order
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Andreas, 2022-08-31, issue #6059: doing anything smarter than
    -- @unknown@ here can lead to non-termination.
    Ordering
LT -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown

    Ordering
EQ -> (Order -> Order -> Order) -> Order -> [Order] -> Order
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
(Order..*.) Order
Order.le ([Order] -> Order) -> TerM [Order] -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
               (Term -> Masked DeBruijnPattern -> TerM Order)
-> [Term] -> MaskedDeBruijnPatterns -> TerM [Order]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
ts) ((Arg (Named_ DeBruijnPattern) -> Masked DeBruijnPattern)
-> NAPs -> MaskedDeBruijnPatterns
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> Masked DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps)
       -- corresponds to taking the size, not the height
       -- allows examples like (x, y) < (Succ x, y)
{- version which does an "order matrix"
   -- Andreas, 2013-02-18 disabled because it is unclear
   -- how to scale idempotency test to matrix-shaped orders (need thinking/researcH)
   -- Trigges issue 787.
        (_,_) -> do -- build "call matrix"
          m <- mapM (\t -> mapM (compareTerm' suc (unArg t)) ps) ts
          let m2 = makeCM (length ps) (length ts) m
          return $ Order.orderMat (Order.mat m2)
-}
{- version which takes height
--    if null ts then Order.Le
--               else Order.infimum (zipWith compareTerm' (map unArg ts) ps)
-}

compareVar :: Nat -> Masked DeBruijnPattern -> TerM Order
compareVar :: Int -> Masked DeBruijnPattern -> TerM Order
compareVar Int
i (Masked Bool
m DeBruijnPattern
p) = do
  suc    <- TerM (Maybe QName)
terGetSizeSuc
  cutoff <- terGetCutOff
  let ?cutoff = cutoff
  let no = Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
  case p of
    ProjP{}   -> TerM Order
no
    IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x  -> Int -> Masked DBPatVar -> TerM Order
compareVarVar Int
i (Bool -> DBPatVar -> Masked DBPatVar
forall a. Bool -> a -> Masked a
Masked Bool
m DBPatVar
x)
    LitP{}    -> TerM Order
no
    DotP{}   -> TerM Order
no
    VarP PatternInfo
_ DBPatVar
x  -> Int -> Masked DBPatVar -> TerM Order
compareVarVar Int
i (Bool -> DBPatVar -> Masked DBPatVar
forall a. Bool -> a -> Masked a
Masked Bool
m DBPatVar
x)

    ConP ConHead
s ConPatternInfo
_ [Arg (Named_ DeBruijnPattern)
p] | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
s) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
suc ->
      Bool -> Order -> Order
setUsability Bool
True (Order -> Order) -> (Order -> Order) -> Order -> Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Order -> Order
decrease Int
1 (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Masked DeBruijnPattern -> TerM Order
compareVar Int
i (DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p)

    ConP ConHead
c ConPatternInfo
pi NAPs
ps -> if Bool
m then TerM Order
no else Bool -> Order -> Order
setUsability Bool
True (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      let
        dropit :: IsForced -> a -> Maybe a
dropit IsForced
Forced a
_ = Maybe a
forall a. Maybe a
Nothing
        dropit IsForced
NotForced a
x = a -> Maybe a
forall a. a -> Maybe a
Just a
x
      ps <- TerM Bool -> TerM NAPs -> TerM NAPs -> TerM NAPs
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optForcedArgumentRecursion (PragmaOptions -> Bool) -> TerM PragmaOptions -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
        {- then -} (NAPs -> TerM NAPs
forall a. a -> TerM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NAPs
ps)
        {- else -} (QName
-> NAPs
-> (IsForced
    -> Arg (Named_ DeBruijnPattern)
    -> Maybe (Arg (Named_ DeBruijnPattern)))
-> TerM NAPs
forall a b. QName -> [a] -> (IsForced -> a -> Maybe b) -> TerM [b]
mapForcedArguments (ConHead -> QName
conName ConHead
c) NAPs
ps IsForced
-> Arg (Named_ DeBruijnPattern)
-> Maybe (Arg (Named_ DeBruijnPattern))
forall {a}. IsForced -> a -> Maybe a
dropit)
      decrease <$> offsetFromConstructor (conName c)
               <*> (Order.supremum <$> mapM (compareVar i . notMasked . namedArg) ps)
    DefP PatternInfo
_ QName
c NAPs
ps -> if Bool
m then TerM Order
no else Bool -> Order -> Order
setUsability Bool
True (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      Int -> Order -> Order
decrease (Int -> Order -> Order) -> TerM Int -> TerM (Order -> Order)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TerM Int
forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
offsetFromConstructor QName
c
               TerM (Order -> Order) -> TerM Order -> TerM Order
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((?cutoff::CutOff) => [Order] -> Order
[Order] -> Order
Order.supremum ([Order] -> Order) -> TerM [Order] -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg (Named_ DeBruijnPattern) -> TerM Order)
-> NAPs -> TerM [Order]
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 (Int -> Masked DeBruijnPattern -> TerM Order
compareVar Int
i (Masked DeBruijnPattern -> TerM Order)
-> (Arg (Named_ DeBruijnPattern) -> Masked DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> TerM Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> Masked DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps)
      -- This should be fine for c == hcomp

-- | Compare two variables.
--
--   The first variable comes from a term, the second from a pattern.
compareVarVar :: Nat -> Masked DBPatVar -> TerM Order
compareVarVar :: Int -> Masked DBPatVar -> TerM Order
compareVarVar Int
i (Masked Bool
m x :: DBPatVar
x@(DBPatVar String
_ Int
j))
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = if Bool -> Bool
not Bool
m then Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le else TCM Order -> TerM Order
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Order -> TerM Order) -> TCM Order -> TerM Order
forall a b. (a -> b) -> a -> b
$
      -- If j is a size, we ignore the mask.
      TCMT IO Bool -> TCM Order -> TCM Order -> TCM Order
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType (Type -> TCMT IO (Maybe BoundedSize))
-> TCMT IO Type -> TCMT IO (Maybe BoundedSize)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
j)
        {- then -} (Order -> TCM Order
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le)
        {- else -} (Order -> TCM Order
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown)
  | Bool
otherwise = do
      -- record usability of variable
      u <- (Int
i Int -> IntSet -> Bool
`VarSet.member`) (IntSet -> Bool) -> TerM IntSet -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM IntSet
terGetUsableVars
      -- Andreas, 2017-07-26, issue #2331.
      -- The usability logic is refuted by bounded size quantification in terms.
      -- Thus, it is switched off (the infrastructure remains in place for now).
      if not u then return Order.unknown else do
      -- Only if usable:
      res <- isBounded i
      case res of
        BoundedSize
BoundedNo  -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
        BoundedLt Term
v -> Bool -> Order -> Order
setUsability Bool
u (Order -> Order) -> (Order -> Order) -> Order -> Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Order -> Order
decrease Int
1 (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
v (Bool -> DeBruijnPattern -> Masked DeBruijnPattern
forall a. Bool -> a -> Masked a
Masked Bool
m (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> DeBruijnPattern
forall a. a -> Pattern' a
varP DBPatVar
x)