-- | The monad for the termination checker.
--
--   The termination monad @TerM@ is an extension of
--   the type checking monad 'TCM' by an environment
--   with information needed by the termination checker.

module Agda.Termination.Monad where

import Prelude hiding (null)

import Control.Applicative hiding (empty)

import qualified Control.Monad.Fail as Fail

import Control.Monad          ( forM )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Except
import Control.Monad.Reader

import Data.DList (DList)
import qualified Data.DList as DL
import Data.Semigroup ( Semigroup(..) )
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.Interaction.Options (optTerminationDepth)

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Literal
import Agda.Syntax.Position (noRange)

import Agda.Termination.CutOff
import Agda.Termination.Order (Order,le,unknown)
import Agda.Termination.RecCheck (MutualNames, anyDefs)

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Benchmark
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

import Agda.Utils.Benchmark as B
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List   ( hasElem )
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Monoid
import Agda.Utils.Null
import Agda.Utils.Pretty (Pretty, prettyShow)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible

-- | The target of the function we are checking.

data Target
  = TargetDef QName
      -- ^ The target of recursion is a @record@, @data@, or unreducible @Def@.
  | TargetRecord
      -- ^ We are termination-checking a record.
  | TargetOther
      -- ^ None of the above two or unknown.
  deriving (Target -> Target -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Target -> Target -> Bool
$c/= :: Target -> Target -> Bool
== :: Target -> Target -> Bool
$c== :: Target -> Target -> Bool
Eq, Int -> Target -> ShowS
[Target] -> ShowS
Target -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Target] -> ShowS
$cshowList :: [Target] -> ShowS
show :: Target -> String
$cshow :: Target -> String
showsPrec :: Int -> Target -> ShowS
$cshowsPrec :: Int -> Target -> ShowS
Show)

-- | The current guardedness level.

type Guarded = Order

-- | The termination environment.

data TerEnv = TerEnv

  -- First part: options, configuration.

  { TerEnv -> Bool
terUseDotPatterns :: Bool
    -- ^ Are we mining dot patterns to find evindence of structal descent?
  , TerEnv -> Maybe QName
terSizeSuc :: Maybe QName
    -- ^ The name of size successor, if any.
  , TerEnv -> Maybe QName
terSharp   :: Maybe QName
    -- ^ The name of the delay constructor (sharp), if any.
  , TerEnv -> CutOff
terCutOff  :: CutOff
    -- ^ Depth at which to cut off the structural order.

  -- Second part: accumulated info during descent into decls./term.

  , TerEnv -> QName
terCurrent :: QName
    -- ^ The name of the function we are currently checking.
  , TerEnv -> MutualNames
terMutual  :: MutualNames
    -- ^ The names of the functions in the mutual block we are checking.
    --   This includes the internally generated functions
    --   (with, extendedlambda, coinduction).
  , TerEnv -> MutualNames
terUserNames :: Set QName
    -- ^ The list of name actually appearing in the file (abstract syntax).
    --   Excludes the internally generated functions.
  , TerEnv -> Bool
terHaveInlinedWith :: Bool
    -- ^ Does the actual clause result from with-inlining?
    --   (If yes, it may be ill-typed.)
  , TerEnv -> Target
terTarget  :: Target
    -- ^ Target type of the function we are currently termination checking.
    --   Only the constructors of 'Target' are considered guarding.
  , TerEnv -> Delayed
terDelayed :: Delayed
    -- ^ Are we checking a delayed definition?
  , TerEnv -> [Bool]
terMaskArgs :: [Bool]
    -- ^ Only consider the 'notMasked' 'False' arguments for establishing termination.
    --   See issue #1023.
  , TerEnv -> Bool
terMaskResult :: Bool
    -- ^ Only consider guardedness if 'False' (not masked).
  , TerEnv -> Int
_terSizeDepth :: Int  -- lazy by intention!
    -- ^ How many @SIZELT@ relations do we have in the context
    --   (= clause telescope).  Used to approximate termination
    --   for metas in call args.
  , TerEnv -> MaskedDeBruijnPatterns
terPatterns :: MaskedDeBruijnPatterns
    -- ^ The patterns of the clause we are checking.
  , TerEnv -> Int
terPatternsRaise :: !Int
    -- ^ Number of additional binders we have gone under
    --   (and consequently need to raise the patterns to compare to terms).
    --   Updated during call graph extraction, hence strict.
  , TerEnv -> Guarded
terGuarded :: !Guarded
    -- ^ The current guardedness status.  Changes as we go deeper into the term.
    --   Updated during call graph extraction, hence strict.
  , TerEnv -> Bool
terUseSizeLt :: Bool
    -- ^ When extracting usable size variables during construction of the call
    --   matrix, can we take the variable for use with SIZELT constraints from the context?
    --   Yes, if we are under an inductive constructor.
    --   No, if we are under a record constructor.
    --   (See issue #1015).
  , TerEnv -> VarSet
terUsableVars :: VarSet
    -- ^ Pattern variables that can be compared to argument variables using SIZELT.
  }

-- | An empty termination environment.
--
--   Values are set to a safe default meaning that with these
--   initial values the termination checker will not miss
--   termination errors it would have seen with better settings
--   of these values.
--
--   Values that do not have a safe default are set to
--   @__IMPOSSIBLE__@.

defaultTerEnv :: TerEnv
defaultTerEnv :: TerEnv
defaultTerEnv = TerEnv
  { terUseDotPatterns :: Bool
terUseDotPatterns           = Bool
False -- must be False initially!
  , terSizeSuc :: Maybe QName
terSizeSuc                  = forall a. Maybe a
Nothing
  , terSharp :: Maybe QName
terSharp                    = forall a. Maybe a
Nothing
  , terCutOff :: CutOff
terCutOff                   = CutOff
defaultCutOff
  , terUserNames :: MutualNames
terUserNames                = forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terMutual :: MutualNames
terMutual                   = forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terCurrent :: QName
terCurrent                  = forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terHaveInlinedWith :: Bool
terHaveInlinedWith          = Bool
False
  , terTarget :: Target
terTarget                   = Target
TargetOther
  , terDelayed :: Delayed
terDelayed                  = Delayed
NotDelayed
  , terMaskArgs :: [Bool]
terMaskArgs                 = forall a. a -> [a]
repeat Bool
False   -- use all arguments (mask none)
  , terMaskResult :: Bool
terMaskResult               = Bool
False          -- use result (do not mask)
  , _terSizeDepth :: Int
_terSizeDepth               = forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terPatterns :: MaskedDeBruijnPatterns
terPatterns                 = forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terPatternsRaise :: Int
terPatternsRaise            = Int
0
  , terGuarded :: Guarded
terGuarded                  = Guarded
le -- not initially guarded
  , terUseSizeLt :: Bool
terUseSizeLt                = Bool
False -- initially, not under data constructor
  , terUsableVars :: VarSet
terUsableVars               = VarSet
VarSet.empty
  }

-- | Termination monad service class.

class (Functor m, Monad m) => MonadTer m where
  terAsk   :: m TerEnv
  terLocal :: (TerEnv -> TerEnv) -> m a -> m a

  terAsks :: (TerEnv -> a) -> m a
  terAsks TerEnv -> a
f = TerEnv -> a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTer m => m TerEnv
terAsk

-- | Termination monad.

newtype TerM a = TerM { forall a. TerM a -> ReaderT TerEnv TCM a
terM :: ReaderT TerEnv TCM a }
  deriving ( forall a b. a -> TerM b -> TerM a
forall a b. (a -> b) -> TerM a -> TerM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TerM b -> TerM a
$c<$ :: forall a b. a -> TerM b -> TerM a
fmap :: forall a b. (a -> b) -> TerM a -> TerM b
$cfmap :: forall a b. (a -> b) -> TerM a -> TerM b
Functor
           , Functor TerM
forall a. a -> TerM a
forall a b. TerM a -> TerM b -> TerM a
forall a b. TerM a -> TerM b -> TerM b
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. TerM a -> TerM b -> TerM a
$c<* :: forall a b. TerM a -> TerM b -> TerM a
*> :: forall a b. TerM a -> TerM b -> TerM b
$c*> :: forall a b. TerM a -> TerM b -> TerM b
liftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
$cliftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
<*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
$c<*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
pure :: forall a. a -> TerM a
$cpure :: forall a. a -> TerM a
Applicative
           , Applicative TerM
forall a. a -> TerM a
forall a b. TerM a -> TerM b -> TerM b
forall a b. TerM a -> (a -> TerM b) -> TerM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TerM a
$creturn :: forall a. a -> TerM a
>> :: forall a b. TerM a -> TerM b -> TerM b
$c>> :: forall a b. TerM a -> TerM b -> TerM b
>>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
$c>>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
Monad
           , Monad TerM
forall a. String -> TerM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: forall a. String -> TerM a
$cfail :: forall a. String -> TerM a
Fail.MonadFail
           , MonadError TCErr
           , ReadTCState TerM
String -> (Integer -> Integer) -> TerM ()
forall (m :: * -> *).
ReadTCState m
-> (String -> (Integer -> Integer) -> m ()) -> MonadStatistics m
modifyCounter :: String -> (Integer -> Integer) -> TerM ()
$cmodifyCounter :: String -> (Integer -> Integer) -> TerM ()
MonadStatistics
           , Monad TerM
Functor TerM
Applicative TerM
TerM PragmaOptions
TerM CommandLineOptions
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
commandLineOptions :: TerM CommandLineOptions
$ccommandLineOptions :: TerM CommandLineOptions
pragmaOptions :: TerM PragmaOptions
$cpragmaOptions :: TerM PragmaOptions
HasOptions
           , Functor TerM
MonadFail TerM
Applicative TerM
String -> TerM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
Functor m
-> Applicative m
-> MonadFail m
-> (String -> m (Maybe (Builtin PrimFun)))
-> HasBuiltins m
getBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun))
$cgetBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun))
HasBuiltins
           , Monad TerM
Functor TerM
Applicative TerM
TerM Bool
TerM Verbosity
TerM ProfileOptions
String -> Int -> TCM Doc -> TerM String
forall a. String -> Int -> String -> TerM a -> TerM a
forall a. TerM a -> TerM a
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> (String -> Int -> TCM Doc -> m String)
-> (forall a. String -> Int -> String -> m a -> m a)
-> (forall a. String -> Int -> String -> m a -> m a)
-> m Verbosity
-> m ProfileOptions
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
nowDebugPrinting :: forall a. TerM a -> TerM a
$cnowDebugPrinting :: forall a. TerM a -> TerM a
isDebugPrinting :: TerM Bool
$cisDebugPrinting :: TerM Bool
getProfileOptions :: TerM ProfileOptions
$cgetProfileOptions :: TerM ProfileOptions
getVerbosity :: TerM Verbosity
$cgetVerbosity :: TerM Verbosity
verboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
$cverboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
traceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
$ctraceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
formatDebugMessage :: String -> Int -> TCM Doc -> TerM String
$cformatDebugMessage :: String -> Int -> TCM Doc -> TerM String
MonadDebug
           , Functor TerM
MonadFail TerM
Applicative TerM
MonadDebug TerM
HasOptions TerM
MonadTCEnv TerM
QName -> TerM RewriteRules
QName -> TerM (Either SigError Definition)
QName -> TerM Definition
forall (m :: * -> *).
Functor m
-> Applicative m
-> MonadFail m
-> HasOptions m
-> MonadDebug m
-> MonadTCEnv m
-> (QName -> m Definition)
-> (QName -> m (Either SigError Definition))
-> (QName -> m RewriteRules)
-> HasConstInfo m
getRewriteRulesFor :: QName -> TerM RewriteRules
$cgetRewriteRulesFor :: QName -> TerM RewriteRules
getConstInfo' :: QName -> TerM (Either SigError Definition)
$cgetConstInfo' :: QName -> TerM (Either SigError Definition)
getConstInfo :: QName -> TerM Definition
$cgetConstInfo :: QName -> TerM Definition
HasConstInfo
           , Monad TerM
forall a. IO a -> TerM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> TerM a
$cliftIO :: forall a. IO a -> TerM a
MonadIO
           , Monad TerM
TerM TCEnv
forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
localTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
askTC :: TerM TCEnv
$caskTC :: TerM TCEnv
MonadTCEnv
           , Monad TerM
TerM TCState
TCState -> TerM ()
(TCState -> TCState) -> TerM ()
forall (m :: * -> *).
Monad m
-> m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
modifyTC :: (TCState -> TCState) -> TerM ()
$cmodifyTC :: (TCState -> TCState) -> TerM ()
putTC :: TCState -> TerM ()
$cputTC :: TCState -> TerM ()
getTC :: TerM TCState
$cgetTC :: TerM TCState
MonadTCState
           , Applicative TerM
MonadIO TerM
HasOptions TerM
MonadTCState TerM
MonadTCEnv TerM
forall a. TCM a -> TerM a
forall (tcm :: * -> *).
Applicative tcm
-> MonadIO tcm
-> MonadTCEnv tcm
-> MonadTCState tcm
-> HasOptions tcm
-> (forall a. TCM a -> tcm a)
-> MonadTCM tcm
liftTCM :: forall a. TCM a -> TerM a
$cliftTCM :: forall a. TCM a -> TerM a
MonadTCM
           , Monad TerM
TerM TCState
forall a. (TCState -> TCState) -> TerM a -> TerM a
forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
withTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
$cwithTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b
$clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b
getTCState :: TerM TCState
$cgetTCState :: TerM TCState
ReadTCState
           , Applicative TerM
HasOptions TerM
MonadTCEnv TerM
ReadTCState TerM
forall a. ReduceM a -> TerM a
forall (m :: * -> *).
Applicative m
-> MonadTCEnv m
-> ReadTCState m
-> HasOptions m
-> (forall a. ReduceM a -> m a)
-> MonadReduce m
liftReduce :: forall a. ReduceM a -> TerM a
$cliftReduce :: forall a. ReduceM a -> TerM a
MonadReduce
           , MonadTCEnv TerM
forall a. Range -> String -> (Name -> TerM a) -> TerM a
forall a. Name -> Term -> Dom Type -> TerM a -> TerM a
forall a. Name -> Dom Type -> TerM a -> TerM a
forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
forall (m :: * -> *).
MonadTCEnv m
-> (forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
withFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
$cwithFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
updateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
$cupdateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
addLetBinding' :: forall a. Name -> Term -> Dom Type -> TerM a -> TerM a
$caddLetBinding' :: forall a. Name -> Term -> Dom Type -> TerM a -> TerM a
addCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
$caddCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
MonadAddContext
           , MonadDebug TerM
MonadTCEnv TerM
MonadReduce TerM
ReadTCState TerM
MonadAddContext TerM
HasBuiltins TerM
HasConstInfo TerM
forall (m :: * -> *).
HasBuiltins m
-> HasConstInfo m
-> MonadAddContext m
-> MonadDebug m
-> MonadReduce m
-> MonadTCEnv m
-> ReadTCState m
-> PureTCM m
PureTCM
           )

-- This could be derived automatically, but the derived type family becomes `BenchPhase (ReaderT TerEnv TCM)` which
-- is *fine* but triggers complaints that the "type family application is no smaller than the instance head, why not
-- nuke everything with UndecidableInstances".
instance MonadBench TerM where
  type BenchPhase TerM = Phase
  getBenchmark :: TerM (Benchmark (BenchPhase TerM))
getBenchmark              = forall a. ReaderT TerEnv TCM a -> TerM a
TerM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadBench m => m (Benchmark (BenchPhase m))
B.getBenchmark
  putBenchmark :: Benchmark (BenchPhase TerM) -> TerM ()
putBenchmark              = forall a. ReaderT TerEnv TCM a -> TerM a
TerM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadBench m =>
Benchmark (BenchPhase m) -> m ()
B.putBenchmark
  modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM))
-> TerM ()
modifyBenchmark           = forall a. ReaderT TerEnv TCM a -> TerM a
TerM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadBench m =>
(Benchmark (BenchPhase m) -> Benchmark (BenchPhase m)) -> m ()
B.modifyBenchmark
  finally :: forall a b. TerM a -> TerM b -> TerM a
finally (TerM ReaderT TerEnv TCM b
m) (TerM ReaderT TerEnv TCM c
f) = forall a. ReaderT TerEnv TCM a -> TerM a
TerM forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *) b c. MonadBench m => m b -> m c -> m b
B.finally ReaderT TerEnv TCM b
m ReaderT TerEnv TCM c
f)

instance MonadTer TerM where
  terAsk :: TerM TerEnv
terAsk     = forall a. ReaderT TerEnv TCM a -> TerM a
TerM forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *). MonadReader r m => m r
ask
  terLocal :: forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
terLocal TerEnv -> TerEnv
f = forall a. ReaderT TerEnv TCM a -> TerM a
TerM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local TerEnv -> TerEnv
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TerM a -> ReaderT TerEnv TCM a
terM

-- | Generic run method for termination monad.
runTer :: TerEnv -> TerM a -> TCM a
runTer :: forall a. TerEnv -> TerM a -> TCM a
runTer TerEnv
tenv (TerM ReaderT TerEnv TCM a
m) = forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT TerEnv TCM a
m TerEnv
tenv

-- | Run TerM computation in default environment (created from options).

runTerDefault :: TerM a -> TCM a
runTerDefault :: forall a. TerM a -> TCM a
runTerDefault TerM a
cont = do

  -- Assemble then initial configuration of the termination environment.

  CutOff
cutoff <- PragmaOptions -> CutOff
optTerminationDepth forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  -- Get the name of size suc (if sized types are enabled)
  Maybe QName
suc <- forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
m (Maybe QName)
sizeSucName

  -- The name of sharp (if available).
  Maybe QName
sharp <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfSharp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe CoinductionKit)
coinductionKit

  let tenv :: TerEnv
tenv = TerEnv
defaultTerEnv
        { terSizeSuc :: Maybe QName
terSizeSuc                  = Maybe QName
suc
        , terSharp :: Maybe QName
terSharp                    = Maybe QName
sharp
        , terCutOff :: CutOff
terCutOff                   = CutOff
cutoff
        }

  forall a. TerEnv -> TerM a -> TCM a
runTer TerEnv
tenv TerM a
cont

-- -- * Termination monad is a 'MonadTCM'.

-- instance MonadError TCErr TerM where
--   throwError = liftTCM . throwError
--   catchError m handler = TerM $ ReaderT $ \ tenv -> do
--     runTer tenv m `catchError` (\ err -> runTer tenv $ handler err)

instance Semigroup m => Semigroup (TerM m) where
  <> :: TerM m -> TerM m -> TerM m
(<>) = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. Semigroup a => a -> a -> a
(<>)

instance (Semigroup m, Monoid m) => Monoid (TerM m) where
  mempty :: TerM m
mempty  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
  mappend :: TerM m -> TerM m -> TerM m
mappend = forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [TerM m] -> TerM m
mconcat = forall a. Monoid a => [a] -> a
mconcat forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence

-- * Modifiers and accessors for the termination environment in the monad.

terGetUseDotPatterns :: TerM Bool
terGetUseDotPatterns :: TerM Bool
terGetUseDotPatterns = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terUseDotPatterns

terSetUseDotPatterns :: Bool -> TerM a -> TerM a
terSetUseDotPatterns :: forall a. Bool -> TerM a -> TerM a
terSetUseDotPatterns Bool
b = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terUseDotPatterns :: Bool
terUseDotPatterns = Bool
b }

terGetSizeSuc :: TerM (Maybe QName)
terGetSizeSuc :: TerM (Maybe QName)
terGetSizeSuc = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Maybe QName
terSizeSuc

terGetCurrent :: TerM QName
terGetCurrent :: TerM QName
terGetCurrent = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> QName
terCurrent

terSetCurrent :: QName -> TerM a -> TerM a
terSetCurrent :: forall a. QName -> TerM a -> TerM a
terSetCurrent QName
q = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terCurrent :: QName
terCurrent = QName
q }

terGetSharp :: TerM (Maybe QName)
terGetSharp :: TerM (Maybe QName)
terGetSharp = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Maybe QName
terSharp

terGetCutOff :: TerM CutOff
terGetCutOff :: TerM CutOff
terGetCutOff = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> CutOff
terCutOff

terGetMutual :: TerM MutualNames
terGetMutual :: TerM MutualNames
terGetMutual = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> MutualNames
terMutual

terGetUserNames :: TerM (Set QName)
terGetUserNames :: TerM MutualNames
terGetUserNames = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> MutualNames
terUserNames

terGetTarget :: TerM Target
terGetTarget :: TerM Target
terGetTarget = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Target
terTarget

terSetTarget :: Target -> TerM a -> TerM a
terSetTarget :: forall a. Target -> TerM a -> TerM a
terSetTarget Target
t = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terTarget :: Target
terTarget = Target
t }

terGetHaveInlinedWith :: TerM Bool
terGetHaveInlinedWith :: TerM Bool
terGetHaveInlinedWith = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terHaveInlinedWith

terSetHaveInlinedWith :: TerM a -> TerM a
terSetHaveInlinedWith :: forall a. TerM a -> TerM a
terSetHaveInlinedWith = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terHaveInlinedWith :: Bool
terHaveInlinedWith = Bool
True }

terGetDelayed :: TerM Delayed
terGetDelayed :: TerM Delayed
terGetDelayed = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Delayed
terDelayed

terSetDelayed :: Delayed -> TerM a -> TerM a
terSetDelayed :: forall a. Delayed -> TerM a -> TerM a
terSetDelayed Delayed
b = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terDelayed :: Delayed
terDelayed = Delayed
b }

terGetMaskArgs :: TerM [Bool]
terGetMaskArgs :: TerM [Bool]
terGetMaskArgs = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> [Bool]
terMaskArgs

terSetMaskArgs :: [Bool] -> TerM a -> TerM a
terSetMaskArgs :: forall a. [Bool] -> TerM a -> TerM a
terSetMaskArgs [Bool]
b = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terMaskArgs :: [Bool]
terMaskArgs = [Bool]
b }

terGetMaskResult :: TerM Bool
terGetMaskResult :: TerM Bool
terGetMaskResult = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terMaskResult

terSetMaskResult :: Bool -> TerM a -> TerM a
terSetMaskResult :: forall a. Bool -> TerM a -> TerM a
terSetMaskResult Bool
b = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terMaskResult :: Bool
terMaskResult = Bool
b }

terGetPatterns :: TerM (MaskedDeBruijnPatterns)
terGetPatterns :: TerM MaskedDeBruijnPatterns
terGetPatterns = do
  Int
n   <- forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Int
terPatternsRaise
  MaskedDeBruijnPatterns
mps <- forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> MaskedDeBruijnPatterns
terPatterns
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Int
n forall a. Eq a => a -> a -> Bool
== Int
0 then MaskedDeBruijnPatterns
mps else forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Subst a => Int -> a -> a
raise Int
n)) MaskedDeBruijnPatterns
mps

terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns :: forall a. MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns MaskedDeBruijnPatterns
ps = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terPatterns :: MaskedDeBruijnPatterns
terPatterns = MaskedDeBruijnPatterns
ps }

terRaise :: TerM a -> TerM a
terRaise :: forall a. TerM a -> TerM a
terRaise = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terPatternsRaise :: Int
terPatternsRaise = TerEnv -> Int
terPatternsRaise TerEnv
e forall a. Num a => a -> a -> a
+ Int
1 }

terGetGuarded :: TerM Guarded
terGetGuarded :: TerM Guarded
terGetGuarded = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Guarded
terGuarded

terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a
terModifyGuarded :: forall a. (Guarded -> Guarded) -> TerM a -> TerM a
terModifyGuarded Guarded -> Guarded
f = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terGuarded :: Guarded
terGuarded = Guarded -> Guarded
f forall a b. (a -> b) -> a -> b
$ TerEnv -> Guarded
terGuarded TerEnv
e }

terSetGuarded :: Order -> TerM a -> TerM a
terSetGuarded :: forall a. Guarded -> TerM a -> TerM a
terSetGuarded = forall a. (Guarded -> Guarded) -> TerM a -> TerM a
terModifyGuarded forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const

terUnguarded :: TerM a -> TerM a
terUnguarded :: forall a. TerM a -> TerM a
terUnguarded = forall a. Guarded -> TerM a -> TerM a
terSetGuarded Guarded
unknown

-- | Lens for '_terSizeDepth'.

terSizeDepth :: Lens' Int TerEnv
terSizeDepth :: Lens' Int TerEnv
terSizeDepth Int -> f Int
f TerEnv
e = Int -> f Int
f (TerEnv -> Int
_terSizeDepth TerEnv
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Int
i -> TerEnv
e { _terSizeDepth :: Int
_terSizeDepth = Int
i }

-- | Lens for 'terUsableVars'.

terGetUsableVars :: TerM VarSet
terGetUsableVars :: TerM VarSet
terGetUsableVars = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> VarSet
terUsableVars

terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
terModifyUsableVars :: forall a. (VarSet -> VarSet) -> TerM a -> TerM a
terModifyUsableVars VarSet -> VarSet
f = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terUsableVars :: VarSet
terUsableVars = VarSet -> VarSet
f forall a b. (a -> b) -> a -> b
$ TerEnv -> VarSet
terUsableVars TerEnv
e }

terSetUsableVars :: VarSet -> TerM a -> TerM a
terSetUsableVars :: forall a. VarSet -> TerM a -> TerM a
terSetUsableVars = forall a. (VarSet -> VarSet) -> TerM a -> TerM a
terModifyUsableVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const

-- | Lens for 'terUseSizeLt'.

terGetUseSizeLt :: TerM Bool
terGetUseSizeLt :: TerM Bool
terGetUseSizeLt = forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terUseSizeLt

terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
terModifyUseSizeLt :: forall a. (Bool -> Bool) -> TerM a -> TerM a
terModifyUseSizeLt Bool -> Bool
f = forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terUseSizeLt :: Bool
terUseSizeLt = Bool -> Bool
f forall a b. (a -> b) -> a -> b
$ TerEnv -> Bool
terUseSizeLt TerEnv
e }

terSetUseSizeLt :: Bool -> TerM a -> TerM a
terSetUseSizeLt :: forall a. Bool -> TerM a -> TerM a
terSetUseSizeLt = forall a. (Bool -> Bool) -> TerM a -> TerM a
terModifyUseSizeLt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const

-- | Compute usable vars from patterns and run subcomputation.
withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
withUsableVars :: forall a b. UsableSizeVars a => a -> TerM b -> TerM b
withUsableVars a
pats TerM b
m = do
  VarSet
vars <- forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars a
pats
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.size" Int
70 forall a b. (a -> b) -> a -> b
$ String
"usableSizeVars = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show VarSet
vars
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.size" Int
20 forall a b. (a -> b) -> a -> b
$ if forall a. Null a => a -> Bool
null VarSet
vars then TCM Doc
"no usuable size vars" else
    TCM Doc
"the size variables amoung these variables are usable: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) forall a b. (a -> b) -> a -> b
$ VarSet -> [Int]
VarSet.toList VarSet
vars)
  forall a. VarSet -> TerM a -> TerM a
terSetUsableVars VarSet
vars forall a b. (a -> b) -> a -> b
$ TerM b
m

-- | Set 'terUseSizeLt' when going under constructor @c@.
conUseSizeLt :: QName -> TerM a -> TerM a
conUseSizeLt :: forall a. QName -> TerM a -> TerM a
conUseSizeLt QName
c TerM a
m = do
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c)  -- Non-eta inductive records are the same as datatypes
    (forall a. Bool -> TerM a -> TerM a
terSetUseSizeLt Bool
False TerM a
m)
    (forall a. Bool -> TerM a -> TerM a
terSetUseSizeLt Bool
True TerM a
m)

-- | Set 'terUseSizeLt' for arguments following projection @q@.
--   We disregard j<i after a non-coinductive projection.
--   However, the projection need not be recursive (Issue 1470).
projUseSizeLt :: QName -> TerM a -> TerM a
projUseSizeLt :: forall a. QName -> TerM a -> TerM a
projUseSizeLt QName
q TerM a
m = do
  Bool
co <- forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection Bool
False QName
q
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.size" Int
20 forall a b. (a -> b) -> a -> b
$ forall a. Bool -> (a -> a) -> a -> a
applyUnless Bool
co (String
"not " forall a. [a] -> [a] -> [a]
++) forall a b. (a -> b) -> a -> b
$
    String
"using SIZELT vars after projection " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
q
  forall a. Bool -> TerM a -> TerM a
terSetUseSizeLt Bool
co TerM a
m

-- | For termination checking purposes flat should not be considered a
--   projection. That is, it flat doesn't preserve either structural order
--   or guardedness like other projections do.
--   Andreas, 2012-06-09: the same applies to projections of recursive records.
isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive :: forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive QName
qn = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  Bool
b <- QName -> TCM Bool
isProjectionButNotCoinductive' QName
qn
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.proj" Int
60 forall a b. (a -> b) -> a -> b
$ do
    TCM Doc
"identifier" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
qn forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
      forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$
        if Bool
b then String
"is an inductive projection"
          else String
"is either not a projection or coinductive"
  forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
  where
    isProjectionButNotCoinductive' :: QName -> TCM Bool
isProjectionButNotCoinductive' QName
qn = do
      Maybe QName
flat <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfFlat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe CoinductionKit)
coinductionKit
      if forall a. a -> Maybe a
Just QName
qn forall a. Eq a => a -> a -> Bool
== Maybe QName
flat
        then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        else do
          Maybe Projection
mp <- forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
qn
          case Maybe Projection
mp of
            Just Projection{ projProper :: Projection -> Maybe QName
projProper = Just{}, projFromType :: Projection -> Arg QName
projFromType = Arg QName
t }
              -> QName -> TCM Bool
isInductiveRecord (forall e. Arg e -> e
unArg Arg QName
t)
            Maybe Projection
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Check whether a projection belongs to a coinductive record
--   and is actually recursive.
--   E.g.
--   @
--      isCoinductiveProjection (Stream.head) = return False
--
--      isCoinductiveProjection (Stream.tail) = return True
--   @
isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection :: forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection Bool
mustBeRecursive QName
q = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 forall a b. (a -> b) -> a -> b
$ String
"checking isCoinductiveProjection " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
q
  Maybe QName
flat <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfFlat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe CoinductionKit)
coinductionKit
  -- yes for ♭
  if forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
flat then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else do
    Definition
pdef <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
    case Defn -> Maybe Projection
isProjection_ (Definition -> Defn
theDef Definition
pdef) of
      Just Projection{ projProper :: Projection -> Maybe QName
projProper = Just{}, projFromType :: Projection -> Arg QName
projFromType = Arg ArgInfo
_ QName
r, projIndex :: Projection -> Int
projIndex = Int
n } ->
        forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r) forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ Defn
rdef -> do
          -- no for inductive or non-recursive record
          if Defn -> Maybe Induction
recInduction Defn
rdef forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Induction
CoInductive then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
            forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ String
" is coinductive; record type is " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
r
            if Bool -> Bool
not Bool
mustBeRecursive then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else do
              forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ String
" must be recursive"
              if Bool -> Bool
not (Defn -> Bool
safeRecRecursive Defn
rdef) then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
                forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ String
" has been declared recursive, doing actual check now..."
                -- TODO: the following test for recursiveness of a projection should be cached.
                -- E.g., it could be stored in the @Projection@ component.
                -- Now check if type of field mentions mutually recursive symbol.
                -- Get the type of the field by dropping record parameters and record argument.
                let TelV Telescope
tel Type
core = Type -> TelV Type
telView' (Definition -> Type
defType Definition
pdef)
                    ([Dom (String, Type)]
pars, [Dom (String, Type)]
tel') = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
                    mut :: [QName]
mut = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Defn -> Maybe [QName]
recMutual Defn
rdef
                -- Check if any recursive symbols appear in the record type.
                -- Q (2014-07-01): Should we normalize the type?
                -- A (2017-01-13): Yes, since we also normalize during positivity check?
                -- See issue #1899.
                forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.guardedness" Int
40 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                  [ TCM Doc
"looking for recursive occurrences of"
                  , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
mut)
                  , TCM Doc
"in"
                  , forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Dom (String, Type)]
pars forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Dom (String, Type)] -> Telescope
telFromList [Dom (String, Type)]
tel')
                  , TCM Doc
"and"
                  , forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
core
                  ]
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null [QName]
mut) forall a. HasCallStack => a
__IMPOSSIBLE__
                MutualNames
names <- forall a. GetDefs a => (QName -> Bool) -> a -> TCM MutualNames
anyDefs ([QName]
mut forall a. Ord a => [a] -> a -> Bool
`hasElem`) (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom (String, Type)]
tel', Type
core)
                forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.guardedness" Int
40 forall a b. (a -> b) -> a -> b
$
                  TCM Doc
"found" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> if forall a. Null a => a -> Bool
null MutualNames
names then TCM Doc
"none" else forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList MutualNames
names)
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null MutualNames
names
      Maybe Projection
_ -> do
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ String
" is not a proper projection"
        forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  where
  -- Andreas, 2018-02-24, issue #2975, example:
  -- @
  -- record R : Set where
  --   coinductive
  --   field force : R

  --   r : R
  --   force r = r
  -- @
  -- The termination checker expects the positivity checker to have run on the
  -- record declaration R to know whether R is recursive.
  -- However, here, because the awkward processing of record declarations (see #434),
  -- that has not happened.  To avoid crashing (as in Agda 2.5.3),
  -- we rather give the possibly wrong answer here,
  -- restoring the behavior of Agda 2.5.2.  TODO: fix record declaration checking.
  safeRecRecursive :: Defn -> Bool
  safeRecRecursive :: Defn -> Bool
safeRecRecursive (Record { recMutual :: Defn -> Maybe [QName]
recMutual = Just [QName]
qs }) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null [QName]
qs
  safeRecRecursive Defn
_ = Bool
False

-- * De Bruijn pattern stuff

-- | How long is the path to the deepest atomic pattern?
patternDepth :: forall a. Pattern' a -> Int
patternDepth :: forall a. Pattern' a -> Int
patternDepth = MaxNat -> Int
getMaxNat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> MaxNat -> MaxNat
depth where
  depth :: Pattern' a -> MaxNat -> MaxNat
  depth :: Pattern' a -> MaxNat -> MaxNat
depth ConP{} = forall a. Enum a => a -> a
succ      -- add 1 to the maximum of the depth of the subpatterns
  depth Pattern' a
_      = forall a. a -> a
id        -- atomic pattern (leaf) has depth 0

-- | A dummy pattern used to mask a pattern that cannot be used
--   for structural descent.

unusedVar :: DeBruijnPattern
unusedVar :: DeBruijnPattern
unusedVar = forall a. Literal -> Pattern' a
litP (Text -> Literal
LitString Text
"term.unused.pat.var")

-- | Extract variables from 'DeBruijnPattern's that could witness a decrease
--   via a SIZELT constraint.
--
--   These variables must be under an inductive constructor (with no record
--   constructor in the way), or after a coinductive projection (with no
--   inductive one in the way).

class UsableSizeVars a where
  usableSizeVars :: a -> TerM VarSet

instance UsableSizeVars DeBruijnPattern where
  usableSizeVars :: DeBruijnPattern -> TerM VarSet
usableSizeVars = forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern forall a b. (a -> b) -> a -> b
$ \case
    VarP PatternInfo
_ DBPatVar
x   -> forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TerM Bool
terGetUseSizeLt (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> VarSet
VarSet.singleton forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x) forall a b. (a -> b) -> a -> b
$
                   {-else-} forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
_ -> forall a. QName -> TerM a -> TerM a
conUseSizeLt forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
    LitP{}     -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    DotP{}     -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    ProjP{}    -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    IApplyP{}  -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    DefP{} -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    where none :: p -> m a
none p
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty

instance UsableSizeVars [DeBruijnPattern] where
  usableSizeVars :: [DeBruijnPattern] -> TerM VarSet
usableSizeVars [DeBruijnPattern]
ps =
    case [DeBruijnPattern]
ps of
      []               -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
      (ProjP ProjOrigin
_ QName
q : [DeBruijnPattern]
ps) -> forall a. QName -> TerM a -> TerM a
projUseSizeLt QName
q forall a b. (a -> b) -> a -> b
$ forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars [DeBruijnPattern]
ps
      (DeBruijnPattern
p         : [DeBruijnPattern]
ps) -> forall a. Monoid a => a -> a -> a
mappend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars DeBruijnPattern
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars [DeBruijnPattern]
ps

instance UsableSizeVars (Masked DeBruijnPattern) where
  usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet
usableSizeVars (Masked Bool
m DeBruijnPattern
p) = (forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
`foldrPattern` DeBruijnPattern
p) forall a b. (a -> b) -> a -> b
$ \case
    VarP PatternInfo
_ DBPatVar
x   -> forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TerM Bool
terGetUseSizeLt (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> VarSet
VarSet.singleton forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x) forall a b. (a -> b) -> a -> b
$
                   {-else-} forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
_ -> if Bool
m then forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none else forall a. QName -> TerM a -> TerM a
conUseSizeLt forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
    LitP{}     -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    DotP{}     -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    ProjP{}    -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    IApplyP{}  -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    DefP{}     -> forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    where none :: p -> m a
none p
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty

instance UsableSizeVars MaskedDeBruijnPatterns where
  usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet
usableSizeVars MaskedDeBruijnPatterns
ps =
    case MaskedDeBruijnPatterns
ps of
      []                          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
      (Masked Bool
_ (ProjP ProjOrigin
_ QName
q) : MaskedDeBruijnPatterns
ps) -> forall a. QName -> TerM a -> TerM a
projUseSizeLt QName
q forall a b. (a -> b) -> a -> b
$ forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars MaskedDeBruijnPatterns
ps
      (Masked DeBruijnPattern
p                    : MaskedDeBruijnPatterns
ps) -> forall a. Monoid a => a -> a -> a
mappend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars Masked DeBruijnPattern
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars MaskedDeBruijnPatterns
ps

-- * Masked patterns (which are not eligible for structural descent, only for size descent)
--   See issue #1023.

type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]

data Masked a = Masked
  { forall a. Masked a -> Bool
getMask   :: Bool  -- ^ True if thing not eligible for structural descent.
  , forall a. Masked a -> a
getMasked :: a     -- ^ Thing.
  } deriving (Masked a -> Masked a -> Bool
forall a. Eq a => Masked a -> Masked a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Masked a -> Masked a -> Bool
$c/= :: forall a. Eq a => Masked a -> Masked a -> Bool
== :: Masked a -> Masked a -> Bool
$c== :: forall a. Eq a => Masked a -> Masked a -> Bool
Eq, Masked a -> Masked a -> Bool
Masked a -> Masked a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Masked a)
forall a. Ord a => Masked a -> Masked a -> Bool
forall a. Ord a => Masked a -> Masked a -> Ordering
forall a. Ord a => Masked a -> Masked a -> Masked a
min :: Masked a -> Masked a -> Masked a
$cmin :: forall a. Ord a => Masked a -> Masked a -> Masked a
max :: Masked a -> Masked a -> Masked a
$cmax :: forall a. Ord a => Masked a -> Masked a -> Masked a
>= :: Masked a -> Masked a -> Bool
$c>= :: forall a. Ord a => Masked a -> Masked a -> Bool
> :: Masked a -> Masked a -> Bool
$c> :: forall a. Ord a => Masked a -> Masked a -> Bool
<= :: Masked a -> Masked a -> Bool
$c<= :: forall a. Ord a => Masked a -> Masked a -> Bool
< :: Masked a -> Masked a -> Bool
$c< :: forall a. Ord a => Masked a -> Masked a -> Bool
compare :: Masked a -> Masked a -> Ordering
$ccompare :: forall a. Ord a => Masked a -> Masked a -> Ordering
Ord, Int -> Masked a -> ShowS
forall a. Show a => Int -> Masked a -> ShowS
forall a. Show a => [Masked a] -> ShowS
forall a. Show a => Masked a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Masked a] -> ShowS
$cshowList :: forall a. Show a => [Masked a] -> ShowS
show :: Masked a -> String
$cshow :: forall a. Show a => Masked a -> String
showsPrec :: Int -> Masked a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Masked a -> ShowS
Show, forall a b. a -> Masked b -> Masked a
forall a b. (a -> b) -> Masked a -> Masked b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Masked b -> Masked a
$c<$ :: forall a b. a -> Masked b -> Masked a
fmap :: forall a b. (a -> b) -> Masked a -> Masked b
$cfmap :: forall a b. (a -> b) -> Masked a -> Masked b
Functor, forall a. Eq a => a -> Masked a -> Bool
forall a. Num a => Masked a -> a
forall a. Ord a => Masked a -> a
forall m. Monoid m => Masked m -> m
forall a. Masked a -> Bool
forall a. Masked a -> Int
forall a. Masked a -> [a]
forall a. (a -> a -> a) -> Masked a -> a
forall m a. Monoid m => (a -> m) -> Masked a -> m
forall b a. (b -> a -> b) -> b -> Masked a -> b
forall a b. (a -> b -> b) -> b -> Masked a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Masked a -> a
$cproduct :: forall a. Num a => Masked a -> a
sum :: forall a. Num a => Masked a -> a
$csum :: forall a. Num a => Masked a -> a
minimum :: forall a. Ord a => Masked a -> a
$cminimum :: forall a. Ord a => Masked a -> a
maximum :: forall a. Ord a => Masked a -> a
$cmaximum :: forall a. Ord a => Masked a -> a
elem :: forall a. Eq a => a -> Masked a -> Bool
$celem :: forall a. Eq a => a -> Masked a -> Bool
length :: forall a. Masked a -> Int
$clength :: forall a. Masked a -> Int
null :: forall a. Masked a -> Bool
$cnull :: forall a. Masked a -> Bool
toList :: forall a. Masked a -> [a]
$ctoList :: forall a. Masked a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Masked a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Masked a -> a
foldr1 :: forall a. (a -> a -> a) -> Masked a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Masked a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Masked a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Masked a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Masked a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Masked a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Masked a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Masked a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Masked a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Masked a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Masked a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Masked a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Masked a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Masked a -> m
fold :: forall m. Monoid m => Masked m -> m
$cfold :: forall m. Monoid m => Masked m -> m
Foldable, Functor Masked
Foldable Masked
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
forall (f :: * -> *) a.
Applicative f =>
Masked (f a) -> f (Masked a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Masked a -> m (Masked b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Masked a -> f (Masked b)
sequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
$csequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Masked a -> m (Masked b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Masked a -> m (Masked b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Masked (f a) -> f (Masked a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Masked (f a) -> f (Masked a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Masked a -> f (Masked b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Masked a -> f (Masked b)
Traversable)

masked :: a -> Masked a
masked :: forall a. a -> Masked a
masked = forall a. Bool -> a -> Masked a
Masked Bool
True

notMasked :: a -> Masked a
notMasked :: forall a. a -> Masked a
notMasked = forall a. Bool -> a -> Masked a
Masked Bool
False

instance Decoration Masked where
  traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Masked a -> m (Masked b)
traverseF a -> m b
f (Masked Bool
m a
a) = forall a. Bool -> a -> Masked a
Masked Bool
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a

-- | Print masked things in double parentheses.
instance PrettyTCM a => PrettyTCM (Masked a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Masked a -> m Doc
prettyTCM (Masked Bool
m a
a) = forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
m (forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). Functor m => m Doc -> m Doc
parens) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a

-- * Call pathes

-- | Call paths.

-- An old comment:
--
--   The call information is stored as free monoid
--   over 'CallInfo'.  As long as we never look at it,
--   only accumulate it, it does not matter whether we use
--   'Set', (nub) list, or 'Tree'.
--   Internally, due to lazyness, it is anyway a binary tree of
--   'mappend' nodes and singleton leafs.
--   Since we define no order on 'CallInfo' (expensive),
--   we cannot use a 'Set' or nub list.
--   Performance-wise, I could not see a difference between Set and list.
--
-- If the binary tree is balanced "incorrectly", then forcing it could
-- be expensive, so a switch was made to difference lists.

newtype CallPath = CallPath (DList CallInfo)
  deriving (Int -> CallPath -> ShowS
[CallPath] -> ShowS
CallPath -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CallPath] -> ShowS
$cshowList :: [CallPath] -> ShowS
show :: CallPath -> String
$cshow :: CallPath -> String
showsPrec :: Int -> CallPath -> ShowS
$cshowsPrec :: Int -> CallPath -> ShowS
Show, NonEmpty CallPath -> CallPath
CallPath -> CallPath -> CallPath
forall b. Integral b => b -> CallPath -> CallPath
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> CallPath -> CallPath
$cstimes :: forall b. Integral b => b -> CallPath -> CallPath
sconcat :: NonEmpty CallPath -> CallPath
$csconcat :: NonEmpty CallPath -> CallPath
<> :: CallPath -> CallPath -> CallPath
$c<> :: CallPath -> CallPath -> CallPath
Semigroup, Semigroup CallPath
CallPath
[CallPath] -> CallPath
CallPath -> CallPath -> CallPath
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [CallPath] -> CallPath
$cmconcat :: [CallPath] -> CallPath
mappend :: CallPath -> CallPath -> CallPath
$cmappend :: CallPath -> CallPath -> CallPath
mempty :: CallPath
$cmempty :: CallPath
Monoid)

-- | The calls making up the call path.

callInfos :: CallPath -> [CallInfo]
callInfos :: CallPath -> [CallInfo]
callInfos (CallPath DList CallInfo
cs) = forall a. DList a -> [a]
DL.toList DList CallInfo
cs

-- | Only show intermediate nodes.  (Drop last 'CallInfo').
instance Pretty CallPath where
  pretty :: CallPath -> Doc
pretty CallPath
cis0 = if forall a. Null a => a -> Bool
null [CallInfo]
cis then forall a. Null a => a
empty else
    forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hsep (forall a b. (a -> b) -> [a] -> [b]
map (\ CallInfo
ci -> Doc
arrow Doc -> Doc -> Doc
P.<+> forall a. Pretty a => a -> Doc
P.pretty CallInfo
ci) [CallInfo]
cis) Doc -> Doc -> Doc
P.<+> Doc
arrow
    where
      cis :: [CallInfo]
cis   = forall a. [a] -> [a]
init (CallPath -> [CallInfo]
callInfos CallPath
cis0)
      arrow :: Doc
arrow = Doc
"-->"

-- * Size depth estimation

-- | A very crude way of estimating the @SIZELT@ chains
--   @i > j > k@ in context.  Returns 3 in this case.
--   Overapproximates.
class TerSetSizeDepth b where
  terSetSizeDepth :: b -> TerM a -> TerM a

instance TerSetSizeDepth Telescope where
  terSetSizeDepth :: forall a. Telescope -> TerM a -> TerM a
terSetSizeDepth = forall b a. TerSetSizeDepth b => b -> TerM a -> TerM a
terSetSizeDepth forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (String, t)]
telToList

-- TODO: more precise analysis, constructing a tree
-- of relations between size variables.
instance TerSetSizeDepth ListTel where
  terSetSizeDepth :: forall a. [Dom (String, Type)] -> TerM a -> TerM a
terSetSizeDepth [Dom (String, Type)]
doms TerM a
cont = do
    Int
n <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Dom (String, Type)]
doms forall a b. (a -> b) -> a -> b
$ \ Dom (String, Type)
dom -> do
        -- Andreas, 2022-03-12, TODO:
        -- use ifBlocked?  Shouldn't blocked types be treated like metas?
        Type
a <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom (String, Type)
dom
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a) (forall (m :: * -> *) a. Monad m => a -> m a
return Int
1) {- else -} forall a b. (a -> b) -> a -> b
$
          case forall t a. Type'' t a -> a
unEl Type
a of
            MetaV{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
            Term
_       -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
    forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal (forall i o. Lens' i o -> LensSet i o
set Lens' Int TerEnv
terSizeDepth Int
n) TerM a
cont