{-# 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 Mikan.Termination.TermCheck
    ( termDecl
    , termMutual
    , Result
    ) where

import Prelude hiding ( null, zip, zipWith )

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

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

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

import Mikan.Termination.Masking
import Mikan.Termination.CutOff
import Mikan.Termination.Monad
import Mikan.Termination.CallGraph hiding (toList)
import Mikan.Termination.CallGraph qualified as CallGraph
import Mikan.Termination.CallMatrix hiding (toList)
import Mikan.Termination.Order     as Order
import Mikan.Termination.SparseMatrix qualified as Matrix
import Mikan.Termination.Termination (Terminates(..), idempotentEndos, terminatesFilter, terminationCounterexample)
import Mikan.Termination.RecCheck

import Mikan.TypeChecking.Pretty.Call () -- instance PrettyTCM CallInfo
import Mikan.TypeChecking.Datatypes
import Mikan.TypeChecking.Functions
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Forcing
import Mikan.TypeChecking.Records -- (isRecordConstructor, isInductiveRecord)
import Mikan.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull, appDefE_)
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope

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

import Mikan.Interaction.Options

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

import Mikan.Utils.Impossible

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

type Calls = CallGraph CallPath

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

type Result = [TerminationError]

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

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


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

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


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

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

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

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

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

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

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

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

     -- Andreas, 2025-05-31, AIM XL, re issue #7906:
     -- Clear previous information about termination to avoid loops in the termination checker.
     Set QName -> (QName -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set QName
allNames ((QName -> TCMT IO ()) -> TCMT IO ())
-> (QName -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ QName
q -> QName -> Maybe Bool -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => QName -> Maybe Bool -> m ()
setTerminates QName
q Maybe Bool
forall a. Maybe a
Nothing

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

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

-- | Run the termination checker.
runTerminationCheck ::
     (Node -> Bool)
  -> TerM Calls
  -> TerM (Terminates CallPath)
runTerminationCheck :: (Nat -> Bool) -> TerM Calls -> TerM (Terminates CallPath)
runTerminationCheck Nat -> Bool
filt TerM Calls
collect = do
    -- Use full precision when extracting calls
    let ?cutoff = ?cutoff::CutOff
CutOff
DontCutOff
    calls <- TerM Calls
collect

    maxcutoff <- terGetCutOff
    -- Iteratively increase cutoff up to its maximal value.
    let
      loop :: CutOff
           -> Maybe CallPath
           -> TerM (Terminates CallPath)
      loop CutOff
cutoff Maybe CallPath
currentResult = do
        let ?cutoff = ?cutoff::CutOff
CutOff
cutoff
        CutOff -> (Nat -> Bool) -> Calls -> TerM ()
reportCalls CutOff
cutoff Nat -> Bool
filt Calls
calls
        r <- Terminates CallPath -> TerM (Terminates CallPath)
forall a. a -> TerM a
billToTerGraph (Terminates CallPath -> TerM (Terminates CallPath))
-> Terminates CallPath -> TerM (Terminates CallPath)
forall a b. (a -> b) -> a -> b
$ (Nat -> Bool) -> Calls -> Terminates CallPath
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
(Nat -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminatesFilter Nat -> Bool
filt Calls
calls
        case r of
          Terminates CallPath
Terminates -> Terminates CallPath -> TerM (Terminates CallPath)
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Terminates CallPath
forall cinfo. Terminates cinfo
Terminates
          TerminatesNot CallPath
cinfo -> do
            let result :: CallPath
result = CallPath -> Maybe CallPath -> CallPath
forall a. a -> Maybe a -> a
fromMaybe CallPath
cinfo Maybe CallPath
currentResult
            if CutOff
cutoff CutOff -> CutOff -> Bool
forall a. Ord a => a -> a -> Bool
>= CutOff
maxcutoff then Terminates CallPath -> TerM (Terminates CallPath)
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Terminates CallPath -> TerM (Terminates CallPath))
-> Terminates CallPath -> TerM (Terminates CallPath)
forall a b. (a -> b) -> a -> b
$ CallPath -> Terminates CallPath
forall cinfo. cinfo -> Terminates cinfo
TerminatesNot CallPath
result
              else CutOff -> Maybe CallPath -> TerM (Terminates CallPath)
loop (CutOff
cutoff CutOff -> CutOff -> CutOff
forall a. Num a => a -> a -> a
+ CutOff
1) (CallPath -> Maybe CallPath
forall a. a -> Maybe a
Just CallPath
result)
    loop 0 Nothing

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

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

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

  r <- runTerminationCheck (const True) collect

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

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

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

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

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

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

reportCalls :: CutOff -> (Node -> Bool) -> Calls -> TerM ()
reportCalls :: CutOff -> (Nat -> Bool) -> Calls -> TerM ()
reportCalls CutOff
cutoff Nat -> Bool
filt Calls
calls = do
  let ?cutoff = ?cutoff::CutOff
CutOff
cutoff

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

    [Char] -> Nat -> [[Char]] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [[Char]] -> m ()
reportS [Char]
"term.lex" Nat
20
      [ [Char]
"Termination depth: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CutOff -> [Char]
forall a. Show a => a -> [Char]
show CutOff
cutoff
      , [Char]
"Calls: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Calls -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Calls
calls
      ]

    -- Print the whole completion phase.
    [Char] -> Nat -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
verboseS [Char]
"term.matrices" Nat
40 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      let header :: [Char] -> [Char]
header [Char]
s = [[Char]] -> [Char]
unlines
            [ Nat -> Char -> [Char]
forall a. Nat -> a -> [a]
replicate Nat
n Char
'='
            , Nat -> Char -> [Char]
forall a. Nat -> a -> [a]
replicate Nat
k Char
'=' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Nat -> Char -> [Char]
forall a. Nat -> a -> [a]
replicate Nat
k' Char
'='
            , Nat -> Char -> [Char]
forall a. Nat -> a -> [a]
replicate Nat
n Char
'='
            ]
            where n :: Nat
n  = Nat
70
                  r :: Nat
r  = Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- [Char] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Char]
s
                  k :: Nat
k  = Nat
r Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`div` Nat
2
                  k' :: Nat
k' = Nat
r Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
k
      let report :: [Char] -> a -> m ()
report [Char]
s a
cs = [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.matrices" Nat
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
header [Char]
s
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM 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.
(Monoid cinfo, ?cutoff::CutOff) =>
CallGraph cinfo
-> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
completionStep Calls
cs0 Calls
cs
            [Char] -> Calls -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, PrettyTCM a) =>
[Char] -> a -> m ()
report [Char]
" New call matrices " Calls
new
            case (Nat -> Bool) -> Calls -> Terminates CallPath
forall cinfo.
(?cutoff::CutOff) =>
(Nat -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminationCounterexample Nat -> Bool
filt Calls
new of
              Terminates CallPath
Terminates | Bool -> Bool
not (Calls -> Bool
forall a. Null a => a -> Bool
null Calls
new) -> Either () Calls -> TCMT IO (Either () Calls)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either () Calls -> TCMT IO (Either () Calls))
-> Either () Calls -> TCMT IO (Either () Calls)
forall a b. (a -> b) -> a -> b
$ Calls -> Either () Calls
forall a b. b -> Either a b
Right Calls
cs'
              Terminates CallPath
_ -> Either () Calls -> TCMT IO (Either () Calls)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either () Calls -> TCMT IO (Either () Calls))
-> Either () Calls -> TCMT IO (Either () Calls)
forall a b. (a -> b) -> a -> b
$ () -> Either () Calls
forall a b. a -> Either a b
Left ()
            -- return $ if null new then Left () else Right cs'
      [Char] -> Calls -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, PrettyTCM a) =>
[Char] -> a -> m ()
report ([Char]
" Initial call matrices (cutoff: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CutOff -> [Char]
forall a. Show a => a -> [Char]
show CutOff
cutoff [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") ") 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.
(Monoid cinfo, ?cutoff::CutOff) =>
CallGraph cinfo -> CallGraph cinfo
CallGraph.complete Calls
calls
        idems :: [CallMatrixAug CallPath]
idems = Calls -> [CallMatrixAug CallPath]
forall cinfo.
(?cutoff::CutOff) =>
CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndos Calls
calls'
    -- TODO
    -- reportSDoc "term.behaviours" 20 $ vcat
    --   [ text $ "Recursion behaviours (" ++ no ++ "dot patterns):"
    --   , nest 2 $ return $ Term.prettyBehaviour calls'
    --   ]
    [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.matrices" Nat
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Idempotent call matrices:\n"
      , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
"\n" ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (CallMatrixAug CallPath -> TCMT IO Doc)
-> [CallMatrixAug CallPath] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' CallMatrixAug CallPath -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
CallMatrixAug CallPath -> m Doc
prettyTCM [CallMatrixAug CallPath]
idems
      ]
    -- reportSDoc "term.matrices" 30 $ vcat
    --   [ text $ "Other call matrices (" ++ no ++ "dot patterns):"
    --   , nest 2 $ pretty $ CallGraph.fromList others
    --   ]
    () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

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

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

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

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

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

    r <- runTerminationCheck (== index) collect

    names <- terGetUserNames
    case r of

      TerminatesNot CallPath
callpaths -> do
        let calls :: [CallInfo]
calls = CallPath -> [CallInfo]
callInfos CallPath
callpaths
        -- Mark as non-terminating.
        QName -> Maybe Bool -> TerM ()
forall (m :: * -> *). MonadTCState m => QName -> Maybe Bool -> m ()
setTerminates QName
name (Maybe Bool -> TerM ()) -> Maybe Bool -> TerM ()
forall a b. (a -> b) -> a -> b
$ Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False

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

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

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

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

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

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

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

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

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

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

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

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

    -- If the result should be disregarded, set all calls to unguarded.
  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
$ TerM Bool -> (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall b (m :: * -> *) a.
(IsBool b, Monad m) =>
m b -> (m a -> m a) -> m a -> m a
applyWhenM TerM Bool
terGetMaskResult TerM Calls -> TerM Calls
forall a. TerM a -> TerM a
terUnguarded case Definition -> Defn
theDef Definition
def of
    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls  } -> [Clause] -> (Clause -> TerM Calls) -> TerM Calls
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' [Clause]
cls ((Clause -> TerM Calls) -> TerM Calls)
-> (Clause -> TerM Calls) -> TerM Calls
forall a b. (a -> b) -> a -> b
$ \ Clause
cl -> do
      if Clause -> Bool
forall a. HasDefP a => a -> Bool
hasDefP Clause
cl -- generated hcomp clause, should be safe.
                                      -- TODO find proper strategy.
        then Calls -> TerM Calls
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Calls
forall a. Null a => a
empty
        else Type -> Clause -> TerM Calls
termClause Type
t Clause
cl

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

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

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

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

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

  -- create n variable patterns
  mkPats :: p -> f [DeBruijnPattern]
mkPats p
n  = ((Nat, Dom Name) -> DeBruijnPattern)
-> [(Nat, Dom Name)] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map' (Nat, Dom Name) -> DeBruijnPattern
forall {a}. Pretty a => (Nat, a) -> DeBruijnPattern
mkPat ([(Nat, Dom Name)] -> [DeBruijnPattern])
-> f [(Nat, Dom Name)] -> f [DeBruijnPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f [(Nat, Dom Name)]
forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom Name)]
getContextVars
  mkPat :: (Nat, a) -> DeBruijnPattern
mkPat (Nat
i, a
x) = PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ ArgName -> Nat -> DBPatVar
DBPatVar ([Char] -> ArgName
TS.pack ([Char] -> ArgName) -> [Char] -> ArgName
forall a b. (a -> b) -> a -> b
$ a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
x) Nat
i

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

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

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

-- | Convert a term (from a dot pattern) to a pattern for the purposes
-- of the termination checker.

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

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

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

instance TermToPattern Term DeBruijnPattern where
  termToPattern :: Term -> TerM DeBruijnPattern
termToPattern Term
t = do
    t <- Term -> TerM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (Term -> TerM Term) -> TerM Term -> TerM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TerM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
t
    let
      -- 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.
      --
      -- Szumi, 2025-03-11:
      -- Instead of completely turning off dot-pattern termination for cubical,
      -- it should be enough to only ignore constructors of HITs in dot patterns.
      -- This way, the issues #5953 and #4725 are also avoided.
      ifNotConsOfHIT :: ConHead -> TerM DeBruijnPattern -> TerM DeBruijnPattern
      ifNotConsOfHIT ConHead
c = TerM Bool
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
-> TerM DeBruijnPattern
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TerM Bool
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
consOfHIT (ConHead -> QName
conName ConHead
c)) TerM DeBruijnPattern
fallback

      -- Andreas, 2025-11-20, issue #8212
      -- Reduce constructor to their original form
      -- as this also happens in the call arguments.
      fallback :: TerM DeBruijnPattern
      fallback = Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP (Term -> DeBruijnPattern) -> TerM Term -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Term -> TerM Term
forall (tcm :: * -> *). MonadTCM tcm => Term -> tcm Term
reduceCon Term
t

    case t of
      Dummy DummyTermKind
s Elims
_   -> [Char] -> TerM DeBruijnPattern
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> [Char]
forall a. Show a => a -> [Char]
show DummyTermKind
s)

      -- None of these terms correspond to "strict" patterns:
      Sort{}  -> TerM DeBruijnPattern
fallback
      Pi{}    -> TerM DeBruijnPattern
fallback
      Def{}   -> TerM DeBruijnPattern
fallback
      Lam{}   -> TerM DeBruijnPattern
fallback
      Level{} -> TerM DeBruijnPattern
fallback
      MetaV{} -> TerM DeBruijnPattern
fallback

      -- DontCare subterms mark irrelevantly-sorted positions, so they
      -- can not be used for termination checking.
      DontCare{} -> TerM DeBruijnPattern
fallback

      -- These terms are in the "strict" pattern language:
      Lit Literal
l        -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> TerM DeBruijnPattern)
-> DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Literal -> DeBruijnPattern
forall a. Literal -> Pattern' a
litP Literal
l
      Con ConHead
c ConInfo
_ Elims
args -> ConHead -> TerM DeBruijnPattern -> TerM DeBruijnPattern
ifNotConsOfHIT ConHead
c (TerM DeBruijnPattern -> TerM DeBruijnPattern)
-> TerM DeBruijnPattern -> TerM DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
        ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo (NAPs -> DeBruijnPattern)
-> ([Arg DeBruijnPattern] -> NAPs)
-> [Arg DeBruijnPattern]
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg DeBruijnPattern -> Arg (Named_ DeBruijnPattern))
-> [Arg DeBruijnPattern] -> NAPs
forall a b. (a -> b) -> [a] -> [b]
map' ((DeBruijnPattern -> Named_ DeBruijnPattern)
-> Arg DeBruijnPattern -> Arg (Named_ DeBruijnPattern)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Named_ DeBruijnPattern
forall a name. a -> Named name a
unnamed) ([Arg DeBruijnPattern] -> DeBruijnPattern)
-> TerM [Arg DeBruijnPattern] -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TerM [Arg DeBruijnPattern]
forall a b. TermToPattern a b => a -> TerM b
termToPattern (Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
args)

      Var Nat
i Elims
es
        -- variables with only projections, none of which are
        -- coinductive, become variable patterns
        | Just [(ProjOrigin, QName)]
oxs <- (Elim -> Maybe (ProjOrigin, QName))
-> Elims -> Maybe [(ProjOrigin, QName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es ->
          ((ProjOrigin, QName) -> TerM All)
-> [(ProjOrigin, QName)] -> TerM All
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool -> All
All (Bool -> All)
-> ((ProjOrigin, QName) -> TerM Bool)
-> (ProjOrigin, QName)
-> TerM All
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> QName -> TerM Bool
forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive (QName -> TerM Bool)
-> ((ProjOrigin, QName) -> QName)
-> (ProjOrigin, QName)
-> TerM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProjOrigin, QName) -> QName
forall a b. (a, b) -> b
snd) [(ProjOrigin, QName)]
oxs TerM All -> (All -> TerM DeBruijnPattern) -> TerM DeBruijnPattern
forall a b. TerM a -> (a -> TerM b) -> TerM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            All Bool
True -> DBPatVar -> DeBruijnPattern
forall a. a -> Pattern' a
varP (DBPatVar -> DeBruijnPattern)
-> (Name -> DBPatVar) -> Name -> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName -> Nat -> DBPatVar
`DBPatVar` Nat
i) (ArgName -> DBPatVar) -> (Name -> ArgName) -> Name -> DBPatVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ArgName
TS.pack ([Char] -> ArgName) -> (Name -> [Char]) -> Name -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> DeBruijnPattern) -> TerM Name -> TerM DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat -> TerM Name
forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Name
nameOfBV Nat
i
            All
_        -> TerM DeBruijnPattern
fallback
        | Bool
otherwise -> TerM DeBruijnPattern
fallback

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

-- | Extract recursive calls from one clause.
termClause :: Type -> Clause -> TerM Calls
termClause :: Type -> Clause -> TerM Calls
termClause Type
fty Clause
clause = do
  Clause{ clauseTel = tel, namedClausePats = ps, clauseBody = body } <- Clause -> TerM Clause
forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm Clause
etaExpandClause Clause
clause
  liftTCM $ reportSDoc "term.check.clause" 25 $ vcat
    [ "termClause"
    , nest 2 $ "tel = " <+> prettyTCM tel
    , nest 2 $ "fty = " <+> prettyTCM fty
    , nest 2 $ "ps  = " <+> do addContext tel $ prettyTCMPatternList ps
    ]
  forM' body $ \ Term
v -> Telescope -> TerM Calls -> TerM Calls
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
forall a b. (a -> b) -> a -> b
$ do
    -- TODO: combine the following two traversals, avoid full normalisation.
    -- Parse dot patterns as patterns as far as possible.
    ps <- (DeBruijnPattern -> TerM DeBruijnPattern) -> NAPs -> TerM NAPs
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM DeBruijnPattern -> TerM DeBruijnPattern
parseDotP NAPs
ps
    -- Blank out coconstructors.
    ps <- preTraversePatternM stripCoCon ps
    -- Mask non-data arguments.
    mdbpats <- maskNonDataArgs fty $ map' namedArg ps
    terSetPatterns mdbpats $ do
      reportBody v
      extract v
  where
    parseDotP :: DeBruijnPattern -> TerM DeBruijnPattern
    parseDotP :: DeBruijnPattern -> TerM DeBruijnPattern
parseDotP = \case
      DotP PatternInfo
o Term
t -> Term -> TerM DeBruijnPattern
forall a b. TermToPattern a b => a -> TerM b
termToPattern Term
t
      DeBruijnPattern
p        -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
    stripCoCon :: DeBruijnPattern -> TerM DeBruijnPattern
    stripCoCon :: DeBruijnPattern -> TerM DeBruijnPattern
stripCoCon = \case
      ConP (ConHead QName
c DataOrRecord
_ Induction
CoInductive [QName]
_) ConPatternInfo
_ NAPs
_ -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
unusedVar
      DeBruijnPattern
p -> DeBruijnPattern -> TerM DeBruijnPattern
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p
    reportBody :: Term -> TerM ()
    reportBody :: Term -> TerM ()
reportBody Term
v = [Char] -> Nat -> TerM () -> TerM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
verboseS [Char]
"term.check.clause" Nat
6 (TerM () -> TerM ()) -> TerM () -> TerM ()
forall a b. (a -> b) -> a -> b
$ do
      f       <- TerM QName
terGetCurrent
      pats    <- terGetPatterns
      liftTCM $ reportSDoc "term.check.clause" 6 $ do
        sep [ text ("termination checking clause of")
                <+> prettyTCM f
            , nest 2 $ "lhs:" <+> sep (map' prettyTCM pats)
            , nest 2 $ "rhs:" <+> prettyTCM v
            ]


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

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

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

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

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

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

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

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

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

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

-- | Extract recursive calls from a type.

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

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

-- | Extract recursive calls from a constructor application.

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

-- | Handles function applications @g es@.

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

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

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

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

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

    -- Then, consider call gArgs itself.

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

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

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

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

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

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

         -- Compute the call matrix.

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

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

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

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

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

-- 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 :: MonadTCM tcm => Term -> tcm Term
reduceCon :: forall (tcm :: * -> *). MonadTCM tcm => Term -> tcm Term
reduceCon = TCMT IO Term -> tcm Term
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> tcm Term)
-> (Term -> TCMT IO Term) -> Term -> tcm Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
traverseTermM \case
  Con ConHead
c ConInfo
ci Elims
vs -> (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
vs) (Term -> Term) -> TCMT IO Term -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO 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 -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t


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

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

  def <- QName -> TerM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
g
  -- -- Then, collect its clauses.
  -- cls <- defClauses <$> getConstInfo g
  -- reportSLn "term.reduce" 40 $ unwords [ "Function has", show (length cls), "clauses"]
  -- reportSDoc "term.reduce" 80 $ vcat $ map (prettyTCM . NamedClause g True) cls
  -- reportSLn  "term.reduce" 80 . ("allowed reductions = " ++) . show . SmallSet.elems
  --   =<< asksTC envAllowedReductions

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

-- | Extract recursive calls from a term.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Extract recursive calls from level expressions.

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

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

{- | @compareArgs es@

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

     The guardedness is the number of projection patterns in @pats@
     minus the number of projections in @es@.
 -}
compareArgs :: [Elim] -> TerM (Int, Int, [[Order]])
compareArgs :: Elims -> TerM (Nat, Nat, [[Order]])
compareArgs Elims
es = do
  pats <- TerM [DeBruijnPattern]
terGetPatterns

  liftTCM $ reportSDoc "term.compareArgs" 90 $ vcat
    [ text $ "comparing " ++ show (length es) ++ " args to " ++ show (length pats) ++ " patterns"
    ]

  matrix <- forM es \ Elim
e -> [DeBruijnPattern]
-> (DeBruijnPattern -> TerM Order) -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DeBruijnPattern]
pats \ DeBruijnPattern
p -> Elim -> DeBruijnPattern -> TerM Order
compareElim Elim
e DeBruijnPattern
p

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

-- | @compareElim e dbpat@

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

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

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

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

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

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

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

-- | Normalize outermost constructor name in a pattern.

{-# SPECIALIZE reduceConPattern :: DeBruijnPattern -> TerM DeBruijnPattern #-}
reduceConPattern :: MonadTCM tcm => DeBruijnPattern -> tcm DeBruijnPattern
reduceConPattern :: forall (tcm :: * -> *).
MonadTCM tcm =>
DeBruijnPattern -> tcm DeBruijnPattern
reduceConPattern = \case
  ConP ConHead
c ConPatternInfo
i NAPs
ps -> (SigError -> tcm ConHead)
-> tcm (Either SigError ConHead) -> tcm ConHead
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m (Either a b) -> m b
fromRightM (\ SigError
err -> ConHead -> tcm ConHead
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c) (TCM (Either SigError ConHead) -> tcm (Either SigError ConHead)
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Either SigError ConHead) -> tcm (Either SigError ConHead))
-> TCM (Either SigError ConHead) -> tcm (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ HasCallStack => QName -> TCM (Either SigError ConHead)
QName -> TCM (Either SigError ConHead)
getConForm (QName -> TCM (Either SigError ConHead))
-> QName -> TCM (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) tcm ConHead -> (ConHead -> DeBruijnPattern) -> tcm DeBruijnPattern
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ ConHead
c' ->
    ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c' ConPatternInfo
i NAPs
ps
  DeBruijnPattern
p -> DeBruijnPattern -> tcm DeBruijnPattern
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
p

-- | @compareTerm' t dbpat@
--
-- Precondition: 'reduceConPattern' has been applied to the pattern.

compareTerm' :: Term -> DeBruijnPattern -> TerM Order
compareTerm' :: Term -> DeBruijnPattern -> TerM Order
compareTerm' Term
v DeBruijnPattern
p = [Char] -> Nat -> [Char] -> TerM Order -> TerM Order
forall a. [Char] -> Nat -> [Char] -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Nat -> [Char] -> m a -> m a
verboseBracket [Char]
"term.compare" Nat
666 [Char]
"compareTerm" (TerM Order -> TerM Order) -> TerM Order -> TerM Order
forall a b. (a -> b) -> a -> b
$ do
  cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  -- v <- liftTCM (instantiate v) -- call extraction already instantiates metas in call arguments
  liftTCM $ reportSDoc "term.compare" 666 $ nest 2 $ prettyTCM v <+> "vs." <+> prettyTCM p
  let fallback = Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Order -> TerM Order) -> Order -> TerM Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
Term -> DeBruijnPattern -> Order
subTerm Term
v DeBruijnPattern
p
  case (v, p) of

    -- Andreas, 2013-11-20 do not drop projections,
    -- in any case not coinductive ones!:
    -- Andreas, 2025-11-05 we may drop all eliminations that are not coinductive projections.
    (Var Nat
i Elims
es, DeBruijnPattern
_) -> (Elim -> TerM All) -> Elims -> TerM All
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool -> All
All (Bool -> All) -> (Elim -> TerM Bool) -> Elim -> TerM All
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Elim -> TerM Bool
forall (tcm :: * -> *) t. MonadTCM tcm => Elim' t -> tcm Bool
elimNotCoinductive) Elims
es TerM All -> (All -> TerM Order) -> TerM Order
forall a b. TerM a -> (a -> TerM b) -> TerM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      All Bool
True -> Nat -> DeBruijnPattern -> TerM Order
compareVar Nat
i DeBruijnPattern
p
      All
_ -> TerM Order
fallback

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

    -- 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@.
    (MetaV{}, DeBruijnPattern
p) -> Order -> TerM Order
forall a. a -> TerM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Order -> TerM Order) -> Order -> TerM Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::CutOff) => Bool -> Nat -> Order
Bool -> Nat -> Order
Order.decr Bool
True case DeBruijnPattern
p of
      MaskP{} -> Nat
0
      DeBruijnPattern
_       -> DeBruijnPattern -> Nat
forall a. Pattern' a -> Nat
patternDepth DeBruijnPattern
p

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

    (Term, DeBruijnPattern)
_ | MaskP{} <- DeBruijnPattern
p -> Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown

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

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

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

    (Con{}, ConP ConHead
c ConPatternInfo
_ NAPs
ps) | (Arg (Named_ DeBruijnPattern) -> Bool) -> NAPs -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
Term -> DeBruijnPattern -> Bool
isSubTerm Term
v (DeBruijnPattern -> Bool)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps -> do
      [Char] -> Nat -> TCMT IO Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compare" Nat
666 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"Con vs. ConP (subterm)"
        , [Bool] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Bool] -> m Doc
prettyTCM ((Arg (Named_ DeBruijnPattern) -> Bool) -> NAPs -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
Term -> DeBruijnPattern -> Bool
isSubTerm Term
v (DeBruijnPattern -> Bool)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps)
        ]
      (?cutoff::CutOff) => Bool -> Nat -> Order
Bool -> Nat -> Order
decr Bool
True (Nat -> Order) -> TerM Nat -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TerM Nat
forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
offsetFromConstructor (ConHead -> QName
conName ConHead
c)

    (Con ConHead
c ConInfo
_ Elims
es, ConP ConHead
c' ConPatternInfo
_ NAPs
ps) | ConHead -> QName
conName ConHead
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c'-> do
      [Char] -> Nat -> TCMT IO Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compare" Nat
666 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"Con vs. ConP (same constructor)"
        , TCMT IO Doc
"subterms?" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Bool] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Bool] -> m Doc
prettyTCM ((Arg (Named_ DeBruijnPattern) -> Bool) -> NAPs -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
Term -> DeBruijnPattern -> Bool
isSubTerm Term
v (DeBruijnPattern -> Bool)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps)
        ]
      let ts :: [Arg Term]
ts = Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
      [Arg Term] -> NAPs -> TerM Order
compareConArgs [Arg Term]
ts NAPs
ps

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

    -- new case for counting constructors / projections
    -- register also increase
    (Con ConHead
c ConInfo
_ Elims
es, DeBruijnPattern
_) -> do
      let ts :: [Arg Term]
ts = Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
      as <- (Arg Term -> TerM Order) -> [Arg Term] -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ Arg Term
t -> Term -> DeBruijnPattern -> TerM Order
compareTerm' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) DeBruijnPattern
p) [Arg Term]
ts
      reportSDoc "term.compare" 666 $ vcat
        [ "Con vs. arbitrary (increasing)"
        , "results:" <+> pretty as
        , "infimum:" <+> pretty (infimum as)
        ]
      flip increase (infimum as) <$> offsetFromConstructor (conName c)

    (Term, DeBruijnPattern)
_ -> TerM Order
fallback

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

  equal Term
_ DeBruijnPattern
_ = Bool
False

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

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

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

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

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

    Ordering
EQ -> [Char] -> Nat -> [Char] -> TerM Order -> TerM Order
forall a. [Char] -> Nat -> [Char] -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Nat -> [Char] -> m a -> m a
verboseBracket [Char]
"term.compare" Nat
666 [Char]
"compareConArgs EQ" do
      [Char] -> Nat -> TCMT IO Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"term.compare" Nat
666 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"compareConArgs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
ts TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"vs." TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [DeBruijnPattern] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [DeBruijnPattern] -> m Doc
prettyTCM (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs
ps)
        , [Bool] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ((Term -> DeBruijnPattern -> Bool)
-> [Term] -> [DeBruijnPattern] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a b c.
Zip f g h =>
(a -> b -> c) -> f a -> g b -> h c
zipWith (?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
Term -> DeBruijnPattern -> Bool
isSubTerm (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> [Arg Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term]
ts) (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs
ps))
        ]
      let
        loop :: Order -> Args -> NAPs -> TerM Order
        loop :: Order -> [Arg Term] -> NAPs -> TerM Order
loop !Order
acc (Arg ArgInfo
_ Term
t:[Arg Term]
ts) ((Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg -> DeBruijnPattern
p):NAPs
ps) = case DeBruijnPattern
p of
          MaskP{} -> Order -> [Arg Term] -> NAPs -> TerM Order
loop Order
acc [Arg Term]
ts NAPs
ps
          DeBruijnPattern
_       -> do
            a <- Term -> DeBruijnPattern -> TerM Order
compareTerm' Term
t DeBruijnPattern
p
            loop (acc Order..*. a) ts ps
        loop Order
acc [Arg Term]
_ NAPs
_ = Order -> TerM Order
forall a. a -> TerM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Order
acc
      as <- Order -> [Arg Term] -> NAPs -> TerM Order
loop Order
Order.le [Arg Term]
ts NAPs
ps
      reportSDoc "term.compare" 666 $ "compareConArgs returns:" <+> pretty as
      pure as

compareVar :: Nat -> DeBruijnPattern -> TerM Order
compareVar :: Nat -> DeBruijnPattern -> TerM Order
compareVar Nat
i DeBruijnPattern
p = do
  cutoff <- TerM CutOff
terGetCutOff
  let ?cutoff = cutoff
  let no = Order -> TerM Order
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return Order
Order.unknown
  case p of
    ProjP{}          -> TerM Order
no
    LitP{}           -> TerM Order
no
    DotP{}           -> TerM Order
no
    MaskP DeBruijnPattern
_          -> TerM Order
no

    IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x  -> Order -> TerM Order
forall a. a -> TerM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Order -> TerM Order) -> Order -> TerM Order
forall a b. (a -> b) -> a -> b
$ Nat -> DBPatVar -> Order
compareVarVar Nat
i DBPatVar
x
    VarP PatternInfo
_ DBPatVar
x         -> Order -> TerM Order
forall a. a -> TerM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Order -> TerM Order) -> Order -> TerM Order
forall a b. (a -> b) -> a -> b
$ Nat -> DBPatVar -> Order
compareVarVar Nat
i DBPatVar
x

    ConP ConHead
c ConPatternInfo
pi NAPs
ps -> 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
      as <- (Arg (Named_ DeBruijnPattern) -> TerM Order)
-> NAPs -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Nat -> DeBruijnPattern -> TerM Order
compareVar Nat
i (DeBruijnPattern -> TerM Order)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> TerM Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps
      off <- offsetFromConstructor (conName c)
      reportSDoc "term.compare" 666 $ vcat
        [ "compareVar" <+> prettyTCM (var i) <+> "vs." <+> prettyTCM (namedArg <$> ps)
        , pretty as <+> "-->" <+> pretty (Order.supremum as)
        , "off:" <+> pretty off
        , "decrease:" <+> pretty (decrease off (Order.supremum as))
        ]
      pure $! decrease off (Order.supremum as)

    DefP PatternInfo
_ QName
c NAPs
ps -> 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
      Nat -> Order -> Order
decrease (Nat -> Order -> Order) -> TerM Nat -> TerM (Order -> Order)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TerM Nat
forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
offsetFromConstructor QName
c
               TerM (Order -> Order) -> TerM Order -> TerM Order
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Order] -> Order
Order.supremum ([Order] -> Order) -> TerM [Order] -> TerM Order
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg (Named_ DeBruijnPattern) -> TerM Order)
-> NAPs -> TerM [Order]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Nat -> DeBruijnPattern -> TerM Order
compareVar Nat
i (DeBruijnPattern -> TerM Order)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> TerM Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) NAPs
ps)
      -- This should be fine for c == hcomp

-- | Compare two variables.
--
--   The first variable comes from a term, the second from a pattern.
compareVarVar :: Nat -> DBPatVar -> Order
compareVarVar :: Nat -> DBPatVar -> Order
compareVarVar Nat
i (DBPatVar ArgName
_ Nat
j)
  | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j    = Order
Order.le
  | Bool
otherwise = Order
Order.unknown