{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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 Mikan.Termination.Monad where

import Prelude hiding (null, zip, zipWith)

import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Except   ( MonadError(..) )

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

import Mikan.Interaction.Options ( optTerminationDepth )

import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty ( Pretty, prettyShow )
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Internal
import Mikan.Syntax.Literal          ( Literal(LitString) )

import Mikan.Termination.CallMatrix ( CallMatrix, CallMatrix'(CallMatrix), CallMatrixAug(CallMatrixAug), CMSet )
import Mikan.Termination.CallMatrix qualified as CallMatrix
import Mikan.Termination.CallGraph  ( CallGraph, callMatrixSet )
import Mikan.Termination.CallGraph  qualified as CallGraph
import Mikan.Termination.CutOff     ( CutOff, defaultCutOff )
import Mikan.Termination.Order      ( Order, le, unknown )
import Mikan.Termination.RecCheck   ( MutualNames, anyDefs )

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Monad.Benchmark
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.Substitute

import Mikan.Utils.Benchmark as B
import Mikan.Utils.Functor
import Mikan.Utils.List
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Monoid
import Mikan.Utils.Null
import Mikan.Utils.Zip     () -- for zip, zipWith instance
import Mikan.Utils.StrictReader

import Mikan.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 -> 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
terMaskResult :: !Bool
    -- ^ Only consider guardedness if 'False' (not masked).
  , TerEnv -> [DeBruijnPattern]
terPatterns :: [DeBruijnPattern]
    -- ^ 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.
  }

-- | 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
  { 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
  , terMaskResult :: Bool
terMaskResult               = Bool
False          -- use result (do not mask)
  , terPatterns :: [DeBruijnPattern]
terPatterns                 = [DeBruijnPattern]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- needs to be set!
  , terPatternsRaise :: Int
terPatternsRaise            = Int
0
  , terGuarded :: Guarded
terGuarded                  = Guarded
le -- not initially guarded
  }

-- | 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
           , MonadError TCErr
           , ReadTCState TerM
String -> Word64 -> TerM ()
ReadTCState TerM =>
(String -> Word64 -> TerM ())
-> (String -> Word64 -> TerM ()) -> MonadStatistics TerM
forall (m :: * -> *).
ReadTCState m =>
(String -> Word64 -> m ())
-> (String -> Word64 -> m ()) -> MonadStatistics m
$ctickN :: String -> Word64 -> TerM ()
tickN :: String -> Word64 -> TerM ()
$ctickMax :: String -> Word64 -> TerM ()
tickMax :: String -> Word64 -> TerM ()
MonadStatistics
           , Monad TerM
Functor TerM
Applicative TerM
TerM CommandLineOptions
TerM PragmaOptions
(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
           , Monad TerM
Functor TerM
Applicative TerM
(Functor TerM, Applicative TerM, Monad TerM) =>
(SomeBuiltin -> TerM (Maybe (Builtin PrimFun))) -> HasBuiltins TerM
SomeBuiltin -> TerM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
(Functor m, Applicative m, Monad 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 Doc)
-> (forall a. String -> Int -> Doc -> 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 Doc
forall a. String -> Int -> String -> TerM a -> TerM a
forall a. String -> Int -> Doc -> TerM a -> TerM a
forall a. TerM a -> TerM a
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(String -> Int -> TCM Doc -> m Doc)
-> (forall a. String -> Int -> Doc -> 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 Doc
formatDebugMessage :: String -> Int -> TCM Doc -> TerM Doc
$ctraceDebugMessage :: forall a. String -> Int -> Doc -> TerM a -> TerM a
traceDebugMessage :: forall a. String -> Int -> Doc -> 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
           , Monad TerM
Monad TerM =>
(HasCallStack => FileId -> TerM File)
-> (File -> TerM FileId) -> MonadFileId TerM
HasCallStack => FileId -> TerM File
File -> TerM FileId
forall (m :: * -> *).
Monad m =>
(HasCallStack => FileId -> m File)
-> (File -> m FileId) -> MonadFileId m
$cfileFromId :: HasCallStack => FileId -> TerM File
fileFromId :: HasCallStack => FileId -> TerM File
$cidFromFile :: File -> TerM FileId
idFromFile :: File -> TerM FileId
MonadFileId
           , Functor TerM
Applicative TerM
HasOptions TerM
MonadDebug TerM
MonadTCEnv TerM
(Functor TerM, Applicative TerM, HasOptions TerM, MonadDebug TerM,
 MonadTCEnv TerM) =>
(HasCallStack => QName -> TerM Definition)
-> (HasCallStack => QName -> TerM (Either SigError Definition))
-> HasConstInfo TerM
HasCallStack => QName -> TerM (Either SigError Definition)
HasCallStack => QName -> TerM Definition
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadDebug m,
 MonadTCEnv m) =>
(HasCallStack => QName -> m Definition)
-> (HasCallStack => QName -> m (Either SigError Definition))
-> HasConstInfo m
$cgetConstInfo :: HasCallStack => QName -> TerM Definition
getConstInfo :: HasCallStack => QName -> TerM Definition
$cgetConstInfo' :: HasCallStack => QName -> TerM (Either SigError Definition)
getConstInfo' :: HasCallStack => QName -> TerM (Either SigError Definition)
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
MonadTCEnv TerM
MonadTCState 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 SessionState
TerM TCState
Monad TerM =>
TerM TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b)
-> TerM SessionState
-> (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)
-> m SessionState
-> (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
$cgetSessionState :: TerM SessionState
getSessionState :: TerM SessionState
$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.
    IsAxiom -> Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a)
-> (forall a.
    Substitution -> (Context -> Context) -> TerM a -> TerM a)
-> (forall a. Range -> ShortText -> (Name -> TerM a) -> TerM a)
-> MonadAddContext TerM
forall a. Range -> ShortText -> (Name -> TerM a) -> TerM a
forall a. Name -> Dom Type -> TerM a -> TerM a
forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a
forall (m :: * -> *).
MonadTCEnv m =>
(forall a. Name -> Dom Type -> m a -> m a)
-> (forall a.
    IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> ShortText -> (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.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a
addLetBinding' :: forall a.
IsAxiom -> 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 -> ShortText -> (Name -> TerM a) -> TerM a
withFreshName :: forall a. Range -> ShortText -> (Name -> TerM a) -> TerM a
MonadAddContext
           , MonadFileId TerM
MonadDebug TerM
MonadReduce TerM
MonadTCEnv TerM
ReadTCState TerM
HasConstInfo TerM
MonadAddContext TerM
HasBuiltins TerM
(HasBuiltins TerM, HasConstInfo TerM, MonadAddContext TerM,
 MonadDebug TerM, MonadFileId TerM, MonadReduce TerM,
 MonadTCEnv TerM, ReadTCState TerM) =>
PureTCM TerM
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
 MonadFileId 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 <- 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

  let tenv = TerEnv
defaultTerEnv
        { terCutOff                   = cutoff
        }

  runTer tenv 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 (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.

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 }

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 }

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 [DeBruijnPattern]
terGetPatterns :: TerM [DeBruijnPattern]
terGetPatterns = do
  n   <- (TerEnv -> Int) -> TerM Int
forall a. (TerEnv -> a) -> TerM a
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Int
terPatternsRaise
  mps <- terAsks terPatterns
  return $ if n == 0 then mps else map' (raise n) mps

terSetPatterns :: [DeBruijnPattern] -> TerM a -> TerM a
terSetPatterns :: forall a. [DeBruijnPattern] -> TerM a -> TerM a
terSetPatterns [DeBruijnPattern]
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

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
  b <- QName -> TCM Bool
forall {m :: * -> *}. HasConstInfo m => QName -> m Bool
isProjectionButNotCoinductive' QName
qn
  reportSDoc "term.proj" 60 $ do
    "identifier" <+> prettyTCM qn <+> do
      text $
        if b then "is an inductive projection"
          else "is either not a projection or coinductive"
  return b
  where
    isProjectionButNotCoinductive' :: QName -> m Bool
isProjectionButNotCoinductive' QName
qn = do
      mp <- QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
qn
      case mp of
        Just Projection{ projProper :: Projection -> Maybe QName
projProper = Just{}, projFromType :: Projection -> Arg QName
projFromType = Arg QName
t }
          -> QName -> m Bool
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isInductiveRecord (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
t)
        Maybe Projection
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Is the given elimination anything but a coinductive projection?
elimNotCoinductive :: MonadTCM tcm => Elim' t -> tcm Bool
elimNotCoinductive :: forall (tcm :: * -> *) t. MonadTCM tcm => Elim' t -> tcm Bool
elimNotCoinductive Elim' t
e = case Elim' t -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elim' t
e of
  Maybe (ProjOrigin, QName)
Nothing      -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  Just (ProjOrigin
_o, QName
x) -> QName -> tcm Bool
forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive QName
x

-- | 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
  pdef <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q
  case isProjectionDefinition 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 RecordData)
-> TCM Bool -> (RecordData -> 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 RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r) TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ ((RecordData -> TCM Bool) -> TCM Bool)
-> (RecordData -> TCM Bool) -> TCM Bool
forall a b. (a -> b) -> a -> b
$ \ RecordData
rdef -> do
        -- no for inductive or non-recursive record
        if RecordData -> Maybe Induction
_recInduction RecordData
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 RecordData -> Bool
notSafeRecRecursive RecordData
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 (ShortText, Type)]
pars, [Dom (ShortText, Type)]
tel') = Int
-> [Dom (ShortText, Type)]
-> ([Dom (ShortText, Type)], [Dom (ShortText, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
n ([Dom (ShortText, Type)]
 -> ([Dom (ShortText, Type)], [Dom (ShortText, Type)]))
-> [Dom (ShortText, Type)]
-> ([Dom (ShortText, Type)], [Dom (ShortText, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (ShortText, Type)]
forall t. Tele (Dom t) -> [Dom (ShortText, 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
$ RecordData -> Maybe [QName]
_recMutual RecordData
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 (ShortText, Type)] -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
[Dom (ShortText, Type)] -> m a -> m a
addContext [Dom (ShortText, 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 (ShortText, Type)] -> Telescope
telFromList [Dom (ShortText, 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when ([QName] -> Bool
forall a. Null a => a -> Bool
null [QName]
mut) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
              names <- MutualNames -> ([Type], Type) -> TCM MutualNames
forall a. GetDefs a => MutualNames -> a -> TCM MutualNames
anyDefs ([QName] -> MutualNames
forall a. Ord a => [a] -> Set a
Set.fromList [QName]
mut) ((Dom (ShortText, Type) -> Type)
-> [Dom (ShortText, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map' ((ShortText, Type) -> Type
forall a b. (a, b) -> b
snd ((ShortText, Type) -> Type)
-> (Dom (ShortText, Type) -> (ShortText, Type))
-> Dom (ShortText, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ShortText, Type) -> (ShortText, Type)
forall t e. Dom' t e -> e
unDom) [Dom (ShortText, Type)]
tel', Type
core)
              reportSDoc "term.guardedness" 40 $
                "found" <+> if null names then "none" else sep (map' prettyTCM $ Set.toList names)
              return $ not $ null 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 : Type 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.
  notSafeRecRecursive :: RecordData -> Bool
  notSafeRecRecursive :: RecordData -> Bool
notSafeRecRecursive = Bool -> ([QName] -> Bool) -> Maybe [QName] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True [QName] -> Bool
forall a. Null a => a -> Bool
null (Maybe [QName] -> Bool)
-> (RecordData -> Maybe [QName]) -> RecordData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordData -> Maybe [QName]
_recMutual
    -- @_recMutual@ should be something (@Just (_:_)@) to be safe

-- * 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 (ShortText -> Literal
LitString ShortText
"term.unused.pat.var")

-- * Call paths
---------------------------------------------------------------------------

-- | 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.

data CallPath = CallPath
  { CallPath -> QName
callPathStart :: QName
  , CallPath -> DList CallInfo
callPathSteps :: 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)

-- | The calls making up the call path.

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

instance Semigroup CallPath where
  CallPath QName
start DList CallInfo
steps <> :: CallPath -> CallPath -> CallPath
<> CallPath QName
_ DList CallInfo
steps' = QName -> DList CallInfo -> CallPath
CallPath QName
start (DList CallInfo
steps DList CallInfo -> DList CallInfo -> DList CallInfo
forall a. Semigroup a => a -> a -> a
<> DList CallInfo
steps')

instance Monoid CallPath where
  mempty :: CallPath
mempty = QName -> DList CallInfo -> CallPath
CallPath QName
forall a. Null a => a
empty DList CallInfo
forall a. Monoid a => a
mempty

-- | 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
"-->"

-- * PrettyTCM
---------------------------------------------------------------------------
--
-- This mostly duplicates the 'Pretty' instances,
-- but we use 'PrettyTCM' for the 'QName' in the 'CallPath'.

-- This conflicts with an existing instance in TypeChecking.Pretty
-- -- | We only print the name of the callee, omitting the actual call term.
-- instance PrettyTCM CallInfo where
--   prettyTCM (CallInfo target _term) = prettyTCM target

-- | Show all nodes.
instance PrettyTCM CallPath where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => CallPath -> m Doc
prettyTCM CallPath
cp = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
    QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (CallPath -> QName
callPathStart CallPath
cp) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
    (CallInfo -> m Doc) -> [CallInfo] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (\ (CallInfo QName
g Closure Term
_) -> m Doc
"-->" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
g) (CallPath -> [CallInfo]
callInfos CallPath
cp)

instance PrettyTCM CallMatrix where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => CallMatrix -> m Doc
prettyTCM (CallMatrix Matrix Int Guarded
m) = Matrix Int Guarded -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Matrix Int Guarded
m

instance PrettyTCM cinfo => PrettyTCM (CallMatrixAug cinfo) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => CallMatrixAug cinfo -> m Doc
prettyTCM (CallMatrixAug CallMatrix
m cinfo
cinfo) = cinfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => cinfo -> m Doc
prettyTCM cinfo
cinfo m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ CallMatrix -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CallMatrix -> m Doc
prettyTCM CallMatrix
m)

instance PrettyTCM cinfo => PrettyTCM (CMSet cinfo) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => CMSet cinfo -> m Doc
prettyTCM = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc)
-> (CMSet cinfo -> [m Doc]) -> CMSet cinfo -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"\n" ([m Doc] -> [m Doc])
-> (CMSet cinfo -> [m Doc]) -> CMSet cinfo -> [m Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallMatrixAug cinfo -> m Doc) -> [CallMatrixAug cinfo] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map' CallMatrixAug cinfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CallMatrixAug cinfo -> m Doc
prettyTCM ([CallMatrixAug cinfo] -> [m Doc])
-> (CMSet cinfo -> [CallMatrixAug cinfo]) -> CMSet cinfo -> [m Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CMSet cinfo -> [CallMatrixAug cinfo]
forall cinfo. CMSet cinfo -> [CallMatrixAug cinfo]
CallMatrix.toList

instance PrettyTCM cinfo => PrettyTCM (CallGraph.Call cinfo) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Call cinfo -> m Doc
prettyTCM = CMSet cinfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CMSet cinfo -> m Doc
prettyTCM (CMSet cinfo -> m Doc)
-> (Call cinfo -> CMSet cinfo) -> Call cinfo -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Call cinfo -> CMSet cinfo
forall cinfo. Call cinfo -> CMSet cinfo
callMatrixSet

instance PrettyTCM cinfo => PrettyTCM (CallGraph cinfo) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => CallGraph cinfo -> m Doc
prettyTCM = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc)
-> (CallGraph cinfo -> [m Doc]) -> CallGraph cinfo -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Call cinfo -> m Doc) -> [Call cinfo] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map' Call cinfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Call cinfo -> m Doc
prettyTCM ([Call cinfo] -> [m Doc])
-> (CallGraph cinfo -> [Call cinfo]) -> CallGraph cinfo -> [m Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> [Call cinfo]
forall cinfo. CallGraph cinfo -> [Call cinfo]
CallGraph.toList