module Agda.Termination.TermCheck
( termDecls
, Result, DeBruijnPat
) where
import Control.Applicative
import Control.Monad.Error
import Data.List as List
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Maybe as Maybe
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal (Literal(LitString))
import Agda.Termination.CallGraph as Term
import qualified Agda.Termination.SparseMatrix as Term
import qualified Agda.Termination.Termination as Term
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull)
import Agda.TypeChecking.Records (isRecordConstructor)
import Agda.TypeChecking.Rules.Builtin.Coinduction
import Agda.TypeChecking.Rules.Term (isType_)
import Agda.TypeChecking.Substitute (abstract,raise,substs)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Signature (isProjection)
import Agda.TypeChecking.Primitive (constructorForm)
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Substitute
import qualified Agda.Interaction.Highlighting.Range as R
import Agda.Interaction.Options
import Agda.Utils.Size
import Agda.Utils.Monad (thread, (<$>), ifM)
#include "../undefined.h"
import Agda.Utils.Impossible
type Calls = Term.CallGraph (Set CallInfo)
type MutualNames = [QName]
type Result = [TerminationError]
termDecls :: [A.Declaration] -> TCM Result
termDecls ds = fmap concat $ mapM termDecl ds
termDecl :: A.Declaration -> TCM Result
termDecl (A.ScopedDecl scope ds) = do
setScope scope
termDecls ds
termDecl d = case d of
A.Axiom {} -> return []
A.Field {} -> return []
A.Primitive {} -> return []
A.Mutual _ ds
| [A.RecSig{}, A.RecDef _ r _ _ _ rds] <- unscopeDefs ds
-> do
let m = mnameFromList $ qnameToList r
setScopeFromDefs ds
termSection m rds
A.Mutual i ds -> termMutual i ds
A.Section _ x _ ds -> termSection x ds
A.Apply {} -> return []
A.Import {} -> return []
A.Pragma {} -> return []
A.Open {} -> return []
A.ScopedDecl{} -> __IMPOSSIBLE__
A.FunDef{} -> __IMPOSSIBLE__
A.DataSig{} -> __IMPOSSIBLE__
A.DataDef{} -> __IMPOSSIBLE__
A.RecSig{} -> __IMPOSSIBLE__
A.RecDef{} -> __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]
collectCalls :: (a -> TCM Calls) -> [a] -> TCM Calls
collectCalls f [] = return Term.empty
collectCalls f (a : as) = do c1 <- f a
c2 <- collectCalls f as
return (c1 `Term.union` c2)
termMutual :: Info.DeclInfo -> [A.Declaration] -> TCM Result
termMutual i ds = if names == [] then return [] else
do
cutoff <- optTerminationDepth <$> pragmaOptions
let ?cutoff = cutoff
reportSLn "term.top" 10 $ "Termination checking " ++ show names ++
" with cutoff=" ++ show cutoff ++ "..."
mutualBlock <- findMutualBlock (head names)
let allNames = Set.elems mutualBlock
let collect use = collectCalls (termDef use allNames) allNames
suc <- sizeSuc
sharp <- fmap nameOfSharp <$> coinductionKit
guardingTypeConstructors <-
optGuardingTypeConstructors <$> pragmaOptions
let conf = DBPConf
{ useDotPatterns = False
, guardingTypeConstructors = guardingTypeConstructors
, withSizeSuc = suc
, sharp = sharp
}
calls1 <- collect conf{ useDotPatterns = False }
reportS "term.lex" 20 $ unlines
[ "Calls (no dot patterns): " ++ show calls1
]
reportSDoc "term.behaviours" 20 $ vcat
[ text "Recursion behaviours (no dot patterns):"
, nest 2 $ return $ Term.prettyBehaviour (Term.complete calls1)
]
reportSDoc "term.matrices" 30 $ vcat
[ text "Call matrices (no dot patterns):"
, nest 2 $ pretty $ Term.complete calls1
]
r <- do let r = Term.terminates calls1
case r of
Right _ -> return r
Left _ -> do
calls2 <- collect conf{ useDotPatterns = True }
reportS "term.lex" 20 $ unlines
[ "Calls (dot patterns): " ++ show calls2
]
reportSDoc "term.behaviours" 20 $ vcat
[ text "Recursion behaviours (dot patterns):"
, nest 2 $ return $
Term.prettyBehaviour (Term.complete calls2)
]
reportSDoc "term.matrices" 30 $ vcat
[ text "Call matrices (dot patterns):"
, nest 2 $ pretty $ Term.complete calls2
]
return $ Term.terminates calls2
case r of
Left calls -> do
return [TerminationError
{ termErrFunctions = names
, termErrCalls = Set.toList calls
}
]
Right _ -> do
reportSLn "term.warn.yes" 2
(show (names) ++ " does termination check")
return []
where
getName (A.FunDef i x cs) = [x]
getName (A.RecDef _ _ _ _ _ ds) = concatMap getName ds
getName (A.Mutual _ ds) = concatMap getName ds
getName (A.Section _ _ _ ds) = concatMap getName ds
getName (A.ScopedDecl _ ds) = concatMap getName ds
getName _ = []
names = concatMap getName ds
concat' :: Ord a => [Set a] -> [a]
concat' = Set.toList . Set.unions
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
termDef :: DBPConf -> MutualNames -> QName -> TCM Calls
termDef use names name = do
def <- getConstInfo name
reportSDoc "term.def.fun" 5 $
sep [ text "termination checking body of" <+> prettyTCM name
, nest 2 $ text ":" <+> (prettyTCM $ defType def)
]
case (theDef def) of
Function{ funClauses = cls } ->
collectCalls (termClause use names name) cls
_ -> return Term.empty
data DeBruijnPat = VarDBP Nat
| ConDBP QName [DeBruijnPat]
| LitDBP Literal
instance PrettyTCM DeBruijnPat where
prettyTCM (VarDBP i) = text $ show i
prettyTCM (ConDBP c ps) = parens (prettyTCM c <+> hsep (map prettyTCM ps))
prettyTCM (LitDBP l) = prettyTCM l
unusedVar :: DeBruijnPat
unusedVar = LitDBP (LitString noRange "term.unused.pat.var")
adjIndexDBP :: (Nat -> Nat) -> DeBruijnPat -> DeBruijnPat
adjIndexDBP f (VarDBP i) = VarDBP (f i)
adjIndexDBP f (ConDBP c args) = ConDBP c (map (adjIndexDBP f) args)
adjIndexDBP f (LitDBP l) = LitDBP l
liftDBP :: DeBruijnPat -> DeBruijnPat
liftDBP = adjIndexDBP (1+)
data DBPConf = DBPConf { useDotPatterns :: Bool
, guardingTypeConstructors :: Bool
, withSizeSuc :: Maybe QName
, sharp :: Maybe QName
}
termToDBP :: DBPConf -> Term -> TCM DeBruijnPat
termToDBP conf t
| not $ useDotPatterns conf = return $ unusedVar
| otherwise = do
t <- stripProjections =<< constructorForm t
case t of
Var i [] -> return $ VarDBP i
Con c args -> ConDBP c <$> mapM (termToDBP conf . unArg) args
Def s [arg]
| Just s == withSizeSuc conf -> ConDBP s . (:[]) <$> termToDBP conf (unArg arg)
Lit l -> return $ LitDBP l
_ -> return unusedVar
stripCoConstructors :: DBPConf -> DeBruijnPat -> TCM DeBruijnPat
stripCoConstructors conf p = case p of
VarDBP _ -> return p
LitDBP _ -> return p
ConDBP c args -> do
ind <- if withSizeSuc conf == Just c then
return Inductive
else
whatInduction c
case ind of
Inductive -> ConDBP c <$> mapM (stripCoConstructors conf) args
CoInductive -> return unusedVar
stripBind :: DBPConf -> Nat -> Pattern -> ClauseBody -> TCM (Maybe (Nat, DeBruijnPat, ClauseBody))
stripBind _ _ _ NoBody = return Nothing
stripBind conf i (VarP x) (Bind b) = return $ Just (i 1, VarDBP i, absBody b)
stripBind conf i (VarP x) (Body b) = __IMPOSSIBLE__
stripBind conf i (DotP t) (Bind b) = do
t <- termToDBP conf t
return $ Just (i 1, t, absBody b)
stripBind conf i (DotP _) (Body b) = __IMPOSSIBLE__
stripBind conf i (LitP l) b = return $ Just (i, LitDBP l, b)
stripBind conf i (ConP c _ args) b = do
r <- stripBinds conf i (map unArg args) b
case r of
Just (i', dbps, b') -> return $ Just (i', ConDBP c dbps, b')
_ -> return Nothing
stripBinds :: DBPConf -> Nat -> [Pattern] -> ClauseBody -> TCM (Maybe (Nat, [DeBruijnPat], ClauseBody))
stripBinds use i [] b = return $ Just (i, [], b)
stripBinds use i (p:ps) b = do
r1 <- stripBind use i p b
case r1 of
Just (i1, dbp, b1) -> do
r2 <- stripBinds use i1 ps b1
case r2 of
Just (i2, dbps, b2) -> return $ Just (i2, dbp:dbps, b2)
Nothing -> return Nothing
Nothing -> return Nothing
termClause :: DBPConf -> MutualNames -> QName -> Clause -> TCM Calls
termClause use names name (Clause { clauseTel = tel
, clausePerm = perm
, clausePats = argPats'
, clauseBody = body }) =
addCtxTel tel $ do
argPats' <- normalise argPats'
let argPats = substs (renamingR perm) argPats'
dbs <- stripBinds use (nVars 1) (map unArg argPats) body
case dbs of
Nothing -> return Term.empty
Just (1, dbpats, Body t) -> do
dbpats <- mapM (stripCoConstructors use) dbpats
termTerm use names name dbpats t
Just (n, dbpats, Body t) -> internalError $ "termClause: misscalculated number of vars: guess=" ++ show nVars ++ ", real=" ++ show (nVars 1 n)
Just (n, dbpats, b) -> internalError $ "termClause: not a Body"
where
nVars = boundVars body
boundVars (Bind b) = 1 + boundVars (absBody b)
boundVars NoBody = 0
boundVars (Body _) = 0
termTerm :: DBPConf -> MutualNames -> QName -> [DeBruijnPat] -> Term -> TCM Calls
termTerm conf names f pats0 t0 = do
cutoff <- optTerminationDepth <$> pragmaOptions
let ?cutoff = cutoff
do
reportSDoc "term.check.clause" 6
(sep [ text "termination checking clause of" <+> prettyTCM f
, nest 2 $ text "lhs:" <+> hsep (map prettyTCM pats0)
, nest 2 $ text "rhs:" <+> prettyTCM t0
])
loop pats0 Term.le t0
where
Just fInd = toInteger <$> List.elemIndex f names
loopSort :: (?cutoff :: Int) => [DeBruijnPat] -> Sort -> TCM Calls
loopSort pats s = do
case s of
Type (Max []) -> return Term.empty
Type (Max [ClosedLevel _]) -> return Term.empty
Type t -> loop pats Term.unknown (Level t)
Prop -> return Term.empty
Inf -> return Term.empty
DLub s1 (NoAbs x s2) -> Term.union <$> loopSort pats s1 <*> loopSort pats s2
DLub s1 (Abs x s2) -> liftM2 Term.union
(loopSort pats s1)
(addCtxString x __IMPOSSIBLE__ $ loopSort (map liftDBP pats) s2)
loopType :: (?cutoff :: Int) => [DeBruijnPat] -> Order -> Type -> TCM Calls
loopType pats guarded (El s t) = liftM2 Term.union
(loopSort pats s)
(loop pats guarded t)
loop
:: (?cutoff :: Int)
=> [DeBruijnPat]
-> Order
-> Term
-> TCM Calls
loop pats guarded t = do
t <- instantiate t
suc <- sizeSuc
let constructor
:: QName
-> Induction
-> [(Arg Term, Bool)]
-> TCM Calls
constructor c ind args = collectCalls loopArg args
where
loopArg (arg , preserves) = do
loop pats g' (unArg arg)
where g' = case (preserves, ind) of
(True, Inductive) -> guarded
(True, CoInductive) -> Term.lt .*. guarded
(False, _) -> Term.unknown
function :: QName -> [Arg Term] -> TCM Calls
function g args0 = do
let args1 = map unArg args0
args2 <- mapM instantiateFull args1
let reduceCon (Con c vs) = (`apply` vs) <$> reduce (Con c [])
reduceCon t = return t
args2 <- mapM reduceCon args2
args <- mapM etaContract args2
isProj <- isProjection g
let unguards = repeat Term.unknown
let guards = maybe unguards
(\ _ -> guarded : unguards)
isProj
calls <- collectCalls (uncurry (loop pats)) (zip guards args)
reportSDoc "term.found.call" 20
(sep [ text "found call from" <+> prettyTCM f
, nest 2 $ text "to" <+> prettyTCM g
])
case List.elemIndex g names of
Nothing -> return calls
Just gInd' -> do
matrix <- compareArgs suc pats args
let (nrows, ncols, matrix') = addGuardedness guarded
(genericLength args)
(genericLength pats)
matrix
reportSDoc "term.kept.call" 5
(sep [ text "kept call from" <+> prettyTCM f
<+> hsep (map prettyTCM pats)
, nest 2 $ text "to" <+> prettyTCM g <+>
hsep (map (parens . prettyTCM) args)
, nest 2 $ text ("call matrix (with guardedness): " ++ show matrix')
])
doc <- prettyTCM (Def g args0)
return
(Term.insert
(Term.Call { Term.source = fInd
, Term.target = toInteger gInd'
, Term.cm = makeCM ncols nrows matrix'
})
(Set.singleton
(CallInfo { callInfoRange = getRange g
, callInfoCall = show doc
}))
calls)
case t of
Con c args
| Just c == sharp conf ->
constructor c CoInductive $ zip args (repeat True)
| otherwise ->
constructor c Inductive $ zip args (repeat True)
Def g args0
| guardingTypeConstructors conf -> do
gDef <- theDef <$> getConstInfo g
case gDef of
Datatype {dataArgOccurrences = occs} -> con occs
Record {recArgOccurrences = occs} -> con occs
_ -> fun
| otherwise -> fun
where
con occs =
constructor g Inductive $
zip args0 (map preserves occs ++ repeat False)
where
preserves Positive = True
preserves Negative = False
preserves Unused = True
fun = function g args0
Lam h (Abs x t) -> addCtxString x (Arg { argHiding = h
, argRelevance = __IMPOSSIBLE__
, unArg = __IMPOSSIBLE__
}) $
loop (map liftDBP pats) guarded t
Lam h (NoAbs _ t) -> loop pats guarded t
Var i args -> collectCalls (loop pats Term.unknown) (map unArg args)
Pi a (Abs x b) ->
do g1 <- loopType pats Term.unknown (unArg a)
g2 <- addCtxString x a $
loopType (map liftDBP pats) piArgumentGuarded b
return $ g1 `Term.union` g2
Pi a (NoAbs _ b) ->
do g1 <- loopType pats Term.unknown (unArg a)
g2 <- loopType pats piArgumentGuarded b
return $ g1 `Term.union` g2
Lit l -> return Term.empty
Sort s -> loopSort pats s
MetaV x args -> return Term.empty
DontCare t -> loop pats guarded t
Level l -> loop pats guarded =<< reallyUnLevelView l
where
piArgumentGuarded =
if guardingTypeConstructors conf then
guarded
else
Term.unknown
compareArgs :: (?cutoff :: Int) => Maybe QName -> [DeBruijnPat] -> [Term] -> TCM [[Term.Order]]
compareArgs suc pats ts = mapM (\t -> mapM (compareTerm suc t) pats) ts
makeCM :: Index -> Index -> [[Term.Order]] -> Term.CallMatrix
makeCM ncols nrows matrix = Term.CallMatrix $
Term.fromLists (Term.Size { Term.rows = nrows
, Term.cols = ncols
})
matrix
addGuardedness :: Integral n => Order -> n -> n -> [[Term.Order]] -> (n, n, [[Term.Order]])
addGuardedness g nrows ncols m =
(nrows + 1, ncols + 1,
(g : genericReplicate ncols Term.unknown) : map (Term.unknown :) m)
decreaseFromConstructor :: QName -> TCM Order
decreaseFromConstructor c = do
isRC <- isRecordConstructor c
return $ if isRC then Term.le else Term.lt
increaseFromConstructor :: (?cutoff :: Int) => QName -> TCM Order
increaseFromConstructor c = do
isRC <- isRecordConstructor c
return $ if isRC then Term.le else Term.decr (1)
subPatterns :: DeBruijnPat -> [DeBruijnPat]
subPatterns p = case p of
VarDBP _ -> []
ConDBP c ps -> ps ++ concatMap subPatterns ps
LitDBP _ -> []
compareTerm :: (?cutoff :: Int) => Maybe QName -> Term -> DeBruijnPat -> TCM Term.Order
compareTerm suc t p = do
t <- stripAllProjections t
compareTerm' suc t p
stripProjections :: Term -> TCM Term
stripProjections (DontCare t) = stripProjections t
stripProjections t@(Def qn ts@(~(r : _))) = do
isProj <- isProjection qn
case isProj of
Just{} | not (null ts) -> stripProjections $ unArg r
_ -> return t
stripProjections t = return t
class StripAllProjections a where
stripAllProjections :: a -> TCM a
instance StripAllProjections a => StripAllProjections (Arg a) where
stripAllProjections (Arg h r a) = Arg h r <$> stripAllProjections a
instance StripAllProjections a => StripAllProjections [a] where
stripAllProjections = mapM stripAllProjections
instance StripAllProjections Term where
stripAllProjections t = do
t <- stripProjections t
case t of
Con c ts -> Con c <$> stripAllProjections ts
Def d ts -> Def d <$> stripAllProjections ts
_ -> return t
compareTerm' :: (?cutoff :: Int) => Maybe QName -> Term -> DeBruijnPat -> TCM Term.Order
compareTerm' _ (Var i _) p = compareVar i p
compareTerm' suc (DontCare t) p = compareTerm' suc t p
compareTerm' _ (Lit l) (LitDBP l')
| l == l' = return Term.le
| otherwise = return Term.unknown
compareTerm' suc (Lit l) p = do
t <- constructorForm (Lit l)
case t of
Lit _ -> return Term.unknown
_ -> compareTerm' suc t p
compareTerm' _ t@Con{} (ConDBP c ps)
| any (isSubTerm t) ps = decreaseFromConstructor c
compareTerm' suc (Con c ts) (ConDBP c' ps)
| c == c' = compareConArgs suc ts ps
compareTerm' suc (Def s ts) (ConDBP s' ps)
| s == s' && Just s == suc = compareConArgs suc ts ps
compareTerm' suc (Def s ts) p | Just s == suc = do
os <- mapM (\ t -> compareTerm' suc (unArg t) p) ts
return $ decr (1) .*. infimum os
compareTerm' suc (Con c ts) p = do
os <- mapM (\ t -> compareTerm' suc (unArg t) p) ts
oc <- increaseFromConstructor c
return $ if (null os) then Term.unknown else oc .*. infimum os
compareTerm' suc t p | isSubTerm t p = return Term.le
compareTerm' _ _ _ = return Term.unknown
isSubTerm :: Term -> DeBruijnPat -> Bool
isSubTerm t p = equal t p || properSubTerm t p
where
equal (Con c ts) (ConDBP c' ps) =
and $ (c == c')
: (length ts == length ps)
: zipWith equal (map unArg ts) ps
equal (Var i []) (VarDBP j) = i == j
equal (Lit l) (LitDBP l') = l == l'
equal _ _ = False
properSubTerm t (ConDBP _ ps) = any (isSubTerm t) ps
properSubTerm _ _ = False
compareConArgs :: (?cutoff :: Int) => Maybe QName -> Args -> [DeBruijnPat] -> TCM Term.Order
compareConArgs suc ts ps =
case (length ts, length ps) of
(0,0) -> return Term.le
(0,1) -> return Term.unknown
(1,0) -> __IMPOSSIBLE__
(1,1) -> compareTerm' suc (unArg (head ts)) (head ps)
(_,_) -> do
m <- mapM (\t -> mapM (compareTerm' suc (unArg t)) ps) ts
let m2 = makeCM (genericLength ps) (genericLength ts) m
return $ Term.orderMat (Term.mat m2)
compareVar :: (?cutoff :: Int) => Nat -> DeBruijnPat -> TCM Term.Order
compareVar i (VarDBP j) = return $ if i == j then Term.le else Term.unknown
compareVar i (LitDBP _) = return $ Term.unknown
compareVar i (ConDBP c ps) = do
os <- mapM (compareVar i) ps
let o = Term.supremum os
oc <- decreaseFromConstructor c
return $ (Term..*.) oc o