summaryrefslogtreecommitdiff
path: root/src/full/Agda/Termination/Monad.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Termination/Monad.hs')
-rw-r--r--src/full/Agda/Termination/Monad.hs45
1 files changed, 24 insertions, 21 deletions
diff --git a/src/full/Agda/Termination/Monad.hs b/src/full/Agda/Termination/Monad.hs
index 529c61a..bae9f93 100644
--- a/src/full/Agda/Termination/Monad.hs
+++ b/src/full/Agda/Termination/Monad.hs
@@ -1,10 +1,5 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-- | The monad for the termination checker.
--
@@ -23,11 +18,12 @@ import Control.Monad.State
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
+import Data.Semigroup (Semigroup)
import Agda.Interaction.Options
import Agda.Syntax.Abstract (IsProjP(..), AllNames)
-import Agda.Syntax.Common (Delayed(..), Induction(..), Dom(..))
+import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Syntax.Position (noRange)
@@ -39,7 +35,7 @@ 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.Pretty as TCP
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
@@ -112,6 +108,7 @@ data TerEnv = TerEnv
-- ^ Are we checking a delayed definition?
, terMaskArgs :: [Bool]
-- ^ Only consider the 'notMasked' 'False' arguments for establishing termination.
+ -- See issue #1023.
, terMaskResult :: Bool
-- ^ Only consider guardedness if 'False' (not masked).
, _terSizeDepth :: Int -- lazy by intention!
@@ -132,6 +129,7 @@ data TerEnv = TerEnv
-- matrix, can we take the variable for use with SIZELT constraints from the context?
-- Yes, if we are under an inductive constructor.
-- No, if we are under a record constructor.
+ -- (See issue #1015).
, terUsableVars :: VarSet
-- ^ Pattern variables that can be compared to argument variables using SIZELT.
}
@@ -247,6 +245,10 @@ instance MonadError TCErr TerM where
catchError m handler = TerM $ ReaderT $ \ tenv -> do
runTer tenv m `catchError` (\ err -> runTer tenv $ handler err)
+instance HasConstInfo TerM where
+ getConstInfo = liftTCM . getConstInfo
+ getRewriteRulesFor = liftTCM . getRewriteRulesFor
+
-- * Modifiers and accessors for the termination environment in the monad.
terGetGuardingTypeConstructors :: TerM Bool
@@ -406,8 +408,8 @@ isProjectionButNotCoinductive qn = liftTCM $ do
else do
mp <- isProjection qn
case mp of
- Just Projection{ projProper = Just{}, projFromType = t }
- -> isInductiveRecord t
+ Just Projection{ projProper = True, projFromType = t }
+ -> isInductiveRecord (unArg t)
_ -> return False
-- | Check whether a projection belongs to a coinductive record
@@ -426,7 +428,7 @@ isCoinductiveProjection mustBeRecursive q = liftTCM $ do
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 } ->
+ Just Projection{ projProper = True, projFromType = Arg _ r, projIndex = n } ->
caseMaybeM (isRecord r) __IMPOSSIBLE__ $ \ rdef -> do
-- no for inductive or non-recursive record
if recInduction rdef /= Just CoInductive then return False else do
@@ -475,20 +477,20 @@ data DeBruijnPat' a
-- ^ Literal. Also abused to censor part of a pattern.
| TermDBP Term
-- ^ Part of dot pattern that cannot be converted into a pattern.
- | ProjDBP QName
+ | ProjDBP ProjOrigin QName
-- ^ Projection pattern.
deriving (Functor, Show)
instance IsProjP (DeBruijnPat' a) where
- isProjP (ProjDBP d) = Just d
- isProjP _ = Nothing
+ isProjP (ProjDBP o d) = Just (o, AmbQ [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
+ prettyTCM (ProjDBP o d) = text "." TCP.<> prettyTCM d
-- | How long is the path to the deepest variable?
patternDepth :: DeBruijnPat' a -> Int
@@ -537,9 +539,9 @@ instance UsableSizeVars DeBruijnPat where
instance UsableSizeVars DeBruijnPats where
usableSizeVars ps =
case ps of
- [] -> return mempty
- (ProjDBP q : ps) -> projUseSizeLt q $ usableSizeVars ps
- (p : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps
+ [] -> return mempty
+ (ProjDBP _ q : ps) -> projUseSizeLt q $ usableSizeVars ps
+ (p : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps
instance UsableSizeVars (Masked DeBruijnPat) where
usableSizeVars (Masked m p) = do
@@ -554,11 +556,12 @@ instance UsableSizeVars (Masked DeBruijnPat) where
instance UsableSizeVars MaskedDeBruijnPats where
usableSizeVars ps =
case ps of
- [] -> return mempty
- (Masked _ (ProjDBP q) : ps) -> projUseSizeLt q $ usableSizeVars ps
- (p : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps
+ [] -> return mempty
+ (Masked _ (ProjDBP _ q) : ps) -> projUseSizeLt q $ usableSizeVars ps
+ (p : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps
-- * Masked patterns (which are not eligible for structural descent, only for size descent)
+-- See issue #1023.
type MaskedDeBruijnPats = [Masked DeBruijnPat]
@@ -593,7 +596,7 @@ instance PrettyTCM a => PrettyTCM (Masked a) where
-- Performance-wise, I could not see a difference between Set and list.
newtype CallPath = CallPath { callInfos :: [CallInfo] }
- deriving (Show, Monoid, AllNames)
+ deriving (Show, Semigroup, Monoid, AllNames)
-- | Only show intermediate nodes. (Drop last 'CallInfo').
instance Pretty CallPath where