module Agda.Termination.TermCheck
( termDecl
, Result, DeBruijnPat
) where
import Prelude hiding (null)
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)
import Data.Monoid
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse)
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
import Agda.Syntax.Position
import Agda.Syntax.Common as Common
import Agda.Syntax.Literal (Literal(LitString))
import Agda.Termination.CutOff
import Agda.Termination.Monad
import Agda.Termination.CallGraph hiding (toList)
import qualified Agda.Termination.CallGraph as CallGraph
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)
import qualified Agda.Termination.Termination as Term
import Agda.Termination.RecCheck
import Agda.Termination.Inlining
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Datatypes
import qualified Agda.TypeChecking.Monad.Base.Benchmark as Benchmark
import Agda.TypeChecking.Monad.Benchmark (billTo, billPureTo)
import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor (($>), (<.>))
import Agda.Utils.List
import Agda.Utils.Size
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (render)
import Agda.Utils.Singleton
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
#include "undefined.h"
import Agda.Utils.Impossible
type Calls = CallGraph CallPath
type Result = [TerminationError]
termDecl :: A.Declaration -> TCM Result
termDecl d = inTopContext $ ignoreAbstractMode $ termDecl' d
termDecls :: [A.Declaration] -> TCM Result
termDecls ds = concat <$> mapM termDecl' ds
termDecl' :: A.Declaration -> TCM Result
termDecl' d = case d of
A.Axiom {} -> return mempty
A.Field {} -> return mempty
A.Primitive {} -> return mempty
A.Mutual _ ds
| [A.RecSig{}, A.RecDef _ _ _ _ _ _ rds] <- unscopeDefs ds
-> termDecls rds
A.Mutual i ds -> termMutual i ds
A.Section _ _ _ ds -> termDecls ds
A.Apply {} -> return mempty
A.Import {} -> return mempty
A.Pragma {} -> return mempty
A.Open {} -> return mempty
A.PatternSynDef {} -> return mempty
A.ScopedDecl _ ds -> termDecls ds
A.RecSig{} -> return mempty
A.RecDef _ r _ _ _ _ ds -> termDecls ds
A.FunDef{} -> __IMPOSSIBLE__
A.DataSig{} -> __IMPOSSIBLE__
A.DataDef{} -> __IMPOSSIBLE__
A.UnquoteDecl{} -> __IMPOSSIBLE__
where
unscopeDefs = concatMap unscopeDef
unscopeDef (A.ScopedDecl _ ds) = unscopeDefs ds
unscopeDef d = [d]
termMutual :: Info.MutualInfo -> [A.Declaration] -> TCM Result
termMutual i ds = if names == [] then return mempty else
setCurrentRange i $ do
mutualBlock <- findMutualBlock (head names)
let allNames = Set.elems mutualBlock
skip = not <$> do
billTo [Benchmark.Termination, Benchmark.RecCheck] $ recursive allNames
if (Info.mutualTermCheck i `elem` [ NoTerminationCheck, Terminating ]) then do
reportSLn "term.warn.yes" 2 $ "Skipping termination check for " ++ show names
forM_ allNames $ \ q -> setTerminates q True
return mempty
else if (Info.mutualTermCheck i == NonTerminating) then do
reportSLn "term.warn.yes" 2 $ "Considering as non-terminating: " ++ show names
forM_ allNames $ \ q -> setTerminates q False
return mempty
else ifM skip (do
reportSLn "term.warn.yes" 2 $ "Trivially terminating: " ++ show names
forM_ allNames $ \ q -> setTerminates q True
return mempty)
$ do
let setNames e = e
{ terMutual = allNames
, terUserNames = names
}
runTerm cont = runTerDefault $ do
cutoff <- terGetCutOff
reportSLn "term.top" 10 $ "Termination checking " ++ show names ++
" with cutoff=" ++ show cutoff ++ "..."
terLocal setNames cont
res <- ifM (optCopatterns <$> pragmaOptions)
(runTerm $ forM' allNames $ termFunction)
(runTerm $ termMutual')
let terminates = null res
forM_ allNames $ \ q -> setTerminates q terminates
return res
where
getName (A.FunDef i x delayed 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
termMutual' :: TerM Result
termMutual' = do
allNames <- terGetMutual
let collect = forM' allNames termDef
calls1 <- collect
reportCalls "no " calls1
cutoff <- terGetCutOff
let ?cutoff = cutoff
r <- billToTerGraph $ Term.terminates calls1
r <- case r of
r@Right{} -> return r
Left{} -> do
calls2 <- terSetUseDotPatterns True $ collect
reportCalls "" calls2
billToTerGraph $ Term.terminates calls2
names <- terGetUserNames
case r of
Left calls -> return $ singleton $ terminationError names $ callInfos calls
Right{} -> do
liftTCM $ reportSLn "term.warn.yes" 2 $
show (names) ++ " does termination check"
return mempty
terminationError :: [QName] -> [CallInfo] -> TerminationError
terminationError names calls = TerminationError names' calls
where names' = names `intersect` toList (allNames calls)
billToTerGraph :: a -> TerM a
billToTerGraph = billPureTo [Benchmark.Termination, Benchmark.Graph]
reportCalls :: String -> Calls -> TerM ()
reportCalls no calls = do
cutoff <- terGetCutOff
let ?cutoff = cutoff
liftTCM $ do
reportS "term.lex" 20 $ unlines
[ "Calls (" ++ no ++ "dot patterns): " ++ show calls
]
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
let calls' = CallGraph.complete calls
idems = filter idempotent $ endos $ CallGraph.toList calls'
reportSDoc "term.matrices" 30 $ vcat
[ text $ "Idempotent call matrices (" ++ no ++ "dot patterns):\n"
, nest 2 $ vcat $ punctuate (text "\n") $ map pretty idems
]
return ()
termFunction :: QName -> TerM Result
termFunction name = do
allNames <- terGetMutual
let index = fromMaybe __IMPOSSIBLE__ $ List.elemIndex name allNames
target <- liftTCM $ do typeEndsInDef =<< typeOfConst name
reportTarget target
terSetTarget target $ do
let collect = (`trampolineM` (Set.singleton index, mempty, mempty)) $ \ (todo, done, calls) -> do
if null todo then return $ Left calls else do
new <- forM' todo $ \ i ->
termDef $ fromMaybe __IMPOSSIBLE__ $ allNames !!! i
let done' = done `mappend` todo
calls' = new `mappend` calls
todo' = CallGraph.targetNodes new Set.\\ done'
return $ Right (todo', done', calls')
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
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)
typeEndsInDef :: MonadTCM tcm => Type -> tcm (Maybe QName)
typeEndsInDef t = liftTCM $ do
TelV _ core <- telView t
case ignoreSharing $ unEl core of
Def d vs -> return $ Just d
_ -> return Nothing
termDef :: QName -> TerM Calls
termDef name = terSetCurrent name $ do
def <- liftTCM $ getConstInfo name
let t = defType def
liftTCM $ reportSDoc "term.def.fun" 5 $
sep [ text "termination checking body of" <+> prettyTCM name
, nest 2 $ text ":" <+> prettyTCM t
]
withoutKEnabled <- liftTCM $ optWithoutK <$> pragmaOptions
applyWhen withoutKEnabled (setMasks t) $ do
applyWhenM terGetMaskResult terUnguarded $ do
case theDef def of
Function{ funClauses = cls, funDelayed = delayed } ->
terSetDelayed delayed $ forM' cls $ termClause
_ -> return empty
setMasks :: Type -> TerM a -> TerM a
setMasks t cont = do
(ds, d) <- liftTCM $ do
TelV tel core <- telView t
ds <- forM (telToList tel) $ \ t -> do
TelV _ t <- telView $ snd $ unDom 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
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 True) $ terSetMaskResult d $ cont
targetElem :: [Target] -> TerM Bool
targetElem ds = maybe False (`elem` ds) <$> terGetTarget
termToDBP :: Term -> TerM DeBruijnPat
termToDBP t = ifNotM terGetUseDotPatterns (return unusedVar) $ do
suc <- terGetSizeSuc
let
loop :: Term -> TCM DeBruijnPat
loop t = do
t <- constructorForm t
case ignoreSharing t of
Con c args -> ConDBP (conName c) <$> mapM (loop . unArg) args
Def s [Apply arg] | Just s == suc
-> ConDBP s . (:[]) <$> loop (unArg arg)
DontCare t -> __IMPOSSIBLE__
Var i [] -> return $ VarDBP i
Lit l -> return $ LitDBP l
t -> return $ TermDBP t
liftTCM $ loop =<< stripAllProjections =<< normalise t
stripCoConstructors :: DeBruijnPat -> TerM DeBruijnPat
stripCoConstructors p = do
case p of
ConDBP c args -> do
ind <- ifM ((Just c ==) <$> terGetSizeSuc) (return Inductive)
(liftTCM $ whatInduction c)
case ind of
Inductive -> ConDBP c <$> mapM stripCoConstructors args
CoInductive -> return unusedVar
VarDBP{} -> return p
LitDBP{} -> return p
TermDBP{} -> return p
ProjDBP{} -> return p
maskNonDataArgs :: [DeBruijnPat] -> TerM [Masked DeBruijnPat]
maskNonDataArgs ps = zipWith mask ps <$> terGetMaskArgs
where
mask p@ProjDBP{} _ = Masked False p
mask p d = Masked d p
openClause :: Permutation -> [Pattern] -> ClauseBody -> TerM ([DeBruijnPat], Maybe Term)
openClause perm ps body = do
unless (permRange perm == genericLength xs) __IMPOSSIBLE__
dbps <- evalStateT (mapM build ps) xs
return . (dbps,) $ case body `apply` map (defaultArg . var) xs of
NoBody -> Nothing
Body v -> Just v
_ -> __IMPOSSIBLE__
where
n = size perm
xs = permute (invertP __IMPOSSIBLE__ perm) $ downFrom (size perm)
tick = do x : xs <- get; put xs; return x
build :: Pattern -> StateT [Nat] TerM DeBruijnPat
build (VarP _) = VarDBP <$> tick
build (ConP con _ ps) = ConDBP (conName con) <$> mapM (build . namedArg) ps
build (DotP t) = tick *> do lift $ termToDBP t
build (LitP l) = return $ LitDBP l
build (ProjP d) = return $ ProjDBP d
termClause :: Clause -> TerM Calls
termClause clause = do
ifNotM (terGetInlineWithFunctions) (termClause' clause) $ do
name <- terGetCurrent
ifM (isJust <$> do isWithFunction name) (return mempty) $ do
mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause
termClause' :: Clause -> TerM Calls
termClause' clause = do
cl @ Clause { clauseTel = tel
, clausePerm = perm
, clauseBody = body } <- introHiddenLambdas clause
let argPats' = clausePats cl
liftTCM $ reportSDoc "term.check.clause" 25 $ vcat
[ text "termClause"
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text ("perm = " ++ show perm)
]
addCtxTel tel $ do
ps <- liftTCM $ normalise $ map unArg argPats'
(dbpats, res) <- openClause perm ps body
case res of
Nothing -> return empty
Just v -> do
dbpats <- mapM stripCoConstructors dbpats
mdbpats <- maskNonDataArgs dbpats
terSetPatterns mdbpats $ do
terSetSizeDepth tel $ do
reportBody v
extract v
where
reportBody :: Term -> TerM ()
reportBody v = verboseS "term.check.clause" 6 $ do
f <- terGetCurrent
delayed <- terGetDelayed
pats <- terGetPatterns
liftTCM $ reportSDoc "term.check.clause" 6 $ do
sep [ text ("termination checking " ++
(if delayed == Delayed then "delayed " else "") ++
"clause of")
<+> prettyTCM f
, nest 2 $ text "lhs:" <+> hsep (map prettyTCM pats)
, nest 2 $ text "rhs:" <+> prettyTCM v
]
introHiddenLambdas :: MonadTCM tcm => Clause -> tcm Clause
introHiddenLambdas clause = liftTCM $ do
case clause of
Clause range ctel perm ps body Nothing -> return clause
Clause range ctel perm ps body (Just t)-> do
case removeHiddenLambdas body of
([], _) -> return clause
(axs, body') -> do
let n = length axs
TelV ttel t' <- telViewUpTo n $ unArg t
when (size ttel < n) __IMPOSSIBLE__
let ctel' = telFromList $ telToList ctel ++ telToList ttel
ps' = ps ++ map toPat axs
perm' = liftP n perm
return $ Clause range ctel' perm' ps' body' $ Just (t $> t')
where
toPat (Common.Arg (Common.ArgInfo h r c) x) =
Common.Arg (Common.ArgInfo h r []) $ namedVarP x
removeHiddenLambdas :: ClauseBody -> ([I.Arg ArgName], ClauseBody)
removeHiddenLambdas = underBinds $ hlamsToBinds
hlamsToBinds :: Term -> ([I.Arg ArgName], ClauseBody)
hlamsToBinds v =
case ignoreSharing v of
Lam info b | getHiding info == Hidden ->
let (xs, b') = hlamsToBinds $ unAbs b
in (Arg info (absName b) : xs, Bind $ b' <$ b)
_ -> ([], Body v)
underBinds :: (Term -> ([a], ClauseBody)) -> ClauseBody -> ([a], ClauseBody)
underBinds k body = loop body where
loop (Bind b) =
let (res, b') = loop $ unAbs b
in (res, Bind $ b' <$ b)
loop NoBody = ([], NoBody)
loop (Body v) = k v
class ExtractCalls a where
extract :: a -> TerM Calls
instance ExtractCalls a => ExtractCalls (Abs a) where
extract (NoAbs _ a) = extract a
extract (Abs x a) = addContext x $ terRaise $ extract a
instance ExtractCalls a => ExtractCalls (I.Arg a) where
extract = extract . unArg
instance ExtractCalls a => ExtractCalls (I.Dom a) where
extract = extract . unDom
instance ExtractCalls a => ExtractCalls (Elim' a) where
extract Proj{} = return empty
extract (Apply a) = extract $ unArg a
instance ExtractCalls a => ExtractCalls [a] where
extract = mapM' extract
instance (ExtractCalls a, ExtractCalls b) => ExtractCalls (a,b) where
extract (a, b) = CallGraph.union <$> extract a <*> extract b
instance ExtractCalls Sort where
extract s = do
liftTCM $ do
reportSDoc "term.sort" 20 $
text "extracting calls from sort" <+> prettyTCM s
reportSDoc "term.sort" 50 $
text ("s = " ++ show s)
case s of
Prop -> return empty
Inf -> return empty
SizeUniv -> return empty
Type t -> terUnguarded $ extract t
DLub s1 s2 -> extract (s1, s2)
instance ExtractCalls Type where
extract (El s t) = extract (s, t)
constructor
:: QName
-> Induction
-> [(I.Arg Term, Bool)]
-> TerM Calls
constructor c ind args = do
cutoff <- terGetCutOff
let ?cutoff = cutoff
mapM' loopArg args
where
loopArg (arg, preserves) = terModifyGuarded g' $ extract arg where
g' = case (preserves, ind) of
(True, Inductive) -> id
(True, CoInductive) -> (Order.lt .*.)
(False, _) -> const Order.unknown
guardPresTyCon :: QName -> Elims -> (QName -> Elims -> TerM Calls) -> TerM Calls
guardPresTyCon g es cont = do
ifNotM (terGetGuardingTypeConstructors) (cont g es) $ do
def <- liftTCM $ getConstInfo g
let occs = defArgOccurrences def
preserves = (StrictPos <=)
con = constructor g Inductive $
zip (argsFromElims es)
(map preserves occs ++ repeat False)
case theDef def of
Datatype{} -> con
Record{} -> con
_ -> cont g es
withFunction :: QName -> Elims -> TerM Calls
withFunction g es = do
v <- liftTCM $
expandWithFunctionCall g es
liftTCM $ reportSDoc "term.with.call" 30 $
text "termination checking expanded with-function call:" <+> prettyTCM v
extract v
function :: QName -> Elims -> TerM Calls
function g es = ifM (terGetInlineWithFunctions `and2M` do isJust <$> isWithFunction g) (withFunction g es)
$ do
f <- terGetCurrent
names <- terGetMutual
guarded <- terGetGuarded
let gArgs = Def g es
liftTCM $ reportSDoc "term.function" 30 $
text "termination checking function call " <+> prettyTCM gArgs
let reduceCon t = case ignoreSharing t of
Con c vs -> (`apply` vs) <$> reduce (Con c [])
_ -> return t
isProj <- isProjectionButNotCoinductive g
let unguards = repeat Order.unknown
let guards = applyWhen isProj (guarded :) unguards
let args = map unArg $ argsFromElims es
calls <- forM' (zip guards args) $ \ (guard, a) -> do
terSetGuarded guard $ extract a
liftTCM $ 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
delayed <- terGetDelayed
pats <- terGetPatterns
es <- liftTCM $
forM es $
etaContract <=< traverse reduceCon <=< instantiateFull
(nrows, ncols, matrix) <- billTo [Benchmark.Termination, Benchmark.Compare] $ compareArgs es
let ifDelayed o | Order.decreasing o && delayed == NotDelayed = Order.le
| otherwise = o
liftTCM $ reportSLn "term.guardedness" 20 $
"composing with guardedness " ++ show guarded ++
" counting as " ++ show (ifDelayed guarded)
cutoff <- terGetCutOff
let ?cutoff = cutoff
let matrix' = composeGuardedness (ifDelayed guarded) matrix
doc <- liftTCM $ withCurrentModule (qnameModule g) $ buildClosure gArgs
let src = fromMaybe __IMPOSSIBLE__ $ List.elemIndex f names
tgt = gInd
cm = makeCM ncols nrows matrix'
info = CallPath [CallInfo
{ callInfoTarget = g
, callInfoRange = getRange g
, callInfoCall = doc
}]
liftTCM $ reportSDoc "term.kept.call" 5 $ vcat
[ text "kept call from" <+> text (show f) <+> hsep (map prettyTCM pats)
, nest 2 $ text "to" <+> text (show g) <+>
hsep (map (parens . prettyTCM) args)
, nest 2 $ text "call matrix (with guardedness): "
, nest 2 $ pretty cm
]
return $ CallGraph.insert src tgt cm info calls
instance ExtractCalls Term where
extract t = do
liftTCM $ reportSDoc "term.check.term" 50 $ do
text "looking for calls in" <+> prettyTCM t
t <- liftTCM $ instantiate t
case ignoreSharing t of
Con ConHead{conName = c} args -> do
let argsg = zip args $ repeat True
ind <- ifM ((Just c ==) <$> terGetSharp) (return CoInductive) $ do
r <- liftTCM $ isRecordConstructor c
case r of
Nothing -> return Inductive
Just (q, def) -> (\ b -> if b then CoInductive else Inductive) <$>
andM [ return $ recRecursive def
, return $ recInduction def == Just CoInductive
, targetElem (q : recMutual def)
]
constructor c ind argsg
Def g es -> guardPresTyCon g es function
Lam h b -> extract b
Var i es -> terUnguarded $ extract es
Pi a (Abs x b) -> CallGraph.union <$> (terUnguarded $ extract a) <*> do
a <- maskSizeLt a
terPiGuarded $ addContext (x, a) $ terRaise $ extract b
Pi a (NoAbs _ b) -> CallGraph.union
<$> terUnguarded (extract a)
<*> terPiGuarded (extract b)
Lit l -> return empty
Sort s -> extract s
MetaV x args -> return empty
DontCare t -> extract t
Level l ->
extract l
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
deriving instance ExtractCalls Level
instance ExtractCalls PlusLevel where
extract (ClosedLevel n) = return $ mempty
extract (Plus n l) = extract l
instance ExtractCalls LevelAtom where
extract (MetaLevel x es) = extract es
extract (BlockedLevel x t) = extract t
extract (NeutralLevel _ t) = extract t
extract (UnreducedLevel t) = extract t
maskSizeLt :: MonadTCM tcm => I.Dom Type -> tcm (I.Dom Type)
maskSizeLt dom@(Dom info a) = liftTCM $ do
(msize, msizelt) <- getBuiltinSize
case (msize, msizelt) of
(_ , Nothing) -> return dom
(Nothing, _) -> __IMPOSSIBLE__
(Just size, Just sizelt) -> do
TelV tel c <- telView a
case ignoreSharingType a of
El s (Def d [v]) | d == sizelt -> return $ Dom info $
abstract tel $ El s $ Def size []
_ -> return dom
compareArgs :: (Integral n) => [Elim] -> TerM (n, n, [[Order]])
compareArgs es = do
pats <- terGetPatterns
matrix <- withUsableVars pats $ forM es $ \ e -> forM pats $ \ p -> compareElim e p
projsCaller <- genericLength <$> do
filterM (isCoinductiveProjection True) $ mapMaybe (isProjP . getMasked) pats
projsCallee <- genericLength <$> do
filterM (isCoinductiveProjection True) $ mapMaybe isProjElim es
cutoff <- terGetCutOff
let ?cutoff = cutoff
let guardedness = decr $ projsCaller projsCallee
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
annotatePatsWithUseSizeLt :: [DeBruijnPat] -> TerM [(Bool,DeBruijnPat)]
annotatePatsWithUseSizeLt = loop where
loop [] = return []
loop (p@(ProjDBP q) : pats) = ((False,p) :) <$> do projUseSizeLt q $ loop pats
loop (p : pats) = (\ b ps -> (b,p) : ps) <$> terGetUseSizeLt <*> loop pats
compareElim :: Elim -> Masked DeBruijnPat -> TerM Order
compareElim e p = do
liftTCM $ do
reportSDoc "term.compare" 30 $ sep
[ text "compareElim"
, nest 2 $ text "e = " <+> prettyTCM e
, nest 2 $ text "p = " <+> prettyTCM p
]
reportSDoc "term.compare" 50 $ sep
[ nest 2 $ text $ "e = " ++ show e
, nest 2 $ text $ "p = " ++ show p
]
case (e, getMasked p) of
(Proj d, ProjDBP d') -> compareProj d d'
(Proj{}, _ ) -> return Order.unknown
(Apply{}, ProjDBP{}) -> return Order.unknown
(Apply arg, _) -> compareTerm (unArg arg) p
compareProj :: MonadTCM tcm => QName -> QName -> tcm Order
compareProj d d'
| d == d' = return Order.le
| otherwise = liftTCM $ do
mr <- getRecordOfField d
mr' <- getRecordOfField d'
case (mr, mr') of
(Just r, Just r') | r == r' -> do
def <- theDef <$> getConstInfo r
case def of
Record{ recFields = fs } -> do
fs <- return $ map unArg fs
case (find (d==) fs, find (d'==) fs) of
(Just i, Just i')
| i < i' -> return Order.lt
| i == i' -> do
__IMPOSSIBLE__
| otherwise -> return Order.unknown
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
_ -> return Order.unknown
makeCM :: Int -> Int -> [[Order]] -> CallMatrix
makeCM ncols nrows matrix = CallMatrix $
Matrix.fromLists (Matrix.Size nrows ncols) matrix
addGuardedness :: Integral n => Order -> n -> n -> [[Order]] -> (n, n, [[Order]])
addGuardedness o nrows ncols m =
(nrows + 1, ncols + 1,
(o : genericReplicate ncols Order.unknown) : map (Order.unknown :) m)
composeGuardedness :: (?cutoff :: CutOff) => Order -> [[Order]] -> [[Order]]
composeGuardedness o ((corner : row) : rows) = ((o .*. corner) : row) : rows
composeGuardedness _ _ = __IMPOSSIBLE__
offsetFromConstructor :: MonadTCM tcm => QName -> tcm Int
offsetFromConstructor c = maybe 1 (const 0) <$> do
liftTCM $ isRecordConstructor c
subPatterns :: DeBruijnPat -> [DeBruijnPat]
subPatterns p = case p of
ConDBP c ps -> ps ++ concatMap subPatterns ps
VarDBP _ -> []
LitDBP _ -> []
TermDBP _ -> []
ProjDBP _ -> []
compareTerm :: Term -> Masked DeBruijnPat -> TerM Order
compareTerm t p = do
t <- liftTCM $ stripAllProjections t
o <- compareTerm' t p
liftTCM $ reportSDoc "term.compare" 25 $
text " comparing term " <+> prettyTCM t <+>
text " to pattern " <+> prettyTCM p <+>
text (" results in " ++ show o)
return o
class StripAllProjections a where
stripAllProjections :: a -> TCM a
instance StripAllProjections a => StripAllProjections (I.Arg a) where
stripAllProjections = traverse stripAllProjections
instance StripAllProjections Elims where
stripAllProjections es =
case es of
[] -> return []
(Apply a : es) -> do
(:) <$> (Apply <$> stripAllProjections a) <*> stripAllProjections es
(Proj p : es) -> do
isP <- isProjectionButNotCoinductive p
applyUnless isP (Proj p :) <$> stripAllProjections es
instance StripAllProjections Args where
stripAllProjections = mapM stripAllProjections
instance StripAllProjections Term where
stripAllProjections t = do
case ignoreSharing t of
Var i es -> Var i <$> stripAllProjections es
Con c ts -> Con c <$> stripAllProjections ts
Def d es -> Def d <$> stripAllProjections es
DontCare t -> stripAllProjections t
_ -> return t
compareTerm' :: Term -> Masked DeBruijnPat -> TerM Order
compareTerm' v mp@(Masked m p) = do
suc <- terGetSizeSuc
cutoff <- terGetCutOff
let ?cutoff = cutoff
v <- return $ ignoreSharing v
case (v, p) of
(Var i es, _) | Just{} <- allApplyElims es ->
compareVar i mp
(DontCare t, _) ->
compareTerm' t mp
(MetaV{}, p) -> Order.decr . max (if m then 0 else patternDepth p) . pred <$>
terAsks _terSizeDepth
(Def s [Apply t], ConDBP s' [p]) | s == s' && Just s == suc ->
compareTerm' (unArg t) (notMasked p)
(Def s [Apply t], p) | Just s == suc ->
increase 1 <$> compareTerm' (unArg t) mp
_ | m -> return Order.unknown
(Lit l, LitDBP l')
| l == l' -> return Order.le
| otherwise -> return Order.unknown
(Lit l, _) -> do
v <- liftTCM $ constructorForm v
case ignoreSharing v of
Lit{} -> return Order.unknown
v -> compareTerm' v mp
(Con{}, ConDBP c ps) | any (isSubTerm v) ps ->
decrease <$> offsetFromConstructor c <*> return Order.le
(Con c ts, ConDBP c' ps) | conName c == c'->
compareConArgs ts ps
(Con c [], _) -> return Order.le
(Con c ts, _) -> do
increase <$> offsetFromConstructor (conName c)
<*> (infimum <$> mapM (\ t -> compareTerm' (unArg t) mp) ts)
(t, p) -> return $ subTerm t p
subTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPat -> Order
subTerm t p = if equal t p then Order.le else properSubTerm t p
where
equal (Shared p) dbp = equal (derefPtr p) dbp
equal (Con c ts) (ConDBP c' ps) =
and $ (conName c == c')
: (length ts == length ps)
: zipWith equal (map unArg ts) ps
equal (Var i []) (VarDBP i') = i == i'
equal (Lit l) (LitDBP l') = l == l'
equal t (TermDBP t') = t == t'
equal _ _ = False
properSubTerm t (ConDBP _ ps) = decrease 1 $ supremum $ map (subTerm t) ps
properSubTerm _ _ = Order.unknown
isSubTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPat -> Bool
isSubTerm t p = nonIncreasing $ subTerm t p
compareConArgs :: Args -> [DeBruijnPat] -> TerM Order
compareConArgs ts ps = do
cutoff <- terGetCutOff
let ?cutoff = cutoff
case (length ts, length ps) of
(0,0) -> return Order.le
(0,1) -> return Order.unknown
(1,0) -> __IMPOSSIBLE__
(1,1) -> compareTerm' (unArg (head ts)) (notMasked (head ps))
(_,_) -> foldl (Order..*.) Order.le <$>
zipWithM compareTerm' (map unArg ts) (map notMasked ps)
compareVar :: Nat -> Masked DeBruijnPat -> TerM Order
compareVar i (Masked m p) = do
suc <- terGetSizeSuc
cutoff <- terGetCutOff
let ?cutoff = cutoff
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)
compareVarVar :: Nat -> Masked Nat -> TerM Order
compareVarVar i (Masked m j)
| i == j = if not m then return Order.le else liftTCM $
ifM (isJust <$> do isSizeType =<< reduce =<< typeOfBV j)
(return Order.le)
(return Order.unknown)
| otherwise = ifNotM ((i `VarSet.member`) <$> terGetUsableVars) (return Order.unknown) $ do
res <- isBounded i
case res of
BoundedNo -> return Order.unknown
BoundedLt v -> decrease 1 <$> compareTerm' v (Masked m (VarDBP j))