{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Termination.Monad where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import qualified Control.Monad.Fail as Fail
import Control.Monad.Reader
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.Monoid ( Monoid(..) )
import Data.Semigroup ( Semigroup(..) )
import qualified Data.Set as Set
import Agda.Interaction.Options
import Agda.Syntax.Abstract (AllNames)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Literal
import Agda.Syntax.Position (noRange)
import Agda.Termination.CutOff
import Agda.Termination.Order (Order,le,unknown)
import Agda.Termination.RecCheck (anyDefs)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Benchmark
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.Utils.Except ( MonadError )
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List ( hasElem )
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Monoid
import Agda.Utils.Null
import Agda.Utils.Pretty (Pretty, prettyShow)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.Impossible
type MutualNames = [QName]
type Target = QName
type Guarded = Order
data TerEnv = TerEnv
{ TerEnv -> Bool
terUseDotPatterns :: Bool
, TerEnv -> Maybe QName
terSizeSuc :: Maybe QName
, TerEnv -> Maybe QName
terSharp :: Maybe QName
, TerEnv -> CutOff
terCutOff :: CutOff
, TerEnv -> QName
terCurrent :: QName
, TerEnv -> MutualNames
terMutual :: MutualNames
, TerEnv -> MutualNames
terUserNames :: [QName]
, TerEnv -> Bool
terHaveInlinedWith :: Bool
, TerEnv -> Maybe QName
terTarget :: Maybe Target
, TerEnv -> Delayed
terDelayed :: Delayed
, TerEnv -> [Bool]
terMaskArgs :: [Bool]
, TerEnv -> Bool
terMaskResult :: Bool
, TerEnv -> Int
_terSizeDepth :: Int
, TerEnv -> MaskedDeBruijnPatterns
terPatterns :: MaskedDeBruijnPatterns
, TerEnv -> Int
terPatternsRaise :: !Int
, TerEnv -> Guarded
terGuarded :: !Guarded
, TerEnv -> Bool
terUseSizeLt :: Bool
, TerEnv -> VarSet
terUsableVars :: VarSet
}
defaultTerEnv :: TerEnv
defaultTerEnv :: TerEnv
defaultTerEnv = $WTerEnv :: Bool
-> Maybe QName
-> Maybe QName
-> CutOff
-> QName
-> MutualNames
-> MutualNames
-> Bool
-> Maybe QName
-> Delayed
-> [Bool]
-> Bool
-> Int
-> MaskedDeBruijnPatterns
-> Int
-> Guarded
-> Bool
-> VarSet
-> TerEnv
TerEnv
{ terUseDotPatterns :: Bool
terUseDotPatterns = Bool
False
, 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__
, terMutual :: MutualNames
terMutual = MutualNames
forall a. HasCallStack => a
__IMPOSSIBLE__
, terCurrent :: QName
terCurrent = QName
forall a. HasCallStack => a
__IMPOSSIBLE__
, terHaveInlinedWith :: Bool
terHaveInlinedWith = Bool
False
, terTarget :: Maybe QName
terTarget = Maybe QName
forall a. Maybe a
Nothing
, terDelayed :: Delayed
terDelayed = Delayed
NotDelayed
, terMaskArgs :: [Bool]
terMaskArgs = Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False
, terMaskResult :: Bool
terMaskResult = Bool
False
, _terSizeDepth :: Int
_terSizeDepth = Int
forall a. HasCallStack => a
__IMPOSSIBLE__
, terPatterns :: MaskedDeBruijnPatterns
terPatterns = MaskedDeBruijnPatterns
forall a. HasCallStack => a
__IMPOSSIBLE__
, terPatternsRaise :: Int
terPatternsRaise = 0
, terGuarded :: Guarded
terGuarded = Guarded
le
, terUseSizeLt :: Bool
terUseSizeLt = Bool
False
, terUsableVars :: VarSet
terUsableVars = VarSet
VarSet.empty
}
class (Functor m, Monad m) => MonadTer m where
terAsk :: m TerEnv
terLocal :: (TerEnv -> TerEnv) -> m a -> m a
terAsks :: (TerEnv -> a) -> m a
terAsks f :: 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
newtype TerM a = TerM { TerM a -> ReaderT TerEnv TCM a
terM :: ReaderT TerEnv TCM a }
deriving ( a -> TerM b -> TerM a
(a -> b) -> TerM a -> TerM b
(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
<$ :: a -> TerM b -> TerM a
$c<$ :: forall a b. a -> TerM b -> TerM a
fmap :: (a -> b) -> TerM a -> TerM b
$cfmap :: forall a b. (a -> b) -> TerM a -> TerM b
Functor
, Functor TerM
a -> TerM a
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
TerM a -> TerM b -> TerM b
TerM a -> TerM b -> TerM a
TerM (a -> b) -> TerM a -> TerM b
(a -> b -> c) -> TerM a -> TerM b -> TerM c
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
<* :: TerM a -> TerM b -> TerM a
$c<* :: forall a b. TerM a -> TerM b -> TerM a
*> :: TerM a -> TerM b -> TerM b
$c*> :: forall a b. TerM a -> TerM b -> TerM b
liftA2 :: (a -> b -> c) -> TerM a -> TerM b -> TerM c
$cliftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
<*> :: TerM (a -> b) -> TerM a -> TerM b
$c<*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
pure :: a -> TerM a
$cpure :: forall a. a -> TerM a
$cp1Applicative :: Functor TerM
Applicative
, Applicative TerM
a -> TerM a
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
TerM a -> (a -> TerM b) -> TerM b
TerM a -> TerM b -> TerM b
forall a. a -> TerM a
forall a b. TerM a -> TerM b -> TerM b
forall a b. TerM a -> (a -> TerM b) -> TerM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> TerM a
$creturn :: forall a. a -> TerM a
>> :: TerM a -> TerM b -> TerM b
$c>> :: forall a b. TerM a -> TerM b -> TerM b
>>= :: TerM a -> (a -> TerM b) -> TerM b
$c>>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
$cp1Monad :: Applicative TerM
Monad
, Monad TerM
Monad TerM => (forall a. String -> TerM a) -> MonadFail TerM
String -> TerM a
forall a. String -> TerM a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
fail :: String -> TerM a
$cfail :: forall a. String -> TerM a
$cp1MonadFail :: Monad TerM
Fail.MonadFail
, MonadError TCErr
, MonadBench Phase
, ReadTCState TerM
String -> (Integer -> Integer) -> TerM ()
ReadTCState TerM =>
(String -> (Integer -> Integer) -> TerM ()) -> MonadStatistics TerM
forall (m :: * -> *).
ReadTCState m =>
(String -> (Integer -> Integer) -> m ()) -> MonadStatistics m
modifyCounter :: String -> (Integer -> Integer) -> TerM ()
$cmodifyCounter :: String -> (Integer -> Integer) -> TerM ()
$cp1MonadStatistics :: ReadTCState 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
commandLineOptions :: TerM CommandLineOptions
$ccommandLineOptions :: TerM CommandLineOptions
pragmaOptions :: TerM PragmaOptions
$cpragmaOptions :: TerM PragmaOptions
$cp3HasOptions :: Monad TerM
$cp2HasOptions :: Applicative TerM
$cp1HasOptions :: Functor TerM
HasOptions
, Functor TerM
MonadFail TerM
Applicative TerM
(Functor TerM, Applicative TerM, MonadFail TerM) =>
(String -> TerM (Maybe (Builtin PrimFun))) -> HasBuiltins TerM
String -> TerM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
(Functor m, Applicative m, MonadFail m) =>
(String -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
getBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun))
$cgetBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun))
$cp3HasBuiltins :: MonadFail TerM
$cp2HasBuiltins :: Applicative TerM
$cp1HasBuiltins :: Functor TerM
HasBuiltins
, Monad TerM
Functor TerM
Applicative TerM
TerM Bool
TerM Verbosity
(Functor TerM, Applicative TerM, Monad TerM) =>
(String -> Int -> String -> TerM ())
-> (forall a. String -> Int -> String -> TerM a -> TerM a)
-> (String -> Int -> TCM Doc -> TerM String)
-> TerM Verbosity
-> TerM Bool
-> (forall a. TerM a -> TerM a)
-> (forall a. String -> Int -> String -> TerM a -> TerM a)
-> MonadDebug TerM
String -> Int -> String -> TerM ()
String -> Int -> String -> TerM a -> TerM a
String -> Int -> String -> TerM a -> TerM a
String -> Int -> TCM Doc -> TerM String
TerM a -> TerM a
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 -> String -> m ())
-> (forall a. String -> Int -> String -> m a -> m a)
-> (String -> Int -> TCM Doc -> m String)
-> m Verbosity
-> m Bool
-> (forall a. m a -> m a)
-> (forall a. String -> Int -> String -> m a -> m a)
-> MonadDebug m
verboseBracket :: String -> Int -> String -> TerM a -> TerM a
$cverboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
nowDebugPrinting :: TerM a -> TerM a
$cnowDebugPrinting :: forall a. TerM a -> TerM a
isDebugPrinting :: TerM Bool
$cisDebugPrinting :: TerM Bool
getVerbosity :: TerM Verbosity
$cgetVerbosity :: TerM Verbosity
formatDebugMessage :: String -> Int -> TCM Doc -> TerM String
$cformatDebugMessage :: String -> Int -> TCM Doc -> TerM String
traceDebugMessage :: String -> Int -> String -> TerM a -> TerM a
$ctraceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
displayDebugMessage :: String -> Int -> String -> TerM ()
$cdisplayDebugMessage :: String -> Int -> String -> TerM ()
$cp3MonadDebug :: Monad TerM
$cp2MonadDebug :: Applicative TerM
$cp1MonadDebug :: Functor TerM
MonadDebug
, Functor TerM
MonadFail TerM
Applicative TerM
MonadTCEnv TerM
HasOptions TerM
MonadDebug 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
getRewriteRulesFor :: QName -> TerM RewriteRules
$cgetRewriteRulesFor :: QName -> TerM RewriteRules
getConstInfo' :: QName -> TerM (Either SigError Definition)
$cgetConstInfo' :: QName -> TerM (Either SigError Definition)
getConstInfo :: QName -> TerM Definition
$cgetConstInfo :: QName -> TerM Definition
$cp6HasConstInfo :: MonadTCEnv TerM
$cp5HasConstInfo :: MonadDebug TerM
$cp4HasConstInfo :: HasOptions TerM
$cp3HasConstInfo :: MonadFail TerM
$cp2HasConstInfo :: Applicative TerM
$cp1HasConstInfo :: Functor TerM
HasConstInfo
, Monad TerM
Monad TerM => (forall a. IO a -> TerM a) -> MonadIO TerM
IO a -> TerM a
forall a. IO a -> TerM a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> TerM a
$cliftIO :: forall a. IO a -> TerM a
$cp1MonadIO :: Monad TerM
MonadIO
, Monad TerM
TerM TCEnv
Monad TerM =>
TerM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a)
-> MonadTCEnv TerM
(TCEnv -> TCEnv) -> TerM a -> TerM a
forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
forall (m :: * -> *).
Monad m =>
m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
askTC :: TerM TCEnv
$caskTC :: TerM TCEnv
$cp1MonadTCEnv :: Monad TerM
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
modifyTC :: (TCState -> TCState) -> TerM ()
$cmodifyTC :: (TCState -> TCState) -> TerM ()
putTC :: TCState -> TerM ()
$cputTC :: TCState -> TerM ()
getTC :: TerM TCState
$cgetTC :: TerM TCState
$cp1MonadTCState :: Monad TerM
MonadTCState
, Applicative TerM
MonadIO TerM
MonadTCState TerM
MonadTCEnv TerM
HasOptions TerM
(Applicative TerM, MonadIO TerM, MonadTCEnv TerM,
MonadTCState TerM, HasOptions TerM) =>
(forall a. TCM a -> TerM a) -> MonadTCM TerM
TCM a -> TerM a
forall a. TCM a -> TerM a
forall (tcm :: * -> *).
(Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm,
HasOptions tcm) =>
(forall a. TCM a -> tcm a) -> MonadTCM tcm
liftTCM :: TCM a -> TerM a
$cliftTCM :: forall a. TCM a -> TerM a
$cp5MonadTCM :: HasOptions TerM
$cp4MonadTCM :: MonadTCState TerM
$cp3MonadTCM :: MonadTCEnv TerM
$cp2MonadTCM :: MonadIO TerM
$cp1MonadTCM :: Applicative TerM
MonadTCM
, Monad TerM
TerM TCState
Monad TerM =>
TerM TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b)
-> (forall a. (TCState -> TCState) -> TerM a -> TerM a)
-> ReadTCState TerM
(TCState -> TCState) -> TerM a -> TerM a
Lens' a TCState -> (a -> a) -> TerM b -> TerM b
forall a. (TCState -> TCState) -> TerM a -> TerM a
forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b
forall (m :: * -> *).
Monad m =>
m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
withTCState :: (TCState -> TCState) -> TerM a -> TerM a
$cwithTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
locallyTCState :: Lens' a TCState -> (a -> a) -> TerM b -> TerM b
$clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b
getTCState :: TerM TCState
$cgetTCState :: TerM TCState
$cp1ReadTCState :: Monad TerM
ReadTCState
, Applicative TerM
MonadTCEnv TerM
HasOptions TerM
ReadTCState TerM
(Applicative TerM, MonadTCEnv TerM, ReadTCState TerM,
HasOptions TerM) =>
(forall a. ReduceM a -> TerM a) -> MonadReduce TerM
ReduceM a -> TerM a
forall a. ReduceM a -> TerM a
forall (m :: * -> *).
(Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
(forall a. ReduceM a -> m a) -> MonadReduce m
liftReduce :: ReduceM a -> TerM a
$cliftReduce :: forall a. ReduceM a -> TerM a
$cp4MonadReduce :: HasOptions TerM
$cp3MonadReduce :: ReadTCState TerM
$cp2MonadReduce :: MonadTCEnv TerM
$cp1MonadReduce :: Applicative TerM
MonadReduce
, MonadTCEnv TerM
Range -> String -> (Name -> TerM a) -> TerM a
Name -> Term -> Dom Type -> TerM a -> TerM a
Name -> Dom Type -> TerM a -> TerM a
Substitution -> (Context -> Context) -> TerM a -> TerM a
MonadTCEnv TerM =>
(forall a. Name -> Dom Type -> TerM a -> TerM a)
-> (forall a. 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. Name -> Term -> Dom Type -> TerM a -> TerM a
forall a. Name -> Dom Type -> TerM a -> TerM a
forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
forall (m :: * -> *).
MonadTCEnv m =>
(forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
withFreshName :: Range -> String -> (Name -> TerM a) -> TerM a
$cwithFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
updateContext :: Substitution -> (Context -> Context) -> TerM a -> TerM a
$cupdateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
addLetBinding' :: Name -> Term -> Dom Type -> TerM a -> TerM a
$caddLetBinding' :: forall a. Name -> Term -> Dom Type -> TerM a -> TerM a
addCtx :: Name -> Dom Type -> TerM a -> TerM a
$caddCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
$cp1MonadAddContext :: MonadTCEnv TerM
MonadAddContext
)
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 :: (TerEnv -> TerEnv) -> TerM a -> TerM a
terLocal f :: 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 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
runTer :: TerEnv -> TerM a -> TCM a
runTer :: TerEnv -> TerM a -> TCM a
runTer tenv :: TerEnv
tenv (TerM m :: ReaderT TerEnv TCM a
m) = ReaderT TerEnv TCM a -> TerEnv -> TCM a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT TerEnv TCM a
m TerEnv
tenv
runTerDefault :: TerM a -> TCM a
runTerDefault :: TerM a -> TCM a
runTerDefault cont :: TerM a
cont = do
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
Maybe QName
suc <- TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
m (Maybe QName)
sizeSucName
Maybe QName
sharp <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
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 :: Maybe QName
terSizeSuc = Maybe QName
suc
, terSharp :: Maybe QName
terSharp = Maybe QName
sharp
, terCutOff :: CutOff
terCutOff = CutOff
cutoff
}
TerEnv -> TerM a -> TCM a
forall a. TerEnv -> TerM a -> TCM a
runTer TerEnv
tenv TerM a
cont
instance Semigroup m => Semigroup (TerM m) where
<> :: TerM m -> TerM m -> TerM m
(<>) = (m -> m -> m) -> TerM m -> TerM m -> TerM m
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 (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)
sequence
terGetUseDotPatterns :: TerM Bool
terGetUseDotPatterns :: TerM Bool
terGetUseDotPatterns = (TerEnv -> Bool) -> TerM Bool
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terUseDotPatterns
terSetUseDotPatterns :: Bool -> TerM a -> TerM a
terSetUseDotPatterns :: Bool -> TerM a -> TerM a
terSetUseDotPatterns b :: Bool
b = (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
$ \ e :: TerEnv
e -> TerEnv
e { terUseDotPatterns :: Bool
terUseDotPatterns = Bool
b }
terGetSizeSuc :: TerM (Maybe QName)
terGetSizeSuc :: TerM (Maybe QName)
terGetSizeSuc = (TerEnv -> Maybe QName) -> TerM (Maybe QName)
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 (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> QName
terCurrent
terSetCurrent :: QName -> TerM a -> TerM a
terSetCurrent :: QName -> TerM a -> TerM a
terSetCurrent q :: QName
q = (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
$ \ e :: TerEnv
e -> TerEnv
e { terCurrent :: QName
terCurrent = QName
q }
terGetSharp :: TerM (Maybe QName)
terGetSharp :: TerM (Maybe QName)
terGetSharp = (TerEnv -> Maybe QName) -> TerM (Maybe QName)
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 (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> CutOff
terCutOff
terGetMutual :: TerM MutualNames
terGetMutual :: TerM MutualNames
terGetMutual = (TerEnv -> MutualNames) -> TerM MutualNames
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> MutualNames
terMutual
terGetUserNames :: TerM [QName]
terGetUserNames :: TerM MutualNames
terGetUserNames = (TerEnv -> MutualNames) -> TerM MutualNames
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> MutualNames
terUserNames
terGetTarget :: TerM (Maybe Target)
terGetTarget :: TerM (Maybe QName)
terGetTarget = (TerEnv -> Maybe QName) -> TerM (Maybe QName)
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Maybe QName
terTarget
terSetTarget :: Maybe Target -> TerM a -> TerM a
terSetTarget :: Maybe QName -> TerM a -> TerM a
terSetTarget t :: Maybe QName
t = (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
$ \ e :: TerEnv
e -> TerEnv
e { terTarget :: Maybe QName
terTarget = Maybe QName
t }
terGetHaveInlinedWith :: TerM Bool
terGetHaveInlinedWith :: TerM Bool
terGetHaveInlinedWith = (TerEnv -> Bool) -> TerM Bool
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terHaveInlinedWith
terSetHaveInlinedWith :: TerM a -> TerM a
terSetHaveInlinedWith :: TerM a -> TerM a
terSetHaveInlinedWith = (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
$ \ e :: TerEnv
e -> TerEnv
e { terHaveInlinedWith :: Bool
terHaveInlinedWith = Bool
True }
terGetDelayed :: TerM Delayed
terGetDelayed :: TerM Delayed
terGetDelayed = (TerEnv -> Delayed) -> TerM Delayed
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Delayed
terDelayed
terSetDelayed :: Delayed -> TerM a -> TerM a
terSetDelayed :: Delayed -> TerM a -> TerM a
terSetDelayed b :: Delayed
b = (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
$ \ e :: TerEnv
e -> TerEnv
e { terDelayed :: Delayed
terDelayed = Delayed
b }
terGetMaskArgs :: TerM [Bool]
terGetMaskArgs :: TerM [Bool]
terGetMaskArgs = (TerEnv -> [Bool]) -> TerM [Bool]
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> [Bool]
terMaskArgs
terSetMaskArgs :: [Bool] -> TerM a -> TerM a
terSetMaskArgs :: [Bool] -> TerM a -> TerM a
terSetMaskArgs b :: [Bool]
b = (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
$ \ e :: TerEnv
e -> TerEnv
e { terMaskArgs :: [Bool]
terMaskArgs = [Bool]
b }
terGetMaskResult :: TerM Bool
terGetMaskResult :: TerM Bool
terGetMaskResult = (TerEnv -> Bool) -> TerM Bool
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terMaskResult
terSetMaskResult :: Bool -> TerM a -> TerM a
terSetMaskResult :: Bool -> TerM a -> TerM a
terSetMaskResult b :: Bool
b = (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
$ \ e :: TerEnv
e -> TerEnv
e { terMaskResult :: Bool
terMaskResult = Bool
b }
terGetPatterns :: TerM (MaskedDeBruijnPatterns)
terGetPatterns :: TerM MaskedDeBruijnPatterns
terGetPatterns = do
Int
n <- (TerEnv -> Int) -> TerM Int
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Int
terPatternsRaise
MaskedDeBruijnPatterns
mps <- (TerEnv -> MaskedDeBruijnPatterns) -> TerM MaskedDeBruijnPatterns
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> MaskedDeBruijnPatterns
terPatterns
MaskedDeBruijnPatterns -> TerM MaskedDeBruijnPatterns
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
== 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> DeBruijnPattern -> DeBruijnPattern
forall t a. Subst t a => Int -> a -> a
raise Int
n)) MaskedDeBruijnPatterns
mps
terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns ps :: MaskedDeBruijnPatterns
ps = (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
$ \ e :: TerEnv
e -> TerEnv
e { terPatterns :: MaskedDeBruijnPatterns
terPatterns = MaskedDeBruijnPatterns
ps }
terRaise :: TerM a -> TerM a
terRaise :: TerM a -> TerM a
terRaise = (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
$ \ e :: TerEnv
e -> TerEnv
e { terPatternsRaise :: Int
terPatternsRaise = TerEnv -> Int
terPatternsRaise TerEnv
e Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
terGetGuarded :: TerM Guarded
terGetGuarded :: TerM Guarded
terGetGuarded = (TerEnv -> Guarded) -> TerM Guarded
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Guarded
terGuarded
terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a
terModifyGuarded :: (Guarded -> Guarded) -> TerM a -> TerM a
terModifyGuarded f :: Guarded -> Guarded
f = (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
$ \ e :: TerEnv
e -> TerEnv
e { terGuarded :: Guarded
terGuarded = Guarded -> Guarded
f (Guarded -> Guarded) -> Guarded -> Guarded
forall a b. (a -> b) -> a -> b
$ TerEnv -> Guarded
terGuarded TerEnv
e }
terSetGuarded :: Order -> TerM a -> TerM a
terSetGuarded :: 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 :: TerM a -> TerM a
terUnguarded = Guarded -> TerM a -> TerM a
forall a. Guarded -> TerM a -> TerM a
terSetGuarded Guarded
unknown
terSizeDepth :: Lens' Int TerEnv
terSizeDepth :: (Int -> f Int) -> TerEnv -> f TerEnv
terSizeDepth f :: Int -> f Int
f e :: TerEnv
e = Int -> f Int
f (TerEnv -> Int
_terSizeDepth TerEnv
e) f Int -> (Int -> TerEnv) -> f TerEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ i :: Int
i -> TerEnv
e { _terSizeDepth :: Int
_terSizeDepth = Int
i }
terGetUsableVars :: TerM VarSet
terGetUsableVars :: TerM VarSet
terGetUsableVars = (TerEnv -> VarSet) -> TerM VarSet
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> VarSet
terUsableVars
terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
terModifyUsableVars f :: VarSet -> VarSet
f = (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
$ \ e :: TerEnv
e -> TerEnv
e { terUsableVars :: VarSet
terUsableVars = VarSet -> VarSet
f (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ TerEnv -> VarSet
terUsableVars TerEnv
e }
terSetUsableVars :: VarSet -> TerM a -> TerM a
terSetUsableVars :: 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
terGetUseSizeLt :: TerM Bool
terGetUseSizeLt :: TerM Bool
terGetUseSizeLt = (TerEnv -> Bool) -> TerM Bool
forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
terAsks TerEnv -> Bool
terUseSizeLt
terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
terModifyUseSizeLt f :: Bool -> Bool
f = (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
$ \ e :: TerEnv
e -> TerEnv
e { terUseSizeLt :: Bool
terUseSizeLt = Bool -> Bool
f (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TerEnv -> Bool
terUseSizeLt TerEnv
e }
terSetUseSizeLt :: Bool -> TerM a -> TerM a
terSetUseSizeLt :: 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
withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
withUsableVars :: a -> TerM b -> TerM b
withUsableVars pats :: a
pats m :: 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 "term.size" 70 (String -> TerM ()) -> String -> TerM ()
forall a b. (a -> b) -> a -> b
$ "usableSizeVars = " String -> String -> String
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 "term.size" 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 "no usuable size vars" else
"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 :: * -> *). Monad m => [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
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
conUseSizeLt :: QName -> TerM a -> TerM a
conUseSizeLt :: QName -> TerM a -> TerM a
conUseSizeLt c :: QName
c m :: 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 (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)
(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)
projUseSizeLt :: QName -> TerM a -> TerM a
projUseSizeLt :: QName -> TerM a -> TerM a
projUseSizeLt q :: QName
q m :: 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 "term.size" 20 (String -> TerM ()) -> String -> TerM ()
forall a b. (a -> b) -> a -> b
$ Bool -> (String -> String) -> String -> String
forall a. Bool -> (a -> a) -> a -> a
applyUnless Bool
co ("not " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
"using SIZELT vars after projection " String -> String -> String
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
isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive :: QName -> tcm Bool
isProjectionButNotCoinductive qn :: QName
qn = TCM Bool -> tcm Bool
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 "term.proj" 60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
"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
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 :: * -> *). Monad m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$
if Bool
b then "is an inductive projection"
else "is either not a projection or coinductive"
Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
where
isProjectionButNotCoinductive' :: QName -> TCM Bool
isProjectionButNotCoinductive' qn :: QName
qn = do
Maybe QName
flat <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
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 (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
isInductiveRecord (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
t)
_ -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection :: Bool -> QName -> tcm Bool
isCoinductiveProjection mustBeRecursive :: Bool
mustBeRecursive q :: QName
q = TCM Bool -> tcm Bool
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 "term.guardedness" 40 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "checking isCoinductiveProjection " String -> String -> String
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 (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
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
flat then Bool -> TCM Bool
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 _ r :: 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
$ \ rdef :: Defn
rdef -> do
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 (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 "term.guardedness" 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ " is coinductive; record type is " String -> String -> String
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 (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 "term.guardedness" 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ " must be recursive"
if Bool -> Bool
not (Defn -> Bool
safeRecRecursive Defn
rdef) then Bool -> TCM Bool
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 "term.guardedness" 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ " has been declared recursive, doing actual check now..."
let TelV tel :: Tele (Dom Type)
tel core :: Type
core = Type -> TelV Type
telView' (Definition -> Type
defType Definition
pdef)
(pars :: [Dom (String, Type)]
pars, tel' :: [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
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel
mut :: MutualNames
mut = MutualNames -> Maybe MutualNames -> MutualNames
forall a. a -> Maybe a -> a
fromMaybe MutualNames
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe MutualNames -> MutualNames)
-> Maybe MutualNames -> MutualNames
forall a b. (a -> b) -> a -> b
$ Defn -> Maybe MutualNames
recMutual Defn
rdef
String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "term.guardedness" 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 :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ "looking for recursive occurrences of"
, [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ((QName -> TCM Doc) -> MutualNames -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MutualNames
mut)
, "in"
, [Dom (String, Type)] -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Dom (String, Type)]
pars (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Dom (String, Type)] -> Tele (Dom Type)
telFromList [Dom (String, Type)]
tel')
, "and"
, Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
core
]
Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MutualNames -> Bool
forall a. Null a => a -> Bool
null MutualNames
mut) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Set QName
names <- (QName -> Bool) -> ([Type], Type) -> TCM (Set QName)
forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
anyDefs (MutualNames
mut MutualNames -> QName -> Bool
forall a. Ord a => [a] -> a -> Bool
`hasElem`) (([Type], Type) -> TCM (Set QName))
-> TCMT IO ([Type], Type) -> TCM (Set QName)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Type], Type) -> TCMT IO ([Type], Type)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise ((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 "term.guardedness" 40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
"found" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> if Set QName -> Bool
forall a. Null a => a -> Bool
null Set QName
names then "none" else [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ((QName -> TCM Doc) -> MutualNames -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MutualNames -> [TCM Doc]) -> MutualNames -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ Set QName -> MutualNames
forall a. Set a -> [a]
Set.toList Set QName
names)
Bool -> TCM Bool
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
$ Set QName -> Bool
forall a. Null a => a -> Bool
null Set QName
names
_ -> do
String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "term.guardedness" 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not a proper projection"
Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
safeRecRecursive :: Defn -> Bool
safeRecRecursive :: Defn -> Bool
safeRecRecursive (Record { recMutual :: Defn -> Maybe MutualNames
recMutual = Just qs :: MutualNames
qs }) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ MutualNames -> Bool
forall a. Null a => a -> Bool
null MutualNames
qs
safeRecRecursive _ = Bool
False
patternDepth :: forall a. Pattern' a -> Int
patternDepth :: 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 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
depth _ = MaxNat -> MaxNat
forall a. a -> a
id
unusedVar :: DeBruijnPattern
unusedVar :: DeBruijnPattern
unusedVar = Literal -> DeBruijnPattern
forall a. Literal -> Pattern' a
litP (Range -> String -> Literal
LitString Range
forall a. Range' a
noRange "term.unused.pat.var")
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 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 _ x :: 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 (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
$
VarSet -> TerM VarSet
forall (m :: * -> *) a. Monad m => a -> m a
return VarSet
forall a. Monoid a => a
mempty
ConP c :: ConHead
c _ _ -> 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 _ = 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 ps :: [DeBruijnPattern]
ps =
case [DeBruijnPattern]
ps of
[] -> VarSet -> TerM VarSet
forall (m :: * -> *) a. Monad m => a -> m a
return VarSet
forall a. Monoid a => a
mempty
(ProjP _ q :: QName
q : ps :: [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
(p :: DeBruijnPattern
p : ps :: [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 (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 m :: Bool
m p :: DeBruijnPattern
p) = ((DeBruijnPattern -> TerM VarSet -> TerM VarSet)
-> DeBruijnPattern -> TerM VarSet
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 _ x :: 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 (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
$
VarSet -> TerM VarSet
forall (m :: * -> *) a. Monad m => a -> m a
return VarSet
forall a. Monoid a => a
mempty
ConP c :: ConHead
c _ _ -> 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 _ = 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 ps :: MaskedDeBruijnPatterns
ps =
case MaskedDeBruijnPatterns
ps of
[] -> VarSet -> TerM VarSet
forall (m :: * -> *) a. Monad m => a -> m a
return VarSet
forall a. Monoid a => a
mempty
(Masked _ (ProjP _ q :: QName
q) : ps :: 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
(p :: Masked DeBruijnPattern
p : ps :: 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 (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
type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]
data Masked a = Masked
{ Masked a -> Bool
getMask :: Bool
, Masked a -> a
getMasked :: a
} 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
/= :: Masked a -> Masked a -> Bool
$c/= :: forall a. Eq a => Masked a -> Masked a -> Bool
== :: Masked a -> Masked a -> Bool
$c== :: forall a. Eq a => Masked a -> Masked a -> Bool
Eq, 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
min :: Masked a -> Masked a -> Masked a
$cmin :: forall a. Ord a => Masked a -> Masked a -> Masked a
max :: Masked a -> Masked a -> Masked a
$cmax :: forall a. Ord a => Masked a -> Masked a -> Masked a
>= :: Masked a -> Masked a -> Bool
$c>= :: forall a. Ord a => Masked a -> Masked a -> Bool
> :: Masked a -> Masked a -> Bool
$c> :: forall a. Ord a => Masked a -> Masked a -> Bool
<= :: Masked a -> Masked a -> Bool
$c<= :: forall a. Ord a => Masked a -> Masked a -> Bool
< :: Masked a -> Masked a -> Bool
$c< :: forall a. Ord a => Masked a -> Masked a -> Bool
compare :: Masked a -> Masked a -> Ordering
$ccompare :: forall a. Ord a => Masked a -> Masked a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Masked a)
Ord, Int -> Masked a -> String -> String
[Masked a] -> String -> String
Masked a -> String
(Int -> Masked a -> String -> String)
-> (Masked a -> String)
-> ([Masked a] -> String -> String)
-> Show (Masked a)
forall a. Show a => Int -> Masked a -> String -> String
forall a. Show a => [Masked a] -> String -> String
forall a. Show a => Masked a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Masked a] -> String -> String
$cshowList :: forall a. Show a => [Masked a] -> String -> String
show :: Masked a -> String
$cshow :: forall a. Show a => Masked a -> String
showsPrec :: Int -> Masked a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> Masked a -> String -> String
Show, a -> Masked b -> Masked a
(a -> b) -> Masked a -> Masked b
(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
<$ :: a -> Masked b -> Masked a
$c<$ :: forall a b. a -> Masked b -> Masked a
fmap :: (a -> b) -> Masked a -> Masked b
$cfmap :: forall a b. (a -> b) -> Masked a -> Masked b
Functor, Masked a -> Bool
(a -> m) -> Masked a -> m
(a -> b -> b) -> b -> Masked a -> b
(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
product :: Masked a -> a
$cproduct :: forall a. Num a => Masked a -> a
sum :: Masked a -> a
$csum :: forall a. Num a => Masked a -> a
minimum :: Masked a -> a
$cminimum :: forall a. Ord a => Masked a -> a
maximum :: Masked a -> a
$cmaximum :: forall a. Ord a => Masked a -> a
elem :: a -> Masked a -> Bool
$celem :: forall a. Eq a => a -> Masked a -> Bool
length :: Masked a -> Int
$clength :: forall a. Masked a -> Int
null :: Masked a -> Bool
$cnull :: forall a. Masked a -> Bool
toList :: Masked a -> [a]
$ctoList :: forall a. Masked a -> [a]
foldl1 :: (a -> a -> a) -> Masked a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Masked a -> a
foldr1 :: (a -> a -> a) -> Masked a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Masked a -> a
foldl' :: (b -> a -> b) -> b -> Masked a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Masked a -> b
foldl :: (b -> a -> b) -> b -> Masked a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Masked a -> b
foldr' :: (a -> b -> b) -> b -> Masked a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Masked a -> b
foldr :: (a -> b -> b) -> b -> Masked a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Masked a -> b
foldMap' :: (a -> m) -> Masked a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Masked a -> m
foldMap :: (a -> m) -> Masked a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Masked a -> m
fold :: Masked m -> m
$cfold :: forall m. Monoid m => Masked m -> m
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
(a -> f b) -> Masked a -> f (Masked b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
forall (f :: * -> *) a.
Applicative f =>
Masked (f a) -> f (Masked a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Masked a -> m (Masked b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Masked a -> f (Masked b)
sequence :: Masked (m a) -> m (Masked a)
$csequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
mapM :: (a -> m b) -> Masked a -> m (Masked b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Masked a -> m (Masked b)
sequenceA :: Masked (f a) -> f (Masked a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Masked (f a) -> f (Masked a)
traverse :: (a -> f b) -> Masked a -> f (Masked b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Masked a -> f (Masked b)
$cp2Traversable :: Foldable Masked
$cp1Traversable :: Functor Masked
Traversable)
masked :: a -> Masked a
masked :: a -> Masked a
masked = Bool -> a -> Masked a
forall a. Bool -> a -> Masked a
Masked Bool
True
notMasked :: a -> Masked a
notMasked :: a -> Masked a
notMasked = Bool -> a -> Masked a
forall a. Bool -> a -> Masked a
Masked Bool
False
instance Decoration Masked where
traverseF :: (a -> m b) -> Masked a -> m (Masked b)
traverseF f :: a -> m b
f (Masked m :: Bool
m a :: 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
instance PrettyTCM a => PrettyTCM (Masked a) where
prettyTCM :: Masked a -> m Doc
prettyTCM (Masked m :: Bool
m a :: a
a) = Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
forall a. Bool -> (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
prettyTCM a
a
newtype CallPath = CallPath { CallPath -> [CallInfo]
callInfos :: [CallInfo] }
deriving (Int -> CallPath -> String -> String
[CallPath] -> String -> String
CallPath -> String
(Int -> CallPath -> String -> String)
-> (CallPath -> String)
-> ([CallPath] -> String -> String)
-> Show CallPath
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [CallPath] -> String -> String
$cshowList :: [CallPath] -> String -> String
show :: CallPath -> String
$cshow :: CallPath -> String
showsPrec :: Int -> CallPath -> String -> String
$cshowsPrec :: Int -> CallPath -> String -> String
Show, b -> CallPath -> CallPath
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
stimes :: b -> CallPath -> CallPath
$cstimes :: forall b. Integral b => b -> CallPath -> CallPath
sconcat :: NonEmpty CallPath -> CallPath
$csconcat :: NonEmpty CallPath -> CallPath
<> :: CallPath -> CallPath -> CallPath
$c<> :: CallPath -> CallPath -> CallPath
Semigroup, Semigroup CallPath
CallPath
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
mconcat :: [CallPath] -> CallPath
$cmconcat :: [CallPath] -> CallPath
mappend :: CallPath -> CallPath -> CallPath
$cmappend :: CallPath -> CallPath -> CallPath
mempty :: CallPath
$cmempty :: CallPath
$cp1Monoid :: Semigroup CallPath
Monoid, CallPath -> Seq QName
(CallPath -> Seq QName) -> AllNames CallPath
forall a. (a -> Seq QName) -> AllNames a
allNames :: CallPath -> Seq QName
$callNames :: CallPath -> Seq QName
AllNames)
instance Pretty CallPath where
pretty :: CallPath -> Doc
pretty (CallPath cis0 :: [CallInfo]
cis0) = if [CallInfo] -> Bool
forall a. Null a => a -> Bool
null [CallInfo]
cis then Doc
forall a. Null a => a
empty else
[Doc] -> Doc
P.hsep ((CallInfo -> Doc) -> [CallInfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ ci :: CallInfo
ci -> Doc
arrow Doc -> Doc -> Doc
P.<+> CallInfo -> Doc
forall a. Pretty a => a -> Doc
P.pretty CallInfo
ci) [CallInfo]
cis) Doc -> Doc -> Doc
P.<+> Doc
arrow
where
cis :: [CallInfo]
cis = [CallInfo] -> [CallInfo]
forall a. [a] -> [a]
init [CallInfo]
cis0
arrow :: Doc
arrow = "-->"
terSetSizeDepth :: Telescope -> TerM a -> TerM a
terSetSizeDepth :: Tele (Dom Type) -> TerM a -> TerM a
terSetSizeDepth tel :: Tele (Dom Type)
tel cont :: TerM a
cont = do
Int
n <- TCM Int -> TerM Int
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 (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 (Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel) ((Dom (String, Type) -> TCM Int) -> TCMT IO [Int])
-> (Dom (String, Type) -> TCM Int) -> TCMT IO [Int]
forall a b. (a -> b) -> a -> b
$ \ dom :: Dom (String, Type)
dom -> do
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)
isSizeType Type
a) (Int -> TCM Int
forall (m :: * -> *) a. Monad m => a -> m a
return 1) (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 (m :: * -> *) a. Monad m => a -> m a
return 1
_ -> Int -> TCM Int
forall (m :: * -> *) a. Monad m => a -> m a
return 0
(TerEnv -> TerEnv) -> TerM a -> TerM a
forall (m :: * -> *) a.
MonadTer m =>
(TerEnv -> TerEnv) -> m a -> m a
terLocal (Lens' Int TerEnv -> LensSet Int TerEnv
forall i o. Lens' i o -> LensSet i o
set Lens' Int TerEnv
terSizeDepth Int
n) TerM a
cont