-- | 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.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.Syntax.Common.Pretty (Pretty, prettyShow)
import qualified Agda.Syntax.Common.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
(Target -> Target -> Bool)
-> (Target -> Target -> Bool) -> Eq Target
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Target -> Target -> Bool
== :: Target -> Target -> Bool
$c/= :: Target -> Target -> Bool
/= :: Target -> Target -> Bool
Eq, Int -> Target -> ShowS
[Target] -> ShowS
Target -> String
(Int -> Target -> ShowS)
-> (Target -> String) -> ([Target] -> ShowS) -> Show Target
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Target -> ShowS
showsPrec :: Int -> Target -> ShowS
$cshow :: Target -> String
show :: Target -> String
$cshowList :: [Target] -> ShowS
showList :: [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 -> [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                  = Maybe QName
forall a. Maybe a
Nothing
  , terSharp :: Maybe QName
terSharp                    = Maybe QName
forall a. Maybe a
Nothing
  , terCutOff :: CutOff
terCutOff                   = CutOff
defaultCutOff
  , terUserNames :: MutualNames
terUserNames                = MutualNames
forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terMutual :: MutualNames
terMutual                   = MutualNames
forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terCurrent :: QName
terCurrent                  = QName
forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terHaveInlinedWith :: Bool
terHaveInlinedWith          = Bool
False
  , terTarget :: Target
terTarget                   = Target
TargetOther
  , terMaskArgs :: [Bool]
terMaskArgs                 = Bool -> [Bool]
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               = Int
forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terPatterns :: MaskedDeBruijnPatterns
terPatterns                 = MaskedDeBruijnPatterns
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 (TerEnv -> a) -> m TerEnv -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TerEnv
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 -> b) -> TerM a -> TerM b)
-> (forall a b. a -> TerM b -> TerM a) -> Functor TerM
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
$cfmap :: forall a b. (a -> b) -> TerM a -> TerM b
fmap :: forall a b. (a -> b) -> TerM a -> TerM b
$c<$ :: forall a b. a -> TerM b -> TerM a
<$ :: forall a b. a -> TerM b -> TerM a
Functor
           , Functor TerM
Functor TerM =>
(forall a. a -> TerM a)
-> (forall a b. TerM (a -> b) -> TerM a -> TerM b)
-> (forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c)
-> (forall a b. TerM a -> TerM b -> TerM b)
-> (forall a b. TerM a -> TerM b -> TerM a)
-> Applicative 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
$cpure :: forall a. a -> TerM a
pure :: forall a. a -> TerM a
$c<*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
<*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
$cliftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
liftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
$c*> :: forall a b. TerM a -> TerM b -> TerM b
*> :: forall a b. TerM a -> TerM b -> TerM b
$c<* :: forall a b. TerM a -> TerM b -> TerM a
<* :: forall a b. TerM a -> TerM b -> TerM a
Applicative
           , Applicative TerM
Applicative TerM =>
(forall a b. TerM a -> (a -> TerM b) -> TerM b)
-> (forall a b. TerM a -> TerM b -> TerM b)
-> (forall a. a -> TerM a)
-> Monad 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
$c>>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
>>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
$c>> :: forall a b. TerM a -> TerM b -> TerM b
>> :: forall a b. TerM a -> TerM b -> TerM b
$creturn :: forall a. a -> TerM a
return :: forall a. a -> TerM a
Monad
           , Monad TerM
Monad TerM => (forall a. String -> TerM a) -> MonadFail TerM
forall a. String -> TerM a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> TerM a
fail :: forall a. String -> TerM a
Fail.MonadFail
           , MonadError TCErr
           , ReadTCState TerM
String -> (Integer -> Integer) -> TerM ()
ReadTCState TerM =>
(String -> (Integer -> Integer) -> TerM ()) -> MonadStatistics TerM
forall (m :: * -> *).
ReadTCState m =>
(String -> (Integer -> Integer) -> m ()) -> MonadStatistics m
$cmodifyCounter :: String -> (Integer -> Integer) -> TerM ()
modifyCounter :: String -> (Integer -> Integer) -> TerM ()
MonadStatistics
           , Monad TerM
Functor TerM
Applicative TerM
TerM PragmaOptions
TerM CommandLineOptions
(Functor TerM, Applicative TerM, Monad TerM) =>
TerM PragmaOptions -> TerM CommandLineOptions -> HasOptions TerM
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
m PragmaOptions -> m CommandLineOptions -> HasOptions m
$cpragmaOptions :: TerM PragmaOptions
pragmaOptions :: TerM PragmaOptions
$ccommandLineOptions :: TerM CommandLineOptions
commandLineOptions :: TerM CommandLineOptions
HasOptions
           , Functor TerM
MonadFail TerM
Applicative TerM
(Functor TerM, Applicative TerM, MonadFail TerM) =>
(SomeBuiltin -> TerM (Maybe (Builtin PrimFun))) -> HasBuiltins TerM
SomeBuiltin -> TerM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
(Functor m, Applicative m, MonadFail m) =>
(SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
$cgetBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun))
getBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun))
HasBuiltins
           , Monad TerM
Functor TerM
Applicative TerM
TerM Bool
TerM Verbosity
TerM ProfileOptions
(Functor TerM, Applicative TerM, Monad TerM) =>
(String -> Int -> TCM Doc -> TerM String)
-> (forall a. String -> Int -> String -> TerM a -> TerM a)
-> (forall a. String -> Int -> String -> TerM a -> TerM a)
-> TerM Verbosity
-> TerM ProfileOptions
-> TerM Bool
-> (forall a. TerM a -> TerM a)
-> MonadDebug TerM
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
$cformatDebugMessage :: String -> Int -> TCM Doc -> TerM String
formatDebugMessage :: String -> Int -> TCM Doc -> TerM String
$ctraceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
traceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
$cverboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
verboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
$cgetVerbosity :: TerM Verbosity
getVerbosity :: TerM Verbosity
$cgetProfileOptions :: TerM ProfileOptions
getProfileOptions :: TerM ProfileOptions
$cisDebugPrinting :: TerM Bool
isDebugPrinting :: TerM Bool
$cnowDebugPrinting :: forall a. TerM a -> TerM a
nowDebugPrinting :: forall a. TerM a -> TerM a
MonadDebug
           , Functor TerM
MonadFail TerM
Applicative TerM
HasOptions TerM
MonadDebug TerM
MonadTCEnv TerM
(Functor TerM, Applicative TerM, MonadFail TerM, HasOptions TerM,
 MonadDebug TerM, MonadTCEnv TerM) =>
(QName -> TerM Definition)
-> (QName -> TerM (Either SigError Definition))
-> (QName -> TerM RewriteRules)
-> HasConstInfo 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
$cgetConstInfo :: QName -> TerM Definition
getConstInfo :: QName -> TerM Definition
$cgetConstInfo' :: QName -> TerM (Either SigError Definition)
getConstInfo' :: QName -> TerM (Either SigError Definition)
$cgetRewriteRulesFor :: QName -> TerM RewriteRules
getRewriteRulesFor :: QName -> TerM RewriteRules
HasConstInfo
           , Monad TerM
Monad TerM => (forall a. IO a -> TerM a) -> MonadIO TerM
forall a. IO a -> TerM a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> TerM a
liftIO :: forall a. IO a -> TerM a
MonadIO
           , Monad TerM
TerM TCEnv
Monad TerM =>
TerM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a)
-> MonadTCEnv TerM
forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
forall (m :: * -> *).
Monad m =>
m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
$caskTC :: TerM TCEnv
askTC :: TerM TCEnv
$clocalTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
localTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
MonadTCEnv
           , Monad TerM
TerM TCState
Monad TerM =>
TerM TCState
-> (TCState -> TerM ())
-> ((TCState -> TCState) -> TerM ())
-> MonadTCState TerM
TCState -> TerM ()
(TCState -> TCState) -> TerM ()
forall (m :: * -> *).
Monad m =>
m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
$cgetTC :: TerM TCState
getTC :: TerM TCState
$cputTC :: TCState -> TerM ()
putTC :: TCState -> TerM ()
$cmodifyTC :: (TCState -> TCState) -> TerM ()
modifyTC :: (TCState -> TCState) -> TerM ()
MonadTCState
           , Applicative TerM
MonadIO TerM
HasOptions TerM
MonadTCState TerM
MonadTCEnv TerM
(Applicative TerM, MonadIO TerM, MonadTCEnv TerM,
 MonadTCState TerM, HasOptions TerM) =>
(forall a. TCM a -> TerM a) -> MonadTCM 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
$cliftTCM :: forall a. TCM a -> TerM a
liftTCM :: forall a. TCM a -> TerM a
MonadTCM
           , Monad TerM
TerM TCState
Monad TerM =>
TerM TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b)
-> (forall a. (TCState -> TCState) -> TerM a -> TerM a)
-> ReadTCState TerM
forall a. (TCState -> TCState) -> TerM a -> TerM a
forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b
forall (m :: * -> *).
Monad m =>
m TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
$cgetTCState :: TerM TCState
getTCState :: TerM TCState
$clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b
$cwithTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
withTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
ReadTCState
           , Applicative TerM
HasOptions TerM
MonadTCEnv TerM
ReadTCState TerM
(Applicative TerM, MonadTCEnv TerM, ReadTCState TerM,
 HasOptions TerM) =>
(forall a. ReduceM a -> TerM a) -> MonadReduce 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
$cliftReduce :: forall a. ReduceM a -> TerM a
liftReduce :: forall a. ReduceM a -> TerM a
MonadReduce
           , MonadTCEnv TerM
MonadTCEnv TerM =>
(forall a. Name -> Dom Type -> TerM a -> TerM a)
-> (forall a.
    Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a)
-> (forall a.
    Substitution -> (Context -> Context) -> TerM a -> TerM a)
-> (forall a. Range -> String -> (Name -> TerM a) -> TerM a)
-> MonadAddContext TerM
forall a. Range -> String -> (Name -> TerM a) -> TerM a
forall a. Origin -> 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. Origin -> 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
$caddCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
addCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
$caddLetBinding' :: forall a. Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a
addLetBinding' :: forall a. Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a
$cupdateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
updateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
$cwithFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
withFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
MonadAddContext
           , MonadDebug TerM
MonadTCEnv TerM
MonadReduce TerM
ReadTCState TerM
MonadAddContext TerM
HasBuiltins TerM
HasConstInfo TerM
(HasBuiltins TerM, HasConstInfo TerM, MonadAddContext TerM,
 MonadDebug TerM, MonadReduce TerM, MonadTCEnv TerM,
 ReadTCState TerM) =>
PureTCM 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              = ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
-> TerM (Benchmark (BenchPhase TerM))
forall a. ReaderT TerEnv TCM a -> TerM a
TerM (ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
 -> TerM (Benchmark (BenchPhase TerM)))
-> ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
-> TerM (Benchmark (BenchPhase TerM))
forall a b. (a -> b) -> a -> b
$ ReaderT TerEnv TCM (Benchmark (BenchPhase (ReaderT TerEnv TCM)))
ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
forall (m :: * -> *). MonadBench m => m (Benchmark (BenchPhase m))
B.getBenchmark
  putBenchmark :: Benchmark (BenchPhase TerM) -> TerM ()
putBenchmark              = ReaderT TerEnv TCM () -> TerM ()
forall a. ReaderT TerEnv TCM a -> TerM a
TerM (ReaderT TerEnv TCM () -> TerM ())
-> (Benchmark Phase -> ReaderT TerEnv TCM ())
-> Benchmark Phase
-> TerM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Benchmark (BenchPhase (ReaderT TerEnv TCM))
-> ReaderT TerEnv TCM ()
Benchmark Phase -> ReaderT TerEnv TCM ()
forall (m :: * -> *).
MonadBench m =>
Benchmark (BenchPhase m) -> m ()
B.putBenchmark
  modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM))
-> TerM ()
modifyBenchmark           = ReaderT TerEnv TCM () -> TerM ()
forall a. ReaderT TerEnv TCM a -> TerM a
TerM (ReaderT TerEnv TCM () -> TerM ())
-> ((Benchmark Phase -> Benchmark Phase) -> ReaderT TerEnv TCM ())
-> (Benchmark Phase -> Benchmark Phase)
-> TerM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Benchmark (BenchPhase (ReaderT TerEnv TCM))
 -> Benchmark (BenchPhase (ReaderT TerEnv TCM)))
-> ReaderT TerEnv TCM ()
(Benchmark Phase -> Benchmark Phase) -> ReaderT TerEnv TCM ()
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) = ReaderT TerEnv TCM b -> TerM b
forall a. ReaderT TerEnv TCM a -> TerM a
TerM (ReaderT TerEnv TCM b -> TerM b) -> ReaderT TerEnv TCM b -> TerM b
forall a b. (a -> b) -> a -> b
$ (ReaderT TerEnv TCM b
-> ReaderT TerEnv TCM c -> ReaderT TerEnv TCM b
forall b c.
ReaderT TerEnv TCM b
-> ReaderT TerEnv TCM c -> ReaderT TerEnv TCM 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     = ReaderT TerEnv TCM TerEnv -> TerM TerEnv
forall a. ReaderT TerEnv TCM a -> TerM a
TerM (ReaderT TerEnv TCM TerEnv -> TerM TerEnv)
-> ReaderT TerEnv TCM TerEnv -> TerM TerEnv
forall a b. (a -> b) -> a -> b
$ ReaderT TerEnv TCM TerEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  terLocal :: forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
terLocal TerEnv -> TerEnv
f = ReaderT TerEnv TCM a -> TerM a
forall a. ReaderT TerEnv TCM a -> TerM a
TerM (ReaderT TerEnv TCM a -> TerM a)
-> (TerM a -> ReaderT TerEnv TCM a) -> TerM a -> TerM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TerEnv -> TerEnv) -> ReaderT TerEnv TCM a -> ReaderT TerEnv TCM a
forall a.
(TerEnv -> TerEnv) -> ReaderT TerEnv TCM a -> ReaderT TerEnv TCM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local TerEnv -> TerEnv
f (ReaderT TerEnv TCM a -> ReaderT TerEnv TCM a)
-> (TerM a -> ReaderT TerEnv TCM a)
-> TerM a
-> ReaderT TerEnv TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TerM a -> ReaderT TerEnv TCM a
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) = ReaderT TerEnv TCM a -> TerEnv -> TCMT IO a
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 (PragmaOptions -> CutOff)
-> TCMT IO PragmaOptions -> TCMT IO CutOff
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

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

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

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

  TerEnv -> TerM a -> TCM a
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
(<>) = (m -> m -> m) -> TerM m -> TerM m -> TerM m
forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 m -> m -> m
forall a. Semigroup a => a -> a -> a
(<>)

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

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

terGetUseDotPatterns :: TerM Bool
terGetUseDotPatterns :: TerM Bool
terGetUseDotPatterns = (TerEnv -> Bool) -> TerM Bool
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terUseDotPatterns = b }

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

terGetCurrent :: TerM QName
terGetCurrent :: TerM QName
terGetCurrent = (TerEnv -> QName) -> TerM QName
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terCurrent = q }

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

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

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

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

terGetTarget :: TerM Target
terGetTarget :: TerM Target
terGetTarget = (TerEnv -> Target) -> TerM Target
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terTarget = t }

terGetHaveInlinedWith :: TerM Bool
terGetHaveInlinedWith :: TerM Bool
terGetHaveInlinedWith = (TerEnv -> Bool) -> TerM Bool
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terHaveInlinedWith = True }

terGetMaskArgs :: TerM [Bool]
terGetMaskArgs :: TerM [Bool]
terGetMaskArgs = (TerEnv -> [Bool]) -> TerM [Bool]
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terMaskArgs = b }

terGetMaskResult :: TerM Bool
terGetMaskResult :: TerM Bool
terGetMaskResult = (TerEnv -> Bool) -> TerM Bool
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terMaskResult = b }

terGetPatterns :: TerM (MaskedDeBruijnPatterns)
terGetPatterns :: TerM MaskedDeBruijnPatterns
terGetPatterns = do
  Int
n   <- (TerEnv -> Int) -> TerM Int
forall a. (TerEnv -> a) -> TerM a
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Int
terPatternsRaise
  MaskedDeBruijnPatterns
mps <- (TerEnv -> MaskedDeBruijnPatterns) -> TerM MaskedDeBruijnPatterns
forall a. (TerEnv -> a) -> TerM a
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> MaskedDeBruijnPatterns
terPatterns
  MaskedDeBruijnPatterns -> TerM MaskedDeBruijnPatterns
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaskedDeBruijnPatterns -> TerM MaskedDeBruijnPatterns)
-> MaskedDeBruijnPatterns -> TerM MaskedDeBruijnPatterns
forall a b. (a -> b) -> a -> b
$ if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then MaskedDeBruijnPatterns
mps else (Masked DeBruijnPattern -> Masked DeBruijnPattern)
-> MaskedDeBruijnPatterns -> MaskedDeBruijnPatterns
forall a b. (a -> b) -> [a] -> [b]
map ((DeBruijnPattern -> DeBruijnPattern)
-> Masked DeBruijnPattern -> Masked DeBruijnPattern
forall a b. (a -> b) -> Masked a -> Masked b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> DeBruijnPattern -> DeBruijnPattern
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terPatterns = ps }

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

terGetGuarded :: TerM Guarded
terGetGuarded :: TerM Guarded
terGetGuarded = (TerEnv -> Guarded) -> TerM Guarded
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terGuarded = f $ terGuarded e }

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

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

-- | Lens for '_terSizeDepth'.

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

-- | Lens for 'terUsableVars'.

terGetUsableVars :: TerM VarSet
terGetUsableVars :: TerM VarSet
terGetUsableVars = (TerEnv -> VarSet) -> TerM VarSet
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terUsableVars = f $ terUsableVars e }

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

-- | Lens for 'terUseSizeLt'.

terGetUseSizeLt :: TerM Bool
terGetUseSizeLt :: TerM Bool
terGetUseSizeLt = (TerEnv -> Bool) -> TerM Bool
forall a. (TerEnv -> a) -> TerM a
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 = (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
-> (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a b. (a -> b) -> a -> b
$ \ TerEnv
e -> TerEnv
e { terUseSizeLt = f $ terUseSizeLt e }

terSetUseSizeLt :: Bool -> TerM a -> TerM a
terSetUseSizeLt :: forall a. Bool -> TerM a -> TerM a
terSetUseSizeLt = (Bool -> Bool) -> TerM a -> TerM a
forall a. (Bool -> Bool) -> TerM a -> TerM a
terModifyUseSizeLt ((Bool -> Bool) -> TerM a -> TerM a)
-> (Bool -> Bool -> Bool) -> Bool -> TerM a -> TerM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool -> Bool
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 <- a -> TerM VarSet
forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars a
pats
  String -> Int -> String -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.size" Int
70 (String -> TerM ()) -> String -> TerM ()
forall a b. (a -> b) -> a -> b
$ String
"usableSizeVars = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VarSet -> String
forall a. Show a => a -> String
show VarSet
vars
  String -> Int -> TCM Doc -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.size" Int
20 (TCM Doc -> TerM ()) -> TCM Doc -> TerM ()
forall a b. (a -> b) -> a -> b
$ if VarSet -> Bool
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: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Int -> TCM Doc) -> [Int] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCM Doc) -> (Int -> Term) -> Int -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) ([Int] -> [TCM Doc]) -> [Int] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ VarSet -> [Int]
VarSet.toList VarSet
vars)
  VarSet -> TerM b -> TerM b
forall a. VarSet -> TerM a -> TerM a
terSetUsableVars VarSet
vars (TerM b -> TerM b) -> TerM b -> TerM b
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
  TerM Bool -> TerM a -> TerM a -> TerM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCM Bool -> TerM Bool
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> TerM Bool) -> TCM Bool -> TerM Bool
forall a b. (a -> b) -> a -> b
$ QName -> TCM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c)  -- Non-eta inductive records are the same as datatypes
    (Bool -> TerM a -> TerM a
forall a. Bool -> TerM a -> TerM a
terSetUseSizeLt Bool
False TerM a
m)
    (Bool -> TerM a -> TerM a
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 <- Bool -> QName -> TerM Bool
forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection Bool
False QName
q
  String -> Int -> String -> TerM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.size" Int
20 (String -> TerM ()) -> String -> TerM ()
forall a b. (a -> b) -> a -> b
$ Bool -> ShowS -> ShowS
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
co (String
"not " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String
"using SIZELT vars after projection " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q
  Bool -> TerM a -> TerM a
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 = TCM Bool -> tcm Bool
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> tcm Bool) -> TCM Bool -> tcm Bool
forall a b. (a -> b) -> a -> b
$ do
  Bool
b <- QName -> TCM Bool
isProjectionButNotCoinductive' QName
qn
  String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.proj" Int
60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
    TCM Doc
"identifier" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
      String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
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"
  Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
  where
    isProjectionButNotCoinductive' :: QName -> TCM Bool
isProjectionButNotCoinductive' QName
qn = do
      Maybe QName
flat <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfFlat (Maybe CoinductionKit -> Maybe QName)
-> TCMT IO (Maybe CoinductionKit) -> TCMT IO (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe CoinductionKit)
coinductionKit
      if QName -> Maybe QName
forall a. a -> Maybe a
Just QName
qn Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
flat
        then Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        else do
          Maybe Projection
mp <- QName -> TCMT IO (Maybe Projection)
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
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isInductiveRecord (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
t)
            Maybe Projection
_ -> Bool -> TCM Bool
forall a. a -> TCMT IO a
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 = TCM Bool -> tcm Bool
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> tcm Bool) -> TCM Bool -> tcm Bool
forall a b. (a -> b) -> a -> b
$ do
  String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"checking isCoinductiveProjection " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q
  Maybe QName
flat <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfFlat (Maybe CoinductionKit -> Maybe QName)
-> TCMT IO (Maybe CoinductionKit) -> TCMT IO (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe CoinductionKit)
coinductionKit
  -- yes for ♭
  if QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
flat then Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else do
    Definition
pdef <- QName -> TCMT IO Definition
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 } ->
        TCMT IO (Maybe Defn) -> TCM Bool -> (Defn -> TCM Bool) -> TCM Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> TCMT IO (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r) TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Defn -> TCM Bool) -> TCM Bool) -> (Defn -> TCM Bool) -> TCM Bool
forall a b. (a -> b) -> a -> b
$ \ Defn
rdef -> do
          -- no for inductive or non-recursive record
          if Defn -> Maybe Induction
recInduction Defn
rdef Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive then Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
            String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is coinductive; record type is " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
r
            if Bool -> Bool
not Bool
mustBeRecursive then Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else do
              String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" must be recursive"
              if Bool -> Bool
not (Defn -> Bool
safeRecRecursive Defn
rdef) then Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
                String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q String -> ShowS
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') = Int
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n ([Dom (String, Type)]
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
                    mut :: [QName]
mut = [QName] -> Maybe [QName] -> [QName]
forall a. a -> Maybe a -> a
fromMaybe [QName]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [QName] -> [QName]) -> Maybe [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ 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.
                String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.guardedness" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                  [ TCM Doc
"looking for recursive occurrences of"
                  , [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((QName -> TCM Doc) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM [QName]
mut)
                  , TCM Doc
"in"
                  , [Dom (String, Type)] -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
[Dom (String, Type)] -> m a -> m a
addContext [Dom (String, Type)]
pars (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM ([Dom (String, Type)] -> Telescope
telFromList [Dom (String, Type)]
tel')
                  , TCM Doc
"and"
                  , Telescope -> TCM Doc -> TCM Doc
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 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
core
                  ]
                Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([QName] -> Bool
forall a. Null a => a -> Bool
null [QName]
mut) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
                MutualNames
names <- (QName -> Bool) -> ([Type], Type) -> TCM MutualNames
forall a. GetDefs a => (QName -> Bool) -> a -> TCM MutualNames
anyDefs ([QName]
mut [QName] -> QName -> Bool
forall a. Ord a => [a] -> a -> Bool
`hasElem`) ((Dom (String, Type) -> Type) -> [Dom (String, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> (Dom (String, Type) -> (String, Type))
-> Dom (String, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
unDom) [Dom (String, Type)]
tel', Type
core)
                String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"term.guardedness" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
                  TCM Doc
"found" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> if MutualNames -> Bool
forall a. Null a => a -> Bool
null MutualNames
names then TCM Doc
"none" else [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((QName -> TCM Doc) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM ([QName] -> [TCM Doc]) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ MutualNames -> [QName]
forall a. Set a -> [a]
Set.toList MutualNames
names)
                Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ MutualNames -> Bool
forall a. Null a => a -> Bool
null MutualNames
names
      Maybe Projection
_ -> do
        String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"term.guardedness" Int
40 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not a proper projection"
        Bool -> TCM Bool
forall a. a -> TCMT IO a
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QName] -> Bool
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 (MaxNat -> Int) -> (Pattern' a -> MaxNat) -> Pattern' a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' a -> MaxNat -> MaxNat) -> Pattern' a -> MaxNat
forall m. Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m
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{} = MaxNat -> MaxNat
forall a. Enum a => a -> a
succ      -- add 1 to the maximum of the depth of the subpatterns
  depth Pattern' a
_      = MaxNat -> MaxNat
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 = Literal -> DeBruijnPattern
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 = (DeBruijnPattern -> TerM VarSet -> TerM VarSet)
-> DeBruijnPattern -> TerM VarSet
forall m.
Monoid m =>
(DeBruijnPattern -> m -> m) -> DeBruijnPattern -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern ((DeBruijnPattern -> TerM VarSet -> TerM VarSet)
 -> DeBruijnPattern -> TerM VarSet)
-> (DeBruijnPattern -> TerM VarSet -> TerM VarSet)
-> DeBruijnPattern
-> TerM VarSet
forall a b. (a -> b) -> a -> b
$ \case
    VarP PatternInfo
_ DBPatVar
x   -> TerM VarSet -> TerM VarSet -> TerM VarSet
forall a b. a -> b -> a
const (TerM VarSet -> TerM VarSet -> TerM VarSet)
-> TerM VarSet -> TerM VarSet -> TerM VarSet
forall a b. (a -> b) -> a -> b
$ TerM Bool -> TerM VarSet -> TerM VarSet -> TerM VarSet
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TerM Bool
terGetUseSizeLt (VarSet -> TerM VarSet
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return (VarSet -> TerM VarSet) -> VarSet -> TerM VarSet
forall a b. (a -> b) -> a -> b
$ Int -> VarSet
VarSet.singleton (Int -> VarSet) -> Int -> VarSet
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x) (TerM VarSet -> TerM VarSet) -> TerM VarSet -> TerM VarSet
forall a b. (a -> b) -> a -> b
$
                   {-else-} VarSet -> TerM VarSet
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return VarSet
forall a. Monoid a => a
mempty
    ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
_ -> QName -> TerM VarSet -> TerM VarSet
forall a. QName -> TerM a -> TerM a
conUseSizeLt (QName -> TerM VarSet -> TerM VarSet)
-> QName -> TerM VarSet -> TerM VarSet
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
    LitP{}     -> TerM VarSet -> TerM VarSet
forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    DotP{}     -> TerM VarSet -> TerM VarSet
forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    ProjP{}    -> TerM VarSet -> TerM VarSet
forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    IApplyP{}  -> TerM VarSet -> TerM VarSet
forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    DefP{} -> TerM VarSet -> TerM VarSet
forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
none
    where none :: p -> m a
none p
_ = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
forall a. Monoid a => a
mempty

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

instance UsableSizeVars MaskedDeBruijnPatterns where
  usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet
usableSizeVars MaskedDeBruijnPatterns
ps =
    case MaskedDeBruijnPatterns
ps of
      []                          -> VarSet -> TerM VarSet
forall a. a -> TerM a
forall (m :: * -> *) a. Monad m => a -> m a
return VarSet
forall a. Monoid a => a
mempty
      (Masked Bool
_ (ProjP ProjOrigin
_ QName
q) : MaskedDeBruijnPatterns
ps) -> QName -> TerM VarSet -> TerM VarSet
forall a. QName -> TerM a -> TerM a
projUseSizeLt QName
q (TerM VarSet -> TerM VarSet) -> TerM VarSet -> TerM VarSet
forall a b. (a -> b) -> a -> b
$ MaskedDeBruijnPatterns -> TerM VarSet
forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars MaskedDeBruijnPatterns
ps
      (Masked DeBruijnPattern
p                    : MaskedDeBruijnPatterns
ps) -> VarSet -> VarSet -> VarSet
forall a. Monoid a => a -> a -> a
mappend (VarSet -> VarSet -> VarSet)
-> TerM VarSet -> TerM (VarSet -> VarSet)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Masked DeBruijnPattern -> TerM VarSet
forall a. UsableSizeVars a => a -> TerM VarSet
usableSizeVars Masked DeBruijnPattern
p TerM (VarSet -> VarSet) -> TerM VarSet -> TerM VarSet
forall a b. TerM (a -> b) -> TerM a -> TerM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MaskedDeBruijnPatterns -> TerM VarSet
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
(Masked a -> Masked a -> Bool)
-> (Masked a -> Masked a -> Bool) -> Eq (Masked a)
forall a. Eq a => Masked a -> Masked a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Masked a -> Masked a -> Bool
Eq, Eq (Masked a)
Eq (Masked a) =>
(Masked a -> Masked a -> Ordering)
-> (Masked a -> Masked a -> Bool)
-> (Masked a -> Masked a -> Bool)
-> (Masked a -> Masked a -> Bool)
-> (Masked a -> Masked a -> Bool)
-> (Masked a -> Masked a -> Masked a)
-> (Masked a -> Masked a -> Masked a)
-> Ord (Masked a)
Masked a -> Masked a -> Bool
Masked a -> Masked a -> Ordering
Masked a -> Masked a -> Masked a
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
$ccompare :: forall a. Ord a => Masked a -> Masked a -> Ordering
compare :: Masked a -> Masked a -> Ordering
$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
>= :: Masked a -> Masked a -> Bool
$cmax :: forall a. Ord a => Masked a -> Masked a -> Masked a
max :: Masked a -> Masked a -> Masked a
$cmin :: forall a. Ord a => Masked a -> Masked a -> Masked a
min :: Masked a -> Masked a -> Masked a
Ord, Int -> Masked a -> ShowS
[Masked a] -> ShowS
Masked a -> String
(Int -> Masked a -> ShowS)
-> (Masked a -> String) -> ([Masked a] -> ShowS) -> Show (Masked a)
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
$cshowsPrec :: forall a. Show a => Int -> Masked a -> ShowS
showsPrec :: Int -> Masked a -> ShowS
$cshow :: forall a. Show a => Masked a -> String
show :: Masked a -> String
$cshowList :: forall a. Show a => [Masked a] -> ShowS
showList :: [Masked a] -> ShowS
Show, (forall a b. (a -> b) -> Masked a -> Masked b)
-> (forall a b. a -> Masked b -> Masked a) -> Functor Masked
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
$cfmap :: forall a b. (a -> b) -> Masked a -> Masked b
fmap :: forall a b. (a -> b) -> Masked a -> Masked b
$c<$ :: forall a b. a -> Masked b -> Masked a
<$ :: forall a b. a -> Masked b -> Masked a
Functor, (forall m. Monoid m => Masked m -> m)
-> (forall m a. Monoid m => (a -> m) -> Masked a -> m)
-> (forall m a. Monoid m => (a -> m) -> Masked a -> m)
-> (forall a b. (a -> b -> b) -> b -> Masked a -> b)
-> (forall a b. (a -> b -> b) -> b -> Masked a -> b)
-> (forall b a. (b -> a -> b) -> b -> Masked a -> b)
-> (forall b a. (b -> a -> b) -> b -> Masked a -> b)
-> (forall a. (a -> a -> a) -> Masked a -> a)
-> (forall a. (a -> a -> a) -> Masked a -> a)
-> (forall a. Masked a -> [a])
-> (forall a. Masked a -> Bool)
-> (forall a. Masked a -> Int)
-> (forall a. Eq a => a -> Masked a -> Bool)
-> (forall a. Ord a => Masked a -> a)
-> (forall a. Ord a => Masked a -> a)
-> (forall a. Num a => Masked a -> a)
-> (forall a. Num a => Masked a -> a)
-> Foldable Masked
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
$cfold :: forall m. Monoid m => Masked m -> m
fold :: forall m. Monoid m => Masked m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Masked a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Masked a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Masked a -> a
foldr1 :: forall a. (a -> a -> a) -> Masked a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Masked a -> a
foldl1 :: forall a. (a -> a -> a) -> Masked a -> a
$ctoList :: forall a. Masked a -> [a]
toList :: forall a. Masked a -> [a]
$cnull :: forall a. Masked a -> Bool
null :: forall a. Masked a -> Bool
$clength :: forall a. Masked a -> Int
length :: forall a. Masked a -> Int
$celem :: forall a. Eq a => a -> Masked a -> Bool
elem :: forall a. Eq a => a -> Masked a -> Bool
$cmaximum :: forall a. Ord a => Masked a -> a
maximum :: forall a. Ord a => Masked a -> a
$cminimum :: forall a. Ord a => Masked a -> a
minimum :: forall a. Ord a => Masked a -> a
$csum :: forall a. Num a => Masked a -> a
sum :: forall a. Num a => Masked a -> a
$cproduct :: forall a. Num a => Masked a -> a
product :: forall a. Num a => Masked a -> a
Foldable, Functor Masked
Foldable Masked
(Functor Masked, Foldable Masked) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Masked a -> f (Masked b))
-> (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 (m :: * -> *) a.
    Monad m =>
    Masked (m a) -> m (Masked a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Masked a -> f (Masked b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Masked a -> f (Masked b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Masked (f a) -> f (Masked a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Masked (f a) -> f (Masked a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Masked a -> m (Masked b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Masked a -> m (Masked b)
$csequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
sequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
Traversable)

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

notMasked :: a -> Masked a
notMasked :: forall a. a -> Masked a
notMasked = Bool -> a -> Masked a
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) = Bool -> b -> Masked b
forall a. Bool -> a -> Masked a
Masked Bool
m (b -> Masked b) -> m b -> m (Masked b)
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) = Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
m (m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> (m Doc -> m Doc) -> m Doc -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). 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
(Int -> CallPath -> ShowS)
-> (CallPath -> String) -> ([CallPath] -> ShowS) -> Show CallPath
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CallPath -> ShowS
showsPrec :: Int -> CallPath -> ShowS
$cshow :: CallPath -> String
show :: CallPath -> String
$cshowList :: [CallPath] -> ShowS
showList :: [CallPath] -> ShowS
Show, NonEmpty CallPath -> CallPath
CallPath -> CallPath -> CallPath
(CallPath -> CallPath -> CallPath)
-> (NonEmpty CallPath -> CallPath)
-> (forall b. Integral b => b -> CallPath -> CallPath)
-> Semigroup 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
$c<> :: CallPath -> CallPath -> CallPath
<> :: CallPath -> CallPath -> CallPath
$csconcat :: NonEmpty CallPath -> CallPath
sconcat :: NonEmpty CallPath -> CallPath
$cstimes :: forall b. Integral b => b -> CallPath -> CallPath
stimes :: forall b. Integral b => b -> CallPath -> CallPath
Semigroup, Semigroup CallPath
CallPath
Semigroup CallPath =>
CallPath
-> (CallPath -> CallPath -> CallPath)
-> ([CallPath] -> CallPath)
-> Monoid CallPath
[CallPath] -> CallPath
CallPath -> CallPath -> CallPath
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: CallPath
mempty :: CallPath
$cmappend :: CallPath -> CallPath -> CallPath
mappend :: CallPath -> CallPath -> CallPath
$cmconcat :: [CallPath] -> CallPath
mconcat :: [CallPath] -> CallPath
Monoid)

-- | The calls making up the call path.

callInfos :: CallPath -> [CallInfo]
callInfos :: CallPath -> [CallInfo]
callInfos (CallPath DList CallInfo
cs) = DList CallInfo -> [CallInfo]
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 [CallInfo] -> Bool
forall a. Null a => a -> Bool
null [CallInfo]
cis then Doc
forall a. Null a => a
empty else
    [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hsep ((CallInfo -> Doc) -> [CallInfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ CallInfo
ci -> Doc
arrow Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> CallInfo -> Doc
forall a. Pretty a => a -> Doc
P.pretty CallInfo
ci) [CallInfo]
cis) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
arrow
    where
      cis :: [CallInfo]
cis   = [CallInfo] -> [CallInfo]
forall a. HasCallStack => [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 = [Dom (String, Type)] -> TerM a -> TerM a
forall a. [Dom (String, Type)] -> TerM a -> TerM a
forall b a. TerSetSizeDepth b => b -> TerM a -> TerM a
terSetSizeDepth ([Dom (String, Type)] -> TerM a -> TerM a)
-> (Telescope -> [Dom (String, Type)])
-> Telescope
-> TerM a
-> TerM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Dom (String, Type)]
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 <- TCM Int -> TerM Int
forall a. TCM a -> TerM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Int -> TerM Int) -> TCM Int -> TerM Int
forall a b. (a -> b) -> a -> b
$ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> TCMT IO [Int] -> TCM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      [Dom (String, Type)]
-> (Dom (String, Type) -> TCM Int) -> TCMT IO [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Dom (String, Type)]
doms ((Dom (String, Type) -> TCM Int) -> TCMT IO [Int])
-> (Dom (String, Type) -> TCM Int) -> TCMT IO [Int]
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 <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type) -> (String, Type) -> Type
forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
unDom Dom (String, Type)
dom
        TCM Bool -> TCM Int -> TCM Int -> TCM Int
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType Type
a) (Int -> TCM Int
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1) {- else -} (TCM Int -> TCM Int) -> TCM Int -> TCM Int
forall a b. (a -> b) -> a -> b
$
          case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
            MetaV{} -> Int -> TCM Int
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
            Term
_       -> Int -> TCM Int
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
    (TerEnv -> TerEnv) -> TerM a -> TerM a
forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal (Lens' TerEnv Int -> LensSet TerEnv Int
forall o i. Lens' o i -> LensSet o i
set (Int -> f Int) -> TerEnv -> f TerEnv
Lens' TerEnv Int
terSizeDepth Int
n) TerM a
cont