{-# LANGUAGE GADTs                      #-}

{-# 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.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.Utils.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 = forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext 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 {}            -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.Field {}            -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.Primitive {}        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.Mutual MutualInfo
i [Declaration]
ds         -> [QName] -> TCM Result
termMutual forall a b. (a -> b) -> a -> b
$ [Declaration] -> [QName]
getNames [Declaration]
ds
    A.Section Range
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds    -> 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 {}            -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.Import {}           -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.Pragma {}           -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.Open {}             -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.PatternSynDef {}    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.Generalize {}       -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 $ -} forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
termDecls [Declaration]
ds
        -- scope is irrelevant as we are termination checking Syntax.Internal
    A.RecSig{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    A.RecDef DefInfo
_ QName
x UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Type
_ [Declaration]
ds -> [QName] -> TCM Result
termMutual [QName
x] forall a. Semigroup a => a -> a -> a
<> 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{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DataSig{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DataDef{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteDecl{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteDef{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteData{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    termDecls :: t Declaration -> TCM Result
termDecls t Declaration
ds = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, 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 = 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 Delayed
delayed [Clause]
cs)   = [QName
x]
    getName (A.RecDef DefInfo
_ QName
x UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Type
_ [Declaration]
ds)   = QName
x 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
_ 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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optTerminationCheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty) forall a b. (a -> b) -> a -> b
$ {-else-}
 forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext 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.
  MutualId
mid <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock
  MutualBlock
mutualBlock <- forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
mid
  let allNames :: Set QName
allNames = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool
isAbsurdLambdaName) forall a b. (a -> b) -> a -> b
$
                 MutualBlock -> Set QName
mutualNames MutualBlock
mutualBlock
      names :: Set QName
names    = if forall a. Null a => a -> Bool
null [QName]
names0 then Set QName
allNames else forall a. Ord a => [a] -> Set a
Set.fromList [QName]
names0
      i :: MutualInfo
i        = MutualBlock -> MutualInfo
mutualInfo MutualBlock
mutualBlock

  -- We set the range to avoid panics when printing error messages.
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MutualInfo
i forall a b. (a -> b) -> a -> b
$ do

  -- The following debug statement is part of a test case for Issue
  -- #3590.
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.mutual.id" Nat
40 forall a b. (a -> b) -> a -> b
$
    [Char]
"Termination checking mutual block " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show MutualId
mid
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.mutual" Nat
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Termination checking " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Set QName
allNames

  -- NO_TERMINATION_CHECK
  if (MutualInfo -> TerminationCheck Name
Info.mutualTerminationCheck MutualInfo
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ forall m. TerminationCheck m
NoTerminationCheck, forall m. TerminationCheck m
Terminating ]) then do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.warn.yes" Nat
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Skipping termination check for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Set QName
names
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set QName
allNames forall a b. (a -> b) -> a -> b
$ \ QName
q -> forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
q Bool
True -- considered terminating!
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
  -- NON_TERMINATING
  else if (MutualInfo -> TerminationCheck Name
Info.mutualTerminationCheck MutualInfo
i forall a. Eq a => a -> a -> Bool
== forall m. TerminationCheck m
NonTerminating) then do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.warn.yes" Nat
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Considering as non-terminating: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Set QName
names
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set QName
allNames forall a b. (a -> b) -> a -> b
$ \ QName
q -> forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
q Bool
False
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
  else do
    [Set QName]
sccs <- do
      -- Andreas, 2016-10-01 issue #2231
      -- Recursivity checker has to see through abstract definitions!
      forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [Phase
Benchmark.Termination, Phase
Benchmark.RecCheck] forall a b. (a -> b) -> a -> b
$ Set QName -> TCMT IO [Set QName]
recursive Set QName
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)?
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null [Set QName]
sccs) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.warn.yes" Nat
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Trivially terminating: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Set QName
names

    -- Actual termination checking needed: go through SCCs.
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
     forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Set QName]
sccs forall a b. (a -> b) -> a -> b
$ \ Set QName
allNames -> do

     -- Set the mutual names in the termination environment.
     let namesSCC :: Set QName
namesSCC = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (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 :: Set QName
terMutual    = Set QName
allNames
           , terUserNames :: Set QName
terUserNames = Set QName
namesSCC
           }
         runTerm :: TerM Result -> TCM Result
runTerm TerM Result
cont = forall a. TerM a -> TCM a
runTerDefault forall a b. (a -> b) -> a -> b
$ do
           CutOff
cutoff <- TerM CutOff
terGetCutOff
           forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.top" Nat
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Termination checking " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Set QName
namesSCC forall a. [a] -> [a] -> [a]
++
             [Char]
" with cutoff=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show CutOff
cutoff forall a. [a] -> [a] -> [a]
++ [Char]
"..."
           forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal TerEnv -> TerEnv
setNames TerM Result
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.
     forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
anyM Set QName
allNames forall a b. (a -> b) -> a -> b
$ \ QName
q -> forall (m :: * -> *). HasConstInfo m => QName -> m Bool
usesCopatterns QName
q forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
q))
         -- Then: New check, one after another.
         (TerM Result -> TCM Result
runTerm forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' Set QName
allNames forall a b. (a -> b) -> a -> b
$ QName -> TerM Result
termFunction)
         -- Else: Old check, all at once.
         (TerM Result -> TCM Result
runTerm 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
  Set QName
allNames <- TerM (Set QName)
terGetMutual
  let collect :: TerM Calls
collect = 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
  Calls
calls1 <- TerM Calls
collect
  [Char] -> Calls -> TerM ()
reportCalls [Char]
"no " Calls
calls1

  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = CutOff
cutoff
  Either CallPath ()
r <- forall a. a -> TerM a
billToTerGraph forall a b. (a -> b) -> a -> b
$ forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CallGraph cinfo -> Either cinfo ()
Term.terminates Calls
calls1
  Either CallPath ()
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.
       forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (forall (m :: * -> *) a. Monad m => a -> m a
return Either CallPath ()
r) {- else -} forall a b. (a -> b) -> a -> b
$
       case Either CallPath ()
r of
         r :: Either CallPath ()
r@Right{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Either CallPath ()
r
         Left{}    -> do
           -- Try again, but include the dot patterns this time.
           Calls
calls2 <- forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
True forall a b. (a -> b) -> a -> b
$ TerM Calls
collect
           [Char] -> Calls -> TerM ()
reportCalls [Char]
"" Calls
calls2
           forall a. a -> TerM a
billToTerGraph forall a b. (a -> b) -> a -> b
$ forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CallGraph cinfo -> Either cinfo ()
Term.terminates Calls
calls2

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

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

    Right{} -> do
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.warn.yes" Nat
2 forall a b. (a -> b) -> a -> b
$
        forall a. Pretty a => a -> [Char]
prettyShow (Set QName
names) forall a. [a] -> [a] -> [a]
++ [Char]
" does termination check"
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
`setTerminates` Bool
True) Set QName
allNames
      forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a b. (a -> b) -> [a] -> [b]
map CallInfo -> QName
callInfoTarget [CallInfo]
calls'
  names' :: [QName]
names'    = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => [a] -> a -> Bool
hasElem [QName]
mentioned) forall a b. (a -> b) -> a -> b
$ 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 = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> c -> m c
billPureTo [Phase
Benchmark.Termination, Phase
Benchmark.Graph] a
a

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

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

  -- We work in TCM exclusively.
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do

    forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Nat -> a -> m ()
reportS [Char]
"term.lex" Nat
20
      [ [Char]
"Calls (" forall a. [a] -> [a] -> [a]
++ [Char]
no forall a. [a] -> [a] -> [a]
++ [Char]
"dot patterns): " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Calls
calls
      ]

    -- Print the whole completion phase.
    forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
verboseS [Char]
"term.matrices" Nat
40 forall a b. (a -> b) -> a -> b
$ do
      let header :: [Char] -> [Char]
header [Char]
s = [[Char]] -> [Char]
unlines
            [ forall a. Nat -> a -> [a]
replicate Nat
n Char
'='
            , forall a. Nat -> a -> [a]
replicate Nat
k Char
'=' forall a. [a] -> [a] -> [a]
++ [Char]
s forall a. [a] -> [a] -> [a]
++ forall a. Nat -> a -> [a]
replicate Nat
k' Char
'='
            , forall a. Nat -> a -> [a]
replicate Nat
n Char
'='
            ]
            where n :: Nat
n  = Nat
70
                  r :: Nat
r  = Nat
n forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Char]
s
                  k :: Nat
k  = Nat
r forall a. Integral a => a -> a -> a
`div` Nat
2
                  k' :: Nat
k' = Nat
r forall a. Num a => a -> a -> a
- Nat
k
      let report :: [Char] -> a -> m ()
report [Char]
s a
cs = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.matrices" Nat
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
header [Char]
s
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
cs
            ]
          cs0 :: Calls
cs0     = Calls
calls
          step :: Calls -> TCMT IO (Either () Calls)
step Calls
cs = do
            let (Calls
new, Calls
cs') = forall cinfo.
(?cutoff::CutOff, Monoid cinfo) =>
CallGraph cinfo
-> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
completionStep Calls
cs0 Calls
cs
            forall {m :: * -> *} {a}.
(MonadDebug m, Pretty a) =>
[Char] -> a -> m ()
report [Char]
" New call matrices " Calls
new
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall a. Null a => a -> Bool
null Calls
new then forall a b. a -> Either a b
Left () else forall a b. b -> Either a b
Right Calls
cs'
      forall {m :: * -> *} {a}.
(MonadDebug m, Pretty a) =>
[Char] -> a -> m ()
report [Char]
" Initial call matrices " Calls
cs0
      forall (m :: * -> *) a b.
Monad m =>
(a -> m (Either b a)) -> a -> m b
trampolineM Calls -> TCMT IO (Either () Calls)
step Calls
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]
idems = forall a. (a -> Bool) -> [a] -> [a]
filter forall cinfo. (?cutoff::CutOff) => CallMatrixAug cinfo -> Bool
idempotent forall a b. (a -> b) -> a -> b
$ forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
endos forall a b. (a -> b) -> a -> b
$ 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'
    --   ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.matrices" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"Idempotent call matrices (" forall a. [a] -> [a] -> [a]
++ [Char]
no forall a. [a] -> [a] -> [a]
++ [Char]
"dot patterns):\n"
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
"\n" forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [CallMatrixAug CallPath]
idems
      ]
    -- reportSDoc "term.matrices" 30 $ vcat
    --   [ text $ "Other call matrices (" ++ no ++ "dot patterns):"
    --   , nest 2 $ pretty $ CallGraph.fromList others
    --   ]
    forall (m :: * -> *) a. Monad m => a -> m a
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 = forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
name 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.

  Set QName
allNames <- TerM (Set QName)
terGetMutual
  let index :: Nat
index = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Maybe Nat
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
target <- case Definition -> Defn
theDef Definition
def of
    -- We are termination-checking a record (calls to record will not be guarding):
    Record{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Target
TargetRecord
    -- We are termination-checking a definition:
    Defn
_ -> forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm (Maybe QName)
typeEndsInDef (Definition -> Type
defType Definition
def) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
           Just QName
d  -> QName -> Target
TargetDef QName
d
           Maybe QName
Nothing -> Target
TargetOther
  forall (m :: * -> *). MonadDebug m => Target -> m ()
reportTarget Target
target
  forall a. Target -> TerM a -> TerM a
terSetTarget Target
target forall a b. (a -> b) -> a -> b
$ do

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

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

    -- First try to termination check ignoring the dot patterns
    Calls
calls1 <- forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
False forall a b. (a -> b) -> a -> b
$ TerM Calls
collect
    [Char] -> Calls -> TerM ()
reportCalls [Char]
"no " Calls
calls1

    Either CallPath ()
r <- do
     CutOff
cutoff <- TerM CutOff
terGetCutOff
     let ?cutoff = CutOff
cutoff
     Either CallPath ()
r <- forall a. a -> TerM a
billToTerGraph forall a b. (a -> b) -> a -> b
$ forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
(Nat -> Bool) -> CallGraph cinfo -> Either cinfo ()
Term.terminatesFilter (forall a. Eq a => a -> a -> Bool
== Nat
index) Calls
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.
     forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (forall (m :: * -> *) a. Monad m => a -> m a
return Either CallPath ()
r) {- else -} forall a b. (a -> b) -> a -> b
$ case Either CallPath ()
r of
       Right () -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ()
       Left{}   -> do
         -- Try again, but include the dot patterns this time.
         Calls
calls2 <- forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
True forall a b. (a -> b) -> a -> b
$ TerM Calls
collect
         [Char] -> Calls -> TerM ()
reportCalls [Char]
"" Calls
calls2
         forall a. a -> TerM a
billToTerGraph forall a b. (a -> b) -> a -> b
$ forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
(Nat -> Bool) -> CallGraph cinfo -> Either cinfo ()
Term.terminatesFilter (forall a. Eq a => a -> a -> Bool
== Nat
index) Calls
calls2

    Set QName
names <- TerM (Set QName)
terGetUserNames
    case forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft CallPath -> [CallInfo]
callInfos Either CallPath ()
r of

      Left [CallInfo]
calls -> do
        -- Mark as non-terminating.
        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
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.warn.no" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
              forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCMT IO Doc
"Record type", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name, TCMT IO Doc
"does not termination check.", TCMT IO Doc
"Problematic calls:" ] forall a. a -> [a] -> [a]
:
              (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn forall a. HasRange a => a -> Range
getRange [CallInfo]
calls)
            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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
names] [CallInfo]
calls
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton TerminationError
err

      Right () -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.warn.yes" Nat
2 forall a b. (a -> b) -> a -> b
$
          forall a. Pretty a => a -> [Char]
prettyShow QName
name forall a. [a] -> [a] -> [a]
++ [Char]
" does termination check"
        forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
name Bool
True
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
   where
     reportTarget :: MonadDebug m => Target -> m ()
     reportTarget :: forall (m :: * -> *). MonadDebug m => Target -> m ()
reportTarget Target
tgt = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.target" Nat
20 forall a b. (a -> b) -> a -> b
$ ([Char]
"  " forall a. [a] -> [a] -> [a]
++) forall a b. (a -> b) -> a -> b
$
       case Target
tgt of
         Target
TargetRecord -> [Char]
"termination checking a record type"
         TargetDef QName
q  -> [[Char]] -> [Char]
unwords [ [Char]
"target type ends in", forall a. Pretty a => a -> [Char]
prettyShow QName
q ]
         Target
TargetOther  -> [Char]
"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 = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  TelV Telescope
_ Type
core <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
  case forall t a. Type'' t a -> a
unEl Type
core of
    Def QName
d Elims
vs -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
d
    Term
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a. QName -> TerM a -> TerM a
terSetCurrent QName
name forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
name 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 forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
       Target
TargetRecord -> Bool
False
       Target
_ -> Bool
True
 forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
isRecord_ forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` TerM Bool
notTargetRecord) forall a. Monoid a => a
mempty {-else-} forall a b. (a -> b) -> a -> b
$ do

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

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

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

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

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

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

    -- If the result should be disregarded, set all calls to unguarded.
    forall (m :: * -> *) a.
Monad m =>
m Bool -> (m a -> m a) -> m a -> m a
applyWhenM TerM Bool
terGetMaskResult forall a. TerM a -> TerM a
terUnguarded forall a b. (a -> b) -> a -> b
$ do

      case Definition -> Defn
theDef Definition
def of
        Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls, funDelayed :: Defn -> Delayed
funDelayed = Delayed
delayed } ->
          forall a. Delayed -> TerM a -> TerM a
terSetDelayed Delayed
delayed forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' [Clause]
cls 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 forall (m :: * -> *) a. Monad m => a -> m a
return 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{ Nat
recPars :: Defn -> Nat
recPars :: Nat
recPars, Telescope
recTel :: Defn -> Telescope
recTel :: Telescope
recTel } -> Nat -> Telescope -> TerM Calls
termRecTel Nat
recPars Telescope
recTel

        Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: Nat -> Telescope -> TerM Calls
termRecTel Nat
npars Telescope
tel = do
  -- Set up the record parameters like function parameters.
  let ([Dom ([Char], Type)]
pars, [Dom ([Char], Type)]
fields) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
npars forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Dom ([Char], Type)]
pars forall a b. (a -> b) -> a -> b
$ do
    MaskedDeBruijnPatterns
ps <- forall {f :: * -> *}.
MonadTCEnv f =>
Nat -> f MaskedDeBruijnPatterns
mkPats Nat
npars
    forall a. MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns MaskedDeBruijnPatterns
ps forall a b. (a -> b) -> a -> b
$ forall b a. TerSetSizeDepth b => b -> TerM a -> TerM a
terSetSizeDepth [Dom ([Char], Type)]
pars forall a b. (a -> b) -> a -> b
$ do
      -- Treat the record fields like the body of a function.
      forall a. ExtractCalls a => a -> TerM Calls
extract forall a b. (a -> b) -> a -> b
$ [Dom ([Char], Type)] -> Telescope
telFromList [Dom ([Char], Type)]
fields
  where
  -- create n variable patterns
  mkPats :: Nat -> f MaskedDeBruijnPatterns
mkPats Nat
n  = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. Pretty a => Nat -> a -> Masked DeBruijnPattern
mkPat (forall a. Integral a => a -> [a]
downFrom Nat
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  mkPat :: Nat -> a -> Masked DeBruijnPattern
mkPat Nat
i a
x = forall a. a -> Masked a
notMasked forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo forall a b. (a -> b) -> a -> b
$ [Char] -> Nat -> DBPatVar
DBPatVar (forall a. Pretty a => a -> [Char]
prettyShow a
x) Nat
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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
-- termType = loop 0  -- Andreas, 2019-04-10 deactivate for backwards-compatibility in 2.6.0 #1556
  where
  loop :: Nat -> Type -> TerM Calls
loop Nat
n Type
t = do
    MaskedDeBruijnPatterns
ps <- forall {f :: * -> *}.
MonadTCEnv f =>
Nat -> f MaskedDeBruijnPatterns
mkPats Nat
n
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.type" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"termType " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Nat
n forall a. [a] -> [a] -> [a]
++ [Char]
" with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length MaskedDeBruijnPatterns
ps) forall a. [a] -> [a] -> [a]
++ [Char]
" patterns"
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"looking at type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      ]
    Telescope
tel <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope  -- Andreas, 2018-11-15, issue #3394, forgotten initialization of terSizeDepth
    forall a. MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns MaskedDeBruijnPatterns
ps forall a b. (a -> b) -> a -> b
$ forall b a. TerSetSizeDepth b => b -> TerM a -> TerM a
terSetSizeDepth Telescope
tel forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
ifNotPiType Type
t {-then-} forall a. ExtractCalls a => a -> TerM Calls
extract {-else-} forall a b. (a -> b) -> a -> b
$ \ Dom' Term Type
dom Abs Type
absB -> do
        forall a. ExtractCalls a => a -> TerM Calls
extract Dom' Term Type
dom forall a. Monoid a => a -> a -> a
`mappend` 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 (Nat -> Type -> TerM Calls
loop forall a b. (a -> b) -> a -> b
$! Nat
n forall a. Num a => a -> a -> a
+ Nat
1)

  -- create n variable patterns
  mkPats :: Nat -> f MaskedDeBruijnPatterns
mkPats Nat
n  = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. Pretty a => Nat -> a -> Masked DeBruijnPattern
mkPat (forall a. Integral a => a -> [a]
downFrom Nat
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  mkPat :: Nat -> a -> Masked DeBruijnPattern
mkPat Nat
i a
x = forall a. a -> Masked a
notMasked forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo forall a b. (a -> b) -> a -> b
$ [Char] -> Nat -> DBPatVar
DBPatVar (forall a. Pretty a => a -> [Char]
prettyShow a
x) Nat
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
  ([Bool]
ds, Bool
d) <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
    TelV Telescope
tel Type
core <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
    -- Check argument types
    [Bool]
ds <- Telescope -> TCM [Bool]
checkArgumentTypes Telescope
tel
    -- Check result types
    Bool
d  <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isNothing forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Term -> TCM (Maybe QName)
isDataOrRecord forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ Type
core
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.mask" Nat
20 forall a b. (a -> b) -> a -> b
$ [Char]
"result type is not data or record type, ignoring guardedness for --without-K"
    forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool]
ds, Bool
d)
  forall a. [Bool] -> TerM a -> TerM a
terSetMaskArgs ([Bool]
ds forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Bool
True) forall a b. (a -> b) -> a -> b
$ forall a. Bool -> TerM a -> TerM a
terSetMaskResult Bool
d forall a b. (a -> b) -> a -> b
$ TerM a
cont

  where
    checkArgumentTypes :: Telescope -> TCM [Bool]
    checkArgumentTypes :: Telescope -> TCM [Bool]
checkArgumentTypes Telescope
EmptyTel = forall (m :: * -> *) a. Monad m => a -> m a
return []
    checkArgumentTypes (ExtendTel Dom' Term Type
dom Abs Telescope
atel) = do
      TelV Telescope
tel2 Type
t <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' Term Type
dom
      Bool
d <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel2 forall a b. (a -> b) -> a -> b
$
        (forall a. Maybe a -> Bool
isNothing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
isDataOrRecord (forall t a. Type'' t a -> a
unEl Type
t)) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
t)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.mask" Nat
20 forall a b. (a -> b) -> a -> b
$ do
          TCMT IO Doc
"argument type "
            forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not data or record type, ignoring structural descent for --without-K"
      forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom' Term Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom' Term Type
dom Abs Telescope
atel forall a b. (a -> b) -> a -> b
$ \Telescope
tel -> (Bool
dforall a. a -> [a] -> [a]
:) 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 forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
  TargetDef QName
d  -> QName
d 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 =
  forall a b. TermToPattern a b => a -> TerM b
termToPattern forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a. StripAllProjections a => a -> TCM a
stripAllProjections forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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 = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
t) 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 forall a b. (a -> b) -> a -> b
$
      forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. TermToPattern a b => a -> TerM b
termToPattern (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
args)
    Def QName
s [Apply Arg Term
arg] -> TerM DeBruijnPattern -> TerM DeBruijnPattern
ifDotPats forall a b. (a -> b) -> a -> b
$ do
      Maybe QName
suc <- TerM (Maybe QName)
terGetSizeSuc
      if forall a. a -> Maybe a
Just QName
s forall a. Eq a => a -> a -> Bool
== Maybe QName
suc then forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
s DataOrRecord
IsData Induction
Inductive []) ConPatternInfo
noConPatternInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. TermToPattern a b => a -> TerM b
termToPattern [Arg Term
arg]
       else TerM DeBruijnPattern
fallback
    DontCare Term
t  -> forall a b. TermToPattern a b => a -> TerM b
termToPattern Term
t -- OR: __IMPOSSIBLE__  -- removed by stripAllProjections
    -- Leaves.
    Var Nat
i []    -> forall a. a -> Pattern' a
varP forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Nat -> DBPatVar
`DBPatVar` Nat
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Name
nameOfBV Nat
i
    Lit Literal
l       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Literal -> Pattern' a
litP Literal
l
    Dummy [Char]
s Elims
_   -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
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           = 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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataOrRecord
IsData forall a. Eq a => a -> a -> Bool
== ConHead -> DataOrRecord
conDataRecord ConHead
c) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM Bool
terGetUseDotPatterns) TerM DeBruijnPattern
fallback
    fallback :: TerM DeBruijnPattern
fallback            = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {x}. Pattern' x -> Bool -> Masked (Pattern' x)
mask [DeBruijnPattern]
ps 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
_ = forall a. Bool -> a -> Masked a
Masked Bool
False Pattern' x
p
    mask Pattern' x
p         Bool
d = forall a. Bool -> a -> Masked a
Masked Bool
d     Pattern' x
p


-- | Extract recursive calls from one clause.
termClause :: Clause -> TerM Calls
termClause :: Clause -> TerM Calls
termClause Clause
clause = do
  Clause{ clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
body } <- forall (tcm :: * -> *). MonadTCM tcm => Clause -> tcm Clause
etaExpandClause Clause
clause
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.check.clause" Nat
25 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"termClause"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
ps
    ]
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' Maybe Term
body forall a b. (a -> b) -> a -> b
$ \ Term
v -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel 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.
    NAPs
ps <- 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.
    NAPs
ps <- forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
preTraversePatternM DeBruijnPattern -> TerM DeBruijnPattern
stripCoCon NAPs
ps
    -- Mask non-data arguments.
    MaskedDeBruijnPatterns
mdbpats <- [DeBruijnPattern] -> TerM MaskedDeBruijnPatterns
maskNonDataArgs forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs
ps
    forall a. MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns MaskedDeBruijnPatterns
mdbpats forall a b. (a -> b) -> a -> b
$ do
      forall b a. TerSetSizeDepth b => b -> TerM a -> TerM a
terSetSizeDepth Telescope
tel forall a b. (a -> b) -> a -> b
$ do
        Term -> TerM ()
reportBody Term
v
        forall a. ExtractCalls a => a -> TerM Calls
extract Term
v

  where
    parseDotP :: DeBruijnPattern -> TerM DeBruijnPattern
parseDotP = \case
      DotP PatternInfo
o Term
t -> Term -> TerM DeBruijnPattern
termToDBP Term
t
      DeBruijnPattern
p        -> forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
    stripCoCon :: DeBruijnPattern -> TerM DeBruijnPattern
stripCoCon DeBruijnPattern
p = case DeBruijnPattern
p of
      ConP (ConHead QName
c DataOrRecord
_ Induction
_ [Arg QName]
_) ConPatternInfo
_ NAPs
_ -> do
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM (Maybe QName)
terGetSizeSuc) (forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p) forall a b. (a -> b) -> a -> b
$ {- else -} do
        forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Induction
whatInduction QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Induction
Inductive   -> forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
          Induction
CoInductive -> forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
unusedVar
      DeBruijnPattern
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
    reportBody :: Term -> TerM ()
    reportBody :: Term -> TerM ()
reportBody Term
v = forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
verboseS [Char]
"term.check.clause" Nat
6 forall a b. (a -> b) -> a -> b
$ do
      QName
f       <- TerM QName
terGetCurrent
      Delayed
delayed <- TerM Delayed
terGetDelayed
      MaskedDeBruijnPatterns
pats    <- TerM MaskedDeBruijnPatterns
terGetPatterns
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.check.clause" Nat
6 forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"termination checking " forall a. [a] -> [a] -> [a]
++
                    (if Delayed
delayed forall a. Eq a => a -> a -> Bool
== Delayed
Delayed then [Char]
"delayed " else [Char]
"") forall a. [a] -> [a] -> [a]
++
                    [Char]
"clause of")
                forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"lhs:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MaskedDeBruijnPatterns
pats)
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"rhs:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
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 [Char]
_ a
a) = forall a. ExtractCalls a => a -> TerM Calls
extract a
a
  extract (Abs [Char]
x a
a)   = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Char]
x forall a b. (a -> b) -> a -> b
$ forall a. TerM a -> TerM a
terRaise forall a b. (a -> b) -> a -> b
$ forall a. ExtractCalls a => a -> TerM Calls
extract a
a

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

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

instance ExtractCalls a => ExtractCalls (Elim' a) where
  extract :: Elim' a -> TerM Calls
extract Proj{}    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
  extract (Apply Arg a
a) = forall a. ExtractCalls a => a -> TerM Calls
extract forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg a
a
  extract (IApply a
x a
y a
a) = 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 = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
(a -> m b) -> t a -> m b
mapM' 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) = forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
CallGraph.union forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ExtractCalls a => a -> TerM Calls
extract a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = 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
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.sort" Nat
20 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"extracting calls from sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.sort" Nat
50 forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"s = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Sort
s)
    case Sort
s of
      Inf IsFibrant
f Integer
n    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
      Sort
SizeUniv   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
      Sort
LockUniv   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
      Sort
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
      Type Level' Term
t     -> forall a. TerM a -> TerM a
terUnguarded forall a b. (a -> b) -> a -> b
$ forall a. ExtractCalls a => a -> TerM Calls
extract Level' Term
t  -- no guarded levels
      Prop Level' Term
t     -> forall a. TerM a -> TerM a
terUnguarded forall a b. (a -> b) -> a -> b
$ forall a. ExtractCalls a => a -> TerM Calls
extract Level' Term
t
      SSet Level' Term
t     -> forall a. TerM a -> TerM a
terUnguarded forall a b. (a -> b) -> a -> b
$ forall a. ExtractCalls a => a -> TerM Calls
extract Level' Term
t
      PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> forall a. ExtractCalls a => a -> TerM Calls
extract (Dom' Term Term
a, Sort
s1, Abs Sort
s2)
      FunSort Sort
s1 Sort
s2 -> forall a. ExtractCalls a => a -> TerM Calls
extract (Sort
s1, Sort
s2)
      UnivSort Sort
s -> forall a. ExtractCalls a => a -> TerM Calls
extract Sort
s
      MetaS MetaId
x Elims
es -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
      DefS QName
d Elims
es  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
      DummyS{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return 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) = 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        -> forall a. Monoid a => a
mempty
    ExtendTel a
a Abs (Tele a)
tel -> forall a. ExtractCalls a => a -> TerM Calls
extract a
a forall a. Semigroup a => a -> a -> a
<> 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
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = CutOff
cutoff
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' [(Arg Term, Bool)]
args forall a b. (a -> b) -> a -> b
$ \ (Arg Term
arg, Bool
preserves) -> do
    let g' :: Order -> Order
g' = case (Bool
preserves, Induction
ind) of
             (Bool
True,  Induction
Inductive)   -> forall a. a -> a
id
             (Bool
True,  Induction
CoInductive) -> (Order
Order.lt (?cutoff::CutOff) => Order -> Order -> Order
.*.)
             (Bool
False, Induction
_)           -> forall a b. a -> b -> a
const Order
Order.unknown
    forall a. (Order -> Order) -> TerM a -> TerM a
terModifyGuarded Order -> Order
g' forall a b. (a -> b) -> a -> b
$ 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

    QName
f       <- TerM QName
terGetCurrent
    Set QName
names   <- TerM (Set QName)
terGetMutual
    Order
guarded <- TerM Order
terGetGuarded

    -- let gArgs = Def g es0
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.function" Nat
30 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"termination checking function call " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
g Elims
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.
    Bool
isProj <- forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive QName
g
    let unguards :: [Order]
unguards = forall a. a -> [a]
repeat Order
Order.unknown
    let guards :: [Order]
guards = forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
isProj (Order
guarded forall a. a -> [a] -> [a]
:) [Order]
unguards
    -- Collect calls in the arguments of this call.
    let args :: [Term]
args = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t. [Elim' t] -> [Arg t]
argsFromElims Elims
es0
    Calls
calls <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' (forall a b. [a] -> [b] -> [(a, b)]
zip [Order]
guards [Term]
args) forall a b. (a -> b) -> a -> b
$ \ (Order
guard, Term
a) -> do
      forall a. Order -> TerM a -> TerM a
terSetGuarded Order
guard forall a b. (a -> b) -> a -> b
$ forall a. ExtractCalls a => a -> TerM Calls
extract Term
a

    -- Then, consider call gArgs itself.

    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.found.call" Nat
20 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"found call from" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"to" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
g
          ]

    -- insert this call into the call list
    case forall a. Ord a => a -> Set a -> Maybe Nat
Set.lookupIndex QName
g Set QName
names of

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

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

         Delayed
delayed <- TerM Delayed
terGetDelayed
         -- 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.
         Elims
es <- -- ifM terGetHaveInlinedWith (return es0) {-else-} $
           forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Elims
es0 forall a b. (a -> b) -> a -> b
$
             -- 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.
             forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> TCMT IO Term
reduceCon forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
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
         (Nat
nrows, Nat
ncols, [[Order]]
matrix) <- forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [Phase
Benchmark.Termination, Phase
Benchmark.Compare] forall a b. (a -> b) -> a -> b
$
           Elims -> TerM (Nat, Nat, [[Order]])
compareArgs Elims
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.
         Order
guarded' <- forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
g forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
           Just{} -> TerM Target
terGetTarget forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
             Target
TargetRecord
               -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
guarded
             Target
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Order
guarded (?cutoff::CutOff) => Order -> Order -> Order
.*. Order
Order.lt)
                    -- guarding when we call a record and not termination checking a record
           Maybe Defn
Nothing
             -- only a delayed definition can be guarded
             | Order -> Bool
Order.decreasing Order
guarded Bool -> Bool -> Bool
&& Delayed
delayed forall a. Eq a => a -> a -> Bool
== Delayed
NotDelayed
               -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le
             | Bool
otherwise
               -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
guarded
         forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.guardedness" Nat
20 forall a b. (a -> b) -> a -> b
$
           [Char]
"composing with guardedness " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Order
guarded forall a. [a] -> [a] -> [a]
++
           [Char]
" counting as " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Order
guarded'
         let matrix' :: [[Order]]
matrix' = (?cutoff::CutOff) => 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.
         Closure Term
doc <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (QName -> ModuleName
qnameModule QName
g) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure forall a b. (a -> b) -> a -> b
$
           QName -> Elims -> Term
Def QName
g forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd ((Origin
Inserted forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensOrigin a => a -> Origin
getOrigin) Elims
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 :: Nat
src  = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Maybe Nat
Set.lookupIndex QName
f Set QName
names
             tgt :: Nat
tgt  = Nat
gInd
             cm :: CallMatrix
cm   = Nat -> Nat -> [[Order]] -> CallMatrix
makeCM Nat
ncols Nat
nrows [[Order]]
matrix'
             info :: CallPath
info = DList CallInfo -> CallPath
CallPath forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$
                    CallInfo
                      { callInfoTarget :: QName
callInfoTarget = QName
g
                      , callInfoCall :: Closure Term
callInfoCall   = Closure Term
doc
                      }
         forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
verboseS [Char]
"term.kept.call" Nat
5 forall a b. (a -> b) -> a -> b
$ do
           MaskedDeBruijnPatterns
pats <- TerM MaskedDeBruijnPatterns
terGetPatterns
           forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.kept.call" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
             [ TCMT IO Doc
"kept call from" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow QName
f) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MaskedDeBruijnPatterns
pats)
             , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"to" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow QName
g) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                         forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) [Term]
args)
             , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"call matrix (with guardedness): "
             , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty CallMatrix
cm
             ]
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall cinfo.
Nat
-> Nat -> CallMatrix -> cinfo -> CallGraph cinfo -> CallGraph cinfo
CallGraph.insert Nat
src Nat
tgt CallMatrix
cm CallPath
info Calls
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 -> TCMT IO Term
reduceCon = forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM forall a b. (a -> b) -> a -> b
$ \case
      Con ConHead
c ConInfo
ci Elims
vs -> (forall t. Apply t => t -> Elims -> t
`applyE` Elims
vs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.reduce" Nat
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Trying to reduce away call: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v0

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

  -- Then, collect its non-recursive clauses.
  [Clause]
cls <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ QName -> TCM [Clause]
getNonRecursiveClauses QName
g
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.reduce" Nat
40 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [ [Char]
"Function has", forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Clause]
cls), [Char]
"non-recursive exact clauses"]
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.reduce" Nat
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
g Bool
True) [Clause]
cls
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn  [Char]
"term.reduce" Nat
80 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"allowed reductions = " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SmallSetElement a => SmallSet a -> [a]
SmallSet.elems
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> SmallSet AllowedReduction
envAllowedReductions

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

getNonRecursiveClauses :: QName -> TCM [Clause]
getNonRecursiveClauses :: QName -> TCM [Clause]
getNonRecursiveClauses QName
q =
  forall a. (a -> Bool) -> [a] -> [a]
filter (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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> [Clause]
defClauses forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  where
  nonrec :: Clause -> Bool
nonrec = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseRecursive
  exact :: Clause -> Bool
exact  = forall a. a -> Maybe a -> a
fromMaybe Bool
False 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
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.check.term" Nat
50 forall a b. (a -> b) -> a -> b
$ do
      TCMT IO Doc
"looking for calls in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t

    -- Instantiate top-level MetaVar.
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
t 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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 = forall a b. [a] -> [b] -> [(a, b)]
zip [Arg Term]
args forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all 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   = forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive    -- not guarding, but preserving
            coinductive :: TerM Induction
coinductive = forall (m :: * -> *) a. Monad m => a -> m a
return Induction
CoInductive  -- guarding
        -- ♯ is guarding
        Induction
ind <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM (Maybe QName)
terGetSharp) TerM Induction
coinductive forall a b. (a -> b) -> a -> b
$ {-else-} do
          -- data constructors are not guarding
          if DataOrRecord
dataOrRec forall a. Eq a => a -> a -> Bool
== DataOrRecord
IsData then TerM Induction
inductive else do
          -- abstract constructors are not guarding
          forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) TerM Induction
inductive forall a b. (a -> b) -> a -> b
$ \ (QName
q, Defn
def) -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"term.check.term" Nat
50 forall a b. (a -> b) -> a -> b
$ [Char]
"constructor " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
c forall a. [a] -> [a] -> [a]
++ [Char]
" has record type " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
q
            -- inductive record constructors are not guarding
            if Defn -> Maybe Induction
recInduction Defn
def forall a. Eq a => a -> a -> Bool
/= 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
            forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([QName] -> TerM Bool
targetElem forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Defn -> Maybe [QName]
recMutual Defn
def)
               {-then-} TerM Induction
coinductive
               {-else-} TerM Induction
inductive
        QName -> Induction -> [(Arg Term, Bool)] -> TerM Calls
constructor QName
c Induction
ind [(Arg Term, Bool)]
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 forall a. ExtractCalls a => a -> TerM Calls
extract 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 -> forall a. ExtractCalls a => a -> TerM Calls
extract Abs Term
b

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

      -- Dependent function space.
      Pi Dom' Term Type
a (Abs [Char]
x Type
b) ->
        forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
CallGraph.union forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        forall a. ExtractCalls a => a -> TerM Calls
extract Dom' Term Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> do
          Dom' Term Type
a <- 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!
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Char]
x, Dom' Term Type
a) forall a b. (a -> b) -> a -> b
$ forall a. TerM a -> TerM a
terRaise forall a b. (a -> b) -> a -> b
$ forall a. ExtractCalls a => a -> TerM Calls
extract Type
b

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

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

      -- Sort.
      Sort Sort
s -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty

      -- Erased and not-yet-erased proof.
      DontCare Term
t -> 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.
        forall a. ExtractCalls a => a -> TerM Calls
extract Level' Term
l

      -- Dummy.
      Dummy{} -> forall (m :: * -> *) a. Monad m => a -> m a
return 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) = 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) = 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 = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  let a :: Type
a = forall t e. Dom' t e -> e
unDom Dom' Term Type
dom
  (Maybe QName
msize, Maybe QName
msizelt) <- forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  case (Maybe QName
msize, Maybe QName
msizelt) of
    (Maybe QName
_ , Maybe QName
Nothing) -> forall (m :: * -> *) a. Monad m => a -> m a
return Dom' Term Type
dom
    (Maybe QName
Nothing, Maybe QName
_)  -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (Just QName
size, Just QName
sizelt) -> do
      TelV Telescope
tel Type
c <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
      case Type
a of
        El Sort
s (Def QName
d [Elim
v]) | QName
d forall a. Eq a => a -> a -> Bool
== QName
sizelt -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
size []) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom' Term Type
dom
        Type
_ -> 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 (Nat, Nat, [[Order]])
compareArgs Elims
es = do
  MaskedDeBruijnPatterns
pats <- TerM MaskedDeBruijnPatterns
terGetPatterns
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compareArgs" Nat
90 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"comparing " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es) forall a. [a] -> [a] -> [a]
++ [Char]
" args to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length MaskedDeBruijnPatterns
pats) forall a. [a] -> [a] -> [a]
++ [Char]
" 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
  [[Order]]
matrix <- forall a b. UsableSizeVars a => a -> TerM b -> TerM b
withUsableVars MaskedDeBruijnPatterns
pats forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Elims
es forall a b. (a -> b) -> a -> b
$ \ Elim
e -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM MaskedDeBruijnPatterns
pats 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).
  Nat
projsCaller <- forall (t :: * -> *) a. Foldable t => t a -> Nat
length forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection Bool
True) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AmbiguousQName -> QName
headAmbQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Masked a -> a
getMasked) MaskedDeBruijnPatterns
pats
  Nat
projsCallee <- forall (t :: * -> *) a. Foldable t => t a -> Nat
length forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection Bool
True) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim) Elims
es
  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = CutOff
cutoff
  Bool
useGuardedness <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall (m :: * -> *). HasOptions m => m Bool
guardednessOption
  let guardedness :: Order
guardedness =
        if Bool
useGuardedness
        then (?cutoff::CutOff) => Bool -> Nat -> Order
decr Bool
True forall a b. (a -> b) -> a -> b
$ Nat
projsCaller forall a. Num a => a -> a -> a
- Nat
projsCallee
        else Order
Order.le
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.guardedness" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"compareArgs:"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"projsCaller = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Nat
projsCaller
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"projsCallee = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Nat
projsCallee
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"guardedness of call: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Order
guardedness
    ]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Order -> (Nat, Nat, [[Order]]) -> (Nat, Nat, [[Order]])
addGuardedness Order
guardedness (forall a. Sized a => a -> Nat
size Elims
es, forall a. Sized a => a -> Nat
size MaskedDeBruijnPatterns
pats, [[Order]]
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
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compare" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"compareElim"
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"e = " forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim
e
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"p = " forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Masked DeBruijnPattern
p
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compare" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"e = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Elim
e
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"p = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Masked DeBruijnPattern
p
      ]
  case (Elim
e, forall a. Masked a -> a
getMasked Masked DeBruijnPattern
p) of
    (Proj ProjOrigin
_ QName
d, ProjP ProjOrigin
_ QName
d') -> do
      QName
d  <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d
      QName
d' <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d'
      Order
o  <- forall (tcm :: * -> *). MonadTCM tcm => QName -> QName -> tcm Order
compareProj QName
d QName
d'
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compare" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"comparing callee projection " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
d
        , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"against caller projection " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
d'
        , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"yields order " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Order
o
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return Order
o
    (Proj{}, DeBruijnPattern
_)            -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
    (Apply{}, ProjP{})     -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
    (Apply Arg Term
arg, DeBruijnPattern
_)         -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm (forall e. Arg e -> e
unArg Arg Term
arg) Masked DeBruijnPattern
p
    -- TODO Andrea: making sense?
    (IApply{}, ProjP{})  -> 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 forall a. Eq a => a -> a -> Bool
== QName
d' = forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le
  | Bool
otherwise = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      -- different projections
      Maybe QName
mr  <- QName -> TCM (Maybe QName)
getRecordOfField QName
d
      Maybe QName
mr' <- QName -> TCM (Maybe QName)
getRecordOfField QName
d'
      case (Maybe QName
mr, Maybe QName
mr') of
        (Just QName
r, Just QName
r') | QName
r forall a. Eq a => a -> a -> Bool
== QName
r' -> do
          -- of same record
          Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
          case Defn
def of
            Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } -> do
              [QName]
fs <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom [Dom QName]
fs
              case (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (QName
dforall a. Eq a => a -> a -> Bool
==) [QName]
fs, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (QName
d'forall a. Eq a => a -> a -> Bool
==) [QName]
fs) of
                (Just QName
i, Just QName
i')
                  -- earlier field is smaller
                  | QName
i forall a. Ord a => a -> a -> Bool
< QName
i'    -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.lt
                  | QName
i forall a. Eq a => a -> a -> Bool
== QName
i'   -> do
                     forall a. HasCallStack => a
__IMPOSSIBLE__
                  | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
                (Maybe QName, Maybe QName)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
            Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
        (Maybe QName, Maybe QName)
_ -> 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 :: Nat -> Nat -> [[Order]] -> CallMatrix
makeCM Nat
ncols Nat
nrows [[Order]]
matrix = forall a. Matrix Nat a -> CallMatrix' a
CallMatrix forall a b. (a -> b) -> a -> b
$
  forall i b.
(Ord i, Num i, Enum i, HasZero b) =>
Size i -> [[b]] -> Matrix i b
Matrix.fromLists (forall i. i -> i -> Size i
Matrix.Size Nat
nrows Nat
ncols) [[Order]]
matrix

-- | 'addGuardedness' adds guardedness flag in the upper left corner
-- (0,0).
addGuardedness :: Order -> (Int, Int, [[Order]]) -> (Int, Int, [[Order]])
addGuardedness :: Order -> (Nat, Nat, [[Order]]) -> (Nat, Nat, [[Order]])
addGuardedness Order
o (Nat
nrows, Nat
ncols, [[Order]]
m) =
  (Nat
nrows forall a. Num a => a -> a -> a
+ Nat
1, Nat
ncols forall a. Num a => a -> a -> a
+ Nat
1,
   (Order
o forall a. a -> [a] -> [a]
: forall a. Nat -> a -> [a]
replicate Nat
ncols Order
Order.unknown) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Order
Order.unknown 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
corner) forall a. a -> [a] -> [a]
: [Order]
row) forall a. a -> [a] -> [a]
: [[Order]]
rows
composeGuardedness 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 Nat
offsetFromConstructor QName
c =
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c) (forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0) (forall (m :: * -> *) a. Monad m => a -> m a
return Nat
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
  Term
t <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
t
  Order
o <- Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
t Masked DeBruijnPattern
p
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compare" Nat
25 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
" comparing term " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCMT IO Doc
" to pattern " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Masked DeBruijnPattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
" results in " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Order
o)
  forall (m :: * -> *) a. Monad m => a -> m a
return Order
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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. StripAllProjections a => a -> TCM a
stripAllProjections

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

instance StripAllProjections Args where
  stripAllProjections :: [Arg Term] -> TCM [Arg Term]
stripAllProjections = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. StripAllProjections a => a -> TCM a
stripAllProjections

instance StripAllProjections Term where
  stripAllProjections :: Term -> TCMT IO Term
stripAllProjections Term
t = do
    case Term
t of
      Var Nat
i Elims
es   -> Nat -> Elims -> Term
Var Nat
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
ts
      Def QName
d Elims
es   -> QName -> Elims -> Term
Def QName
d forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
es
      DontCare Term
t -> forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
t
      Term
_ -> 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 -> forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m (Either a b) -> m b
fromRightM (\ SigError
err -> forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c) (QName -> TCM (Either SigError ConHead)
getConForm (ConHead -> QName
conName ConHead
c)) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ ConHead
c' ->
    forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c' ConPatternInfo
i NAPs
ps
  DeBruijnPattern
p -> 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
  Maybe QName
suc  <- TerM (Maybe QName)
terGetSizeSuc
  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = CutOff
cutoff
  Term
v <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v)
  DeBruijnPattern
p <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TCM DeBruijnPattern
reduceConPattern DeBruijnPattern
p
  case (Term
v, DeBruijnPattern
p) of

    -- Andreas, 2013-11-20 do not drop projections,
    -- in any case not coinductive ones!:
    (Var Nat
i Elims
es, DeBruijnPattern
_) | Just{} <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
      Nat -> Masked DeBruijnPattern -> TerM Order
compareVar Nat
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 -> Nat -> Order
Order.decr Bool
True forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max (if Bool
m then Nat
0 else forall a. Pattern' a -> Nat
patternDepth DeBruijnPattern
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => a -> a
pred forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
       forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Nat
_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 forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
s' Bool -> Bool -> Bool
&& forall a. a -> Maybe a
Just QName
s forall a. Eq a => a -> a -> Bool
== Maybe QName
suc ->
      Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (forall e. Arg e -> e
unArg Arg Term
t) (forall a. a -> Masked a
notMasked forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p)

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

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

    (Lit Literal
l, DeBruijnPattern
_) -> do
      Term
v <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v
      case Term
v of
        Lit{}       -> 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) | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
isSubTerm Term
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) NAPs
ps ->
      (?cutoff::CutOff) => Bool -> Nat -> Order
decr Bool
True forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
offsetFromConstructor (ConHead -> QName
conName ConHead
c)

    (Con ConHead
c ConInfo
_ Elims
es, ConP ConHead
c' ConPatternInfo
_ NAPs
ps) | ConHead -> QName
conName ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c'->
      let ts :: [Arg Term]
ts = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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
_) -> 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      Nat -> Order -> Order
increase forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
offsetFromConstructor (ConHead -> QName
conName ConHead
c)
               forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((?cutoff::CutOff) => [Order] -> Order
infimum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Arg Term
t -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (forall e. Arg e -> e
unArg Arg Term
t) Masked DeBruijnPattern
mp) [Arg Term]
ts)

    (Term
t, DeBruijnPattern
p) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => 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
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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es in
      forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ (ConHead -> QName
conName ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c')
          forall a. a -> [a] -> [a]
: (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Term]
ts forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length NAPs
ps)
          forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg Term
t Arg (Named_ DeBruijnPattern)
p -> Term -> DeBruijnPattern -> Bool
equal (forall e. Arg e -> e
unArg Arg Term
t) (forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p)) [Arg Term]
ts NAPs
ps
    equal (Var Nat
i []) (VarP PatternInfo
_ DBPatVar
x) = Nat
i forall a. Eq a => a -> a -> Bool
== DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
    equal (Lit Literal
l)    (LitP PatternInfo
_ Literal
l') = Literal
l 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 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 forall a b. (a -> b) -> a -> b
$ Nat -> Order -> Order
decrease Nat
1 forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => [Order] -> Order
supremum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
subTerm Term
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => 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
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = CutOff
cutoff
  case forall a. Ord a => a -> a -> Ordering
compare (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Term]
ts) (forall (t :: * -> *) a. Foldable t => t a -> Nat
length NAPs
ps) of

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

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

    Ordering
EQ -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (?cutoff::CutOff) => Order -> Order -> Order
(Order..*.) Order
Order.le forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
               forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Term]
ts) (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Masked a
notMasked forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: Nat -> Masked DeBruijnPattern -> TerM Order
compareVar Nat
i (Masked Bool
m DeBruijnPattern
p) = do
  Maybe QName
suc    <- TerM (Maybe QName)
terGetSizeSuc
  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = CutOff
cutoff
  let no :: TerM Order
no = forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
  case DeBruijnPattern
p of
    ProjP{}   -> TerM Order
no
    IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x  -> Nat -> Masked DBPatVar -> TerM Order
compareVarVar Nat
i (forall a. Bool -> a -> Masked a
Masked Bool
m DBPatVar
x)
    LitP{}    -> TerM Order
no
    DotP{}   -> TerM Order
no
    VarP PatternInfo
_ DBPatVar
x  -> Nat -> Masked DBPatVar -> TerM Order
compareVarVar Nat
i (forall a. Bool -> a -> Masked a
Masked Bool
m DBPatVar
x)

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

    ConP ConHead
c ConPatternInfo
_ NAPs
ps -> if Bool
m then TerM Order
no else Bool -> Order -> Order
setUsability Bool
True forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      Nat -> Order -> Order
decrease forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
offsetFromConstructor (ConHead -> QName
conName ConHead
c)
               forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((?cutoff::CutOff) => [Order] -> Order
Order.supremum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Nat -> Masked DeBruijnPattern -> TerM Order
compareVar Nat
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Masked a
notMasked forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) NAPs
ps)
    DefP PatternInfo
_ QName
c NAPs
ps -> if Bool
m then TerM Order
no else Bool -> Order -> Order
setUsability Bool
True forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      Nat -> Order -> Order
decrease forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
offsetFromConstructor QName
c
               forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((?cutoff::CutOff) => [Order] -> Order
Order.supremum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Nat -> Masked DeBruijnPattern -> TerM Order
compareVar Nat
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Masked a
notMasked forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: Nat -> Masked DBPatVar -> TerM Order
compareVarVar Nat
i (Masked Bool
m x :: DBPatVar
x@(DBPatVar [Char]
_ Nat
j))
  | Nat
i forall a. Eq a => a -> a -> Bool
== Nat
j = if Bool -> Bool
not Bool
m then forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le else forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$
      -- If j is a size, we ignore the mask.
      forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
j)
        {- then -} (forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le)
        {- else -} (forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown)
  | Bool
otherwise = do
      -- record usability of variable
      Bool
u <- (Nat
i Nat -> IntSet -> Bool
`VarSet.member`) 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 Bool -> Bool
not Bool
u then forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown else do
      -- Only if usable:
      BoundedSize
res <- forall (m :: * -> *). PureTCM m => Nat -> m BoundedSize
isBounded Nat
i
      case BoundedSize
res of
        BoundedSize
BoundedNo  -> forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
        BoundedLt Term
v -> Bool -> Order -> Order
setUsability Bool
u forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Order -> Order
decrease Nat
1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
v (forall a. Bool -> a -> Masked a
Masked Bool
m forall a b. (a -> b) -> a -> b
$ forall a. a -> Pattern' a
varP DBPatVar
x)