module Agda.Termination.Monad where
import Control.Applicative
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.State
import Data.Functor ((<$>))
import qualified Data.List as List
import Agda.Interaction.Options
import Agda.Syntax.Abstract (QName,IsProjP(..))
import Agda.Syntax.Common (Delayed(..), Induction(..), Dom(..))
import Agda.Syntax.Internal
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.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (Pretty)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
#include "undefined.h"
import Agda.Utils.Impossible
type MutualNames = [QName]
type Target = QName
type Guarded = Order
data TerEnv = TerEnv
{ terUseDotPatterns :: Bool
, terGuardingTypeConstructors :: Bool
, terInlineWithFunctions :: Bool
, terSizeSuc :: Maybe QName
, terSharp :: Maybe QName
, terCutOff :: CutOff
, terCurrent :: QName
, terMutual :: MutualNames
, terUserNames :: [QName]
, terTarget :: Maybe Target
, terDelayed :: Delayed
, terMaskArgs :: [Bool]
, terMaskResult :: Bool
, terPatterns :: [DeBruijnPat]
, terPatternsRaise :: !Int
, terGuarded :: !Guarded
, terUseSizeLt :: Bool
, terUsableVars :: VarSet
}
defaultTerEnv :: TerEnv
defaultTerEnv = TerEnv
{ terUseDotPatterns = False
, terGuardingTypeConstructors = False
, terInlineWithFunctions = True
, terSizeSuc = Nothing
, terSharp = Nothing
, terCutOff = defaultCutOff
, terUserNames = __IMPOSSIBLE__
, terMutual = __IMPOSSIBLE__
, terCurrent = __IMPOSSIBLE__
, terTarget = Nothing
, terDelayed = NotDelayed
, terMaskArgs = repeat True
, terMaskResult = True
, terPatterns = __IMPOSSIBLE__
, terPatternsRaise = 0
, terGuarded = le
, terUseSizeLt = False
, terUsableVars = 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 = f <$> terAsk
newtype TerM a = TerM { terM :: ReaderT TerEnv TCM a }
deriving (Functor, Applicative, Monad)
instance MonadTer TerM where
terAsk = TerM $ ask
terLocal f = TerM . local f . terM
runTer :: TerEnv -> TerM a -> TCM a
runTer tenv (TerM m) = runReaderT m tenv
runTerDefault :: TerM a -> TCM a
runTerDefault cont = do
cutoff <- optTerminationDepth <$> pragmaOptions
suc <- sizeSucName
sharp <- fmap nameOfSharp <$> coinductionKit
guardingTypeConstructors <-
optGuardingTypeConstructors <$> pragmaOptions
inlineWithFunctions <- not . optWithoutK <$> pragmaOptions
let tenv = defaultTerEnv
{ terGuardingTypeConstructors = guardingTypeConstructors
, terInlineWithFunctions = inlineWithFunctions
, terSizeSuc = suc
, terSharp = sharp
, terCutOff = cutoff
}
runTer tenv cont
instance MonadReader TCEnv TerM where
ask = TerM $ lift $ ask
local f m = TerM $ ReaderT $ local f . runReaderT (terM m)
instance MonadState TCState TerM where
get = TerM $ lift $ get
put = TerM . lift . put
instance MonadIO TerM where
liftIO = TerM . liftIO
instance MonadTCM TerM where
liftTCM = TerM . lift
instance MonadError TCErr TerM where
throwError = liftTCM . throwError
catchError m handler = TerM $ ReaderT $ \ tenv -> do
runTer tenv m `catchError` (\ err -> runTer tenv $ handler err)
terGetGuardingTypeConstructors :: TerM Bool
terGetGuardingTypeConstructors = terAsks terGuardingTypeConstructors
terGetInlineWithFunctions :: TerM Bool
terGetInlineWithFunctions = terAsks terInlineWithFunctions
terGetUseDotPatterns :: TerM Bool
terGetUseDotPatterns = terAsks terUseDotPatterns
terSetUseDotPatterns :: Bool -> TerM a -> TerM a
terSetUseDotPatterns b = terLocal $ \ e -> e { terUseDotPatterns = b }
terGetSizeSuc :: TerM (Maybe QName)
terGetSizeSuc = terAsks terSizeSuc
terGetCurrent :: TerM QName
terGetCurrent = terAsks terCurrent
terSetCurrent :: QName -> TerM a -> TerM a
terSetCurrent q = terLocal $ \ e -> e { terCurrent = q }
terGetSharp :: TerM (Maybe QName)
terGetSharp = terAsks terSharp
terGetCutOff :: TerM CutOff
terGetCutOff = terAsks terCutOff
terGetMutual :: TerM MutualNames
terGetMutual = terAsks terMutual
terGetUserNames :: TerM [QName]
terGetUserNames = terAsks terUserNames
terGetTarget :: TerM (Maybe Target)
terGetTarget = terAsks terTarget
terSetTarget :: Maybe Target -> TerM a -> TerM a
terSetTarget t = terLocal $ \ e -> e { terTarget = t }
terGetDelayed :: TerM Delayed
terGetDelayed = terAsks terDelayed
terSetDelayed :: Delayed -> TerM a -> TerM a
terSetDelayed b = terLocal $ \ e -> e { terDelayed = b }
terGetMaskArgs :: TerM [Bool]
terGetMaskArgs = terAsks terMaskArgs
terSetMaskArgs :: [Bool] -> TerM a -> TerM a
terSetMaskArgs b = terLocal $ \ e -> e { terMaskArgs = b }
terGetMaskResult :: TerM Bool
terGetMaskResult = terAsks terMaskResult
terSetMaskResult :: Bool -> TerM a -> TerM a
terSetMaskResult b = terLocal $ \ e -> e { terMaskResult = b }
terGetPatterns :: TerM DeBruijnPats
terGetPatterns = raiseDBP <$> terAsks terPatternsRaise <*> terAsks terPatterns
terSetPatterns :: DeBruijnPats -> TerM a -> TerM a
terSetPatterns ps = terLocal $ \ e -> e { terPatterns = ps }
terRaise :: TerM a -> TerM a
terRaise = terLocal $ \ e -> e { terPatternsRaise = terPatternsRaise e + 1 }
terGetGuarded :: TerM Guarded
terGetGuarded = terAsks terGuarded
terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a
terModifyGuarded f = terLocal $ \ e -> e { terGuarded = f $ terGuarded e }
terSetGuarded :: Order -> TerM a -> TerM a
terSetGuarded = terModifyGuarded . const
terUnguarded :: TerM a -> TerM a
terUnguarded = terSetGuarded unknown
terPiGuarded :: TerM a -> TerM a
terPiGuarded m = ifM terGetGuardingTypeConstructors m $ terUnguarded m
terGetUsableVars :: TerM VarSet
terGetUsableVars = terAsks terUsableVars
terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
terModifyUsableVars f = terLocal $ \ e -> e { terUsableVars = f $ terUsableVars e }
terSetUsableVars :: VarSet -> TerM a -> TerM a
terSetUsableVars = terModifyUsableVars . const
terGetUseSizeLt :: TerM Bool
terGetUseSizeLt = terAsks terUseSizeLt
terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
terModifyUseSizeLt f = terLocal $ \ e -> e { terUseSizeLt = f $ terUseSizeLt e }
terSetUseSizeLt :: Bool -> TerM a -> TerM a
terSetUseSizeLt = terModifyUseSizeLt . const
withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
withUsableVars pats m = do
vars <- usableSizeVars pats
terSetUsableVars vars $ m
conUseSizeLt :: QName -> TerM a -> TerM a
conUseSizeLt c m = do
caseMaybeM (liftTCM $ isRecordConstructor c)
(terSetUseSizeLt True m)
(const $ terSetUseSizeLt False m)
projUseSizeLt :: QName -> TerM a -> TerM a
projUseSizeLt q m = isCoinductiveProjection q >>= (`terSetUseSizeLt` m)
isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool
isProjectionButNotCoinductive qn = liftTCM $ do
b <- isProjectionButNotCoinductive' qn
reportSDoc "term.proj" 60 $ do
text "identifier" <+> prettyTCM qn <+> do
text $
if b then "is an inductive projection"
else "is either not a projection or coinductive"
return b
where
isProjectionButNotCoinductive' qn = do
flat <- fmap nameOfFlat <$> coinductionKit
if Just qn == flat
then return False
else do
mp <- isProjection qn
case mp of
Just Projection{ projProper = Just{}, projFromType = t }
-> isInductiveRecord t
_ -> return False
isCoinductiveProjection :: MonadTCM tcm => QName -> tcm Bool
isCoinductiveProjection q = liftTCM $ do
flat <- fmap nameOfFlat <$> coinductionKit
if Just q == flat then return True else do
pdef <- getConstInfo q
case isProjection_ (theDef pdef) of
Just Projection{ projProper = Just{}, projFromType = r, projIndex = n }
-> caseMaybeM (isRecord r) __IMPOSSIBLE__ $ \ rdef -> do
if recInduction rdef /= Just CoInductive then return False else do
if not (recRecursive rdef) then return False else do
let TelV tel core = telView' (defType pdef)
tel' = drop n $ telToList tel
names <- anyDefs (r : recMutual rdef) (map (snd . unDom) tel', core)
return $ not $ null names
_ -> return False
type DeBruijnPats = [DeBruijnPat]
type DeBruijnPat = DeBruijnPat' Int
data DeBruijnPat' a
= VarDBP a
| ConDBP QName [DeBruijnPat' a]
| LitDBP Literal
| TermDBP Term
| ProjDBP QName
deriving (Functor, Show)
instance IsProjP (DeBruijnPat' a) where
isProjP (ProjDBP d) = Just d
isProjP _ = Nothing
instance PrettyTCM DeBruijnPat where
prettyTCM (VarDBP i) = prettyTCM $ var i
prettyTCM (ConDBP c ps) = parens $ do prettyTCM c <+> hsep (map prettyTCM ps)
prettyTCM (LitDBP l) = prettyTCM l
prettyTCM (TermDBP v) = parens $ prettyTCM v
prettyTCM (ProjDBP d) = prettyTCM d
patternDepth :: DeBruijnPat' a -> Int
patternDepth p =
case p of
ConDBP _ ps -> succ $ maximum $ 0 : map patternDepth ps
VarDBP{} -> 0
LitDBP{} -> 0
TermDBP{} -> 0
ProjDBP{} -> 0
unusedVar :: DeBruijnPat
unusedVar = LitDBP (LitString noRange "term.unused.pat.var")
raiseDBP :: Int -> DeBruijnPats -> DeBruijnPats
raiseDBP 0 = id
raiseDBP n = map $ fmap (n +)
class UsableSizeVars a where
usableSizeVars :: a -> TerM VarSet
instance UsableSizeVars DeBruijnPat where
usableSizeVars p =
case p of
VarDBP i -> ifM terGetUseSizeLt (return $ VarSet.singleton i) (return $ mempty)
ConDBP c ps -> conUseSizeLt c $ usableSizeVars ps
LitDBP{} -> return mempty
TermDBP{} -> return mempty
ProjDBP{} -> return mempty
instance UsableSizeVars [DeBruijnPat] where
usableSizeVars ps =
case ps of
[] -> return mempty
(ProjDBP q : ps) -> projUseSizeLt q $ usableSizeVars ps
(p : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps
newtype CallPath = CallPath { callInfos :: [CallInfo] }
deriving (Show, Monoid)
instance Pretty CallPath where
pretty (CallPath cis0) = if List.null cis then P.empty else
P.hsep (map (\ ci -> arrow P.<+> P.pretty ci) cis) P.<+> arrow
where
cis = init cis0
arrow = P.text "-->"