{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.Termination.TermCheck
( termDecl
, termMutual
, Result
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), null )
#else
import Prelude hiding ( null )
#endif
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.State
import Data.Foldable (toList)
import qualified Data.List as List
import Data.Monoid hiding ((<>))
import qualified Data.Set as Set
import Data.Traversable (Traversable, traverse)
import Agda.Syntax.Abstract (IsProjP(..), AllNames(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Internal.Generic
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Translation.InternalToAbstract ( reifyPatterns )
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.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull)
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import qualified Agda.Benchmarking 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 (prettyShow)
import Agda.Utils.Singleton
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 $ termDecl' d
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 $ getNames 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 scope 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__
A.UnquoteDef{} -> __IMPOSSIBLE__
where
termDecls ds = concat <$> mapM termDecl' ds
unscopeDefs = concatMap unscopeDef
unscopeDef (A.ScopedDecl _ ds) = unscopeDefs ds
unscopeDef d = [d]
getNames = concatMap getName
getName (A.FunDef i x delayed cs) = [x]
getName (A.RecDef _ _ _ _ _ _ _ ds) = getNames ds
getName (A.Mutual _ ds) = getNames ds
getName (A.Section _ _ _ ds) = getNames ds
getName (A.ScopedDecl _ ds) = getNames ds
getName (A.UnquoteDecl _ _ xs _) = xs
getName (A.UnquoteDef _ xs _) = xs
getName _ = []
termMutual
:: [QName]
-> TCM Result
termMutual names0 = ifNotM (optTerminationCheck <$> pragmaOptions) (return mempty) $
inTopContext $ disableDestructiveUpdate $ do
mid <- fromMaybe __IMPOSSIBLE__ <$> asks envMutualBlock
mutualBlock <- lookupMutualBlock mid
let allNames = Set.elems $ mutualNames mutualBlock
names = if null names0 then allNames else names0
i = mutualInfo mutualBlock
skip = not <$> do
ignoreAbstractMode $ do
billTo [Benchmark.Termination, Benchmark.RecCheck] $ recursive allNames
setCurrentRange i $ do
reportSLn "term.mutual" 10 $ "Termination checking " ++ prettyShow allNames
if (Info.mutualTermCheck i `elem` [ NoTerminationCheck, Terminating ]) then do
reportSLn "term.warn.yes" 10 $ "Skipping termination check for " ++ prettyShow names
forM_ allNames $ \ q -> setTerminates q True
return mempty
else if (Info.mutualTermCheck i == NonTerminating) then do
reportSLn "term.warn.yes" 10 $ "Considering as non-terminating: " ++ prettyShow names
forM_ allNames $ \ q -> setTerminates q False
return mempty
else ifM skip (do
reportSLn "term.warn.yes" 10 $ "Trivially terminating: " ++ prettyShow 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 " ++ prettyShow names ++
" with cutoff=" ++ show cutoff ++ "..."
terLocal setNames cont
res <- ifM (orM $ map usesCopatterns allNames)
(runTerm $ forM' allNames $ termFunction)
(runTerm $ termMutual')
let terminates = null res
forM_ allNames $ \ q -> setTerminates q terminates
return res
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 $
prettyShow (names) ++ " does termination check"
return mempty
terminationError :: [QName] -> [CallInfo] -> TerminationError
terminationError names calls = TerminationError names' calls
where names' = names `List.intersect` toList (allNames calls)
billToTerGraph :: a -> TerM a
billToTerGraph a = liftTCM $ billPureTo [Benchmark.Termination, Benchmark.Graph] a
reportCalls :: String -> Calls -> TerM ()
reportCalls no calls = do
cutoff <- terGetCutOff
let ?cutoff = cutoff
liftTCM $ do
reportS "term.lex" 20 $ unlines
[ "Calls (" ++ no ++ "dot patterns): " ++ prettyShow 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] `List.intersect` names) calls
Right () -> do
liftTCM $ reportSLn "term.warn.yes" 2 $
prettyShow name ++ " does termination check"
return mempty
where
reportTarget r = liftTCM $
reportSLn "term.target" 20 $ " target type " ++
caseMaybe r "not recognized" (\ q ->
"ends in " ++ prettyShow q)
typeEndsInDef :: MonadTCM tcm => Type -> tcm (Maybe QName)
typeEndsInDef t = liftTCM $ do
TelV _ core <- telView t
case unEl core of
Def d vs -> return $ Just d
_ -> return Nothing
termDef :: QName -> TerM Calls
termDef name = terSetCurrent name $ inConcreteOrAbstractMode name $ \ def -> do
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 DeBruijnPattern
termToDBP t = ifNotM terGetUseDotPatterns (return unusedVar) $ do
termToPattern =<< do liftTCM $ stripAllProjections =<< normalise t
class TermToPattern a b where
termToPattern :: a -> TerM b
default termToPattern :: (TermToPattern a' b', Traversable f, a ~ f a', b ~ f b') => a -> TerM b
termToPattern = traverse termToPattern
instance TermToPattern a b => TermToPattern [a] [b] where
instance TermToPattern a b => TermToPattern (Arg a) (Arg b) where
instance TermToPattern a b => TermToPattern (Named c a) (Named c b) where
instance TermToPattern Term DeBruijnPattern where
termToPattern t = (liftTCM $ constructorForm t) >>= \case
Con c _ args -> ConP c noConPatternInfo . map (fmap unnamed) <$> termToPattern (fromMaybe __IMPOSSIBLE__ $ allApplyElims args)
Def s [Apply arg] -> do
suc <- terGetSizeSuc
if Just s == suc then ConP (ConHead s Inductive []) noConPatternInfo . map (fmap unnamed) <$> termToPattern [arg]
else return $ dotP t
DontCare t -> termToPattern t
Var i [] -> varP . (`DBPatVar` i) . prettyShow <$> nameOfBV i
Lit l -> return $ LitP l
t -> return $ dotP t
maskNonDataArgs :: [DeBruijnPattern] -> TerM [Masked DeBruijnPattern]
maskNonDataArgs ps = zipWith mask ps <$> terGetMaskArgs
where
mask p@ProjP{} _ = Masked False p
mask p d = Masked d p
termClause :: Clause -> TerM Calls
termClause clause = do
let fallback = termClause' clause
ifNotM (terGetInlineWithFunctions) fallback $ do
name <- terGetCurrent
ifM (isJust <$> isWithFunction name) (return mempty) $ do
(liftTCM $ inlineWithClauses name clause) >>= \case
Nothing -> fallback
Just cls -> terSetHaveInlinedWith $ mapM' termClause' cls
termClause' :: Clause -> TerM Calls
termClause' clause = do
Clause{ clauseTel = tel, namedClausePats = ps, clauseBody = body } <- etaExpandClause clause
liftTCM $ reportSDoc "term.check.clause" 25 $ vcat
[ text "termClause"
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text "ps =" <+> do addContext tel $ prettyTCMPatternList ps
]
forM' body $ \ v -> addContext tel $ do
ps <- postTraversePatternM parseDotP ps
ps <- preTraversePatternM stripCoCon ps
mdbpats <- maskNonDataArgs $ map namedArg ps
terSetPatterns mdbpats $ do
terSetSizeDepth tel $ do
reportBody v
extract v
where
parseDotP = \case
DotP o t -> termToDBP t
p -> return p
stripCoCon p = case p of
ConP (ConHead c _ _) _ _ -> do
ifM ((Just c ==) <$> terGetSizeSuc) (return p) $ do
whatInduction c >>= \case
Inductive -> return p
CoInductive -> return unusedVar
_ -> return p
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:" <+> sep (map prettyTCM pats)
, nest 2 $ text "rhs:" <+> prettyTCM 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 (Arg a) where
extract = extract . unArg
instance ExtractCalls a => ExtractCalls (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
PiSort s1 s2 -> extract (s1, s2)
UnivSort s -> extract s
MetaS x es -> return empty
instance ExtractCalls Type where
extract (El s t) = extract (s, t)
constructor
:: QName
-> Induction
-> [(Arg Term, Bool)]
-> TerM Calls
constructor c ind args = do
cutoff <- terGetCutOff
let ?cutoff = cutoff
forM' args $ \ (arg, preserves) -> do
let g' = case (preserves, ind) of
(True, Inductive) -> id
(True, CoInductive) -> (Order.lt .*.)
(False, _) -> const Order.unknown
terModifyGuarded g' $ extract arg
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 es0 = ifM (terGetInlineWithFunctions `and2M` do isJust <$> isWithFunction g) (withFunction g es0)
$ do
f <- terGetCurrent
names <- terGetMutual
guarded <- terGetGuarded
liftTCM $ reportSDoc "term.function" 30 $
text "termination checking function call " <+> prettyTCM (Def g es0)
let (reduceCon :: Term -> TCM Term) = traverseTermM $ \ t -> case t of
Con c ci vs -> (`applyE` vs) <$> reduce (Con c ci [])
_ -> return t
isProj <- isProjectionButNotCoinductive g
let unguards = repeat Order.unknown
let guards = applyWhen isProj (guarded :) unguards
let args = map unArg $ argsFromElims es0
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 es0 $
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 " ++ prettyShow guarded ++
" counting as " ++ prettyShow (ifDelayed guarded)
cutoff <- terGetCutOff
let ?cutoff = cutoff
let matrix' = composeGuardedness (ifDelayed guarded) matrix
doc <- liftTCM $ withCurrentModule (qnameModule g) $ buildClosure $
Def g $ filter ((/= Inserted) . getOrigin) es0
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 (prettyShow f) <+> hsep (map prettyTCM pats)
, nest 2 $ text "to" <+> text (prettyShow 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 t of
Con ConHead{conName = c} _ es -> do
let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
let argsg = zip args $ repeat True
ind <- ifM ((Just c ==) <$> terGetSharp) (return CoInductive) $ do
caseMaybeM (liftTCM $ isRecordConstructor c) (return Inductive) $ \ (q, def) -> do
reportSLn "term.check.term" 50 $ "constructor " ++ prettyShow c ++ " has record type " ++ prettyShow q
(\ b -> if b then CoInductive else Inductive) <$>
andM [ return $ recInduction def == Just CoInductive
, targetElem . fromMaybe __IMPOSSIBLE__ $ 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
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 => Dom Type -> tcm (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 a of
El s (Def d [v]) | d == sizelt -> return $ Dom info $
abstract tel $ El s $ Def size []
_ -> return dom
compareArgs :: [Elim] -> TerM (Int, Int, [[Order]])
compareArgs es = do
liftTCM $ reportSDoc "term.compareArgs" 90 $ vcat
[ text $ "comparing " ++ show (length es) ++ " args"
]
pats <- terGetPatterns
matrix <- withUsableVars pats $ forM es $ \ e -> forM pats $ \ p -> compareElim e p
projsCaller <- length <$> do
filterM (isCoinductiveProjection True) $ mapMaybe (fmap (headAmbQ . snd) . isProjP . getMasked) pats
projsCallee <- length <$> do
filterM (isCoinductiveProjection True) $ mapMaybe (fmap snd . isProjElim) es
cutoff <- terGetCutOff
let ?cutoff = cutoff
let guardedness = decr True $ projsCaller - projsCallee
liftTCM $ reportSDoc "term.guardedness" 30 $ sep
[ text "compareArgs:"
, nest 2 $ text $ "projsCaller = " ++ prettyShow projsCaller
, nest 2 $ text $ "projsCallee = " ++ prettyShow projsCallee
, nest 2 $ text $ "guardedness of call: " ++ prettyShow guardedness
]
return $ addGuardedness guardedness (size es) (size pats) matrix
annotatePatsWithUseSizeLt :: [DeBruijnPattern] -> TerM [(Bool,DeBruijnPattern)]
annotatePatsWithUseSizeLt = loop where
loop [] = return []
loop (p@(ProjP _ q) : pats) = ((False,p) :) <$> do projUseSizeLt q $ loop pats
loop (p : pats) = (\ b ps -> (b,p) : ps) <$> terGetUseSizeLt <*> loop pats
compareElim :: Elim -> Masked DeBruijnPattern -> 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, ProjP _ d') -> do
d <- getOriginalProjection d
d' <- getOriginalProjection d'
o <- compareProj d d'
reportSDoc "term.compare" 30 $ sep
[ text $ "comparing callee projection " ++ prettyShow d
, text $ "against caller projection " ++ prettyShow d'
, text $ "yields order " ++ prettyShow o
]
return o
(Proj{}, _) -> return Order.unknown
(Apply{}, ProjP{}) -> 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 (List.find (d==) fs, List.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 :: Order -> Int -> Int -> [[Order]] -> (Int, Int, [[Order]])
addGuardedness o nrows ncols m =
(nrows + 1, ncols + 1,
(o : replicate 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 :: DeBruijnPattern -> [DeBruijnPattern]
subPatterns = foldPattern $ \case
ConP _ _ ps -> map namedArg ps
VarP _ _ -> mempty
LitP _ -> mempty
DotP _ _ -> mempty
ProjP _ _ -> mempty
compareTerm :: Term -> Masked DeBruijnPattern -> 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 " ++ prettyShow o)
return o
class StripAllProjections a where
stripAllProjections :: a -> TCM a
instance StripAllProjections a => StripAllProjections (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 o p : es) -> do
isP <- isProjectionButNotCoinductive p
applyUnless isP (Proj o p :) <$> stripAllProjections es
instance StripAllProjections Args where
stripAllProjections = mapM stripAllProjections
instance StripAllProjections Term where
stripAllProjections t = do
case t of
Var i es -> Var i <$> stripAllProjections es
Con c ci ts -> Con c ci <$> stripAllProjections ts
Def d es -> Def d <$> stripAllProjections es
DontCare t -> stripAllProjections t
_ -> return t
compareTerm' :: Term -> Masked DeBruijnPattern -> TerM Order
compareTerm' v mp@(Masked m p) = do
suc <- terGetSizeSuc
cutoff <- terGetCutOff
let ?cutoff = cutoff
v <- liftTCM (instantiate v)
case (v, p) of
(Var i es, _) | Just{} <- allApplyElims es ->
compareVar i mp
(DontCare t, _) ->
compareTerm' t mp
(MetaV{}, p) -> Order.decr True . max (if m then 0 else patternDepth p) . pred <$>
terAsks _terSizeDepth
(Def s [Apply t], ConP s' _ [p]) | s == conName s' && Just s == suc ->
compareTerm' (unArg t) (notMasked $ namedArg p)
(Def s [Apply t], p) | Just s == suc ->
increase 1 <$> compareTerm' (unArg t) mp
_ | m -> return Order.unknown
(Lit l, LitP l')
| l == l' -> return Order.le
| otherwise -> return Order.unknown
(Lit l, _) -> do
v <- liftTCM $ constructorForm v
case v of
Lit{} -> return Order.unknown
v -> compareTerm' v mp
(Con{}, ConP c _ ps) | any (isSubTerm v . namedArg) ps ->
decr True <$> offsetFromConstructor (conName c)
(Con c _ es, ConP c' _ ps) | conName c == conName c'->
let ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es in
compareConArgs ts ps
(Con _ _ [], _) -> return Order.le
(Con c _ es, _) -> do
let ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
increase <$> offsetFromConstructor (conName c)
<*> (infimum <$> mapM (\ t -> compareTerm' (unArg t) mp) ts)
(t, p) -> return $ subTerm t p
subTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPattern -> Order
subTerm t p = if equal t p then Order.le else properSubTerm t p
where
equal (Con c _ es) (ConP c' _ ps) =
let ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es in
and $ (conName c == conName c')
: (length ts == length ps)
: zipWith (\ t p -> equal (unArg t) (namedArg p)) ts ps
equal (Var i []) (VarP _ x) = i == dbPatVarIndex x
equal (Lit l) (LitP l') = l == l'
equal t (DotP _ t') = t == t'
equal _ _ = False
properSubTerm t (ConP _ _ ps) =
setUsability True $ decrease 1 $ supremum $ map (subTerm t . namedArg) ps
properSubTerm _ _ = Order.unknown
isSubTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPattern -> Bool
isSubTerm t p = nonIncreasing $ subTerm t p
compareConArgs :: Args -> [NamedArg DeBruijnPattern] -> 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 $ namedArg $ head ps)
(_,_) -> foldl (Order..*.) Order.le <$>
zipWithM compareTerm' (map unArg ts) (map (notMasked . namedArg) ps)
compareVar :: Nat -> Masked DeBruijnPattern -> TerM Order
compareVar i (Masked m p) = do
suc <- terGetSizeSuc
cutoff <- terGetCutOff
let ?cutoff = cutoff
let no = return Order.unknown
case p of
ProjP{} -> no
LitP{} -> no
DotP{} -> no
VarP _ x -> compareVarVar i (Masked m x)
ConP s _ [p] | Just (conName s) == suc ->
setUsability True . decrease 1 <$> compareVar i (notMasked $ namedArg p)
ConP c _ ps -> if m then no else setUsability True <$> do
decrease <$> offsetFromConstructor (conName c)
<*> (Order.supremum <$> mapM (compareVar i . notMasked . namedArg) ps)
compareVarVar :: Nat -> Masked DBPatVar -> TerM Order
compareVarVar i (Masked m x@(DBPatVar _ 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 = do
u <- (i `VarSet.member`) <$> terGetUsableVars
if not u then return Order.unknown else do
res <- isBounded i
case res of
BoundedNo -> return Order.unknown
BoundedLt v -> setUsability u . decrease 1 <$> compareTerm' v (Masked m $ varP x)