{-# 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 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 = TCM Result -> TCM Result
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Result -> TCM Result) -> TCM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM Result
termDecl' Declaration
d


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

termDecl' :: A.Declaration -> TCM Result
termDecl' :: Declaration -> TCM Result
termDecl' = \case
    A.Axiom {}            -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Field {}            -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Primitive {}        -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Mutual MutualInfo
i [Declaration]
ds         -> [QName] -> TCM Result
termMutual ([QName] -> TCM Result) -> [QName] -> TCM Result
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [QName]
getNames [Declaration]
ds
    A.Section Range
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds    -> [Declaration] -> TCM Result
forall (t :: * -> *). Traversable t => t Declaration -> TCM Result
termDecls [Declaration]
ds
        -- section structure can be ignored as we are termination checking
        -- definitions lifted to the top-level
    A.Apply {}            -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Import {}           -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Pragma {}           -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Open {}             -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.PatternSynDef {}    -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.Generalize {}       -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
        -- open, pattern synonym and generalize defs are just artifacts from the concrete syntax
    A.ScopedDecl ScopeInfo
scope [Declaration]
ds -> {- withScope_ scope $ -} [Declaration] -> TCM Result
forall (t :: * -> *). Traversable t => t Declaration -> TCM Result
termDecls [Declaration]
ds
        -- scope is irrelevant as we are termination checking Syntax.Internal
    A.RecSig{}            -> Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
    A.RecDef DefInfo
_ QName
r UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
ds -> [Declaration] -> TCM Result
forall (t :: * -> *). Traversable t => t Declaration -> TCM Result
termDecls [Declaration]
ds
    -- These should all be wrapped in mutual blocks
    A.FunDef{}      -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DataSig{}     -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DataDef{}     -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteDecl{} -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.UnquoteDef{}  -> TCM Result
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    termDecls :: t Declaration -> TCM Result
termDecls t Declaration
ds = t Result -> Result
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (t Result -> Result) -> TCMT IO (t Result) -> TCM Result
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> TCM Result) -> t Declaration -> TCMT IO (t Result)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Declaration -> TCM Result
termDecl' t Declaration
ds

    -- The mutual names mentioned in the abstract syntax
    -- for symbols that need to be termination-checked.
    getNames :: [Declaration] -> [QName]
getNames = (Declaration -> [QName]) -> [Declaration] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Declaration -> [QName]
getName
    getName :: Declaration -> [QName]
getName (A.FunDef DefInfo
i QName
x Delayed
delayed [Clause]
cs)   = [QName
x]
    getName (A.RecDef DefInfo
_ QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
ds)   = [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 Expr
_)    = [QName]
xs
    getName (A.UnquoteDef [DefInfo]
_ [QName]
xs Expr
_)       = [QName]
xs
    getName Declaration
_                           = []


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

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

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

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

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

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

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

     -- Set the mutual names in the termination environment.
     let namesSCC :: [QName]
namesSCC = (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter ([QName]
allNames [QName] -> QName -> Bool
forall a. Ord a => [a] -> a -> Bool
`hasElem`) [QName]
names
     let setNames :: TerEnv -> TerEnv
setNames TerEnv
e = TerEnv
e
           { terMutual :: [QName]
terMutual    = [QName]
allNames
           , terUserNames :: [QName]
terUserNames = [QName]
namesSCC
           }
         runTerm :: TerM Result -> TCM Result
runTerm TerM Result
cont = TerM Result -> TCM Result
forall a. TerM a -> TCM a
runTerDefault (TerM Result -> TCM Result) -> TerM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ do
           CutOff
cutoff <- TerM CutOff
terGetCutOff
           VerboseKey -> VerboseLevel -> VerboseKey -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.top" VerboseLevel
10 (VerboseKey -> TerM ()) -> VerboseKey -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Termination checking " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [QName] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [QName]
namesSCC VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
             VerboseKey
" with cutoff=" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ CutOff -> VerboseKey
forall a. Show a => a -> VerboseKey
show CutOff
cutoff VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"..."
           (TerEnv -> TerEnv) -> TerM Result -> TerM Result
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.
     -- Since it is slow, only invoke it if
     -- any of the definitions uses copatterns.
     Result
res <- TCMT IO Bool -> TCM Result -> TCM Result -> TCM Result
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([TCMT IO Bool] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM ([TCMT IO Bool] -> TCMT IO Bool) -> [TCMT IO Bool] -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (QName -> TCMT IO Bool) -> [QName] -> [TCMT IO Bool]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCMT IO Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
usesCopatterns [QName]
allNames)
         -- Then: New check, one after another.
         (TerM Result -> TCM Result
runTerm (TerM Result -> TCM Result) -> TerM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ [QName] -> (QName -> TerM Result) -> TerM Result
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' [QName]
allNames ((QName -> TerM Result) -> TerM Result)
-> (QName -> TerM Result) -> TerM Result
forall a b. (a -> b) -> a -> b
$ QName -> TerM Result
termFunction)
         -- Else: Old check, all at once.
         (TerM Result -> TCM Result
runTerm (TerM Result -> TCM Result) -> TerM Result -> TCM Result
forall a b. (a -> b) -> a -> b
$ TerM Result
termMutual')

     -- Record result of termination check in signature.
     -- If there are some termination errors, we collect them in
     -- the state and mark the definition as non-terminating so
     -- that it does not get unfolded
     let terminates :: Bool
terminates = Result -> Bool
forall a. Null a => a -> Bool
null Result
res
     [QName] -> (QName -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
allNames ((QName -> TCMT IO ()) -> TCMT IO ())
-> (QName -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ QName
q -> QName -> Bool -> TCMT IO ()
setTerminates QName
q Bool
terminates
     Result -> TCM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
res

-- | @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
  [QName]
allNames <- TerM [QName]
terGetMutual
  let collect :: TerM Calls
collect = [QName] -> (QName -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' [QName]
allNames QName -> TerM Calls
termDef

  -- first try to termination check ignoring the dot patterns
  Calls
calls1 <- TerM Calls
collect
  VerboseKey -> Calls -> TerM ()
reportCalls VerboseKey
"no " Calls
calls1

  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  Either CallPath ()
r <- Either CallPath () -> TerM (Either CallPath ())
forall a. a -> TerM a
billToTerGraph (Either CallPath () -> TerM (Either CallPath ()))
-> Either CallPath () -> TerM (Either CallPath ())
forall a b. (a -> b) -> a -> b
$ Calls -> Either CallPath ()
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.
       TerM Bool
-> TerM (Either CallPath ())
-> TerM (Either CallPath ())
-> TerM (Either CallPath ())
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Cubical -> Bool)
-> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical (PragmaOptions -> Bool) -> TerM PragmaOptions -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (Either CallPath () -> TerM (Either CallPath ())
forall (m :: * -> *) a. Monad m => a -> m a
return Either CallPath ()
r) {- else -} (TerM (Either CallPath ()) -> TerM (Either CallPath ()))
-> TerM (Either CallPath ()) -> TerM (Either CallPath ())
forall a b. (a -> b) -> a -> b
$
       case Either CallPath ()
r of
         r :: Either CallPath ()
r@Right{} -> Either CallPath () -> TerM (Either CallPath ())
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 <- Bool -> TerM Calls -> TerM Calls
forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
True (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ TerM Calls
collect
           VerboseKey -> Calls -> TerM ()
reportCalls VerboseKey
"" Calls
calls2
           Either CallPath () -> TerM (Either CallPath ())
forall a. a -> TerM a
billToTerGraph (Either CallPath () -> TerM (Either CallPath ()))
-> Either CallPath () -> TerM (Either CallPath ())
forall a b. (a -> b) -> a -> b
$ Calls -> Either CallPath ()
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.
  [QName]
names <- TerM [QName]
terGetUserNames
  case Either CallPath ()
r of
    Left CallPath
calls -> Result -> TerM Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> TerM Result) -> Result -> TerM Result
forall a b. (a -> b) -> a -> b
$ TerminationError -> Result
forall el coll. Singleton el coll => el -> coll
singleton (TerminationError -> Result) -> TerminationError -> Result
forall a b. (a -> b) -> a -> b
$ [QName] -> [CallInfo] -> TerminationError
terminationError [QName]
names ([CallInfo] -> TerminationError) -> [CallInfo] -> TerminationError
forall a b. (a -> b) -> a -> b
$ CallPath -> [CallInfo]
callInfos CallPath
calls
    Right{} -> do
      TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.warn.yes" VerboseLevel
2 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        [QName] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow ([QName]
names) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" does termination check"
      Result -> TerM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty

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

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

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

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

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

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

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

-- | @termFunction name@ checks @name@ for termination.

termFunction :: QName -> TerM Result
termFunction :: QName -> TerM Result
termFunction QName
name = do

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

  [QName]
allNames <- TerM [QName]
terGetMutual
  let index :: VerboseLevel
index = VerboseLevel -> Maybe VerboseLevel -> VerboseLevel
forall a. a -> Maybe a -> a
fromMaybe VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe VerboseLevel -> VerboseLevel)
-> Maybe VerboseLevel -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> Maybe VerboseLevel
forall a. Eq a => a -> [a] -> Maybe VerboseLevel
List.elemIndex QName
name [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.
  Maybe QName
target <- TCM (Maybe QName) -> TerM (Maybe QName)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe QName) -> TerM (Maybe QName))
-> TCM (Maybe QName) -> TerM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ do Type -> TCM (Maybe QName)
forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm (Maybe QName)
typeEndsInDef (Type -> TCM (Maybe QName))
-> (Definition -> Type) -> Definition -> TCM (Maybe QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCM (Maybe QName))
-> TCMT IO Definition -> TCM (Maybe QName)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
  Maybe QName -> TerM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, Pretty a) =>
Maybe a -> tcm ()
reportTarget Maybe QName
target
  Maybe QName -> TerM Result -> TerM Result
forall a. Maybe QName -> TerM a -> TerM a
terSetTarget Maybe QName
target (TerM Result -> TerM Result) -> TerM Result -> TerM Result
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 = (((Set VerboseLevel, Set VerboseLevel, Calls)
 -> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)))
-> (Set VerboseLevel, Set VerboseLevel, Calls) -> TerM Calls
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Either b a)) -> a -> m b
`trampolineM` (VerboseLevel -> Set VerboseLevel
forall a. a -> Set a
Set.singleton VerboseLevel
index, Set VerboseLevel
forall a. Monoid a => a
mempty, Calls
forall a. Monoid a => a
mempty)) (((Set VerboseLevel, Set VerboseLevel, Calls)
  -> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)))
 -> TerM Calls)
-> ((Set VerboseLevel, Set VerboseLevel, Calls)
    -> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)))
-> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ (Set VerboseLevel
todo, Set VerboseLevel
done, Calls
calls) -> do
          if Set VerboseLevel -> Bool
forall a. Null a => a -> Bool
null Set VerboseLevel
todo then Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
-> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
 -> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)))
-> Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
-> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls))
forall a b. (a -> b) -> a -> b
$ Calls -> Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
forall a b. a -> Either a b
Left Calls
calls else do
            -- Extract calls originating from indices in @todo@.
            Calls
new <- Set VerboseLevel -> (VerboseLevel -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' Set VerboseLevel
todo ((VerboseLevel -> TerM Calls) -> TerM Calls)
-> (VerboseLevel -> TerM Calls) -> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ VerboseLevel
i ->
              QName -> TerM Calls
termDef (QName -> TerM Calls) -> QName -> TerM Calls
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> Maybe QName -> QName
forall a b. (a -> b) -> a -> b
$ [QName]
allNames [QName] -> VerboseLevel -> Maybe QName
forall a. [a] -> VerboseLevel -> Maybe a
!!! VerboseLevel
i
            -- Mark those functions as processed and add the calls to the result.
            let done' :: Set VerboseLevel
done'  = Set VerboseLevel
done Set VerboseLevel -> Set VerboseLevel -> Set VerboseLevel
forall a. Monoid a => a -> a -> a
`mappend` Set VerboseLevel
todo
                calls' :: Calls
calls' = Calls
new  Calls -> Calls -> Calls
forall a. Monoid a => a -> a -> a
`mappend` Calls
calls
            -- Compute the new todo list:
                todo' :: Set VerboseLevel
todo' = Calls -> Set VerboseLevel
forall cinfo. CallGraph cinfo -> Set VerboseLevel
CallGraph.targetNodes Calls
new Set VerboseLevel -> Set VerboseLevel -> Set VerboseLevel
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set VerboseLevel
done'
            -- Jump the trampoline.
            Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
-> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
 -> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)))
-> Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
-> TerM (Either Calls (Set VerboseLevel, Set VerboseLevel, Calls))
forall a b. (a -> b) -> a -> b
$ (Set VerboseLevel, Set VerboseLevel, Calls)
-> Either Calls (Set VerboseLevel, Set VerboseLevel, Calls)
forall a b. b -> Either a b
Right (Set VerboseLevel
todo', Set VerboseLevel
done', Calls
calls')

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

    Either [CallInfo] ()
r <- do
     CutOff
cutoff <- TerM CutOff
terGetCutOff
     let ?cutoff = cutoff
     Either CallPath ()
r <- Either CallPath () -> TerM (Either CallPath ())
forall a. a -> TerM a
billToTerGraph (Either CallPath () -> TerM (Either CallPath ()))
-> Either CallPath () -> TerM (Either CallPath ())
forall a b. (a -> b) -> a -> b
$ (VerboseLevel -> Bool) -> Calls -> Either CallPath ()
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
(VerboseLevel -> Bool) -> CallGraph cinfo -> Either cinfo ()
Term.terminatesFilter (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
index) Calls
calls1
     case Either CallPath ()
r of
       Right () -> Either [CallInfo] () -> TerM (Either [CallInfo] ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [CallInfo] () -> TerM (Either [CallInfo] ()))
-> Either [CallInfo] () -> TerM (Either [CallInfo] ())
forall a b. (a -> b) -> a -> b
$ () -> Either [CallInfo] ()
forall a b. b -> Either a b
Right ()
       Left{}    -> do
         -- Try again, but include the dot patterns this time.
         Calls
calls2 <- Bool -> TerM Calls -> TerM Calls
forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
True (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ TerM Calls
collect
         VerboseKey -> Calls -> TerM ()
reportCalls VerboseKey
"" Calls
calls2
         Either [CallInfo] () -> TerM (Either [CallInfo] ())
forall a. a -> TerM a
billToTerGraph (Either [CallInfo] () -> TerM (Either [CallInfo] ()))
-> Either [CallInfo] () -> TerM (Either [CallInfo] ())
forall a b. (a -> b) -> a -> b
$ (CallPath -> [CallInfo])
-> Either CallPath () -> Either [CallInfo] ()
forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft CallPath -> [CallInfo]
callInfos (Either CallPath () -> Either [CallInfo] ())
-> Either CallPath () -> Either [CallInfo] ()
forall a b. (a -> b) -> a -> b
$ (VerboseLevel -> Bool) -> Calls -> Either CallPath ()
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
(VerboseLevel -> Bool) -> CallGraph cinfo -> Either cinfo ()
Term.terminatesFilter (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
index) Calls
calls2

    [QName]
names <- TerM [QName]
terGetUserNames
    case Either [CallInfo] ()
r of
      Left [CallInfo]
calls -> Result -> TerM Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> TerM Result) -> Result -> TerM Result
forall a b. (a -> b) -> a -> b
$ TerminationError -> Result
forall el coll. Singleton el coll => el -> coll
singleton (TerminationError -> Result) -> TerminationError -> Result
forall a b. (a -> b) -> a -> b
$ [QName] -> [CallInfo] -> TerminationError
terminationError ([QName
name] [QName] -> [QName] -> [QName]
forall a. Eq a => [a] -> [a] -> [a]
`List.intersect` [QName]
names) [CallInfo]
calls
      Right () -> do
        TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.warn.yes" VerboseLevel
2 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
          QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
name VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" does termination check"
        Result -> TerM Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
forall a. Monoid a => a
mempty
   where
     reportTarget :: Maybe a -> tcm ()
reportTarget Maybe a
r = TCMT IO () -> tcm ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
forall a b. (a -> b) -> a -> b
$
       VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.target" VerboseLevel
20 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  target type " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
         Maybe a -> VerboseKey -> (a -> VerboseKey) -> VerboseKey
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe a
r VerboseKey
"not recognized" (\ a
q ->
           VerboseKey
"ends in " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ a -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow a
q)

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

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

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

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

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

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

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

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

        Defn
_ -> Calls -> TerM Calls
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
  where
    hasDefP :: [NamedArg DeBruijnPattern] -> Bool
    hasDefP :: [NamedArg DeBruijnPattern] -> Bool
hasDefP [NamedArg DeBruijnPattern]
ps = Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ ((DeBruijnPattern -> Any) -> [NamedArg DeBruijnPattern] -> Any)
-> [NamedArg DeBruijnPattern] -> (DeBruijnPattern -> Any) -> Any
forall a b c. (a -> b -> c) -> b -> a -> c
flip (DeBruijnPattern -> Any) -> [NamedArg DeBruijnPattern] -> Any
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern [NamedArg DeBruijnPattern]
ps ((DeBruijnPattern -> Any) -> Any)
-> (DeBruijnPattern -> Any) -> Any
forall a b. (a -> b) -> a -> b
$ \ (DeBruijnPattern
x :: DeBruijnPattern) ->
                  case DeBruijnPattern
x of
                    DefP{} -> Bool -> Any
Any Bool
True
                    DeBruijnPattern
_      -> Bool -> Any
Any Bool
False


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

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

  -- create n variable patterns
  mkPats :: VerboseLevel -> f [Masked DeBruijnPattern]
mkPats VerboseLevel
n  = (VerboseLevel -> Name -> Masked DeBruijnPattern)
-> [VerboseLevel] -> [Name] -> [Masked DeBruijnPattern]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VerboseLevel -> Name -> Masked DeBruijnPattern
forall a. Pretty a => VerboseLevel -> a -> Masked DeBruijnPattern
mkPat (VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
n) ([Name] -> [Masked DeBruijnPattern])
-> f [Name] -> f [Masked DeBruijnPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f [Name]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  mkPat :: VerboseLevel -> a -> Masked DeBruijnPattern
mkPat VerboseLevel
i a
x = DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> DBPatVar
DBPatVar (a -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow a
x) VerboseLevel
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 :: Type -> TerM a -> TerM a
setMasks Type
t TerM a
cont = do
  ([Bool]
ds, Bool
d) <- TCM ([Bool], Bool) -> TerM ([Bool], Bool)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM ([Bool], Bool) -> TerM ([Bool], Bool))
-> TCM ([Bool], Bool) -> TerM ([Bool], Bool)
forall a b. (a -> b) -> a -> b
$ do
    TelV Tele (Dom Type)
tel Type
core <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
    -- Check argument types
    [Bool]
ds <- [Dom (VerboseKey, Type)]
-> (Dom (VerboseKey, Type) -> TCMT IO Bool) -> TCMT IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel) ((Dom (VerboseKey, Type) -> TCMT IO Bool) -> TCMT IO [Bool])
-> (Dom (VerboseKey, Type) -> TCMT IO Bool) -> TCMT IO [Bool]
forall a b. (a -> b) -> a -> b
$ \ Dom (VerboseKey, Type)
t -> do
      TelV Tele (Dom Type)
_ Type
t <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ (VerboseKey, Type) -> Type
forall a b. (a, b) -> b
snd ((VerboseKey, Type) -> Type) -> (VerboseKey, Type) -> Type
forall a b. (a -> b) -> a -> b
$ Dom (VerboseKey, Type) -> (VerboseKey, Type)
forall t e. Dom' t e -> e
unDom Dom (VerboseKey, Type)
t
      Bool
d <- (Maybe QName -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe QName -> Bool) -> TCM (Maybe QName) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
isDataOrRecord (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t)) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
t)
      Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.mask" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
          TCM Doc
"argument type "
            TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" is not data or record type, ignoring structural descent for --without-K"
      Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
d
    -- Check result types
    Bool
d  <- Maybe QName -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe QName -> Bool)
-> (Type -> TCM (Maybe QName)) -> Type -> TCMT IO Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Term -> TCM (Maybe QName)
isDataOrRecord (Term -> TCM (Maybe QName))
-> (Type -> Term) -> Type -> TCM (Maybe QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> TCMT IO Bool) -> Type -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type
core
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.mask" VerboseLevel
20 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"result type is not data or record type, ignoring guardedness for --without-K"
    ([Bool], Bool) -> TCM ([Bool], Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool]
ds, Bool
d)
  [Bool] -> TerM a -> TerM a
forall a. [Bool] -> TerM a -> TerM a
terSetMaskArgs ([Bool]
ds [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True) (TerM a -> TerM a) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ Bool -> TerM a -> TerM a
forall a. Bool -> TerM a -> TerM a
terSetMaskResult Bool
d (TerM a -> TerM a) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ TerM a
cont


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

targetElem :: [Target] -> TerM Bool
targetElem :: [QName] -> TerM Bool
targetElem [QName]
ds = Bool -> (QName -> Bool) -> Maybe QName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
ds) (Maybe QName -> Bool) -> TerM (Maybe QName) -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM (Maybe QName)
terGetTarget

{-
-- | The target type of the considered recursive definition.
data Target
  = Set        -- ^ Constructing a Set (only meaningful with 'guardingTypeConstructors').
  | Data QName -- ^ Constructing a coinductive or mixed type (could be data or record).
  deriving (Eq, Show)

-- | Check wether a 'Target" corresponds to the current one.
matchingTarget :: DBPConf -> Target -> TCM Bool
matchingTarget conf t = maybe (return True) (match t) (currentTarget conf)
  where
    match Set      Set       = return True
    match (Data d) (Data d') = mutuallyRecursive d d'
    match _ _                = return False
-}

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

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

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

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

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

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

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

instance TermToPattern Term DeBruijnPattern where
  termToPattern :: Term -> TerM DeBruijnPattern
termToPattern Term
t = TCM Term -> TerM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (Term -> TCM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
t) TerM Term -> (Term -> TerM DeBruijnPattern) -> TerM DeBruijnPattern
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    -- Constructors.
    Con ConHead
c ConInfo
_ Elims
args -> ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> ([Arg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [Arg DeBruijnPattern]
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg DeBruijnPattern -> NamedArg DeBruijnPattern)
-> [Arg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> Arg DeBruijnPattern -> NamedArg DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Named NamedName DeBruijnPattern
forall a name. a -> Named name a
unnamed) ([Arg DeBruijnPattern] -> DeBruijnPattern)
-> TerM [Arg DeBruijnPattern] -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TerM [Arg DeBruijnPattern]
forall a b. TermToPattern a b => a -> TerM b
termToPattern ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
args)
    Def QName
s [Apply Arg Term
arg] -> do
      Maybe QName
suc <- TerM (Maybe QName)
terGetSizeSuc
      if QName -> Maybe QName
forall a. a -> Maybe a
Just QName
s Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
suc then ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
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 ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> ([Arg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [Arg DeBruijnPattern]
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg DeBruijnPattern -> NamedArg DeBruijnPattern)
-> [Arg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> Arg DeBruijnPattern -> NamedArg DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Named NamedName DeBruijnPattern
forall a name. a -> Named name a
unnamed) ([Arg DeBruijnPattern] -> DeBruijnPattern)
-> TerM [Arg DeBruijnPattern] -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TerM [Arg DeBruijnPattern]
forall a b. TermToPattern a b => a -> TerM b
termToPattern [Arg Term
arg]
       else DeBruijnPattern -> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> TerM DeBruijnPattern)
-> DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Term
t
    DontCare Term
t  -> Term -> TerM DeBruijnPattern
forall a b. TermToPattern a b => a -> TerM b
termToPattern Term
t -- OR: __IMPOSSIBLE__  -- removed by stripAllProjections
    -- Leaves.
    Var VerboseLevel
i []    -> DBPatVar -> DeBruijnPattern
forall a. a -> Pattern' a
varP (DBPatVar -> DeBruijnPattern)
-> (Name -> DBPatVar) -> Name -> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseKey -> VerboseLevel -> DBPatVar
`DBPatVar` VerboseLevel
i) (VerboseKey -> DBPatVar)
-> (Name -> VerboseKey) -> Name -> DBPatVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Name -> DeBruijnPattern) -> TerM Name -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> TerM Name
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Name
nameOfBV VerboseLevel
i
    Lit Literal
l       -> DeBruijnPattern -> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> TerM DeBruijnPattern)
-> DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Literal -> DeBruijnPattern
forall a. Literal -> Pattern' a
litP Literal
l
    Dummy VerboseKey
s Elims
_   -> VerboseKey -> TerM DeBruijnPattern
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s
    Term
t           -> DeBruijnPattern -> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> TerM DeBruijnPattern)
-> DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Term
t


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


-- | Extract recursive calls from one clause.
termClause :: Clause -> TerM Calls
termClause :: Clause -> TerM Calls
termClause Clause
clause = do
  Clause{ clauseTel :: Clause -> Tele (Dom Type)
clauseTel = Tele (Dom Type)
tel, namedClausePats :: Clause -> [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
body } <- Clause -> TerM Clause
forall (tcm :: * -> *). MonadTCM tcm => Clause -> tcm Clause
etaExpandClause Clause
clause
  TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.check.clause" VerboseLevel
25 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"termClause"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ps  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> TCM Doc
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
ps
    ]
  Maybe Term -> (Term -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' Maybe Term
body ((Term -> TerM Calls) -> TerM Calls)
-> (Term -> TerM Calls) -> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ Term
v -> Tele (Dom Type) -> TerM Calls -> TerM Calls
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do
    -- TODO: combine the following two traversals, avoid full normalisation.
    -- Parse dot patterns as patterns as far as possible.
    [NamedArg DeBruijnPattern]
ps <- (DeBruijnPattern -> TerM DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> TerM [NamedArg DeBruijnPattern]
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM DeBruijnPattern -> TerM DeBruijnPattern
parseDotP [NamedArg DeBruijnPattern]
ps
    -- Blank out coconstructors.
    [NamedArg DeBruijnPattern]
ps <- (DeBruijnPattern -> TerM DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> TerM [NamedArg DeBruijnPattern]
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
preTraversePatternM DeBruijnPattern -> TerM DeBruijnPattern
stripCoCon [NamedArg DeBruijnPattern]
ps
    -- Mask non-data arguments.
    [Masked DeBruijnPattern]
mdbpats <- [DeBruijnPattern] -> TerM [Masked DeBruijnPattern]
maskNonDataArgs ([DeBruijnPattern] -> TerM [Masked DeBruijnPattern])
-> [DeBruijnPattern] -> TerM [Masked DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg [NamedArg DeBruijnPattern]
ps
    [Masked DeBruijnPattern] -> TerM Calls -> TerM Calls
forall a. [Masked DeBruijnPattern] -> TerM a -> TerM a
terSetPatterns [Masked DeBruijnPattern]
mdbpats (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do
      Tele (Dom Type) -> TerM Calls -> TerM Calls
forall a. Tele (Dom Type) -> TerM a -> TerM a
terSetSizeDepth Tele (Dom Type)
tel (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do
        Term -> TerM ()
reportBody Term
v
        Term -> TerM Calls
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        -> DeBruijnPattern -> TerM DeBruijnPattern
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
_ [NamedArg DeBruijnPattern]
_ -> do
        TerM Bool
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe QName -> Bool) -> TerM (Maybe QName) -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM (Maybe QName)
terGetSizeSuc) (DeBruijnPattern -> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p) (TerM DeBruijnPattern -> TerM DeBruijnPattern)
-> TerM DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ {- else -} do
        QName -> TerM Induction
forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Induction
whatInduction QName
c TerM Induction
-> (Induction -> TerM DeBruijnPattern) -> TerM DeBruijnPattern
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Induction
Inductive   -> DeBruijnPattern -> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
          Induction
CoInductive -> DeBruijnPattern -> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
unusedVar
      DeBruijnPattern
_ -> DeBruijnPattern -> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
    reportBody :: Term -> TerM ()
    reportBody :: Term -> TerM ()
reportBody Term
v = VerboseKey -> VerboseLevel -> TerM () -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"term.check.clause" VerboseLevel
6 (TerM () -> TerM ()) -> TerM () -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
      QName
f       <- TerM QName
terGetCurrent
      Delayed
delayed <- TerM Delayed
terGetDelayed
      [Masked DeBruijnPattern]
pats    <- TerM [Masked DeBruijnPattern]
terGetPatterns
      TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.check.clause" VerboseLevel
6 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
        [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"termination checking " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                    (if Delayed
delayed Delayed -> Delayed -> Bool
forall a. Eq a => a -> a -> Bool
== Delayed
Delayed then VerboseKey
"delayed " else VerboseKey
"") VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                    VerboseKey
"clause of")
                TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"lhs:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Masked DeBruijnPattern -> TCM Doc)
-> [Masked DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Masked DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Masked DeBruijnPattern]
pats)
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"rhs:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM 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 VerboseKey
_ a
a) = a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract a
a
  extract (Abs VerboseKey
x a
a)   = VerboseKey -> TerM Calls -> TerM Calls
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext VerboseKey
x (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ TerM Calls -> TerM Calls
forall a. TerM a -> TerM a
terRaise (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ a -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract a
a

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

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

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

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

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

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

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

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

-- | Extract recursive calls from a type.

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

-- | 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
  [(Arg Term, Bool)]
-> ((Arg Term, Bool) -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' [(Arg Term, Bool)]
args (((Arg Term, Bool) -> TerM Calls) -> TerM Calls)
-> ((Arg Term, Bool) -> TerM Calls) -> TerM Calls
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)   -> Order -> Order
forall a. a -> a
id
             (Bool
True,  Induction
CoInductive) -> (Order
Order.lt (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
.*.)
             (Bool
False, Induction
_)           -> Order -> Order -> Order
forall a b. a -> b -> a
const Order
Order.unknown
    (Order -> Order) -> TerM Calls -> TerM Calls
forall a. (Order -> Order) -> TerM a -> TerM a
terModifyGuarded Order -> Order
g' (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ Arg Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract Arg Term
arg

-- | Handles function applications @g es@.

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

    QName
f       <- TerM QName
terGetCurrent
    [QName]
names   <- TerM [QName]
terGetMutual
    Order
guarded <- TerM Order
terGetGuarded

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

    -- Then, consider call gArgs itself.

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

    -- insert this call into the call list
    case QName -> [QName] -> Maybe VerboseLevel
forall a. Eq a => a -> [a] -> Maybe VerboseLevel
List.elemIndex QName
g [QName]
names of

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

       -- call is to one of the mutally recursive functions
       Just VerboseLevel
gInd -> do
         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-} $
           TCM Elims -> TerM Elims
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Elims -> TerM Elims) -> TCM Elims -> TerM Elims
forall a b. (a -> b) -> a -> b
$ Elims -> (Elim' Term -> TCMT IO (Elim' Term)) -> TCM Elims
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Elims
es0 ((Elim' Term -> TCMT IO (Elim' Term)) -> TCM Elims)
-> (Elim' Term -> TCMT IO (Elim' Term)) -> TCM Elims
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.
             (Term -> TCM Term) -> Elim' Term -> TCMT IO (Elim' Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> TCM Term
reduceCon (Elim' Term -> TCMT IO (Elim' Term))
-> (Elim' Term -> TCMT IO (Elim' Term))
-> Elim' Term
-> TCMT IO (Elim' Term)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Elim' Term -> TCMT IO (Elim' Term)
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
         (VerboseLevel
nrows, VerboseLevel
ncols, [[Order]]
matrix) <- Account (BenchPhase TerM)
-> TerM (VerboseLevel, VerboseLevel, [[Order]])
-> TerM (VerboseLevel, VerboseLevel, [[Order]])
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [BenchPhase TerM
Phase
Benchmark.Termination, BenchPhase TerM
Phase
Benchmark.Compare] (TerM (VerboseLevel, VerboseLevel, [[Order]])
 -> TerM (VerboseLevel, VerboseLevel, [[Order]]))
-> TerM (VerboseLevel, VerboseLevel, [[Order]])
-> TerM (VerboseLevel, VerboseLevel, [[Order]])
forall a b. (a -> b) -> a -> b
$
           Elims -> TerM (VerboseLevel, VerboseLevel, [[Order]])
compareArgs Elims
es
         -- only a delayed definition can be guarded
         let ifDelayed :: Order -> Order
ifDelayed Order
o | Order -> Bool
Order.decreasing Order
o Bool -> Bool -> Bool
&& Delayed
delayed Delayed -> Delayed -> Bool
forall a. Eq a => a -> a -> Bool
== Delayed
NotDelayed = Order
Order.le
                         | Bool
otherwise                                  = Order
o
         TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.guardedness" VerboseLevel
20 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
           VerboseKey
"composing with guardedness " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Order -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Order
guarded VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
           VerboseKey
" counting as " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Order -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Order -> Order
ifDelayed Order
guarded)
         CutOff
cutoff <- TerM CutOff
terGetCutOff
         let ?cutoff = cutoff
         let matrix' :: [[Order]]
matrix' = (?cutoff::CutOff) => Order -> [[Order]] -> [[Order]]
Order -> [[Order]] -> [[Order]]
composeGuardedness (Order -> Order
ifDelayed 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 <- TCM (Closure Term) -> TerM (Closure Term)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Closure Term) -> TerM (Closure Term))
-> TCM (Closure Term) -> TerM (Closure Term)
forall a b. (a -> b) -> a -> b
$ ModuleName -> TCM (Closure Term) -> TCM (Closure Term)
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (QName -> ModuleName
qnameModule QName
g) (TCM (Closure Term) -> TCM (Closure Term))
-> TCM (Closure Term) -> TCM (Closure Term)
forall a b. (a -> b) -> a -> b
$ Term -> TCM (Closure Term)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (Term -> TCM (Closure Term)) -> Term -> TCM (Closure Term)
forall a b. (a -> b) -> a -> b
$
           QName -> Elims -> Term
Def QName
g (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Bool) -> Elims -> Elims
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd ((Origin
Inserted Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
==) (Origin -> Bool) -> (Elim' Term -> Origin) -> Elim' Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> Origin
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 :: VerboseLevel
src  = VerboseLevel -> Maybe VerboseLevel -> VerboseLevel
forall a. a -> Maybe a -> a
fromMaybe VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe VerboseLevel -> VerboseLevel)
-> Maybe VerboseLevel -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> Maybe VerboseLevel
forall a. Eq a => a -> [a] -> Maybe VerboseLevel
List.elemIndex QName
f [QName]
names
             tgt :: VerboseLevel
tgt  = VerboseLevel
gInd
             cm :: CallMatrix
cm   = VerboseLevel -> VerboseLevel -> [[Order]] -> CallMatrix
makeCM VerboseLevel
ncols VerboseLevel
nrows [[Order]]
matrix'
             info :: CallPath
info = [CallInfo] -> CallPath
CallPath [CallInfo :: QName -> Range -> Closure Term -> CallInfo
CallInfo
                      { callInfoTarget :: QName
callInfoTarget = QName
g
                      , callInfoRange :: Range
callInfoRange  = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
g
                      , callInfoCall :: Closure Term
callInfoCall   = Closure Term
doc
                      }]
         VerboseKey -> VerboseLevel -> TerM () -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"term.kept.call" VerboseLevel
5 (TerM () -> TerM ()) -> TerM () -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
           [Masked DeBruijnPattern]
pats <- TerM [Masked DeBruijnPattern]
terGetPatterns
           VerboseKey -> VerboseLevel -> TCM Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.kept.call" VerboseLevel
5 (TCM Doc -> TerM ()) -> TCM Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
             [ TCM Doc
"kept call from" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
f) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ((Masked DeBruijnPattern -> TCM Doc)
-> [Masked DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Masked DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Masked DeBruijnPattern]
pats)
             , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"to" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
g) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                         [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ((Term -> TCM Doc) -> [Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCM Doc -> TCM Doc) -> (Term -> TCM Doc) -> Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) [Term]
args)
             , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"call matrix (with guardedness): "
             , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ CallMatrix -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty CallMatrix
cm
             ]
         Calls -> TerM Calls
forall (m :: * -> *) a. Monad m => a -> m a
return (Calls -> TerM Calls) -> Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ VerboseLevel
-> VerboseLevel -> CallMatrix -> CallPath -> Calls -> Calls
forall cinfo.
VerboseLevel
-> VerboseLevel
-> CallMatrix
-> cinfo
-> CallGraph cinfo
-> CallGraph cinfo
CallGraph.insert VerboseLevel
src VerboseLevel
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 -> TCM Term
reduceCon = (Term -> TCM Term) -> Term -> TCM Term
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM ((Term -> TCM Term) -> Term -> TCM Term)
-> (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ \case
      Con ConHead
c ConInfo
ci Elims
vs -> (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
vs) (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci [])  -- make sure we don't reduce the arguments
      Term
t -> Term -> TCM Term
forall (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
  VerboseKey -> VerboseLevel -> TCM Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.reduce" VerboseLevel
40 (TCM Doc -> TerM ()) -> TCM Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Trying to reduce away call: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v0

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

  -- Then, collect its non-recursive clauses.
  [Clause]
cls <- TCM [Clause] -> TerM [Clause]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [Clause] -> TerM [Clause]) -> TCM [Clause] -> TerM [Clause]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [Clause]
getNonRecursiveClauses QName
g
  VerboseKey -> VerboseLevel -> VerboseKey -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.reduce" VerboseLevel
40 (VerboseKey -> TerM ()) -> VerboseKey -> TerM ()
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> VerboseKey
unwords [ VerboseKey
"Function has", VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Clause] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Clause]
cls), VerboseKey
"non-recursive exact clauses"]
  VerboseKey -> VerboseLevel -> TCM Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.reduce" VerboseLevel
80 (TCM Doc -> TerM ()) -> TCM Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NamedClause -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (NamedClause -> TCM Doc)
-> (Clause -> NamedClause) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
g Bool
True) [Clause]
cls
  VerboseKey -> VerboseLevel -> VerboseKey -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
"term.reduce" VerboseLevel
80 (VerboseKey -> TerM ())
-> (SmallSet AllowedReduction -> VerboseKey)
-> SmallSet AllowedReduction
-> TerM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseKey
"allowed reductions = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++) (VerboseKey -> VerboseKey)
-> (SmallSet AllowedReduction -> VerboseKey)
-> SmallSet AllowedReduction
-> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AllowedReduction] -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([AllowedReduction] -> VerboseKey)
-> (SmallSet AllowedReduction -> [AllowedReduction])
-> SmallSet AllowedReduction
-> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SmallSet AllowedReduction -> [AllowedReduction]
forall a. SmallSetElement a => SmallSet a -> [a]
SmallSet.elems
    (SmallSet AllowedReduction -> TerM ())
-> TerM (SmallSet AllowedReduction) -> TerM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> SmallSet AllowedReduction)
-> TerM (SmallSet AllowedReduction)
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 <- TCM (Reduced (Blocked Term) Term)
-> TerM (Reduced (Blocked Term) Term)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Reduced (Blocked Term) Term)
 -> TerM (Reduced (Blocked Term) Term))
-> TCM (Reduced (Blocked Term) Term)
-> TerM (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$ (SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> TCM (Reduced (Blocked Term) Term)
-> TCM (Reduced (Blocked Term) Term)
forall (m :: * -> *) a.
MonadTCEnv m =>
(SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> m a -> m a
modifyAllowedReductions (AllowedReduction
-> SmallSet AllowedReduction -> SmallSet AllowedReduction
forall a. SmallSetElement a => a -> SmallSet a -> SmallSet a
SmallSet.delete AllowedReduction
UnconfirmedReductions) (TCM (Reduced (Blocked Term) Term)
 -> TCM (Reduced (Blocked Term) Term))
-> TCM (Reduced (Blocked Term) Term)
-> TCM (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$
    ReduceM (Reduced (Blocked Term) Term)
-> TCM (Reduced (Blocked Term) Term)
forall a. ReduceM a -> TCM a
runReduceM (ReduceM (Reduced (Blocked Term) Term)
 -> TCM (Reduced (Blocked Term) Term))
-> ReduceM (Reduced (Blocked Term) Term)
-> TCM (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$ Term
-> [Clause]
-> RewriteRules
-> MaybeReducedElims
-> ReduceM (Reduced (Blocked Term) Term)
appDefE' Term
v0 [Clause]
cls [] ((Elim' Term -> MaybeReduced (Elim' Term))
-> Elims -> MaybeReducedElims
forall a b. (a -> b) -> [a] -> [b]
map Elim' Term -> MaybeReduced (Elim' Term)
forall a. a -> MaybeReduced a
notReduced Elims
es)
  case Reduced (Blocked Term) Term
r of
    NoReduction{}    -> TerM Calls
fallback
    YesReduction Simplification
_ Term
v -> do
      VerboseKey -> VerboseLevel -> TCM Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.reduce" VerboseLevel
30 (TCM Doc -> TerM ()) -> TCM Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"Termination checker: Successfully reduced away call:"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v0
        ]
      VerboseKey -> VerboseLevel -> TerM () -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"term.reduce" VerboseLevel
5 (TerM () -> TerM ()) -> TerM () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TerM ()
forall (m :: * -> *). MonadStatistics m => VerboseKey -> m ()
tick VerboseKey
"termination-checker-reduced-nonrecursive-call"
      Term -> TerM Calls
continue Term
v

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

-- | Extract recursive calls from a term.

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

    -- Instantiate top-level MetaVar.
    Term
t <- TCM Term -> TerM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
t
    case Term
t of

      -- Constructed value.
      Con ConHead{conName :: ConHead -> QName
conName = QName
c, conDataRecord :: ConHead -> DataOrRecord
conDataRecord = DataOrRecord
dataOrRec} ConInfo
_ Elims
es -> do
        let args :: [Arg Term]
args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        -- A constructor preserves the guardedness of all its arguments.
        let argsg :: [(Arg Term, Bool)]
argsg = [Arg Term] -> [Bool] -> [(Arg Term, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Arg Term]
args ([Bool] -> [(Arg Term, Bool)]) -> [Bool] -> [(Arg Term, Bool)]
forall a b. (a -> b) -> a -> b
$ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True

        -- If we encounter a coinductive record constructor
        -- in a type mutual with the current target
        -- then we count it as guarding.
        let inductive :: TerM Induction
inductive   = Induction -> TerM Induction
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive
            coinductive :: TerM Induction
coinductive = Induction -> TerM Induction
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
CoInductive
        Induction
ind <- TerM Bool -> TerM Induction -> TerM Induction -> TerM Induction
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe QName -> Bool) -> TerM (Maybe QName) -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM (Maybe QName)
terGetSharp) TerM Induction
coinductive (TerM Induction -> TerM Induction)
-> TerM Induction -> TerM Induction
forall a b. (a -> b) -> a -> b
$ {-else-} do
          if DataOrRecord
dataOrRec DataOrRecord -> DataOrRecord -> Bool
forall a. Eq a => a -> a -> Bool
== DataOrRecord
IsData then TerM Induction
inductive else do
          TerM (Maybe (QName, Defn))
-> TerM Induction
-> ((QName, Defn) -> TerM Induction)
-> TerM Induction
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCM (Maybe (QName, Defn)) -> TerM (Maybe (QName, Defn))
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe (QName, Defn)) -> TerM (Maybe (QName, Defn)))
-> TCM (Maybe (QName, Defn)) -> TerM (Maybe (QName, Defn))
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe (QName, Defn))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) TerM Induction
inductive (((QName, Defn) -> TerM Induction) -> TerM Induction)
-> ((QName, Defn) -> TerM Induction) -> TerM Induction
forall a b. (a -> b) -> a -> b
$ \ (QName
q, Defn
def) -> do
            VerboseKey -> VerboseLevel -> VerboseKey -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"term.check.term" VerboseLevel
50 (VerboseKey -> TerM ()) -> VerboseKey -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"constructor " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
c VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" has record type " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q
            if Defn -> Maybe Induction
recInduction Defn
def Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive then TerM Induction
inductive else do
            TerM Bool -> TerM Induction -> TerM Induction -> TerM Induction
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([QName] -> TerM Bool
targetElem ([QName] -> TerM Bool)
-> (Maybe [QName] -> [QName]) -> Maybe [QName] -> TerM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName] -> Maybe [QName] -> [QName]
forall a. a -> Maybe a -> a
fromMaybe [QName]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [QName] -> TerM Bool) -> Maybe [QName] -> TerM Bool
forall a b. (a -> b) -> a -> b
$ 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 Term -> TerM Calls
forall a. ExtractCalls a => a -> TerM Calls
extract (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> TerM Calls
function QName
g Elims
es

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

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

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

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

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

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

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

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

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

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

-- | Extract recursive calls from level expressions.

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

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

-- | Rewrite type @tel -> Size< u@ to @tel -> Size@.
maskSizeLt :: MonadTCM tcm => Dom Type -> tcm (Dom Type)
maskSizeLt :: Dom Type -> tcm (Dom Type)
maskSizeLt !Dom Type
dom = TCM (Dom Type) -> tcm (Dom Type)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Dom Type) -> tcm (Dom Type))
-> TCM (Dom Type) -> tcm (Dom Type)
forall a b. (a -> b) -> a -> b
$ do
  let a :: Type
a = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
  (Maybe QName
msize, Maybe QName
msizelt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  case (Maybe QName
msize, Maybe QName
msizelt) of
    (Maybe QName
_ , Maybe QName
Nothing) -> Dom Type -> TCM (Dom Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Dom Type
dom
    (Maybe QName
Nothing, Maybe QName
_)  -> TCM (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Just QName
size, Just QName
sizelt) -> do
      TelV Tele (Dom Type)
tel Type
c <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
      case Type
a of
        El Sort
s (Def QName
d [Elim' Term
v]) | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt -> Dom Type -> TCM (Dom Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type -> TCM (Dom Type)) -> Dom Type -> TCM (Dom Type)
forall a b. (a -> b) -> a -> b
$
          Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
size []) Type -> Dom Type -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
dom
        Type
_ -> Dom Type -> TCM (Dom Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Dom 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 (VerboseLevel, VerboseLevel, [[Order]])
compareArgs Elims
es = do
  [Masked DeBruijnPattern]
pats <- TerM [Masked DeBruijnPattern]
terGetPatterns
  TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.compareArgs" VerboseLevel
90 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"comparing " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Elims -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
es) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" args to " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Masked DeBruijnPattern] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Masked DeBruijnPattern]
pats) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" 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 <- [Masked DeBruijnPattern] -> TerM [[Order]] -> TerM [[Order]]
forall a b. UsableSizeVars a => a -> TerM b -> TerM b
withUsableVars [Masked DeBruijnPattern]
pats (TerM [[Order]] -> TerM [[Order]])
-> TerM [[Order]] -> TerM [[Order]]
forall a b. (a -> b) -> a -> b
$ Elims -> (Elim' Term -> TerM [Order]) -> TerM [[Order]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Elims
es ((Elim' Term -> TerM [Order]) -> TerM [[Order]])
-> (Elim' Term -> TerM [Order]) -> TerM [[Order]]
forall a b. (a -> b) -> a -> b
$ \ Elim' Term
e -> [Masked DeBruijnPattern]
-> (Masked DeBruijnPattern -> TerM Order) -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Masked DeBruijnPattern]
pats ((Masked DeBruijnPattern -> TerM Order) -> TerM [Order])
-> (Masked DeBruijnPattern -> TerM Order) -> TerM [Order]
forall a b. (a -> b) -> a -> b
$ \ Masked DeBruijnPattern
p -> Elim' Term -> Masked DeBruijnPattern -> TerM Order
compareElim Elim' Term
e Masked DeBruijnPattern
p

  -- Count the number of coinductive projection(pattern)s in caller and callee.
  -- Only recursive coinductive projections are eligible (Issue 1209).
  VerboseLevel
projsCaller <- [QName] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([QName] -> VerboseLevel) -> TerM [QName] -> TerM VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    (QName -> TerM Bool) -> [QName] -> TerM [QName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> QName -> TerM Bool
forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection Bool
True) ([QName] -> TerM [QName]) -> [QName] -> TerM [QName]
forall a b. (a -> b) -> a -> b
$ (Masked DeBruijnPattern -> Maybe QName)
-> [Masked DeBruijnPattern] -> [QName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (((ProjOrigin, AmbiguousQName) -> QName)
-> Maybe (ProjOrigin, AmbiguousQName) -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AmbiguousQName -> QName
headAmbQ (AmbiguousQName -> QName)
-> ((ProjOrigin, AmbiguousQName) -> AmbiguousQName)
-> (ProjOrigin, AmbiguousQName)
-> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProjOrigin, AmbiguousQName) -> AmbiguousQName
forall a b. (a, b) -> b
snd) (Maybe (ProjOrigin, AmbiguousQName) -> Maybe QName)
-> (Masked DeBruijnPattern -> Maybe (ProjOrigin, AmbiguousQName))
-> Masked DeBruijnPattern
-> Maybe QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP (DeBruijnPattern -> Maybe (ProjOrigin, AmbiguousQName))
-> (Masked DeBruijnPattern -> DeBruijnPattern)
-> Masked DeBruijnPattern
-> Maybe (ProjOrigin, AmbiguousQName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Masked DeBruijnPattern -> DeBruijnPattern
forall a. Masked a -> a
getMasked) [Masked DeBruijnPattern]
pats
  VerboseLevel
projsCallee <- [QName] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([QName] -> VerboseLevel) -> TerM [QName] -> TerM VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    (QName -> TerM Bool) -> [QName] -> TerM [QName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> QName -> TerM Bool
forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection Bool
True) ([QName] -> TerM [QName]) -> [QName] -> TerM [QName]
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Maybe QName) -> Elims -> [QName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (((ProjOrigin, QName) -> QName)
-> Maybe (ProjOrigin, QName) -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProjOrigin, QName) -> QName
forall a b. (a, b) -> b
snd (Maybe (ProjOrigin, QName) -> Maybe QName)
-> (Elim' Term -> Maybe (ProjOrigin, QName))
-> Elim' Term
-> Maybe QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim) Elims
es
  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  Bool
useGuardedness <- TCMT IO Bool -> TerM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
guardednessOption
  let guardedness :: Order
guardedness =
        if Bool
useGuardedness
        then (?cutoff::CutOff) => Bool -> VerboseLevel -> Order
Bool -> VerboseLevel -> Order
decr Bool
True (VerboseLevel -> Order) -> VerboseLevel -> Order
forall a b. (a -> b) -> a -> b
$ VerboseLevel
projsCaller VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
projsCallee
        else Order
Order.Unknown
  TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.guardedness" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCM Doc
"compareArgs:"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"projsCaller = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow VerboseLevel
projsCaller
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"projsCallee = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow VerboseLevel
projsCallee
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"guardedness of call: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Order -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Order
guardedness
    ]
  (VerboseLevel, VerboseLevel, [[Order]])
-> TerM (VerboseLevel, VerboseLevel, [[Order]])
forall (m :: * -> *) a. Monad m => a -> m a
return ((VerboseLevel, VerboseLevel, [[Order]])
 -> TerM (VerboseLevel, VerboseLevel, [[Order]]))
-> (VerboseLevel, VerboseLevel, [[Order]])
-> TerM (VerboseLevel, VerboseLevel, [[Order]])
forall a b. (a -> b) -> a -> b
$ Order
-> (VerboseLevel, VerboseLevel, [[Order]])
-> (VerboseLevel, VerboseLevel, [[Order]])
addGuardedness Order
guardedness (Elims -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Elims
es, [Masked DeBruijnPattern] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Masked DeBruijnPattern]
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' Term -> Masked DeBruijnPattern -> TerM Order
compareElim Elim' Term
e Masked DeBruijnPattern
p = do
  TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
    VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.compare" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCM Doc
"compareElim"
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"e = " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> Elim' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim' Term
e
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"p = " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> Masked DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Masked DeBruijnPattern
p
      ]
    VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.compare" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"e = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Elim' Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Elim' Term
e
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"p = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Masked DeBruijnPattern -> VerboseKey
forall a. Show a => a -> VerboseKey
show Masked DeBruijnPattern
p
      ]
  case (Elim' Term
e, Masked DeBruijnPattern -> DeBruijnPattern
forall a. Masked a -> a
getMasked Masked DeBruijnPattern
p) of
    (Proj ProjOrigin
_ QName
d, ProjP ProjOrigin
_ QName
d') -> do
      QName
d  <- QName -> TerM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d
      QName
d' <- QName -> TerM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d'
      Order
o  <- QName -> QName -> TerM Order
forall (tcm :: * -> *). MonadTCM tcm => QName -> QName -> tcm Order
compareProj QName
d QName
d'
      VerboseKey -> VerboseLevel -> TCM Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.compare" VerboseLevel
30 (TCM Doc -> TerM ()) -> TCM Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"comparing callee projection " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
d
        , VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"against caller projection " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
d'
        , VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"yields order " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Order -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Order
o
        ]
      Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
o
    (Proj{}, DeBruijnPattern
_)            -> Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
    (Apply{}, ProjP{})     -> Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
    (Apply Arg Term
arg, DeBruijnPattern
_)         -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg) Masked DeBruijnPattern
p
    -- TODO Andrea: making sense?
    (IApply{}, ProjP{})  -> Order -> TerM Order
forall (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 :: QName -> QName -> tcm Order
compareProj QName
d QName
d'
  | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' = Order -> tcm Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le
  | Bool
otherwise = TCM Order -> tcm Order
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Order -> tcm Order) -> TCM Order -> tcm Order
forall a b. (a -> b) -> a -> b
$ do
      -- different projections
      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 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
r' -> do
          -- of same record
          Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
          case Defn
def of
            Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } -> do
              [QName]
fs <- [QName] -> TCMT IO [QName]
forall (m :: * -> *) a. Monad m => a -> m a
return ([QName] -> TCMT IO [QName]) -> [QName] -> TCMT IO [QName]
forall a b. (a -> b) -> a -> b
$ (Dom QName -> QName) -> [Dom QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> QName
forall t e. Dom' t e -> e
unDom [Dom QName]
fs
              case ((QName -> Bool) -> [QName] -> Maybe QName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (QName
dQName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) [QName]
fs, (QName -> Bool) -> [QName] -> Maybe QName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (QName
d'QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) [QName]
fs) of
                (Just QName
i, Just QName
i')
                  -- earlier field is smaller
                  | QName
i QName -> QName -> Bool
forall a. Ord a => a -> a -> Bool
< QName
i'    -> Order -> TCM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.lt
                  | QName
i QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
i'   -> do
                     TCM Order
forall a. HasCallStack => a
__IMPOSSIBLE__
                  | Bool
otherwise -> Order -> TCM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
                (Maybe QName, Maybe QName)
_ -> TCM Order
forall a. HasCallStack => a
__IMPOSSIBLE__
            Defn
_ -> TCM Order
forall a. HasCallStack => a
__IMPOSSIBLE__
        (Maybe QName, Maybe QName)
_ -> Order -> TCM Order
forall (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 :: VerboseLevel -> VerboseLevel -> [[Order]] -> CallMatrix
makeCM VerboseLevel
ncols VerboseLevel
nrows [[Order]]
matrix = Matrix VerboseLevel Order -> CallMatrix
forall a. Matrix VerboseLevel a -> CallMatrix' a
CallMatrix (Matrix VerboseLevel Order -> CallMatrix)
-> Matrix VerboseLevel Order -> CallMatrix
forall a b. (a -> b) -> a -> b
$
  Size VerboseLevel -> [[Order]] -> Matrix VerboseLevel Order
forall i b.
(Ord i, Num i, Enum i, HasZero b) =>
Size i -> [[b]] -> Matrix i b
Matrix.fromLists (VerboseLevel -> VerboseLevel -> Size VerboseLevel
forall i. i -> i -> Size i
Matrix.Size VerboseLevel
nrows VerboseLevel
ncols) [[Order]]
matrix

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

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

-- | Stripping off a record constructor is not counted as decrease, in
--   contrast to a data constructor.
--   A record constructor increases/decreases by 0, a data constructor by 1.
offsetFromConstructor :: HasConstInfo tcm => QName -> tcm Int
offsetFromConstructor :: QName -> tcm VerboseLevel
offsetFromConstructor QName
c =
  tcm Bool
-> tcm VerboseLevel -> tcm VerboseLevel -> tcm VerboseLevel
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> tcm Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c) (VerboseLevel -> tcm VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
0) (VerboseLevel -> tcm VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
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 <- TCM Term -> TerM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
t
  Order
o <- Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
t Masked DeBruijnPattern
p
  TCMT IO () -> TerM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"term.compare" VerboseLevel
25 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
" comparing term " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCM Doc
" to pattern " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Masked DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Masked DeBruijnPattern
p TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
" results in " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Order -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Order
o)
  Order -> TerM Order
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 = (a -> TCMT IO a) -> Arg a -> TCM (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> TCMT IO a
forall a. StripAllProjections a => a -> TCM a
stripAllProjections

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

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

instance StripAllProjections Term where
  stripAllProjections :: Term -> TCM Term
stripAllProjections Term
t = do
    case Term
t of
      Var VerboseLevel
i Elims
es   -> VerboseLevel -> Elims -> Term
Var VerboseLevel
i (Elims -> Term) -> TCM Elims -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
es
      Con ConHead
c ConInfo
ci Elims
ts -> do
        -- Andreas, 2019-02-23, re #2613.  This is apparently not necessary:
        -- c <- fromRightM (\ err -> return c) $ getConForm (conName c)
        ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> TCM Elims -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
ts
      Def QName
d Elims
es   -> QName -> Elims -> Term
Def QName
d (Elims -> Term) -> TCM Elims -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> TCM Elims
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Elims
es
      DontCare Term
t -> Term -> TCM Term
forall a. StripAllProjections a => a -> TCM a
stripAllProjections Term
t
      Term
_ -> Term -> TCM Term
forall (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 [NamedArg DeBruijnPattern]
ps -> (SigError -> TCMT IO ConHead)
-> TCMT IO (Either SigError ConHead) -> TCMT IO ConHead
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m (Either a b) -> m b
fromRightM (\ SigError
err -> ConHead -> TCMT IO ConHead
forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c) (QName -> TCMT IO (Either SigError ConHead)
getConForm (ConHead -> QName
conName ConHead
c)) TCMT IO ConHead
-> (ConHead -> DeBruijnPattern) -> TCM DeBruijnPattern
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ ConHead
c' ->
    ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c' ConPatternInfo
i [NamedArg DeBruijnPattern]
ps
  DeBruijnPattern
p -> DeBruijnPattern -> TCM DeBruijnPattern
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
  Term
v <- TCM Term -> TerM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v)
  DeBruijnPattern
p <- TCM DeBruijnPattern -> TerM DeBruijnPattern
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM DeBruijnPattern -> TerM DeBruijnPattern)
-> TCM DeBruijnPattern -> TerM DeBruijnPattern
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 VerboseLevel
i Elims
es, DeBruijnPattern
_) | Just{} <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
      VerboseLevel -> Masked DeBruijnPattern -> TerM Order
compareVar VerboseLevel
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 -> VerboseLevel -> Order
Bool -> VerboseLevel -> Order
Order.decr Bool
True (VerboseLevel -> Order)
-> (VerboseLevel -> VerboseLevel) -> VerboseLevel -> Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Ord a => a -> a -> a
max (if Bool
m then VerboseLevel
0 else DeBruijnPattern -> VerboseLevel
forall a. Pattern' a -> VerboseLevel
patternDepth DeBruijnPattern
p) (VerboseLevel -> VerboseLevel)
-> (VerboseLevel -> VerboseLevel) -> VerboseLevel -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> VerboseLevel
forall a. Enum a => a -> a
pred (VerboseLevel -> Order) -> TerM VerboseLevel -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
       (TerEnv -> VerboseLevel) -> TerM VerboseLevel
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> VerboseLevel
_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
_ [NamedArg DeBruijnPattern
p]) | QName
s QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
s' Bool -> Bool -> Bool
&& QName -> Maybe QName
forall a. a -> Maybe a
Just QName
s Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
suc ->
      Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) (DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p)

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

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

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

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

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

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

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

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

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

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

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

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

compareConArgs :: Args -> [NamedArg DeBruijnPattern] -> TerM Order
compareConArgs :: [Arg Term] -> [NamedArg DeBruijnPattern] -> TerM Order
compareConArgs [Arg Term]
ts [NamedArg DeBruijnPattern]
ps = do
  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  -- we may assume |ps| >= |ts|, otherwise c ps would be of functional type
  -- which is impossible
  case ([Arg Term] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Arg Term]
ts, [NamedArg DeBruijnPattern] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [NamedArg DeBruijnPattern]
ps) of
    (VerboseLevel
0,VerboseLevel
0) -> Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le        -- c <= c
    (VerboseLevel
0,VerboseLevel
1) -> Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown   -- c not<= c x
    (VerboseLevel
1,VerboseLevel
0) -> TerM Order
forall a. HasCallStack => a
__IMPOSSIBLE__
    (VerboseLevel
1,VerboseLevel
1) -> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' (Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> Arg Term
forall a. [a] -> a
head [Arg Term]
ts)) (DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern
forall a. [a] -> a
head [NamedArg DeBruijnPattern]
ps)
    (VerboseLevel
_,VerboseLevel
_) -> (Order -> Order -> Order) -> Order -> [Order] -> Order
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
(Order..*.) Order
Order.le ([Order] -> Order) -> TerM [Order] -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
               (Term -> Masked DeBruijnPattern -> TerM Order)
-> [Term] -> [Masked DeBruijnPattern] -> TerM [Order]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
ts) ((NamedArg DeBruijnPattern -> Masked DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [Masked DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Masked DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
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 :: VerboseLevel -> Masked DeBruijnPattern -> TerM Order
compareVar VerboseLevel
i (Masked Bool
m DeBruijnPattern
p) = do
  Maybe QName
suc    <- TerM (Maybe QName)
terGetSizeSuc
  CutOff
cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  let no :: TerM Order
no = Order -> TerM Order
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  -> VerboseLevel -> Masked DBPatVar -> TerM Order
compareVarVar VerboseLevel
i (Bool -> DBPatVar -> Masked DBPatVar
forall a. Bool -> a -> Masked a
Masked Bool
m DBPatVar
x)
    LitP{}    -> TerM Order
no
    DotP{}   -> TerM Order
no
    VarP PatternInfo
_ DBPatVar
x  -> VerboseLevel -> Masked DBPatVar -> TerM Order
compareVarVar VerboseLevel
i (Bool -> DBPatVar -> Masked DBPatVar
forall a. Bool -> a -> Masked a
Masked Bool
m DBPatVar
x)

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

    ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps -> if Bool
m then TerM Order
no else Bool -> Order -> Order
setUsability Bool
True (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      VerboseLevel -> Order -> Order
decrease (VerboseLevel -> Order -> Order)
-> TerM VerboseLevel -> TerM (Order -> Order)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TerM VerboseLevel
forall (tcm :: * -> *).
HasConstInfo tcm =>
QName -> tcm VerboseLevel
offsetFromConstructor (ConHead -> QName
conName ConHead
c)
               TerM (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((?cutoff::CutOff) => [Order] -> Order
[Order] -> Order
Order.supremum ([Order] -> Order) -> TerM [Order] -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamedArg DeBruijnPattern -> TerM Order)
-> [NamedArg DeBruijnPattern] -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (VerboseLevel -> Masked DeBruijnPattern -> TerM Order
compareVar VerboseLevel
i (Masked DeBruijnPattern -> TerM Order)
-> (NamedArg DeBruijnPattern -> Masked DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TerM Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Masked DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps)
    DefP PatternInfo
_ QName
c [NamedArg DeBruijnPattern]
ps -> if Bool
m then TerM Order
no else Bool -> Order -> Order
setUsability Bool
True (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      VerboseLevel -> Order -> Order
decrease (VerboseLevel -> Order -> Order)
-> TerM VerboseLevel -> TerM (Order -> Order)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TerM VerboseLevel
forall (tcm :: * -> *).
HasConstInfo tcm =>
QName -> tcm VerboseLevel
offsetFromConstructor QName
c
               TerM (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((?cutoff::CutOff) => [Order] -> Order
[Order] -> Order
Order.supremum ([Order] -> Order) -> TerM [Order] -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamedArg DeBruijnPattern -> TerM Order)
-> [NamedArg DeBruijnPattern] -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (VerboseLevel -> Masked DeBruijnPattern -> TerM Order
compareVar VerboseLevel
i (Masked DeBruijnPattern -> TerM Order)
-> (NamedArg DeBruijnPattern -> Masked DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TerM Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> Masked DeBruijnPattern
forall a. a -> Masked a
notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Masked DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
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 :: VerboseLevel -> Masked DBPatVar -> TerM Order
compareVarVar VerboseLevel
i (Masked Bool
m x :: DBPatVar
x@(DBPatVar VerboseKey
_ VerboseLevel
j))
  | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j = if Bool -> Bool
not Bool
m then Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le else TCM Order -> TerM Order
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Order -> TerM Order) -> TCM Order -> TerM Order
forall a b. (a -> b) -> a -> b
$
      -- If j is a size, we ignore the mask.
      TCMT IO Bool -> TCM Order -> TCM Order -> TCM Order
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType (Type -> TCMT IO (Maybe BoundedSize))
-> TCMT IO Type -> TCMT IO (Maybe BoundedSize)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseLevel -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
j)
        {- then -} (Order -> TCM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.le)
        {- else -} (Order -> TCM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown)
  | Bool
otherwise = do
      -- record usability of variable
      Bool
u <- (VerboseLevel
i VerboseLevel -> IntSet -> Bool
`VarSet.member`) (IntSet -> Bool) -> TerM IntSet -> TerM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TerM IntSet
terGetUsableVars
      -- Andreas, 2017-07-26, issue #2331.
      -- The usability logic is refuted by bounded size quantification in terms.
      -- Thus, it is switched off (the infrastructure remains in place for now).
      if Bool -> Bool
not Bool
u then Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown else do
      -- Only if usable:
      BoundedSize
res <- VerboseLevel -> TerM BoundedSize
forall (m :: * -> *). PureTCM m => VerboseLevel -> m BoundedSize
isBounded VerboseLevel
i
      case BoundedSize
res of
        BoundedSize
BoundedNo  -> Order -> TerM Order
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
        BoundedLt Term
v -> Bool -> Order -> Order
setUsability Bool
u (Order -> Order) -> (Order -> Order) -> Order -> Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Order -> Order
decrease VerboseLevel
1 (Order -> Order) -> TerM Order -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' Term
v (Bool -> DeBruijnPattern -> Masked DeBruijnPattern
forall a. Bool -> a -> Masked a
Masked Bool
m (DeBruijnPattern -> Masked DeBruijnPattern)
-> DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> DeBruijnPattern
forall a. a -> Pattern' a
varP DBPatVar
x)