module Agda.Termination.TermCheck
( termDecls
, Result, DeBruijnPat
) where
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 Text.PrettyPrint (Doc)
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.Matrix 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.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.Primitive (constructorForm)
import qualified Agda.Interaction.Highlighting.Range as R
import Agda.Interaction.Options
import Agda.Utils.Size
import Agda.Utils.String
import Agda.Utils.Monad (thread, (<$>), ifM)
#include "../undefined.h"
import Agda.Utils.Impossible
type Calls = Term.CallGraph (Set R.Range)
type MutualNames = [QName]
type Result = [([A.QName], [R.Range])]
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.Definition _ _ ds
| [A.RecDef _ r _ _ _ rds] <- unscopeDefs ds
-> do
let m = mnameFromList $ qnameToList r
setScopeFromDefs ds
termSection m rds
A.Definition i ts ds -> termMutual i ts ds
A.Section _ x _ ds -> termSection x ds
A.Apply {} -> return []
A.Import {} -> return []
A.Pragma {} -> return []
A.Open {} -> return []
A.ScopedDecl{} -> __IMPOSSIBLE__
where
setScopeFromDefs = mapM_ setScopeFromDef
setScopeFromDef (A.ScopedDef scope d) =
setScope scope >> setScopeFromDef d
setScopeFromDef _ = return ()
unscopeDefs = concatMap unscopeDef
unscopeDef (A.ScopedDef _ d) = unscopeDef d
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.TypeSignature] -> [A.Definition] -> TCM Result
termMutual i ts ds = if names == [] then return [] else
do
reportSLn "term.top" 20 $ "Termination checking " ++ show names ++ "..."
mutualBlock <- findMutualBlock (head names)
let allNames = Set.elems mutualBlock
let collect use = collectCalls (termDef use allNames) allNames
suc <- sizeSuc
let conf = DBPConf { useDotPatterns = False, withSizeSuc = suc }
calls1 <- collect conf{ useDotPatterns = False }
reportS "term.lex" 30 $ unlines
[ "Calls (no dot patterns): " ++ show calls1
]
reportS "term.behaviours" 30 $ unlines
[ "Recursion behaviours (no dot patterns):"
, indent 2 $ Term.showBehaviour (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" 30 $ unlines
[ "Calls (dot patterns): " ++ show calls2
]
reportS "term.behaviours" 30 $ unlines
[ "Recursion behaviours (no dot patterns):"
, indent 2 $ Term.showBehaviour (Term.complete calls1)
, "Recursion behaviours (dot patterns):"
, indent 2 $ Term.showBehaviour (Term.complete calls2)
]
return $ Term.terminates calls2
case r of
Left errDesc -> do
let callSites = Set.toList errDesc
return [(names, callSites)]
Right _ -> do
reportSLn "term.warn.yes" 2
(show (names) ++ " does termination check")
return []
where
getName (A.FunDef i x cs) = [x]
getName (A.ScopedDef _ d) = getName d
getName (A.RecDef _ _ _ _ _ ds) = concatMap getNameD ds
getName _ = []
getNameD (A.Definition _ _ ds) = concatMap getName ds
getNameD (A.Section _ _ _ ds) = concatMap getNameD ds
getNameD (A.ScopedDecl _ ds) = concatMap getNameD ds
getNameD _ = []
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" 10 $
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
, withSizeSuc :: Maybe QName
}
termToDBP :: DBPConf -> Term -> TCM DeBruijnPat
termToDBP conf t
| not $ useDotPatterns conf = return $ unusedVar
| otherwise = do
t <- 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) (NoBind b) = return $ Just (i, unusedVar, b)
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) (NoBind b) = do
t <- termToDBP conf t
return $ Just (i, t, b)
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 }) = do
argPats' <- addCtxTel tel $ 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 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 (NoBind b) = boundVars b
boundVars NoBody = 0
boundVars (Body _) = 0
termTerm :: MutualNames -> QName -> [DeBruijnPat] -> Term -> TCM Calls
termTerm names f pats0 t0 = do
reportSDoc "term.check.clause" 11
(sep [ text "termination checking clause of" <+> prettyTCM f
, nest 2 $ text "lhs:" <+> hsep (map prettyTCM pats0)
, nest 2 $ text "rhs:" <+> prettyTCM t0
])
loop pats0 Le t0
where
Just fInd = toInteger <$> List.elemIndex f names
loop :: [DeBruijnPat] -> Order -> Term -> TCM Calls
loop pats guarded t = do
t <- instantiate t
suc <- sizeSuc
case t of
Def g args0 ->
do let args1 = map unArg args0
args2 <- mapM instantiateFull args1
let reduceCon t@(Con _ _) = reduce t
reduceCon t = return t
args2 <- mapM reduceCon args2
args <- mapM etaContract args2
calls <- collectCalls (loop pats Unknown) args
reportSDoc "term.found.call" 10
(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 ncols = genericLength pats + 1
nrows = genericLength args + 1
matrix' = addGuardedness guarded (ncols 1) matrix
reportSDoc "term.kept.call" 10
(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: " ++ show matrix)
])
return
(Term.insert
(Term.Call { Term.source = fInd
, Term.target = toInteger gInd'
, Term.cm = makeCM ncols nrows matrix'
})
(Set.fromList $ fst $ R.getRangesA g)
calls)
Lam _ (Abs _ t) -> loop (map liftDBP pats) guarded t
Var i args -> collectCalls (loop pats Unknown) (map unArg args)
Con c args -> do
ind <- whatInduction c
let g' = case ind of
Inductive -> guarded
CoInductive -> Lt .*. guarded
collectCalls (loop pats g') (map unArg args)
Pi (Arg _ (El _ a)) (Abs _ (El _ b)) ->
do g1 <- loop pats guarded a
g2 <- loop (map liftDBP pats) guarded b
return $ g1 `Term.union` g2
Fun (Arg _ (El _ a)) (El _ b) ->
do g1 <- loop pats guarded a
g2 <- loop pats guarded b
return $ g1 `Term.union` g2
Lit l -> return Term.empty
Sort s -> return Term.empty
MetaV x args -> return Term.empty
compareArgs :: 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 -> [[Term.Order]] -> [[Term.Order]]
addGuardedness g ncols m =
(g : genericReplicate ncols Unknown) : map (Unknown :) m
subPatterns :: DeBruijnPat -> [DeBruijnPat]
subPatterns p = case p of
VarDBP _ -> []
ConDBP c ps -> ps ++ concatMap subPatterns ps
LitDBP _ -> []
compareTerm :: Maybe QName -> Term -> DeBruijnPat -> TCM Term.Order
compareTerm suc t p = compareTerm' suc t p
compareTerm' :: Maybe QName -> Term -> DeBruijnPat -> TCM Term.Order
compareTerm' _ (Var i _) p = compareVar i 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' 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' _ t@Con{} (ConDBP _ ps)
| any (isSubTerm t) ps = return Lt
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 :: 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.Mat (Term.mat m2)
compareVar :: 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
return $ (Term..*.) Term.Lt o