module Agda.Termination.TermCheck
( termDecl
, Result, DeBruijnPat
) where
import Control.Applicative
import Control.Monad.Error
import Control.Monad.State
import Data.List as List
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Maybe as Maybe
import Data.Monoid
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.Syntax.Translation.InternalToAbstract
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, isRecord, isInductiveRecord)
import Agda.TypeChecking.Rules.Builtin.Coinduction
import Agda.TypeChecking.Rules.Term (isType_)
import Agda.TypeChecking.Substitute (abstract,raise)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Signature (isProjection, mutuallyRecursive)
import Agda.TypeChecking.Primitive (constructorForm)
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.SizedTypes
import qualified Agda.Interaction.Highlighting.Range as R
import Agda.Interaction.Options
import Agda.Utils.List
import Agda.Utils.Size
import Agda.Utils.Monad ((<$>), mapM', forM', ifM)
import Agda.Utils.Pointed
import Agda.Utils.Permutation
#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 = 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 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.Mutual i ds -> termMutual i ds
A.Section _ x _ ds -> termSection x ds
A.Apply {} -> return mempty
A.Import {} -> return mempty
A.Pragma {} -> return mempty
A.Open {} -> return mempty
A.ScopedDecl{} -> __IMPOSSIBLE__
A.RecSig{} -> return mempty
A.RecDef _ r _ _ _ _ ds -> checkRecDef [] r ds
A.FunDef{} -> __IMPOSSIBLE__
A.DataSig{} -> __IMPOSSIBLE__
A.DataDef{} -> __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
termMutual :: Info.MutualInfo -> [A.Declaration] -> TCM Result
termMutual i ds = if names == [] then return mempty else
traceCall (SetRange (Info.mutualRange i)) $ do
mutualBlock <- findMutualBlock (head names)
let allNames = Set.elems mutualBlock
if not (Info.mutualTermCheck i) then do
reportSLn "term.warn.yes" 2 $ "Skipping termination check for " ++ show names
forM_ allNames $ \ q -> setTerminates q True
return mempty
else do
cutoff <- optTerminationDepth <$> pragmaOptions
let ?cutoff = cutoff
reportSLn "term.top" 10 $ "Termination checking " ++ show names ++
" with cutoff=" ++ show cutoff ++ "..."
suc <- sizeSucName
sharp <- fmap nameOfSharp <$> coinductionKit
guardingTypeConstructors <-
optGuardingTypeConstructors <$> pragmaOptions
let conf = DBPConf
{ useDotPatterns = False
, guardingTypeConstructors = guardingTypeConstructors
, withSizeSuc = suc
, sharp = sharp
, currentTarget = Nothing
}
res <- ifM (optCopatterns <$> pragmaOptions)
(forM' allNames $ termFunction conf names allNames)
(termMutual' conf names allNames)
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' :: (?cutoff :: Int) => DBPConf -> [QName] -> MutualNames -> TCM Result
termMutual' conf names allNames = do
let collect conf = mapM' (termDef conf allNames) allNames
calls1 <- collect conf{ useDotPatterns = False }
reportCalls "no " calls1
r <- case Term.terminates calls1 of
r@Right{} -> return r
Left{} -> do
calls2 <- collect conf{ useDotPatterns = True }
reportCalls "" calls2
return $ Term.terminates calls2
case r of
Left calls -> do
return $ point $ TerminationError
{ termErrFunctions = names
, termErrCalls = Set.toList calls
}
Right _ -> do
reportSLn "term.warn.yes" 2
(show (names) ++ " does termination check")
return mempty
where
reportCalls no calls = do
reportS "term.lex" 20 $ unlines
[ "Calls (" ++ no ++ "dot patterns): " ++ show calls
]
reportSDoc "term.behaviours" 20 $ vcat
[ text $ "Recursion behaviours (" ++ no ++ "dot patterns):"
, nest 2 $ return $ Term.prettyBehaviour (Term.complete calls)
]
reportSDoc "term.matrices" 30 $ vcat
[ text $ "Call matrices (" ++ no ++ "dot patterns):"
, nest 2 $ pretty $ Term.complete calls
]
termFunction :: (?cutoff :: Int) => DBPConf -> [QName] -> MutualNames -> QName -> TCM Result
termFunction conf0 names allNames name = do
let index = toInteger $ maybe __IMPOSSIBLE__ id $
List.elemIndex name allNames
conf <- do
r <- typeEndsInDef =<< typeOfConst name
reportTarget r
return $ conf0 { currentTarget = r }
let collect conf = mapM' (termDef conf allNames) allNames
calls1 <- collect conf{ useDotPatterns = False }
reportCalls "no " calls1
r <- case Term.terminatesFilter (== index) calls1 of
r@Right{} -> return r
Left{} -> do
calls2 <- collect conf{ useDotPatterns = True }
reportCalls "" calls2
return $ Term.terminatesFilter (== index) calls2
case r of
Left calls -> do
return $ point $ TerminationError
{ termErrFunctions = if name `elem` names then [name] else []
, termErrCalls = Set.toList calls
}
Right _ -> do
reportSLn "term.warn.yes" 2
(show (name) ++ " does termination check")
return mempty
where
reportTarget r = reportSLn "term.target" 20 $ maybe
(" target type not recognized")
(\ q -> " target type ends in " ++ show q)
r
typeEndsInDef :: Type -> TCM (Maybe QName)
typeEndsInDef t = do
TelV _ core <- telView t
case ignoreSharing $ unEl core of
Def d vs -> return $ Just d
_ -> return Nothing
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, funDelayed = delayed } ->
mapM' (termClause use names name delayed) 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
, currentTarget :: Maybe Target
}
type Target = QName
targetElem :: DBPConf -> [Target] -> Bool
targetElem conf ds = maybe False (`elem` ds) (currentTarget conf)
termToDBP :: DBPConf -> Term -> TCM DeBruijnPat
termToDBP conf t
| not $ useDotPatterns conf = return $ unusedVar
| otherwise = do
t <- stripProjections =<< constructorForm t
case ignoreSharing 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
openClause :: DBPConf -> Permutation -> [Pattern] -> ClauseBody -> TCM ([DeBruijnPat], Maybe Term)
openClause conf 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 perm) $ downFrom (size perm)
tick = do x : xs <- get; put xs; return x
build :: Pattern -> StateT [Nat] TCM DeBruijnPat
build (VarP _) = VarDBP <$> tick
build (ConP con _ ps) = ConDBP con <$> mapM (build . unArg) ps
build (DotP t) = tick *> do lift $ termToDBP conf t
build (LitP l) = return $ LitDBP l
termClause :: DBPConf -> MutualNames -> QName -> Delayed -> Clause -> TCM Calls
termClause conf names name delayed
(Clause { clauseTel = tel
, clausePerm = perm
, clausePats = argPats'
, clauseBody = body }) = do
reportSDoc "term.check.clause" 25 $ vcat
[ text "termClause"
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text ("perm = " ++ show perm)
]
addCtxTel tel $ do
ps <- normalise $ map unArg argPats'
(dbpats, res) <- openClause conf perm ps body
case res of
Nothing -> return Term.empty
Just t -> do
dbpats <- mapM (stripCoConstructors conf) dbpats
termTerm conf names name delayed dbpats t
termTerm :: DBPConf -> MutualNames -> QName -> Delayed -> [DeBruijnPat] -> Term -> TCM Calls
termTerm conf names f delayed pats0 t0 = do
cutoff <- optTerminationDepth <$> pragmaOptions
let ?cutoff = cutoff
do
reportSDoc "term.check.clause" 6
(sep [ text ("termination checking " ++
(if delayed == Delayed then "delayed " else "") ++ "clause of")
<+> prettyTCM f
, nest 2 $ text "lhs:" <+> hsep (map prettyTCM pats0)
, nest 2 $ text "rhs:" <+> prettyTCM t0
])
let guarded = Term.le
loop pats0 guarded t0
where
ifDelayed o | Term.decreasing o && delayed == NotDelayed = Term.le
| otherwise = o
Just fInd = toInteger <$> List.elemIndex f names
loopSort :: (?cutoff :: Int) => [DeBruijnPat] -> Sort -> TCM Calls
loopSort pats s = do
reportSDoc "term.sort" 20 $ text "extracting calls from sort" <+> prettyTCM s
reportSDoc "term.sort" 50 $ text ("s = " ++ show s)
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
let constructor
:: QName
-> Induction
-> [(Arg Term, Bool)]
-> TCM Calls
constructor c ind args = mapM' 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 t = case ignoreSharing t of
Con c vs -> (`apply` vs) <$> reduce (Con c [])
_ -> return t
args2 <- mapM reduceCon args2
args <- mapM etaContract args2
isProj <- isProjectionButNotFlat g
let unguards = repeat Term.unknown
let guards = if isProj then guarded : unguards
else unguards
calls <- mapM' (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 (withSizeSuc conf) pats args
let (nrows, ncols, matrix') = addGuardedness
(ifDelayed 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 ignoreSharing t of
Con c args
| Just c == sharp conf ->
constructor c CoInductive $ zip args (repeat True)
| otherwise -> do
ind <- do
r <- isRecordConstructor c
case r of
Nothing -> return Inductive
Just (q, def) -> return . (\ b -> if b then CoInductive else Inductive) $
and [ recRecursive def
, recInduction def == CoInductive
, targetElem conf (q : recMutual def)
]
constructor c ind $ zip args (repeat True)
Def g args0
| guardingTypeConstructors conf -> do
def <- getConstInfo g
let occs = defArgOccurrences def
case theDef def of
Datatype{} -> con occs
Record{} -> con occs
_ -> fun
| otherwise -> fun
where
con occs =
constructor g Inductive $
zip args0 (map preserves occs ++ repeat False)
where
preserves = (StrictPos <=)
fun = function g args0
Lam h (Abs x t) -> addCtxString_ x $
loop (map liftDBP pats) guarded t
Lam h (NoAbs _ t) -> loop pats guarded t
Var i args -> mapM' (loop pats Term.unknown) (map unArg args)
Pi a (Abs x b) ->
do g1 <- loopType pats Term.unknown (unDom a)
a <- maskSizeLt 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 (unDom 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 -> do
l <- catchError (reallyUnLevelView l) $ const $ internalError $
"Termination checker: cannot view level expression, " ++
"probably due to missing level built-ins."
loop pats guarded l
Shared{} -> __IMPOSSIBLE__
where
piArgumentGuarded =
if guardingTypeConstructors conf then
guarded
else
Term.unknown
maskSizeLt :: Dom Type -> TCM (Dom Type)
maskSizeLt dom@(Dom h r a) = 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 h r $
abstract tel $ El s $ Def size []
_ -> return dom
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)
offsetFromConstructor :: QName -> TCM Int
offsetFromConstructor c = maybe 1 (const 0) <$> isRecordConstructor c
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
isProjectionButNotFlat :: QName -> TCM Bool
isProjectionButNotFlat qn = do
flat <- fmap nameOfFlat <$> coinductionKit
if Just qn == flat
then return False
else do
mp <- isProjection qn
case mp of
Nothing -> return False
Just (r, _) -> isInductiveRecord r
stripProjections :: Term -> TCM Term
stripProjections t = case ignoreSharing t of
DontCare t -> stripProjections t
Def qn ts@(~(r : _)) -> do
isProj <- isProjectionButNotFlat qn
case isProj of
True | not (null ts) -> stripProjections $ unArg r
_ -> return 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 ignoreSharing 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' suc (Shared x) p = compareTerm' suc (derefPtr x) p
compareTerm' suc (Var i _) p = compareVar suc 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 ignoreSharing t of
Lit _ -> return Term.unknown
_ -> compareTerm' suc t p
compareTerm' _ t@Con{} (ConDBP c ps)
| any (isSubTerm t) ps = decrease <$> offsetFromConstructor c <*> return Term.le
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 [t]) p | Just s == suc = do
increase 1 <$> compareTerm' suc (unArg t) p
compareTerm' suc (Con c []) p = return Term.le
compareTerm' suc (Con c ts) p = do
increase <$> offsetFromConstructor c
<*> (infimum <$> mapM (\ t -> compareTerm' suc (unArg t) p) ts)
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 (Shared p) dbp = equal (derefPtr p) dbp
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) => Maybe QName -> Nat -> DeBruijnPat -> TCM Term.Order
compareVar suc i (VarDBP j) = compareVarVar suc i j
compareVar suc i (LitDBP _) = return $ Term.unknown
compareVar suc i (ConDBP c ps) = do
decrease <$> offsetFromConstructor c
<*> (Term.supremum <$> mapM (compareVar suc i) ps)
compareVarVar :: (?cutoff :: Int) => Maybe QName -> Nat -> Nat -> TCM Term.Order
compareVarVar suc i j
| i == j = return Term.le
| otherwise = do
res <- isBounded i
case res of
BoundedNo -> return Term.unknown
BoundedLt v -> decrease 1 <$> compareTerm' suc v (VarDBP j)