summaryrefslogtreecommitdiff
path: root/src/full/Agda/Termination
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Termination')
-rw-r--r--src/full/Agda/Termination/CallGraph.hs39
-rw-r--r--src/full/Agda/Termination/CallMatrix.hs40
-rw-r--r--src/full/Agda/Termination/CutOff.hs4
-rw-r--r--src/full/Agda/Termination/Inlining.hs38
-rw-r--r--src/full/Agda/Termination/Monad.hs198
-rw-r--r--src/full/Agda/Termination/Order.hs9
-rw-r--r--src/full/Agda/Termination/SparseMatrix.hs18
-rw-r--r--src/full/Agda/Termination/TermCheck.hs480
8 files changed, 459 insertions, 367 deletions
diff --git a/src/full/Agda/Termination/CallGraph.hs b/src/full/Agda/Termination/CallGraph.hs
index 635ea95..4bd5c65 100644
--- a/src/full/Agda/Termination/CallGraph.hs
+++ b/src/full/Agda/Termination/CallGraph.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
-- | Call graphs and related concepts, more or less as defined in
-- \"A Predicative Analysis of Structural Recursion\" by
@@ -23,8 +22,6 @@ module Agda.Termination.CallGraph
, targetNodes
, fromList
, toList
- , empty
- , null
, union
, insert
, complete, completionStep
@@ -65,10 +62,11 @@ import Agda.Utils.List hiding (tests)
import Agda.Utils.Map
import Agda.Utils.Maybe
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.PartialOrd
-import Agda.Utils.Pretty hiding (empty)
-import qualified Agda.Utils.Pretty as P
+import Agda.Utils.Pretty
import Agda.Utils.QuickCheck hiding (label)
+import Agda.Utils.Singleton
import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
@@ -96,7 +94,7 @@ callMatrixSet = label
-- | Make a call with a single matrix.
mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo
-mkCall s t m cinfo = Edge s t $ CMSet.singleton $ CallMatrixAug m cinfo
+mkCall s t m cinfo = Edge s t $ singleton $ CallMatrixAug m cinfo
-- | Make a call with empty @cinfo@.
mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo
@@ -145,15 +143,10 @@ toList = Graph.edges . theCallGraph
fromList :: Monoid cinfo => [Call cinfo] -> CallGraph cinfo
fromList = CallGraph . Graph.fromListWith CMSet.union
--- | Creates an empty call graph.
-
-empty :: CallGraph cinfo
-empty = CallGraph Graph.empty
-
--- | Check whether the call graph is completely disconnected.
-
-null :: CallGraph cinfo -> Bool
-null = List.all (CMSet.null . label) . toList
+-- | 'null' checks whether the call graph is completely disconnected.
+instance Null (CallGraph cinfo) where
+ empty = CallGraph Graph.empty
+ null = List.all (null . label) . toList
-- | Takes the union of two call graphs.
@@ -202,7 +195,7 @@ instance (Monoid a, CombineNewOld a, Ord s, Ord t) => CombineNewOld (Graph s t a
-- -- | otherwise = __IMPOSSIBLE__
-- Filter unlabelled edges from the resulting new graph.
- -- filt = Graph.filterEdges (not . CMSet.null)
+ -- filt = Graph.filterEdges (not . null)
-- | Call graph combination.
--
@@ -263,7 +256,7 @@ completionStep gOrig gThis = combineNewOldCallGraph gOrig gThis
instance Pretty cinfo => Pretty (CallGraph cinfo) where
pretty = vcat . map prettyCall . toList
where
- prettyCall e = if CMSet.null (callMatrixSet e) then P.empty else align 20 $
+ prettyCall e = if null (callMatrixSet e) then empty else align 20 $
[ ("Source:", text $ show $ source e)
, ("Target:", text $ show $ target e)
, ("Matrix:", pretty $ callMatrixSet e)
diff --git a/src/full/Agda/Termination/CallMatrix.hs b/src/full/Agda/Termination/CallMatrix.hs
index 40a30e9..9ce5ed1 100644
--- a/src/full/Agda/Termination/CallMatrix.hs
+++ b/src/full/Agda/Termination/CallMatrix.hs
@@ -1,13 +1,12 @@
--- {-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
+-- {-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE StandaloneDeriving #-}
module Agda.Termination.CallMatrix where
@@ -34,9 +33,11 @@ import qualified Agda.Termination.Semiring as Semiring
import Agda.Utils.Favorites (Favorites)
import qualified Agda.Utils.Favorites as Fav
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.PartialOrd hiding (tests)
import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.QuickCheck
+import Agda.Utils.Singleton
import Agda.Utils.TestHelpers
------------------------------------------------------------------------
@@ -181,8 +182,11 @@ noAug m = CallMatrixAug m mempty
-- * Sets of incomparable call matrices augmented with path information.
------------------------------------------------------------------------
+-- | Sets of incomparable call matrices augmented with path information.
+-- Use overloaded 'null', 'empty', 'singleton', 'mappend'.
newtype CMSet cinfo = CMSet { cmSet :: Favorites (CallMatrixAug cinfo) }
- deriving (Show, Arbitrary, CoArbitrary, Monoid)
+ deriving ( Show, Arbitrary, CoArbitrary
+ , Monoid, Null, Singleton (CallMatrixAug cinfo) )
-- | Call matrix set product is the Cartesian product.
@@ -190,22 +194,6 @@ instance Monoid cinfo => CallComb (CMSet cinfo) where
CMSet as >*< CMSet bs = CMSet $ Fav.fromList $
[ a >*< b | a <- Fav.toList as, b <- Fav.toList bs ]
--- | An empty call matrix set.
-
-empty :: CMSet cinfo
-empty = mempty
--- empty = CMSet $ Fav.empty
-
--- | Call matrix is empty?
-
-null :: CMSet cinfo -> Bool
-null (CMSet as) = Fav.null as
-
--- | A singleton call matrix set.
-
-singleton :: CallMatrixAug cinfo -> CMSet cinfo
-singleton = CMSet . Fav.singleton
-
-- | Insert into a call matrix set.
insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo
diff --git a/src/full/Agda/Termination/CutOff.hs b/src/full/Agda/Termination/CutOff.hs
index f0bb9fb..97cb823 100644
--- a/src/full/Agda/Termination/CutOff.hs
+++ b/src/full/Agda/Termination/CutOff.hs
@@ -1,6 +1,6 @@
--- | Defines 'CutOff' type which is used in 'Agda.Interaction.Options'.
+-- | Defines 'CutOff' type which is used in "Agda.Interaction.Options".
-- This module's purpose is to eliminate the dependency of
--- 'Agda.TypeChecking.Monad.Base' on the termination checker and
+-- "Agda.TypeChecking.Monad.Base" on the termination checker and
-- everything it imports.
module Agda.Termination.CutOff where
diff --git a/src/full/Agda/Termination/Inlining.hs b/src/full/Agda/Termination/Inlining.hs
index 9cb52a6..97cb3dd 100644
--- a/src/full/Agda/Termination/Inlining.hs
+++ b/src/full/Agda/Termination/Inlining.hs
@@ -1,5 +1,9 @@
{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
+
-- Author: Ulf Norell
-- Created: 2013-11-09
@@ -54,7 +58,7 @@ import Data.Foldable (foldMap)
import Data.Traversable (traverse)
import Data.List as List
-import Agda.Syntax.Common hiding (NamedArg)
+import Agda.Syntax.Common as Common hiding (NamedArg)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Monad
@@ -187,12 +191,11 @@ inline f pcl t wf wcl = inTopContext $ addCtxTel (clauseTel wcl) $ do
where n' = n - 1
dispToPats :: DisplayTerm -> TCM ([NamedArg Pattern], Permutation)
- dispToPats (DWithApp (DDef _ vs) ws zs) = do
- let us = vs ++ map defaultArg ws ++ map (fmap DTerm) zs
- (ps, (j, ren)) <- (`runStateT` (0, [])) $
- map (fmap unnamed) <$> mapM (traverse dtermToPat) us
+ dispToPats (DWithApp (DDef _ es) ws zs) = do
+ let es' = es ++ map Apply (map defaultArg ws ++ map (fmap DTerm) zs)
+ (ps, (j, ren)) <- (`runStateT` (0, [])) $ mapM (traverse dtermToPat) es'
let perm = Perm j (map snd $ List.sort ren)
- return (ps, perm)
+ return (map ePatToPat ps, perm)
dispToPats t = __IMPOSSIBLE__
bindVar i = do
@@ -204,17 +207,26 @@ inline f pcl t wf wcl = inTopContext $ addCtxTel (clauseTel wcl) $ do
skip = modify $ \(j, is) -> (j + 1, is)
+ ePatToPat :: Elim' Pattern -> NamedArg Pattern
+ ePatToPat (Apply p) = fmap unnamed p
+ ePatToPat (Proj d) = defaultNamedArg $ ProjP d
+
+ dtermToPat :: DisplayTerm -> StateT (Int, [(Int, Int)]) TCM Pattern
dtermToPat v =
case v of
DWithApp{} -> __IMPOSSIBLE__ -- I believe
- DCon c vs -> ConP c Nothing . map (fmap unnamed)
+ DCon c vs -> ConP c noConPatternInfo . map (fmap unnamed)
<$> mapM (traverse dtermToPat) vs
- DDef{} -> DotP (dtermToTerm v) <$ skip
+ DDef d es -> do
+ ifM (return (null es) `and2M` do isJust <$> lift (isProjection d))
+ {-then-} (return $ ProjP d)
+ {-else-} (DotP (dtermToTerm v) <$ skip)
DDot v -> DotP v <$ skip
DTerm (Var i []) ->
ifM (bindVar i) (VarP . nameToPatVarName <$> lift (nameOfBV i))
(pure $ DotP (Var i []))
- DTerm (Con c vs) -> ConP c Nothing . map (fmap unnamed) <$> mapM (traverse (dtermToPat . DTerm)) vs
+ DTerm (Con c vs) -> ConP c noConPatternInfo . map (fmap unnamed) <$>
+ mapM (traverse (dtermToPat . DTerm)) vs
DTerm v -> DotP v <$ skip
isWithFunction :: MonadTCM tcm => QName -> tcm (Maybe QName)
@@ -230,11 +242,3 @@ expandWithFunctionCall f es = do
return $ dtermToTerm disp `applyE` es'
where
(vs, es') = splitApplyElims es
-
-dtermToTerm :: DisplayTerm -> Term
-dtermToTerm (DWithApp d ds vs) = dtermToTerm d `apply` (map (defaultArg . dtermToTerm) ds ++ vs)
-dtermToTerm (DCon c args) = Con c $ map (fmap dtermToTerm) args
-dtermToTerm (DDef f args) = Def f $ map (Apply . fmap dtermToTerm) args
-dtermToTerm (DDot v) = v
-dtermToTerm (DTerm v) = v
-
diff --git a/src/full/Agda/Termination/Monad.hs b/src/full/Agda/Termination/Monad.hs
index 91bef83..cd7f687 100644
--- a/src/full/Agda/Termination/Monad.hs
+++ b/src/full/Agda/Termination/Monad.hs
@@ -1,9 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
-- | The monad for the termination checker.
--
@@ -13,17 +14,21 @@
module Agda.Termination.Monad where
-import Control.Applicative
+import Prelude hiding (null)
+
+import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.State
+import Data.Foldable (Foldable)
import Data.Functor ((<$>))
import qualified Data.List as List
+import Data.Traversable (Traversable)
import Agda.Interaction.Options
-import Agda.Syntax.Abstract (QName,IsProjP(..))
+import Agda.Syntax.Abstract (QName, IsProjP(..), AllNames)
import Agda.Syntax.Common (Delayed(..), Induction(..), Dom(..))
import Agda.Syntax.Internal
import Agda.Syntax.Literal
@@ -37,12 +42,17 @@ import Agda.TypeChecking.Monad
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(catchError, throwError) )
+import Agda.Utils.Function
+import Agda.Utils.Functor
+import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
-import Agda.Utils.Pretty (Pretty)
+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
@@ -102,10 +112,14 @@ data TerEnv = TerEnv
, terDelayed :: Delayed
-- ^ Are we checking a delayed definition?
, terMaskArgs :: [Bool]
- -- ^ Only consider the 'True' arguments for establishing termination.
+ -- ^ Only consider the 'notMasked' 'False' arguments for establishing termination.
, terMaskResult :: Bool
- -- ^ Only consider guardedness if 'True'.
- , terPatterns :: [DeBruijnPat]
+ -- ^ Only consider guardedness if 'False' (not masked).
+ , _terSizeDepth :: Int -- lazy by intention!
+ -- ^ How many @SIZELT@ relations do we have in the context
+ -- (= clause telescope). Used to approximate termination
+ -- for metas in call args.
+ , terPatterns :: MaskedDeBruijnPats
-- ^ The patterns of the clause we are checking.
, terPatternsRaise :: !Int
-- ^ Number of additional binders we have gone under
@@ -149,8 +163,9 @@ defaultTerEnv = TerEnv
, terCurrent = __IMPOSSIBLE__ -- needs to be set!
, terTarget = Nothing
, terDelayed = NotDelayed
- , terMaskArgs = repeat True -- use all arguments
- , terMaskResult = True -- use result
+ , terMaskArgs = repeat False -- use all arguments (mask none)
+ , terMaskResult = False -- use result (do not mask)
+ , _terSizeDepth = __IMPOSSIBLE__ -- needs to be set!
, terPatterns = __IMPOSSIBLE__ -- needs to be set!
, terPatternsRaise = 0
, terGuarded = le -- not initially guarded
@@ -292,10 +307,13 @@ 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
+terGetPatterns :: TerM (MaskedDeBruijnPats)
+terGetPatterns = do
+ n <- terAsks terPatternsRaise
+ mps <- terAsks terPatterns
+ return $ if n == 0 then mps else map (fmap (fmap (n +))) mps
-terSetPatterns :: DeBruijnPats -> TerM a -> TerM a
+terSetPatterns :: MaskedDeBruijnPats -> TerM a -> TerM a
terSetPatterns ps = terLocal $ \ e -> e { terPatterns = ps }
terRaise :: TerM a -> TerM a
@@ -317,6 +335,11 @@ terUnguarded = terSetGuarded unknown
terPiGuarded :: TerM a -> TerM a
terPiGuarded m = ifM terGetGuardingTypeConstructors m $ terUnguarded m
+-- | Lens for '_terSizeDepth'.
+
+terSizeDepth :: Lens' Int TerEnv
+terSizeDepth f e = f (_terSizeDepth e) <&> \ i -> e { _terSizeDepth = i }
+
-- | Lens for 'terUsableVars'.
terGetUsableVars :: TerM VarSet
@@ -343,6 +366,7 @@ terSetUseSizeLt = terModifyUseSizeLt . const
withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
withUsableVars pats m = do
vars <- usableSizeVars pats
+ reportSLn "term.size" 20 $ "usableSizeVars = " ++ show vars
terSetUsableVars vars $ m
-- | Set 'terUseSizeLt' when going under constructor @c@.
@@ -353,12 +377,14 @@ conUseSizeLt c m = do
(const $ terSetUseSizeLt False m)
-- | Set 'terUseSizeLt' for arguments following projection @q@.
+-- We disregard j<i after a non-coinductive projection.
+-- However, the projection need not be recursive (Issue 1470).
projUseSizeLt :: QName -> TerM a -> TerM a
-projUseSizeLt q m = isCoinductiveProjection q >>= (`terSetUseSizeLt` m)
--- projUseSizeLt q m = do
--- ifM (liftTCM $ isProjectionButNotCoinductive q)
--- (terSetUseSizeLt False m)
--- (terSetUseSizeLt True m)
+projUseSizeLt q m = do
+ co <- isCoinductiveProjection False q
+ reportSLn "term.size" 20 $ applyUnless co ("not " ++) $
+ "using SIZELT vars after projection " ++ prettyShow q
+ terSetUseSizeLt co m
-- | For termination checking purposes flat should not be considered a
-- projection. That is, it flat doesn't preserve either structural order
@@ -393,29 +419,44 @@ isProjectionButNotCoinductive qn = liftTCM $ do
--
-- isCoinductiveProjection (Stream.tail) = return True
-- @
-isCoinductiveProjection :: MonadTCM tcm => QName -> tcm Bool
-isCoinductiveProjection q = liftTCM $ do
+isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
+isCoinductiveProjection mustBeRecursive q = liftTCM $ do
+ reportSLn "term.guardedness" 40 $ "checking isCoinductiveProjection " ++ prettyShow q
flat <- fmap nameOfFlat <$> coinductionKit
-- yes for ♭
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
- -- no for inductive or non-recursive record
- if recInduction rdef /= Just CoInductive then return False else do
- if not (recRecursive rdef) then return False else do
- -- 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 tel core = telView' (defType pdef)
- tel' = drop n $ telToList tel
- -- Check if any recursive symbols appear in the record type.
- -- Q (2014-07-01): Should we normalize the type?
- names <- anyDefs (r : recMutual rdef) (map (snd . unDom) tel', core)
- return $ not $ null names
- _ -> return False
+ pdef <- getConstInfo q
+ case isProjection_ (theDef pdef) of
+ Just Projection{ projProper = Just{}, projFromType = 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
+ reportSLn "term.guardedness" 40 $ prettyShow q ++ " is coinductive"
+ if not mustBeRecursive then return True else do
+ reportSLn "term.guardedness" 40 $ prettyShow q ++ " must be recursive"
+ if not (recRecursive rdef) then return False else do
+ reportSLn "term.guardedness" 40 $ prettyShow q ++ " 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 tel core = telView' (defType pdef)
+ tel' = drop n $ telToList tel
+ -- Check if any recursive symbols appear in the record type.
+ -- Q (2014-07-01): Should we normalize the type?
+ reportSDoc "term.guardedness" 40 $ sep
+ [ text "looking for recursive occurrences in"
+ , prettyTCM (telFromList tel')
+ , text "and"
+ , prettyTCM core
+ ]
+ names <- anyDefs (r : recMutual rdef) (map (snd . unDom) tel', core)
+ reportSDoc "term.guardedness" 40 $
+ text "found" <+> sep (map prettyTCM names)
+ return $ not $ null names
+ _ -> do
+ reportSLn "term.guardedness" 40 $ prettyShow q ++ " is not a proper projection"
+ return False
-- * De Bruijn patterns.
@@ -485,21 +526,61 @@ class UsableSizeVars a where
usableSizeVars :: a -> TerM VarSet
instance UsableSizeVars DeBruijnPat where
- usableSizeVars p =
+ usableSizeVars p = do
+ let none = return mempty
case p of
- VarDBP i -> ifM terGetUseSizeLt (return $ VarSet.singleton i) (return $ mempty)
+ VarDBP i -> ifM terGetUseSizeLt (return $ VarSet.singleton i) {- else -} none
ConDBP c ps -> conUseSizeLt c $ usableSizeVars ps
- LitDBP{} -> return mempty
- TermDBP{} -> return mempty
- ProjDBP{} -> return mempty
+ LitDBP{} -> none
+ TermDBP{} -> none
+ ProjDBP{} -> none
-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
+instance UsableSizeVars (Masked DeBruijnPat) where
+ usableSizeVars (Masked m p) = do
+ let none = return mempty
+ case p of
+ VarDBP i -> ifM terGetUseSizeLt (return $ VarSet.singleton i) {- else -} none
+ ConDBP c ps -> if m then none else conUseSizeLt c $ usableSizeVars ps
+ LitDBP{} -> none
+ TermDBP{} -> none
+ ProjDBP{} -> none
+
+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
+
+-- * Masked patterns (which are not eligible for structural descent, only for size descent)
+
+type MaskedDeBruijnPats = [Masked DeBruijnPat]
+
+data Masked a = Masked
+ { getMask :: Bool -- ^ True if thing not eligible for structural descent.
+ , getMasked :: a -- ^ Thing.
+ } deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+masked :: a -> Masked a
+masked = Masked True
+
+notMasked :: a -> Masked a
+notMasked = Masked False
+
+instance Decoration Masked where
+ traverseF f (Masked m a) = Masked m <$> f a
+
+-- | Print masked things in double parentheses.
+instance PrettyTCM a => PrettyTCM (Masked a) where
+ prettyTCM (Masked m a) = applyWhen m (parens . parens) $ prettyTCM a
+
-- * Call pathes
-- | The call information is stored as free monoid
@@ -513,12 +594,31 @@ instance UsableSizeVars [DeBruijnPat] where
-- Performance-wise, I could not see a difference between Set and list.
newtype CallPath = CallPath { callInfos :: [CallInfo] }
- deriving (Show, Monoid)
+ deriving (Show, Monoid, AllNames)
-- | Only show intermediate nodes. (Drop last 'CallInfo').
instance Pretty CallPath where
- pretty (CallPath cis0) = if List.null cis then P.empty else
+ pretty (CallPath cis0) = if null cis then empty else
P.hsep (map (\ ci -> arrow P.<+> P.pretty ci) cis) P.<+> arrow
where
cis = init cis0
arrow = P.text "-->"
+
+-- * Size depth estimation
+
+-- | A very crude way of estimating the @SIZELT@ chains
+-- @i > j > k@ in context. Returns 3 in this case.
+-- Overapproximates.
+
+-- TODO: more precise analysis, constructing a tree
+-- of relations between size variables.
+terSetSizeDepth :: Telescope -> TerM a -> TerM a
+terSetSizeDepth tel cont = do
+ n <- liftTCM $ sum <$> do
+ forM (telToList tel) $ \ dom -> do
+ a <- reduce $ snd $ unDom dom
+ ifM (isJust <$> isSizeType a) (return 1) {- else -} $ do
+ case ignoreSharing $ unEl a of
+ MetaV{} -> return 1
+ _ -> return 0
+ terLocal (set terSizeDepth n) cont
diff --git a/src/full/Agda/Termination/Order.hs b/src/full/Agda/Termination/Order.hs
index b513927..de59d0d 100644
--- a/src/full/Agda/Termination/Order.hs
+++ b/src/full/Agda/Termination/Order.hs
@@ -1,7 +1,6 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ImplicitParams #-}
-- | An Abstract domain of relative sizes, i.e., differences
-- between size of formal function parameter and function argument
@@ -31,7 +30,7 @@ import Agda.Termination.Semiring (HasZero(..), Semiring)
import qualified Agda.Termination.Semiring as Semiring
import Agda.Utils.PartialOrd hiding (tests)
-import Agda.Utils.Pretty hiding (empty)
+import Agda.Utils.Pretty
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
diff --git a/src/full/Agda/Termination/SparseMatrix.hs b/src/full/Agda/Termination/SparseMatrix.hs
index b90a538..f3ff6e5 100644
--- a/src/full/Agda/Termination/SparseMatrix.hs
+++ b/src/full/Agda/Termination/SparseMatrix.hs
@@ -1,13 +1,13 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
{- | Sparse matrices.
diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs
index 5139949..18d0af3 100644
--- a/src/full/Agda/Termination/TermCheck.hs
+++ b/src/full/Agda/Termination/TermCheck.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
{- Checking for Structural recursion
Authors: Andreas Abel, Nils Anders Danielsson, Ulf Norell,
@@ -22,9 +21,10 @@ module Agda.Termination.TermCheck
import Prelude hiding (null)
-import Control.Applicative
+import Control.Applicative hiding (empty)
import Control.Monad.State
+import Data.Foldable (toList)
import Data.List hiding (null)
import qualified Data.List as List
import Data.Maybe (mapMaybe, isJust, fromMaybe)
@@ -34,7 +34,7 @@ import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse)
-import Agda.Syntax.Abstract (IsProjP(..))
+import Agda.Syntax.Abstract (IsProjP(..), AllNames(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import qualified Agda.Syntax.Info as Info
@@ -44,9 +44,9 @@ import Agda.Syntax.Literal (Literal(LitString))
import Agda.Termination.CutOff
import Agda.Termination.Monad
-import Agda.Termination.CallGraph hiding (null)
+import Agda.Termination.CallGraph hiding (toList)
import qualified Agda.Termination.CallGraph as CallGraph
-import Agda.Termination.CallMatrix hiding (null)
+import Agda.Termination.CallMatrix hiding (toList)
import Agda.Termination.Order as Order
import qualified Agda.Termination.SparseMatrix as Matrix
import Agda.Termination.Termination (endos, idempotent)
@@ -79,8 +79,8 @@ import Agda.Utils.Maybe
import Agda.Utils.Monad -- (mapM', forM', ifM, or2M, and2M)
import Agda.Utils.Null
import Agda.Utils.Permutation
-import Agda.Utils.Pointed
import Agda.Utils.Pretty (render)
+import Agda.Utils.Singleton
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
@@ -92,14 +92,14 @@ import Agda.Utils.Impossible
type Calls = CallGraph CallPath
-- | The result of termination checking a module.
--- Must be 'Pointed' and a 'Monoid'.
+-- Must be a 'Monoid' and have 'Singleton'.
type Result = [TerminationError]
--- | Termination check a single declaration.
+-- | Entry point: Termination check a single declaration.
termDecl :: A.Declaration -> TCM Result
-termDecl d = ignoreAbstractMode $ termDecl' d
+termDecl d = inTopContext $ ignoreAbstractMode $ termDecl' d
-- | Termination check a sequence of declarations.
@@ -112,28 +112,27 @@ termDecls ds = concat <$> mapM termDecl' ds
-- (without necessarily ignoring @abstract@).
termDecl' :: A.Declaration -> TCM Result
-termDecl' (A.ScopedDecl scope ds) = do
- setScope scope
- termDecls ds
termDecl' d = case d of
A.Axiom {} -> return mempty
A.Field {} -> return mempty
A.Primitive {} -> return mempty
A.Mutual _ ds
- | [A.RecSig{}, A.RecDef _ r _ _ _ _ rds] <- unscopeDefs ds
- -> checkRecDef ds r rds
+ | [A.RecSig{}, A.RecDef _ _ _ _ _ _ rds] <- unscopeDefs ds
+ -> termDecls rds
A.Mutual i ds -> termMutual i ds
- A.Section _ x _ ds -> termSection x ds
+ A.Section _ _ _ ds -> termDecls ds
+ -- section structure can be ignored as we are termination checking
+ -- definitions lifted to the top-level
A.Apply {} -> return mempty
A.Import {} -> return mempty
A.Pragma {} -> return mempty
A.Open {} -> return mempty
A.PatternSynDef {} -> return mempty
-- open and pattern synonym defs are just artifacts from the concrete syntax
- A.ScopedDecl{} -> __IMPOSSIBLE__
- -- taken care of above
+ A.ScopedDecl _ ds -> termDecls ds
+ -- scope is irrelevant as we are termination checking Syntax.Internal
A.RecSig{} -> return mempty
- A.RecDef _ r _ _ _ _ ds -> checkRecDef [] r ds
+ A.RecDef _ r _ _ _ _ ds -> termDecls ds
-- These should all be wrapped in mutual blocks
A.FunDef{} -> __IMPOSSIBLE__
A.DataSig{} -> __IMPOSSIBLE__
@@ -141,32 +140,11 @@ termDecl' d = case d of
-- This should have been expanded to a proper declaration before termination checking
A.UnquoteDecl{} -> __IMPOSSIBLE__
where
- setScopeFromDefs = mapM_ setScopeFromDef
- setScopeFromDef (A.ScopedDecl scope d) = setScope scope
- setScopeFromDef _ = return ()
-
unscopeDefs = concatMap unscopeDef
unscopeDef (A.ScopedDecl _ ds) = unscopeDefs ds
unscopeDef d = [d]
- checkRecDef ds r rds = do
- setScopeFromDefs ds
- termSection (mnameFromList $ qnameToList r) rds
-
-
--- | Termination check a module.
-
-termSection :: ModuleName -> [A.Declaration] -> TCM Result
-termSection x ds = do
- tel <- lookupSection x
- reportSDoc "term.section" 10 $
- sep [ text "termination checking section"
- , prettyTCM x
- , prettyTCM tel
- ]
- withCurrentModule x $ addCtxTel tel $ termDecls ds
-
-- | Termination check a bunch of mutually inductive recursive definitions.
@@ -174,7 +152,7 @@ termMutual :: Info.MutualInfo -> [A.Declaration] -> TCM Result
termMutual i ds = if names == [] then return mempty else
-- We set the range to avoid panics when printing error messages.
- traceCall (SetRange (Info.mutualRange i)) $ do
+ setCurrentRange i $ do
-- Get set of mutually defined names from the TCM.
-- This includes local and auxiliary functions introduced
@@ -226,7 +204,7 @@ termMutual i ds = if names == [] then return mempty else
(runTerm $ termMutual')
-- record result of termination check in signature
- let terminates = List.null res
+ let terminates = null res
forM_ allNames $ \ q -> setTerminates q terminates
return res
@@ -274,16 +252,18 @@ termMutual' = do
-- the names the user has declared. This is for error reporting.
names <- terGetUserNames
case r of
- Left calls -> do
- return $ point $ TerminationError
- { termErrFunctions = names
- , termErrCalls = callInfos calls
- }
+ Left calls -> return $ singleton $ terminationError names $ callInfos calls
Right{} -> do
liftTCM $ reportSLn "term.warn.yes" 2 $
show (names) ++ " does termination check"
return mempty
+-- | Smart constructor for 'TerminationError'.
+-- Removes 'termErrFunctions' that are not mentioned in 'termErrCalls'.
+terminationError :: [QName] -> [CallInfo] -> TerminationError
+terminationError names calls = TerminationError names' calls
+ where names' = names `intersect` toList (allNames calls)
+
-- ASR (08 November 2014). The type of the function could be
--
-- @Either a b -> TerM (Either a b)@.
@@ -296,123 +276,119 @@ billToTerGraph = billPureTo [Benchmark.Termination, Benchmark.Graph]
reportCalls :: String -> Calls -> TerM ()
reportCalls no calls = do
- cutoff <- terGetCutOff
- let ?cutoff = cutoff
+ cutoff <- terGetCutOff
+ let ?cutoff = cutoff
- -- We work in TCM exclusively.
- liftTCM $ do
+ -- We work in TCM exclusively.
+ liftTCM $ do
- reportS "term.lex" 20 $ unlines
- [ "Calls (" ++ no ++ "dot patterns): " ++ show calls
- ]
+ reportS "term.lex" 20 $ unlines
+ [ "Calls (" ++ no ++ "dot patterns): " ++ show calls
+ ]
- -- Print the whole completion phase.
- verboseS "term.matrices" 40 $ do
- let header s = unlines
- [ replicate n '='
- , replicate k '=' ++ s ++ replicate k' '='
- , replicate n '='
- ]
- where n = 70
- r = n - length s
- k = r `div` 2
- k' = r - k
- let report s cs = reportSDoc "term.matrices" 40 $ vcat
- [ text $ header s
- , nest 2 $ pretty cs
- ]
- cs0 = calls
- step cs = do
- let (new, cs') = completionStep cs0 cs
- report " New call matrices " new
- return $ if CallGraph.null new then Left () else Right cs'
- report " Initial call matrices " cs0
- trampolineM step cs0
-
- -- Print the result of completion.
- let calls' = CallGraph.complete calls
- idems = filter idempotent $ endos $ CallGraph.toList calls'
- -- TODO
- -- reportSDoc "term.behaviours" 20 $ vcat
- -- [ text $ "Recursion behaviours (" ++ no ++ "dot patterns):"
- -- , nest 2 $ return $ Term.prettyBehaviour calls'
- -- ]
- reportSDoc "term.matrices" 30 $ vcat
- [ text $ "Idempotent call matrices (" ++ no ++ "dot patterns):\n"
- , nest 2 $ vcat $ punctuate (text "\n") $ map pretty idems
- ]
- -- reportSDoc "term.matrices" 30 $ vcat
- -- [ text $ "Other call matrices (" ++ no ++ "dot patterns):"
- -- , nest 2 $ pretty $ CallGraph.fromList others
- -- ]
- return ()
+ -- Print the whole completion phase.
+ verboseS "term.matrices" 40 $ do
+ let header s = unlines
+ [ replicate n '='
+ , replicate k '=' ++ s ++ replicate k' '='
+ , replicate n '='
+ ]
+ where n = 70
+ r = n - length s
+ k = r `div` 2
+ k' = r - k
+ let report s cs = reportSDoc "term.matrices" 40 $ vcat
+ [ text $ header s
+ , nest 2 $ pretty cs
+ ]
+ cs0 = calls
+ step cs = do
+ let (new, cs') = completionStep cs0 cs
+ report " New call matrices " new
+ return $ if null new then Left () else Right cs'
+ report " Initial call matrices " cs0
+ trampolineM step cs0
+
+ -- Print the result of completion.
+ let calls' = CallGraph.complete calls
+ idems = filter idempotent $ endos $ CallGraph.toList calls'
+ -- TODO
+ -- reportSDoc "term.behaviours" 20 $ vcat
+ -- [ text $ "Recursion behaviours (" ++ no ++ "dot patterns):"
+ -- , nest 2 $ return $ Term.prettyBehaviour calls'
+ -- ]
+ reportSDoc "term.matrices" 30 $ vcat
+ [ text $ "Idempotent call matrices (" ++ no ++ "dot patterns):\n"
+ , nest 2 $ vcat $ punctuate (text "\n") $ map pretty idems
+ ]
+ -- reportSDoc "term.matrices" 30 $ vcat
+ -- [ text $ "Other call matrices (" ++ no ++ "dot patterns):"
+ -- , nest 2 $ pretty $ CallGraph.fromList others
+ -- ]
+ return ()
-- | @termFunction name@ checks @name@ for termination.
termFunction :: QName -> TerM Result
termFunction name = do
- -- Function @name@ is henceforth referred to by its @index@
- -- in the list of @allNames@ of the mutual block.
-
- allNames <- terGetMutual
- let index = fromMaybe __IMPOSSIBLE__ $ List.elemIndex name allNames
-
- -- Retrieve the target type of the function to check.
-
- target <- liftTCM $ do typeEndsInDef =<< typeOfConst name
- reportTarget target
- terSetTarget target $ do
-
- -- Collect the recursive calls in the block which (transitively)
- -- involve @name@,
- -- taking the target of @name@ into account for computing guardedness.
-
- let collect = (`trampolineM` (Set.singleton index, mempty, mempty)) $ \ (todo, done, calls) -> do
- if null todo then return $ Left calls else do
- -- Extract calls originating from indices in @todo@.
- new <- forM' todo $ \ i ->
- termDef $ fromMaybe __IMPOSSIBLE__ $ allNames !!! i
- -- Mark those functions as processed and add the calls to the result.
- let done' = done `mappend` todo
- calls' = new `mappend` calls
- -- Compute the new todo list:
- todo' = CallGraph.targetNodes new Set.\\ done'
- -- Jump the trampoline.
- return $ Right (todo', done', calls')
-
- -- First try to termination check ignoring the dot patterns
- calls1 <- terSetUseDotPatterns False $ collect
- reportCalls "no " calls1
-
- r <- do
- cutoff <- terGetCutOff
- let ?cutoff = cutoff
- r <- billToTerGraph $ Term.terminatesFilter (== index) calls1
- case r of
- Right () -> return $ Right ()
- Left{} -> do
- -- Try again, but include the dot patterns this time.
- calls2 <- terSetUseDotPatterns True $ collect
- reportCalls "" calls2
- billToTerGraph $ mapLeft callInfos $ Term.terminatesFilter (== index) calls2
-
- names <- terGetUserNames
+ -- Function @name@ is henceforth referred to by its @index@
+ -- in the list of @allNames@ of the mutual block.
+
+ allNames <- terGetMutual
+ let index = fromMaybe __IMPOSSIBLE__ $ List.elemIndex name allNames
+
+ -- Retrieve the target type of the function to check.
+
+ target <- liftTCM $ do typeEndsInDef =<< typeOfConst name
+ reportTarget target
+ terSetTarget target $ do
+
+ -- Collect the recursive calls in the block which (transitively)
+ -- involve @name@,
+ -- taking the target of @name@ into account for computing guardedness.
+
+ let collect = (`trampolineM` (Set.singleton index, mempty, mempty)) $ \ (todo, done, calls) -> do
+ if null todo then return $ Left calls else do
+ -- Extract calls originating from indices in @todo@.
+ new <- forM' todo $ \ i ->
+ termDef $ fromMaybe __IMPOSSIBLE__ $ allNames !!! i
+ -- Mark those functions as processed and add the calls to the result.
+ let done' = done `mappend` todo
+ calls' = new `mappend` calls
+ -- Compute the new todo list:
+ todo' = CallGraph.targetNodes new Set.\\ done'
+ -- Jump the trampoline.
+ return $ Right (todo', done', calls')
+
+ -- First try to termination check ignoring the dot patterns
+ calls1 <- terSetUseDotPatterns False $ collect
+ reportCalls "no " calls1
+
+ r <- do
+ cutoff <- terGetCutOff
+ let ?cutoff = cutoff
+ r <- billToTerGraph $ Term.terminatesFilter (== index) calls1
case r of
- Left calls -> do
- return $ point $ TerminationError
- { termErrFunctions = if name `elem` names then [name] else []
- , termErrCalls = calls
- }
- Right () -> do
- liftTCM $ reportSLn "term.warn.yes" 2 $
- show (name) ++ " does termination check"
- return mempty
- where
- reportTarget r = liftTCM $
- reportSLn "term.target" 20 $ " target type " ++
- caseMaybe r "not recognized" (\ q ->
- "ends in " ++ show q)
+ Right () -> return $ Right ()
+ Left{} -> do
+ -- Try again, but include the dot patterns this time.
+ calls2 <- terSetUseDotPatterns True $ collect
+ reportCalls "" calls2
+ billToTerGraph $ mapLeft callInfos $ Term.terminatesFilter (== index) calls2
+
+ names <- terGetUserNames
+ case r of
+ Left calls -> return $ singleton $ terminationError ([name] `intersect` names) calls
+ Right () -> do
+ liftTCM $ reportSLn "term.warn.yes" 2 $
+ show name ++ " does termination check"
+ return mempty
+ where
+ reportTarget r = liftTCM $
+ reportSLn "term.target" 20 $ " target type " ++
+ caseMaybe r "not recognized" (\ q ->
+ "ends in " ++ show q)
-- | To process the target type.
typeEndsInDef :: MonadTCM tcm => Type -> tcm (Maybe QName)
@@ -451,13 +427,13 @@ termDef name = terSetCurrent name $ do
applyWhen withoutKEnabled (setMasks t) $ do
-- If the result should be disregarded, set all calls to unguarded.
- applyUnlessM terGetMaskResult terUnguarded $ do
+ applyWhenM terGetMaskResult terUnguarded $ do
case theDef def of
Function{ funClauses = cls, funDelayed = delayed } ->
terSetDelayed delayed $ forM' cls $ termClause
- _ -> return CallGraph.empty
+ _ -> return empty
-- | Mask arguments and result for termination checking
-- according to type of function.
@@ -469,13 +445,19 @@ setMasks t cont = do
-- Check argument types
ds <- forM (telToList tel) $ \ t -> do
TelV _ t <- telView $ snd $ unDom t
- (isJust <$> isDataOrRecord (unEl t)) `or2M` (isJust <$> isSizeType t)
+ d <- (isNothing <$> isDataOrRecord (unEl t)) `or2M` (isJust <$> isSizeType t)
+ when d $
+ reportSDoc "term.mask" 20 $ do
+ text "argument type "
+ <+> prettyTCM t
+ <+> text " is not data or record type, ignoring structural descent for --without-K"
+ return d
-- Check result types
- d <- isJust <.> isDataOrRecord . unEl $ core
- unless d $
+ d <- isNothing <.> isDataOrRecord . unEl $ core
+ when d $
reportSLn "term.mask" 20 $ "result type is not data or record type, ignoring guardedness for --without-K"
return (ds, d)
- terSetMaskArgs (ds ++ repeat False) $ terSetMaskResult d $ cont
+ terSetMaskArgs (ds ++ repeat True) $ terSetMaskResult d $ cont
{- Termination check clauses:
@@ -560,11 +542,11 @@ stripCoConstructors p = do
ProjDBP{} -> return p
-- | Masks all non-data/record type patterns if --without-K.
-maskNonDataArgs :: [DeBruijnPat] -> TerM [DeBruijnPat]
+maskNonDataArgs :: [DeBruijnPat] -> TerM [Masked DeBruijnPat]
maskNonDataArgs ps = zipWith mask ps <$> terGetMaskArgs
where
- mask p@ProjDBP{} _ = p
- mask p d = if d then p else unusedVar
+ mask p@ProjDBP{} _ = Masked False p
+ mask p d = Masked d p
-- | cf. 'TypeChecking.Coverage.Match.buildMPatterns'
openClause :: Permutation -> [Pattern] -> ClauseBody -> TerM ([DeBruijnPat], Maybe Term)
@@ -595,9 +577,9 @@ openClause perm ps body = do
termClause :: Clause -> TerM Calls
termClause clause = do
ifNotM (terGetInlineWithFunctions) (termClause' clause) $ {- else -} do
- name <- terGetCurrent
- ifM (isJust <$> do isWithFunction name) (return mempty) $ do
- mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause
+ name <- terGetCurrent
+ ifM (isJust <$> do isWithFunction name) (return mempty) $ do
+ mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause
termClause' :: Clause -> TerM Calls
termClause' clause = do
@@ -616,11 +598,12 @@ termClause' clause = do
ps <- liftTCM $ normalise $ map unArg argPats'
(dbpats, res) <- openClause perm ps body
case res of
- Nothing -> return CallGraph.empty
+ Nothing -> return empty
Just v -> do
dbpats <- mapM stripCoConstructors dbpats
- dbpats <- maskNonDataArgs dbpats
- terSetPatterns dbpats $ do
+ mdbpats <- maskNonDataArgs dbpats
+ terSetPatterns mdbpats $ do
+ terSetSizeDepth tel $ do
reportBody v
{-
-- if we are checking a delayed definition, we treat it as if there were
@@ -704,7 +687,7 @@ instance ExtractCalls a => ExtractCalls (I.Dom a) where
extract = extract . unDom
instance ExtractCalls a => ExtractCalls (Elim' a) where
- extract Proj{} = return CallGraph.empty
+ extract Proj{} = return empty
extract (Apply a) = extract $ unArg a
instance ExtractCalls a => ExtractCalls [a] where
@@ -726,8 +709,9 @@ instance ExtractCalls Sort where
reportSDoc "term.sort" 50 $
text ("s = " ++ show s)
case s of
- Prop -> return CallGraph.empty
- Inf -> return CallGraph.empty
+ Prop -> return empty
+ Inf -> return empty
+ SizeUniv -> return empty
Type t -> terUnguarded $ extract t -- no guarded levels
DLub s1 s2 -> extract (s1, s2)
@@ -897,7 +881,10 @@ function g es = ifM (terGetInlineWithFunctions `and2M` do isJust <$> isWithFunct
-- So we build a closure such that we can print the call
-- whenever we really need to.
-- This saves 30s (12%) on the std-lib!
- doc <- liftTCM $ buildClosure gArgs
+ -- Andreas, 2015-01-21 Issue 1410: Go to the module where g is defined
+ -- otherwise its free variables with be prepended to the call
+ -- in the error message.
+ doc <- liftTCM $ withCurrentModule (qnameModule g) $ buildClosure gArgs
let src = fromMaybe __IMPOSSIBLE__ $ List.elemIndex f names
tgt = gInd
@@ -967,14 +954,14 @@ instance ExtractCalls Term where
<*> terPiGuarded (extract b)
-- Literal.
- Lit l -> return CallGraph.empty
+ Lit l -> return empty
-- Sort.
Sort s -> extract s
-- Unsolved metas are not considered termination problems, there
-- will be a warning for them anyway.
- MetaV x args -> return CallGraph.empty
+ MetaV x args -> return empty
-- Erased and not-yet-erased proof.
DontCare t -> extract t
@@ -998,7 +985,7 @@ instance ExtractCalls PlusLevel where
instance ExtractCalls LevelAtom where
extract (MetaLevel x es) = extract es
extract (BlockedLevel x t) = extract t
- extract (NeutralLevel t) = extract t
+ extract (NeutralLevel _ t) = extract t
extract (UnreducedLevel t) = extract t
-- | Rewrite type @tel -> Size< u@ to @tel -> Size@.
@@ -1033,18 +1020,21 @@ compareArgs es = do
-- matrix <- forM es $ \ e -> forM apats $ \ (b, p) -> terSetUseSizeLt b $ compareElim e p
matrix <- withUsableVars pats $ forM es $ \ e -> forM pats $ \ p -> compareElim e p
- -- Count the number of coinductive projection(pattern)s in caller and callee
+ -- Count the number of coinductive projection(pattern)s in caller and callee.
+ -- Only recursive coinductive projections are eligible (Issue 1209).
projsCaller <- genericLength <$> do
- filterM isCoinductiveProjection $ mapMaybe isProjP pats
- -- filterM (not <.> isProjectionButNotCoinductive) $ mapMaybe isProjP pats
+ filterM (isCoinductiveProjection True) $ mapMaybe (isProjP . getMasked) pats
projsCallee <- genericLength <$> do
- filterM isCoinductiveProjection $ mapMaybe isProjElim es
- -- filterM (not <.> isProjectionButNotCoinductive) $ mapMaybe isProjElim es
+ filterM (isCoinductiveProjection True) $ mapMaybe isProjElim es
cutoff <- terGetCutOff
let ?cutoff = cutoff
let guardedness = decr $ projsCaller - projsCallee
- liftTCM $ reportSLn "term.guardedness" 30 $
- "compareArgs: guardedness of call: " ++ show guardedness
+ liftTCM $ reportSDoc "term.guardedness" 30 $ sep
+ [ text "compareArgs:"
+ , nest 2 $ text $ "projsCaller = " ++ show projsCaller
+ , nest 2 $ text $ "projsCallee = " ++ show projsCallee
+ , nest 2 $ text $ "guardedness of call: " ++ show guardedness
+ ]
return $ addGuardedness guardedness (size es) (size pats) matrix
-- | Traverse patterns from left to right.
@@ -1063,7 +1053,7 @@ annotatePatsWithUseSizeLt = loop where
-- | @compareElim e dbpat@
-compareElim :: Elim -> DeBruijnPat -> TerM Order
+compareElim :: Elim -> Masked DeBruijnPat -> TerM Order
compareElim e p = do
liftTCM $ do
reportSDoc "term.compare" 30 $ sep
@@ -1075,11 +1065,11 @@ compareElim e p = do
[ nest 2 $ text $ "e = " ++ show e
, nest 2 $ text $ "p = " ++ show p
]
- case (e, p) of
+ case (e, getMasked p) of
(Proj d, ProjDBP d') -> compareProj d d'
(Proj{}, _ ) -> return Order.unknown
(Apply{}, ProjDBP{}) -> return Order.unknown
- (Apply arg, p) -> compareTerm (unArg arg) p
+ (Apply arg, _) -> compareTerm (unArg arg) p
-- | In dependent records, the types of later fields may depend on the
-- values of earlier fields. Thus when defining an inhabitant of a
@@ -1153,7 +1143,7 @@ subPatterns p = case p of
TermDBP _ -> []
ProjDBP _ -> []
-compareTerm :: Term -> DeBruijnPat -> TerM Order
+compareTerm :: Term -> Masked DeBruijnPat -> TerM Order
compareTerm t p = do
-- reportSDoc "term.compare" 25 $
-- text " comparing term " <+> prettyTCM t <+>
@@ -1215,8 +1205,8 @@ instance StripAllProjections Term where
--
-- Precondition: top meta variable resolved
-compareTerm' :: Term -> DeBruijnPat -> TerM Order
-compareTerm' v p = do
+compareTerm' :: Term -> Masked DeBruijnPat -> TerM Order
+compareTerm' v mp@(Masked m p) = do
suc <- terGetSizeSuc
cutoff <- terGetCutOff
let ?cutoff = cutoff
@@ -1225,21 +1215,47 @@ compareTerm' v p = do
-- Andreas, 2013-11-20 do not drop projections,
-- in any case not coinductive ones!:
- (Var i es, p) | Just{} <- allApplyElims es ->
- compareVar i p
+ (Var i es, _) | Just{} <- allApplyElims es ->
+ compareVar i mp
+
+ (DontCare t, _) ->
+ compareTerm' t mp
+
+ -- Andreas, 2014-09-22, issue 1281:
+ -- For metas, termination checking should be optimistic.
+ -- If there is any instance of the meta making termination
+ -- checking succeed, then we should not fail.
+ -- Thus, we assume the meta will be instantiated with the
+ -- deepest variable in @p@.
+ -- For sized types, the depth is maximally
+ -- the number of SIZELT hypotheses one can have in a context.
+ (MetaV{}, p) -> Order.decr . max (if m then 0 else patternDepth p) . pred <$>
+ terAsks _terSizeDepth
+
+ -- Successor on both sides cancel each other.
+ -- We ignore the mask for sizes.
+ (Def s [Apply t], ConDBP s' [p]) | s == s' && Just s == suc ->
+ compareTerm' (unArg t) (notMasked p)
+
+ -- Register also size increase.
+ (Def s [Apply t], p) | Just s == suc ->
+ -- Andreas, 2012-10-19 do not cut off here
+ increase 1 <$> compareTerm' (unArg t) mp
- (DontCare t, p) ->
- compareTerm' t p
+ -- In all cases that do not concern sizes,
+ -- we cannot continue if pattern is masked.
+
+ _ | m -> return Order.unknown
(Lit l, LitDBP l')
| l == l' -> return Order.le
| otherwise -> return Order.unknown
- (Lit l, p) -> do
+ (Lit l, _) -> do
v <- liftTCM $ constructorForm v
case ignoreSharing v of
Lit{} -> return Order.unknown
- v -> compareTerm' v p
+ v -> compareTerm' v mp
-- Andreas, 2011-04-19 give subterm priority over matrix order
@@ -1249,30 +1265,13 @@ compareTerm' v p = do
(Con c ts, ConDBP c' ps) | conName c == c'->
compareConArgs ts ps
- (Def s [Apply t], ConDBP s' [p]) | s == s' && Just s == suc ->
- compareTerm' (unArg t) p
+ (Con c [], _) -> return Order.le
- -- new cases for counting constructors / projections
+ -- new case for counting constructors / projections
-- register also increase
- (Def s [Apply t], p) | Just s == suc ->
- -- Andreas, 2012-10-19 do not cut off here
- increase 1 <$> compareTerm' (unArg t) p
-
- (Con c [], p) -> return Order.le
-
- (Con c ts, p) -> do
+ (Con c ts, _) -> do
increase <$> offsetFromConstructor (conName c)
- <*> (infimum <$> mapM (\ t -> compareTerm' (unArg t) p) ts)
-
- -- Andreas, 2014-09-22, issue 1281:
- -- For metas, termination checking should be optimistic.
- -- If there is any instance of the meta making termination
- -- checking succeed, then we should not fail.
- -- Thus, we assume the meta will be instantiated with the
- -- deepest variable in @p@.
- -- For sized types, the depth is maximally context length - 1,
- -- which is the number of SIZELT hypotheses one can have in a context.
- (MetaV{}, p) -> Order.decr . max (patternDepth p) . pred <$> getContextSize
+ <*> (infimum <$> mapM (\ t -> compareTerm' (unArg t) mp) ts)
(t, p) -> return $ subTerm t p
@@ -1310,9 +1309,9 @@ compareConArgs ts ps = do
(0,0) -> return Order.le -- c <= c
(0,1) -> return Order.unknown -- c not<= c x
(1,0) -> __IMPOSSIBLE__
- (1,1) -> compareTerm' (unArg (head ts)) (head ps)
+ (1,1) -> compareTerm' (unArg (head ts)) (notMasked (head ps))
(_,_) -> foldl (Order..*.) Order.le <$>
- zipWithM compareTerm' (map unArg ts) ps
+ zipWithM compareTerm' (map unArg ts) (map notMasked ps)
-- corresponds to taking the size, not the height
-- allows examples like (x, y) < (Succ x, y)
{- version which does an "order matrix"
@@ -1329,25 +1328,34 @@ compareConArgs ts ps = do
-- else Order.infimum (zipWith compareTerm' (map unArg ts) ps)
-}
-compareVar :: Nat -> DeBruijnPat -> TerM Order
-compareVar i (VarDBP j) = compareVarVar i j
-compareVar i (ConDBP c ps) = do
+compareVar :: Nat -> Masked DeBruijnPat -> TerM Order
+compareVar i (Masked m p) = do
+ suc <- terGetSizeSuc
cutoff <- terGetCutOff
let ?cutoff = cutoff
- decrease <$> offsetFromConstructor c
- <*> (Order.supremum <$> mapM (compareVar i) ps)
-compareVar i LitDBP{} = return $ Order.unknown
-compareVar i TermDBP{} = return $ Order.unknown
-compareVar i ProjDBP{} = return $ Order.unknown
+ let no = return Order.unknown
+ case p of
+ ProjDBP{} -> no
+ LitDBP{} -> no
+ TermDBP{} -> no
+ VarDBP j -> compareVarVar i (Masked m j)
+ ConDBP s [p] | Just s == suc -> decrease 1 <$> compareVar i (notMasked p)
+ ConDBP c ps -> if m then no else do
+ decrease <$> offsetFromConstructor c
+ <*> (Order.supremum <$> mapM (compareVar i . notMasked) ps)
-- | Compare two variables.
--
-- The first variable comes from a term, the second from a pattern.
-compareVarVar :: Nat -> Nat -> TerM Order
-compareVarVar i j
- | i == j = return Order.le
+compareVarVar :: Nat -> Masked Nat -> TerM Order
+compareVarVar i (Masked m j)
+ | i == j = if not m then return Order.le else liftTCM $
+ -- If j is a size, we ignore the mask.
+ ifM (isJust <$> do isSizeType =<< reduce =<< typeOfBV j)
+ {- then -} (return Order.le)
+ {- else -} (return Order.unknown)
| otherwise = ifNotM ((i `VarSet.member`) <$> terGetUsableVars) (return Order.unknown) $ {- else -} do
res <- isBounded i
case res of
BoundedNo -> return Order.unknown
- BoundedLt v -> decrease 1 <$> compareTerm' v (VarDBP j)
+ BoundedLt v -> decrease 1 <$> compareTerm' v (Masked m (VarDBP j))