{-|
Module      : Idris.Termination
Description : The termination checker for Idris

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Termination (buildSCG, checkAllCovering, checkDeclTotality,
                          checkIfGuarded, checkPositive, checkSizeChange,
                          verifyTotality) where

import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Error
import Idris.Options
import Idris.Output (iWarn)

import Control.Monad.State.Strict
import Data.Either
import Data.List
import Data.Maybe
import Debug.Trace

-- | Check whether function and all descendants cover all cases
-- (partial is okay, as long as it's due to recursion)
checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering FC
fc [Name]
done Name
top Name
n | Bool -> Bool
not (Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
done)
   = do IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
        case Name -> Context -> [Totality]
lookupTotal Name
n (IState -> Context
tt_ctxt IState
i) of
             [tot :: Totality
tot@(Partial PReason
NotCovering)] ->
                    do let msg :: [Char]
msg = forall a. Show a => a -> [Char]
show Name
top forall a. [a] -> [a] -> [a]
++ [Char]
" is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Totality
tot forall a. [a] -> [a] -> [a]
++ [Char]
" due to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n
                       IState -> Idris ()
putIState IState
i { idris_totcheckfail :: [(FC, [Char])]
idris_totcheckfail = (FC
fc, [Char]
msg) forall a. a -> [a] -> [a]
: IState -> [(FC, [Char])]
idris_totcheckfail IState
i }
                       IBCWrite -> Idris ()
addIBC (FC -> [Char] -> IBCWrite
IBCTotCheckErr FC
fc [Char]
msg)
             [Partial (Other [Name]
ns)] ->
                     -- Check that none of the partial functions it relies
                     -- on are partial due to missing cases
                     forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering FC
fc (Name
n forall a. a -> [a] -> [a]
: [Name]
done) Name
top) [Name]
ns
             [Totality]
x -> forall (m :: * -> *) a. Monad m => a -> m a
return () -- stop if total, or partial due to recursion
checkAllCovering FC
_ [Name]
_ Name
_ Name
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Check whether all 'Inf' arguments to the name end up guaranteed to be
-- guarded by constructors (conservatively... maybe this can do better later).
-- Essentially, all it does is check that every branch is a constructor application
-- with no other function applications.
--
-- If so, set the 'AllGuarded' flag which can be used by the productivity check
checkIfGuarded :: Name -> Idris ()
checkIfGuarded :: Name -> Idris ()
checkIfGuarded Name
n
   = do IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
        let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
i
        case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
             Just (CaseOp CaseInfo
_ Term
ty [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
cases) ->
                  let gnames :: [Name]
gnames = forall a b. (a, b) -> a
fst (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cases) in
                      if forall {t :: * -> *}. Foldable t => t Name -> IState -> SC -> Bool
allGuarded [Name]
gnames IState
i (forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cases))
                         then -- trace (show (n, gnames, ty, cases_compiletime cases)) $
                              Name -> FnOpt -> Idris ()
addFnOpt Name
n FnOpt
AllGuarded
                         else forall (m :: * -> *) a. Monad m => a -> m a
return ()
             Maybe Def
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    guard :: Name -> IState -> Bool
guard Name
n IState
ist = Name -> Context -> Bool
isConName Name
n (IState -> Context
tt_ctxt IState
ist) Bool -> Bool -> Bool
|| Name -> IState -> Bool
guardFlag Name
n IState
ist
    guardFlag :: Name -> IState -> Bool
guardFlag Name
n IState
ist = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [FnOpt]
idris_flags IState
ist) of
                           Maybe [FnOpt]
Nothing -> Bool
False
                           Just [FnOpt]
fs -> FnOpt
AllGuarded forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
fs

    -- Top level thing always needs to be a constructor application if
    -- the delayed things are going to be definitely guarded by this definition
    allGuarded :: t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i (STerm Term
t)
          | (P NameType
_ Name
fn Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t,
            Name -> IState -> Bool
guard Name
fn IState
i
            = forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b. (a -> b) -> [a] -> [b]
map (forall {t :: * -> *}.
Foldable t =>
t Name -> IState -> Term -> Bool
guardedTerm t Name
names IState
i) [Term]
args)
          | Bool
otherwise = Bool
False
    allGuarded t Name
names IState
i (ProjCase Term
_ [CaseAlt' Term]
alts) = forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> CaseAlt' Term -> Bool
guardedAlt t Name
names IState
i) [CaseAlt' Term]
alts)
    allGuarded t Name
names IState
i (Case CaseType
_ Name
_ [CaseAlt' Term]
alts) = forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> CaseAlt' Term -> Bool
guardedAlt t Name
names IState
i) [CaseAlt' Term]
alts)
    allGuarded t Name
names IState
i SC
_ = Bool
True

    guardedTerm :: t Name -> IState -> Term -> Bool
guardedTerm t Name
names IState
i (P NameType
_ Name
v Term
_) = Name
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
names Bool -> Bool -> Bool
|| Name -> IState -> Bool
guard Name
v IState
i
    guardedTerm t Name
names IState
i (Bind Name
n (Let RigCount
rig Term
t Term
v) Term
sc)
          = t Name -> IState -> Term -> Bool
guardedTerm t Name
names IState
i Term
v Bool -> Bool -> Bool
&& t Name -> IState -> Term -> Bool
guardedTerm t Name
names IState
i Term
sc
    guardedTerm t Name
names IState
i (Bind Name
n Binder Term
b Term
sc) = Bool
False
    guardedTerm t Name
names IState
i ap :: Term
ap@(App AppStatus Name
_ Term
_ Term
_)
          | (P NameType
_ Name
fn Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
            Name -> IState -> Bool
guard Name
fn IState
i Bool -> Bool -> Bool
|| Name
fn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
names
                = forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> Term -> Bool
guardedTerm t Name
names IState
i) [Term]
args)
    guardedTerm t Name
names IState
i (App AppStatus Name
_ Term
f Term
a) = Bool
False
    guardedTerm t Name
names IState
i Term
tm = Bool
True

    guardedAlt :: t Name -> IState -> CaseAlt' Term -> Bool
guardedAlt t Name
names IState
i (ConCase Name
_ Int
_ [Name]
_ SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
    guardedAlt t Name
names IState
i (FnCase Name
_ [Name]
_ SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
    guardedAlt t Name
names IState
i (ConstCase Const
_ SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
    guardedAlt t Name
names IState
i (SucCase Name
_ SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
    guardedAlt t Name
names IState
i (DefaultCase SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t

-- | Check if, in a given group of type declarations mut_ns, the
-- constructor cn : ty is strictly positive, and update the context
-- accordingly
checkPositive :: [Name]       -- ^ the group of type declarations
              -> (Name, Type) -- ^ the constructor
              -> Idris Totality
checkPositive :: [Name] -> (Name, Term) -> Idris Totality
checkPositive [Name]
mut_ns (Name
cn, Term
ty')
    = do IState
i <- Idris IState
getIState
         let ty :: Term
ty = Bool -> Term -> Term
delazy' Bool
True (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
i) [] Term
ty')
         let p :: Bool
p = IState -> Term -> Bool
cp IState
i Term
ty
         let tot :: Totality
tot = if Bool
p then [Int] -> Totality
Total (forall {n}. TT n -> [Int]
args Term
ty) else PReason -> Totality
Partial PReason
NotPositive
         let ctxt' :: Context
ctxt' = Name -> Totality -> Context -> Context
setTotal Name
cn Totality
tot (IState -> Context
tt_ctxt IState
i)
         IState -> Idris ()
putIState (IState
i { tt_ctxt :: Context
tt_ctxt = Context
ctxt' })
         Int -> [Char] -> Idris ()
logCoverage Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"Constructor " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
cn forall a. [a] -> [a] -> [a]
++ [Char]
" is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Totality
tot forall a. [a] -> [a] -> [a]
++ [Char]
" with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Name]
mut_ns
         IBCWrite -> Idris ()
addIBC (Name -> Totality -> IBCWrite
IBCTotal Name
cn Totality
tot)
         forall (m :: * -> *) a. Monad m => a -> m a
return Totality
tot
  where
    args :: TT n -> [Int]
args TT n
t = [Int
0..forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall n. TT n -> [(n, TT n)]
getArgTys TT n
t)forall a. Num a => a -> a -> a
-Int
1]

    cp :: IState -> Term -> Bool
cp IState
i (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
aty Term
_) Term
sc)
         = IState -> Term -> Bool
posArg IState
i Term
aty Bool -> Bool -> Bool
&& IState -> Term -> Bool
cp IState
i Term
sc
    cp IState
i Term
t | (P NameType
_ Name
n' Term
_ , [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t,
             Name
n' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
mut_ns = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
noRec [Term]
args
    cp IState
i Term
_ = Bool
True

    posArg :: IState -> Term -> Bool
posArg IState
ist (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ Term
nty Term
_) Term
sc) = Term -> Bool
noRec Term
nty Bool -> Bool -> Bool
&& IState -> Term -> Bool
posArg IState
ist Term
sc
    posArg IState
ist Term
t = IState -> Term -> Bool
posParams IState
ist Term
t

    noRec :: Term -> Bool
noRec Term
arg = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Name
x -> Name
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
mut_ns) (forall n. Eq n => TT n -> [n]
allTTNames Term
arg)

    -- If the type appears recursively in a parameter argument, that's
    -- fine, otherwise if it appears in an argument it's not fine.
    posParams :: IState -> Term -> Bool
posParams IState
ist Term
t | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t
       = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
              Just TypeInfo
ti -> forall {t :: * -> *} {t}.
(Foldable t, Eq t, Num t) =>
t t -> t -> [Term] -> Bool
checkParamsOK (TypeInfo -> [Int]
param_pos TypeInfo
ti) Int
0 [Term]
args
              Maybe TypeInfo
Nothing -> forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b. (a -> b) -> [a] -> [b]
map (IState -> Term -> Bool
posParams IState
ist) [Term]
args)
    posParams IState
ist Term
t = Term -> Bool
noRec Term
t

    checkParamsOK :: t t -> t -> [Term] -> Bool
checkParamsOK t t
ppos t
i [] = Bool
True
    checkParamsOK t t
ppos t
i (Term
p : [Term]
ps)
          | t
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t t
ppos = t t -> t -> [Term] -> Bool
checkParamsOK t t
ppos (t
i forall a. Num a => a -> a -> a
+ t
1) [Term]
ps
          | Bool
otherwise = Term -> Bool
noRec Term
p Bool -> Bool -> Bool
&& t t -> t -> [Term] -> Bool
checkParamsOK t t
ppos (t
i forall a. Num a => a -> a -> a
+ t
1) [Term]
ps

-- | Calculate the totality of a function from its patterns.  Either
-- follow the size change graph (if inductive) or check for
-- productivity (if coinductive)
calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
calcTotality FC
fc Name
n [([Name], Term, Term)]
pats
    = do IState
i <- Idris IState
getIState
         case forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (IState -> Term -> Maybe Totality
checkLHS IState
i) (forall a b. (a -> b) -> [a] -> [b]
map (\ ([Name]
_, Term
l, Term
r) -> Term
l) [([Name], Term, Term)]
pats) of
            (Totality
failure : [Totality]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Totality
failure
            [Totality]
_ -> Name -> Idris Totality
checkSizeChange Name
n
  where
    checkLHS :: IState -> Term -> Maybe Totality
checkLHS IState
i (P NameType
_ Name
fn Term
_)
        = case Name -> Context -> Maybe Totality
lookupTotalExact Name
fn (IState -> Context
tt_ctxt IState
i) of
               Just (Partial PReason
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (PReason -> Totality
Partial ([Name] -> PReason
Other [Name
fn]))
               Maybe Totality
_ -> forall a. Maybe a
Nothing
    checkLHS IState
i (App AppStatus Name
_ Term
f Term
a) = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (IState -> Term -> Maybe Totality
checkLHS IState
i Term
f) (IState -> Term -> Maybe Totality
checkLHS IState
i Term
a)
    checkLHS IState
_ Term
_ = forall a. Maybe a
Nothing

checkTotality :: [Name] -> FC -> Name -> Idris Totality
checkTotality :: [Name] -> FC -> Name -> Idris Totality
checkTotality [Name]
path FC
fc Name
n
    | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
path = forall (m :: * -> *) a. Monad m => a -> m a
return (PReason -> Totality
Partial ([Name] -> PReason
Mutual (Name
n forall a. a -> [a] -> [a]
: [Name]
path)))
    | Bool
otherwise = do
        Totality
t <- Name -> Idris Totality
getTotality Name
n
        IState
i <- Idris IState
getIState
        Context
ctxt' <- do Context
ctxt <- StateT IState (ExceptT Err IO) Context
getContext
                    forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef Name
n [] [] (IState -> ErasureInfo
getErasureInfo IState
i) Context
ctxt
        Context -> Idris ()
setContext Context
ctxt'
        Context
ctxt <- StateT IState (ExceptT Err IO) Context
getContext
        IState
i <- Idris IState
getIState
        let opts :: [FnOpt]
opts = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [FnOpt]
idris_flags IState
i) of
                            [[FnOpt]
fs] -> [FnOpt]
fs
                            [[FnOpt]]
_ -> []
        Totality
t' <- case Totality
t of
                Totality
Unchecked ->
                    case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
                        [CaseOp CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
pats CaseDefs
_] ->
                            do Totality
t' <- if FnOpt
AssertTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts
                                        then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Int] -> Totality
Total []
                                        else FC -> Name -> [([Name], Term, Term)] -> Idris Totality
calcTotality FC
fc Name
n [([Name], Term, Term)]
pats
                               Int -> [Char] -> Idris ()
logCoverage Int
2 forall a b. (a -> b) -> a -> b
$ [Char]
"Set to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Totality
t'
                               Name -> Totality -> Idris ()
setTotality Name
n Totality
t'
                               IBCWrite -> Idris ()
addIBC (Name -> Totality -> IBCWrite
IBCTotal Name
n Totality
t')
                               forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
                        [TyDecl (DCon Int
_ Int
_ Bool
_) Term
ty] ->
                            case forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
getRetTy Term
ty) of
                              (P NameType
_ Name
tyn Term
_, [Term]
_) -> do
                                 let ms :: [Name]
ms = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
tyn (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
                                       [TI [Name]
_ Bool
_ DataOpts
_ [Int]
_ xs :: [Name]
xs@(Name
_:[Name]
_) Bool
_] -> [Name]
xs
                                       [TypeInfo]
ts -> [Name
tyn]
                                 [Name] -> (Name, Term) -> Idris Totality
checkPositive [Name]
ms (Name
n, Term
ty)
                              (Term, [Term])
_-> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Int] -> Totality
Total []
                        [Def]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Int] -> Totality
Total []
                Totality
x -> forall (m :: * -> *) a. Monad m => a -> m a
return Totality
x
        case Totality
t' of
            Total [Int]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
            Totality
Productive -> forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
            Totality
e -> do Bool
w <- Opt -> Idris Bool
cmdOptType Opt
WarnPartial
                    if FnOpt
TotalFn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts
                       then do forall {p}. Show p => p -> Idris ()
totalityError Totality
t'; forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
                       else do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
w Bool -> Bool -> Bool
&& Bool -> Bool
not (FnOpt
PartialFn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts)) forall a b. (a -> b) -> a -> b
$
                                   forall {a}. Show a => Name -> a -> Idris ()
warnPartial Name
n Totality
t'
                               forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
  where
    totalityError :: p -> Idris ()
totalityError p
t = do IState
i <- Idris IState
getIState
                         let msg :: [Char]
msg = forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show p
t
                         IState -> Idris ()
putIState IState
i { idris_totcheckfail :: [(FC, [Char])]
idris_totcheckfail = (FC
fc, [Char]
msg) forall a. a -> [a] -> [a]
: IState -> [(FC, [Char])]
idris_totcheckfail IState
i}
                         IBCWrite -> Idris ()
addIBC (FC -> [Char] -> IBCWrite
IBCTotCheckErr FC
fc [Char]
msg)

    warnPartial :: Name -> a -> Idris ()
warnPartial Name
n a
t
       = do IState
i <- Idris IState
getIState
            case Name -> Context -> [Def]
lookupDef Name
n (IState -> Context
tt_ctxt IState
i) of
               [Def
x] -> do
                  FC -> OutputDoc -> Idris ()
iWarn FC
fc forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> Err -> OutputDoc
pprintErr IState
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. [Char] -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ [Char]
"Warning - " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
t
--                                ++ "\n" ++ show x
--                   let cg = lookupCtxtName Nothing n (idris_callgraph i)
--                   iputStrLn (show cg)


checkDeclTotality :: (FC, Name) -> Idris Totality
checkDeclTotality :: (FC, Name) -> Idris Totality
checkDeclTotality (FC
fc, Name
n)
    = do Int -> [Char] -> Idris ()
logCoverage Int
2 forall a b. (a -> b) -> a -> b
$ [Char]
"Checking " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" for totality"
         IState
i <- Idris IState
getIState
         let opts :: [FnOpt]
opts = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [FnOpt]
idris_flags IState
i) of
                              Just [FnOpt]
fs -> [FnOpt]
fs
                              Maybe [FnOpt]
_ -> []
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
CoveringFn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts) forall a b. (a -> b) -> a -> b
$ FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering FC
fc [] Name
n Name
n
         Totality
t <- [Name] -> FC -> Name -> Idris Totality
checkTotality [] FC
fc Name
n
         forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t

-- If the name calls something which is partial, set it as partial
verifyTotality :: (FC, Name) -> Idris ()
verifyTotality :: (FC, Name) -> Idris ()
verifyTotality (FC
fc, Name
n)
    = do Int -> [Char] -> Idris ()
logCoverage Int
2 forall a b. (a -> b) -> a -> b
$ [Char]
"Checking " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
"'s descendents are total"
         IState
ist <- Idris IState
getIState
         case Name -> Context -> Maybe Totality
lookupTotalExact Name
n (IState -> Context
tt_ctxt IState
ist) of
              Just (Total [Int]
_) -> do
                 let ns :: [Name]
ns = Context -> [Name]
getNames (IState -> Context
tt_ctxt IState
ist)

                 case IState -> [Name] -> [Name] -> Maybe [Name]
getPartial IState
ist [] [Name]
ns of
                      Maybe [Name]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                      Just [Name]
bad -> do let t' :: Totality
t' = PReason -> Totality
Partial ([Name] -> PReason
Other [Name]
bad)
                                     Int -> [Char] -> Idris ()
logCoverage Int
2 forall a b. (a -> b) -> a -> b
$ [Char]
"Set in verify to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Totality
t'
                                     Name -> Totality -> Idris ()
setTotality Name
n Totality
t'
                                     IBCWrite -> Idris ()
addIBC (Name -> Totality -> IBCWrite
IBCTotal Name
n Totality
t')
              Maybe Totality
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    getNames :: Context -> [Name]
getNames Context
ctxt = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
                         Just (CaseOp  CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
defs)
                           -> let ([Name]
top, SC
def) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
defs in
                                  forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (Bool -> SC -> [Name] -> [(Name, [[Name]])]
findCalls' Bool
True SC
def [Name]
top)
                         Maybe Def
_ -> []

    getPartial :: IState -> [Name] -> [Name] -> Maybe [Name]
getPartial IState
ist [] [] = forall a. Maybe a
Nothing
    getPartial IState
ist [Name]
bad [] = forall a. a -> Maybe a
Just [Name]
bad
    getPartial IState
ist [Name]
bad (Name
n : [Name]
ns)
        = case Name -> Context -> Maybe Totality
lookupTotalExact Name
n (IState -> Context
tt_ctxt IState
ist) of
               Just (Partial PReason
_) -> IState -> [Name] -> [Name] -> Maybe [Name]
getPartial IState
ist (Name
n forall a. a -> [a] -> [a]
: [Name]
bad) [Name]
ns
               Maybe Totality
_ -> IState -> [Name] -> [Name] -> Maybe [Name]
getPartial IState
ist [Name]
bad [Name]
ns

-- | Calculate the size change graph for this definition
--
-- SCG for a function f consists of a list of:
--    (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
--
-- where g is a function called
-- a1 ... an are the arguments of f in positions 1..n of g
-- sizechange1 ... sizechange2 is how their size has changed wrt the input
-- to f
--    Nothing, if the argument is unrelated to the input
buildSCG :: (FC, Name) -> Idris ()
buildSCG :: (FC, Name) -> Idris ()
buildSCG (FC
_, Name
n) = do
   IState
ist <- Idris IState
getIState
   case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt CGInfo
idris_callgraph IState
ist) of
       Just CGInfo
cg -> case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
ist) of
           Just (CaseOp CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
pats [([Name], Term, Term)]
_ CaseDefs
cd) ->
             let ([Name]
args, SC
sc) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd in
               do Int -> [Char] -> Idris ()
logCoverage Int
2 forall a b. (a -> b) -> a -> b
$ [Char]
"Building SCG for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" from\n"
                                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Either Term (Term, Term)]
pats forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SC
sc
                  let newscg :: [SCGEntry]
newscg = IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
buildSCG' IState
ist Name
n (forall a b. [Either a b] -> [b]
rights [Either Term (Term, Term)]
pats) [Name]
args
                  Int -> [Char] -> Idris ()
logCoverage Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"SCG is: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [SCGEntry]
newscg
                  Name -> CGInfo -> Idris ()
addToCG Name
n ( CGInfo
cg { scg :: [SCGEntry]
scg = [SCGEntry]
newscg } )
           Maybe Def
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return () -- CG comes from a type declaration only
       Maybe CGInfo
_ -> Int -> [Char] -> Idris ()
logCoverage Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"Could not build SCG for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
"\n"

delazy :: Term -> Term
delazy = Bool -> Term -> Term
delazy' Bool
False -- not lazy codata
delazy' :: Bool -> Term -> Term
delazy' Bool
all t :: Term
t@(App AppStatus Name
_ Term
f Term
a)
     | (P NameType
_ (UN Text
l) Term
_, [P NameType
_ (UN Text
lty) Term
_, Term
_, Term
arg]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t,
       Text
l forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Force" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty forall a. Eq a => a -> a -> Bool
/= [Char] -> Text
txt [Char]
"Infinite") = Bool -> Term -> Term
delazy' Bool
all Term
arg
     | (P NameType
_ (UN Text
l) Term
_, [P NameType
_ (UN Text
lty) Term
_, Term
_, Term
arg]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t,
       Text
l forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Delay" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty forall a. Eq a => a -> a -> Bool
/= [Char] -> Text
txt [Char]
"Infinite") = Term -> Term
delazy Term
arg
     | (P NameType
_ (UN Text
l) Term
_, [P NameType
_ (UN Text
lty) Term
_, Term
arg]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t,
       Text
l forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Delayed" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty forall a. Eq a => a -> a -> Bool
/= [Char] -> Text
txt [Char]
"Infinite") = Bool -> Term -> Term
delazy' Bool
all Term
arg
delazy' Bool
all (App AppStatus Name
s Term
f Term
a) = forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Bool -> Term -> Term
delazy' Bool
all Term
f) (Bool -> Term -> Term
delazy' Bool
all Term
a)
delazy' Bool
all (Bind Name
n Binder Term
b Term
sc) = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Term -> Term
delazy' Bool
all) Binder Term
b) (Bool -> Term -> Term
delazy' Bool
all Term
sc)
delazy' Bool
all Term
t = Term
t

data Guardedness = Toplevel | Unguarded | Guarded | Delayed
  deriving Int -> Guardedness -> ShowS
[Guardedness] -> ShowS
Guardedness -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Guardedness] -> ShowS
$cshowList :: [Guardedness] -> ShowS
show :: Guardedness -> [Char]
$cshow :: Guardedness -> [Char]
showsPrec :: Int -> Guardedness -> ShowS
$cshowsPrec :: Int -> Guardedness -> ShowS
Show

buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
buildSCG' IState
ist Name
topfn [(Term, Term)]
pats [Name]
args = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Term, Term) -> [SCGEntry]
scgPat [(Term, Term)]
pats where
  scgPat :: (Term, Term) -> [SCGEntry]
scgPat (Term
lhs, Term
rhs) = let lhs' :: Term
lhs' = Term -> Term
delazy Term
lhs
                          rhs' :: Term
rhs' = Term -> Term
delazy Term
rhs
                          (Term
_, [Term]
pargs) = forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
dePat Term
lhs') in
                            [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [] Guardedness
Toplevel (forall n. TT n -> TT n
dePat Term
rhs') (forall {a}. TT a -> [a]
patvars Term
lhs')
                                      (forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
pargs [Int
0..])

  -- Under a delay, calls are excluded from the graph - if it's a call to a
  -- non-total function we'll find that in the final totality check
  findCalls :: [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Delayed ap :: Term
ap@(P NameType
_ Name
n Term
_) [Name]
pvs [(Term, Int)]
args = []
  findCalls [Name]
cases Guardedness
guarded ap :: Term
ap@(App AppStatus Name
_ Term
f Term
a) [Name]
pvs [(Term, Int)]
pargs
     -- under a call to "assert_total", don't do any checking, just believe
     -- that it is total.
     | (P NameType
_ (UN Text
at) Term
_, [Term
_, Term
_]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Text
at forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"assert_total" = []
     -- don't go under calls to functions which are asserted total
     | (P NameType
_ Name
n Term
_, [Term]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Just [FnOpt]
opts <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [FnOpt]
idris_flags IState
ist),
       FnOpt
AssertTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts = []
     -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't
     -- check under guarded constructors.
     | (P NameType
_ (UN Text
del) Term
_, [Term
_,Term
_,Term
arg]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Guardedness
Guarded <- Guardedness
guarded,
       Text
del forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Delay"
           = [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Delayed Term
arg [Name]
pvs [(Term, Int)]
pargs
     | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Guardedness
Delayed <- Guardedness
guarded,
       Name -> Context -> Bool
isConName Name
n (IState -> Context
tt_ctxt IState
ist) Bool -> Bool -> Bool
|| Name -> IState -> Bool
allGuarded Name
n IState
ist
           = -- Still under a 'Delay' and constructor guarded, so check
             -- just the arguments to the constructor, remaining Delayed
             forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Term
x -> [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Term
x [Name]
pvs [(Term, Int)]
pargs) [Term]
args
     | (P NameType
_ Name
ifthenelse Term
_, [Term
_, Term
_, Term
t, Term
e]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Name
ifthenelse forall a. Eq a => a -> a -> Bool
== Name -> [[Char]] -> Name
sNS ([Char] -> Name
sUN [Char]
"ifThenElse") [[Char]
"Bool", [Char]
"Prelude"]
       -- Continue look inside if...then...else blocks
       -- TODO: Consider whether we should do this for user defined ifThenElse
       -- rather than just the one in the Prelude as a special case
       = [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Term
t [Name]
pvs [(Term, Int)]
pargs forall a. [a] -> [a] -> [a]
++
         [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Term
e [Name]
pvs [(Term, Int)]
pargs
     | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Name -> Bool
caseName Name
n Bool -> Bool -> Bool
&& Name
n forall a. Eq a => a -> a -> Bool
/= Name
topfn,
       Maybe Totality -> Bool
notPartial (Name -> Context -> Maybe Totality
lookupTotalExact Name
n (IState -> Context
tt_ctxt IState
ist))
       -- case block - look inside the block, as long as it was covering
       -- (i.e. not currently set at Partial) to get a more accurate size
       -- change result from the top level patterns (also to help pass
       -- information through from guarded corecursion accurately)
       = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Term
x -> [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Term
x [Name]
pvs [(Term, Int)]
pargs) [Term]
args forall a. [a] -> [a] -> [a]
++
             if Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
cases
                then [Name]
-> Guardedness
-> Name
-> [Term]
-> [Name]
-> [(Term, Int)]
-> [SCGEntry]
findCallsCase (Name
n forall a. a -> [a] -> [a]
: [Name]
cases) Guardedness
guarded Name
n [Term]
args [Name]
pvs [(Term, Int)]
pargs
                else []
     | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Guardedness
Delayed <- Guardedness
guarded
       -- Under a delayed recursive call just check the arguments
           = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Term
x -> [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Term
x [Name]
pvs [(Term, Int)]
pargs) [Term]
args
     | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
       Bool -> Bool
not (Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
pvs)
        -- Ordinary call, not under a delay.
        -- If n is a constructor, set 'args' as Guarded
        = let nguarded :: Guardedness
nguarded = case Guardedness
guarded of
                              Guardedness
Unguarded -> Guardedness
Unguarded
                              Guardedness
x -> if Name -> Context -> Bool
isConName Name
n (IState -> Context
tt_ctxt IState
ist)
                                       Bool -> Bool -> Bool
|| Name -> IState -> Bool
allGuarded Name
n IState
ist
                                      then Guardedness
Guarded
                                      else Guardedness
Unguarded in
              forall {a}.
Name -> [Term] -> [(Term, a)] -> [(Name, [Maybe (a, SizeChange)])]
mkChange Name
n [Term]
args [(Term, Int)]
pargs forall a. [a] -> [a] -> [a]
++
                 forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Term
x -> [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
nguarded Term
x [Name]
pvs [(Term, Int)]
pargs) [Term]
args
    where notPartial :: Maybe Totality -> Bool
notPartial (Just (Partial PReason
NotCovering)) = Bool
False
          notPartial Maybe Totality
_ = Bool
True
  findCalls [Name]
cases Guardedness
guarded (App AppStatus Name
_ Term
f Term
a) [Name]
pvs [(Term, Int)]
pargs
        = [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Term
f [Name]
pvs [(Term, Int)]
pargs forall a. [a] -> [a] -> [a]
++ [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Term
a [Name]
pvs [(Term, Int)]
pargs
  findCalls [Name]
cases Guardedness
guarded (Bind Name
n (Let RigCount
rig Term
t Term
v) Term
e) [Name]
pvs [(Term, Int)]
pargs
        = [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Term
t [Name]
pvs [(Term, Int)]
pargs forall a. [a] -> [a] -> [a]
++
          [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Term
v [Name]
pvs [(Term, Int)]
pargs forall a. [a] -> [a] -> [a]
++
          -- Substitute in the scope since this might reveal some useful
          -- structure
          [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded (forall n. TT n -> TT n -> TT n
substV Term
v Term
e) [Name]
pvs [(Term, Int)]
pargs
  findCalls [Name]
cases Guardedness
guarded (Bind Name
n Binder Term
t Term
e) [Name]
pvs [(Term, Int)]
pargs
        = [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded (forall b. Binder b -> b
binderTy Binder Term
t) [Name]
pvs [(Term, Int)]
pargs forall a. [a] -> [a] -> [a]
++
          [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Term
e (Name
n forall a. a -> [a] -> [a]
: [Name]
pvs) [(Term, Int)]
pargs
  findCalls [Name]
cases Guardedness
guarded (P NameType
_ Name
f Term
_ ) [Name]
pvs [(Term, Int)]
pargs
      | Bool -> Bool
not (Name
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
pvs) = [(Name
f, [])]
  findCalls [Name]
_ Guardedness
_ Term
_ [Name]
_ [(Term, Int)]
_ = []

  -- Assumption is that names are preserved in the case block (shadowing
  -- dealt with by the elaborator) so we can just assume the top level names
  -- are okay for building the size change
  findCallsCase :: [Name]
-> Guardedness
-> Name
-> [Term]
-> [Name]
-> [(Term, Int)]
-> [SCGEntry]
findCallsCase [Name]
cases Guardedness
guarded Name
n [Term]
args [Name]
pvs [(Term, Int)]
pargs
      = case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
ist) of
           Just (CaseOp CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
pats [([Name], Term, Term)]
_ CaseDefs
cd) ->
                forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Name]
-> [Name]
-> [(Term, Int)]
-> [Term]
-> Guardedness
-> (Term, Term)
-> [SCGEntry]
fccPat [Name]
cases [Name]
pvs [(Term, Int)]
pargs [Term]
args Guardedness
guarded) (forall a b. [Either a b] -> [b]
rights [Either Term (Term, Term)]
pats)
           Maybe Def
Nothing -> []

  fccPat :: [Name]
-> [Name]
-> [(Term, Int)]
-> [Term]
-> Guardedness
-> (Term, Term)
-> [SCGEntry]
fccPat [Name]
cases [Name]
pvs [(Term, Int)]
pargs [Term]
args Guardedness
g (Term
lhs, Term
rhs)
      = let lhs' :: Term
lhs' = Term -> Term
delazy Term
lhs
            rhs' :: Term
rhs' = Term -> Term
delazy Term
rhs
            (Term
_, [Term]
pargs_case) = forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
dePat Term
lhs')
            -- pargs is a pair of a term, and the argument position that
            -- term appears in. If any of the arguments to the case block
            -- are also on the lhs, we also want those patterns to appear
            -- in the parg list so that we'll spot patterns which are
            -- smaller than then
            newpargs :: [Maybe (Term, Int)]
newpargs = [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
newPArg [Term]
args [(Term, Int)]
pargs
            -- Now need to update the rhs of the case with the names in the
            -- outer definition: In rhs', wherever we see what's in pargs_case,
            -- replace it with the corresponding thing in pargs
            csubs :: [(Term, Term)]
csubs = forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
pargs_case [Term]
args
            newrhs :: Term
newrhs = forall {n}. Eq n => [(TT n, TT n)] -> TT n -> TT n
doCaseSubs [(Term, Term)]
csubs (forall n. TT n -> TT n
dePat Term
rhs')
            pargs' :: [(Term, Int)]
pargs' = [(Term, Int)]
pargs forall a. [a] -> [a] -> [a]
++ forall {a} {b} {a}. [Maybe (a, b)] -> [a] -> [(a, b)]
addPArg [Maybe (Term, Int)]
newpargs [Term]
pargs_case in
               [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
g Term
newrhs [Name]
pvs [(Term, Int)]
pargs'
    where
      doCaseSubs :: [(TT n, TT n)] -> TT n -> TT n
doCaseSubs [] TT n
tm = TT n
tm
      doCaseSubs ((TT n
x, TT n
x') : [(TT n, TT n)]
cs) TT n
tm
           = [(TT n, TT n)] -> TT n -> TT n
doCaseSubs (forall {n}.
Eq n =>
TT n -> TT n -> [(TT n, TT n)] -> [(TT n, TT n)]
subIn TT n
x TT n
x' [(TT n, TT n)]
cs) (forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm TT n
x TT n
x' TT n
tm)

      subIn :: TT n -> TT n -> [(TT n, TT n)] -> [(TT n, TT n)]
subIn TT n
x TT n
x' [] = []
      subIn TT n
x TT n
x' ((TT n
l, TT n
r) : [(TT n, TT n)]
cs)
          = (forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm TT n
x TT n
x' TT n
l, forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm TT n
x TT n
x' TT n
r) forall a. a -> [a] -> [a]
: TT n -> TT n -> [(TT n, TT n)] -> [(TT n, TT n)]
subIn TT n
x TT n
x' [(TT n, TT n)]
cs

  addPArg :: [Maybe (a, b)] -> [a] -> [(a, b)]
addPArg (Just (a
t, b
i) : [Maybe (a, b)]
ts) (a
t' : [a]
ts') = (a
t', b
i) forall a. a -> [a] -> [a]
: [Maybe (a, b)] -> [a] -> [(a, b)]
addPArg [Maybe (a, b)]
ts [a]
ts'
  addPArg (Maybe (a, b)
Nothing : [Maybe (a, b)]
ts) (a
t' : [a]
ts') = [Maybe (a, b)] -> [a] -> [(a, b)]
addPArg [Maybe (a, b)]
ts [a]
ts'
  addPArg [Maybe (a, b)]
_ [a]
_ = []

  newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
  newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
newPArg (Term
t : [Term]
ts) [(Term, Int)]
pargs = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Term
t [(Term, Int)]
pargs of
                                Just Int
i -> forall a. a -> Maybe a
Just (Term
t, Int
i) forall a. a -> [a] -> [a]
: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
newPArg [Term]
ts [(Term, Int)]
pargs
                                Maybe Int
Nothing -> forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
newPArg [Term]
ts [(Term, Int)]
pargs
  newPArg [] [(Term, Int)]
pargs = []

  expandToArity :: Name -> [Maybe a] -> [Maybe a]
expandToArity Name
n [Maybe a]
args
     = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
            [Term
ty] -> forall {t} {n} {a}. Num t => t -> TT n -> [Maybe a] -> [Maybe a]
expand Integer
0 (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
ty) [Maybe a]
args
            [Term]
_ -> [Maybe a]
args
     where expand :: t -> TT n -> [Maybe a] -> [Maybe a]
expand t
i (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
_ TT n
_) TT n
sc) (Maybe a
x : [Maybe a]
xs) = Maybe a
x forall a. a -> [a] -> [a]
: t -> TT n -> [Maybe a] -> [Maybe a]
expand (t
i forall a. Num a => a -> a -> a
+ t
1) TT n
sc [Maybe a]
xs
           expand t
i (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
_ TT n
_) TT n
sc) [] = forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: t -> TT n -> [Maybe a] -> [Maybe a]
expand (t
i forall a. Num a => a -> a -> a
+ t
1) TT n
sc []
           expand t
i TT n
_ [Maybe a]
xs = [Maybe a]
xs

  mkChange :: Name -> [Term] -> [(Term, a)] -> [(Name, [Maybe (a, SizeChange)])]
mkChange Name
n [Term]
args [(Term, a)]
pargs = [(Name
n, forall {a}. Name -> [Maybe a] -> [Maybe a]
expandToArity Name
n ([Term] -> [Maybe (a, SizeChange)]
sizes [Term]
args))]
    where
      sizes :: [Term] -> [Maybe (a, SizeChange)]
sizes [] = []
      sizes (Term
a : [Term]
as) = forall {a}. Term -> [(Term, a)] -> Maybe (a, SizeChange)
checkSize Term
a [(Term, a)]
pargs forall a. a -> [a] -> [a]
: [Term] -> [Maybe (a, SizeChange)]
sizes [Term]
as

      -- find which argument in pargs <a> is smaller than, if any
      checkSize :: Term -> [(Term, a)] -> Maybe (a, SizeChange)
checkSize Term
a ((Term
p, a
i) : [(Term, a)]
ps)
          | Term
a forall a. Eq a => a -> a -> Bool
== Term
p = forall a. a -> Maybe a
Just (a
i, SizeChange
Same)
          | (P NameType
_ (UN Text
as) Term
_, [Term
_,Term
_,Term
arg,Term
_]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
a,
            Text
as forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"assert_smaller" Bool -> Bool -> Bool
&& Term
arg forall a. Eq a => a -> a -> Bool
== Term
p
                  = forall a. a -> Maybe a
Just (a
i, SizeChange
Smaller)
          | Maybe Term -> Term -> (Term, Maybe Term) -> Bool
smaller forall a. Maybe a
Nothing Term
a (Term
p, forall a. Maybe a
Nothing) = forall a. a -> Maybe a
Just (a
i, SizeChange
Smaller)
          | Bool
otherwise = Term -> [(Term, a)] -> Maybe (a, SizeChange)
checkSize Term
a [(Term, a)]
ps
      checkSize Term
a [] = forall a. Maybe a
Nothing

      -- Can't be smaller than an erased thing (need to be careful here
      -- because Erased equals everything)
      smaller :: Maybe Term -> Term -> (Term, Maybe Term) -> Bool
smaller Maybe Term
_ Term
_ (Term
Erased, Maybe Term
_) = Bool
False -- never smaller than an erased thing
      -- If a == t, and we're under a cosntructor, we've found something
      -- smaller
      smaller (Just Term
tyn) Term
a (Term
t, Just Term
tyt) | Term
a forall a. Eq a => a -> a -> Bool
== Term
t = Bool
True
      smaller Maybe Term
ty Term
a (ap :: Term
ap@(App AppStatus Name
_ Term
f Term
s), Maybe Term
_)
          -- Nothing can be smaller than a delayed infinite thing...
          | (P (DCon Int
_ Int
_ Bool
_) (UN Text
d) Term
_, [P NameType
_ (UN Text
reason) Term
_, Term
_, Term
_]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
            Text
d forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Delay" Bool -> Bool -> Bool
&& Text
reason forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Infinite"
               = Bool
False
          | (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap
               = let tyn :: Term
tyn = Name -> Term
getType Name
n in
                     forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Term -> Term -> (Term, Maybe Term) -> Bool
smaller (Maybe Term
ty forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. a -> Maybe a
Just Term
tyn) Term
a)
                         (forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
args (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (a, a) -> Maybe a
toJust (forall n. TT n -> [(n, TT n)]
getArgTys Term
tyn)))
      -- check higher order recursive arguments
      smaller Maybe Term
ty (App AppStatus Name
_ Term
f Term
s) (Term, Maybe Term)
a = Maybe Term -> Term -> (Term, Maybe Term) -> Bool
smaller Maybe Term
ty Term
f (Term, Maybe Term)
a
      smaller Maybe Term
_ Term
_ (Term, Maybe Term)
_ = Bool
False

      toJust :: (a, a) -> Maybe a
toJust (a
n, a
t) = forall a. a -> Maybe a
Just a
t

      getType :: Name -> Term
getType Name
n = case Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
                       Just Term
ty -> Term -> Term
delazy (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
ty) -- must exist

  dePat :: TT n -> TT n
dePat (Bind n
x (PVar RigCount
_ TT n
ty) TT n
sc) = TT n -> TT n
dePat (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
x TT n
ty) TT n
sc)
  dePat TT n
t = TT n
t

  patvars :: TT a -> [a]
patvars (Bind a
x (PVar RigCount
_ TT a
_) TT a
sc) = a
x forall a. a -> [a] -> [a]
: TT a -> [a]
patvars TT a
sc
  patvars TT a
_ = []

  allGuarded :: Name -> IState -> Bool
allGuarded Name
n IState
ist = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [FnOpt]
idris_flags IState
ist) of
                          Maybe [FnOpt]
Nothing -> Bool
False
                          Just [FnOpt]
fs -> FnOpt
AllGuarded forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
fs

checkSizeChange :: Name -> Idris Totality
checkSizeChange :: Name -> Idris Totality
checkSizeChange Name
n = do
   IState
ist <- Idris IState
getIState
   case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt CGInfo
idris_callgraph IState
ist) of
       [CGInfo
cg] -> do let ms :: [[SCGEntry]]
ms = IState -> [SCGEntry] -> [SCGEntry] -> [[SCGEntry]]
mkMultiPaths IState
ist [] (CGInfo -> [SCGEntry]
scg CGInfo
cg)
                  Int -> [Char] -> Idris ()
logCoverage Int
5 ([Char]
"Multipath for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
":\n" forall a. [a] -> [a] -> [a]
++
                            [Char]
"from " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (CGInfo -> [SCGEntry]
scg CGInfo
cg) forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++
                            forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [[SCGEntry]]
ms) forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++
                            [Char] -> [[Char]] -> [Char]
showSep [Char]
"\n" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [[SCGEntry]]
ms))
                  Int -> [Char] -> Idris ()
logCoverage Int
6 (forall a. Show a => a -> [Char]
show CGInfo
cg)
                  -- every multipath must have an infinitely descending
                  -- thread, then the function terminates
                  -- also need to checks functions called are all total
                  -- (Unchecked is okay as we'll spot problems here)
                  let tot :: [Totality]
tot = forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> Int -> [SCGEntry] -> Totality
checkMP IState
ist Name
n (IState -> Name -> Int
getArity IState
ist Name
n)) [[SCGEntry]]
ms
                  Int -> [Char] -> Idris ()
logCoverage Int
4 forall a b. (a -> b) -> a -> b
$ [Char]
"Generated " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Totality]
tot) forall a. [a] -> [a] -> [a]
++ [Char]
" paths"
                  Int -> [Char] -> Idris ()
logCoverage Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"Paths for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" yield " forall a. [a] -> [a] -> [a]
++
                       ([Char] -> [[Char]] -> [Char]
showSep [Char]
"\n" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show (forall a b. [a] -> [b] -> [(a, b)]
zip [[SCGEntry]]
ms [Totality]
tot)))
                  forall (m :: * -> *) a. Monad m => a -> m a
return ([Totality] -> Totality
noPartial [Totality]
tot)
       [] -> do Int -> [Char] -> Idris ()
logCoverage Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"No paths for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name
n
                forall (m :: * -> *) a. Monad m => a -> m a
return Totality
Unchecked
  where getArity :: IState -> Name -> Int
getArity IState
ist Name
n
          = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
                 [Term
ty] -> forall n. TT n -> Int
arity (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
ty)
                 [Term]
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Can't happen: checkSizeChange.getArity"

type MultiPath = [SCGEntry]

mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
mkMultiPaths :: IState -> [SCGEntry] -> [SCGEntry] -> [[SCGEntry]]
mkMultiPaths IState
ist [SCGEntry]
path [] = [forall a. [a] -> [a]
reverse [SCGEntry]
path]
mkMultiPaths IState
ist [SCGEntry]
path [SCGEntry]
cg = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SCGEntry -> [[SCGEntry]]
extend [SCGEntry]
cg
  where extend :: SCGEntry -> [[SCGEntry]]
extend (Name
nextf, [Maybe (Int, SizeChange)]
args)
           | (Name
nextf, [Maybe (Int, SizeChange)]
args) SCGEntry -> [SCGEntry] -> Bool
`inPath` [SCGEntry]
path = [ forall a. [a] -> [a]
reverse ((Name
nextf, [Maybe (Int, SizeChange)]
args) forall a. a -> [a] -> [a]
: [SCGEntry]
path) ]
           | [Totality
Unchecked] <- Name -> Context -> [Totality]
lookupTotal Name
nextf (IState -> Context
tt_ctxt IState
ist)
               = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
nextf (IState -> Ctxt CGInfo
idris_callgraph IState
ist) of
                    [CGInfo
ncg] -> IState -> [SCGEntry] -> [SCGEntry] -> [[SCGEntry]]
mkMultiPaths IState
ist ((Name
nextf, [Maybe (Int, SizeChange)]
args) forall a. a -> [a] -> [a]
: [SCGEntry]
path) (CGInfo -> [SCGEntry]
scg CGInfo
ncg)
                    [CGInfo]
_ -> [ forall a. [a] -> [a]
reverse ((Name
nextf, [Maybe (Int, SizeChange)]
args) forall a. a -> [a] -> [a]
: [SCGEntry]
path) ]
           | Bool
otherwise = [ forall a. [a] -> [a]
reverse ((Name
nextf, [Maybe (Int, SizeChange)]
args) forall a. a -> [a] -> [a]
: [SCGEntry]
path) ]

        inPath :: SCGEntry -> [SCGEntry] -> Bool
        inPath :: SCGEntry -> [SCGEntry] -> Bool
inPath SCGEntry
f [] = Bool
False
        inPath SCGEntry
f (SCGEntry
g : [SCGEntry]
gs) = SCGEntry -> SCGEntry -> Bool
smallerEq SCGEntry
f SCGEntry
g Bool -> Bool -> Bool
|| SCGEntry
f forall a. Eq a => a -> a -> Bool
== SCGEntry
g Bool -> Bool -> Bool
|| SCGEntry -> [SCGEntry] -> Bool
inPath SCGEntry
f [SCGEntry]
gs

        smallerEq :: SCGEntry -> SCGEntry -> Bool
        smallerEq :: SCGEntry -> SCGEntry -> Bool
smallerEq (Name
f, [Maybe (Int, SizeChange)]
args) (Name
g, [Maybe (Int, SizeChange)]
args')
            = Name
f forall a. Eq a => a -> a -> Bool
== Name
g Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. Maybe (a, SizeChange) -> Bool
smallers [Maybe (Int, SizeChange)]
args))
                     Bool -> Bool -> Bool
&& forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. Maybe (a, SizeChange) -> Bool
smallers [Maybe (Int, SizeChange)]
args forall a. Eq a => a -> a -> Bool
== forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. Maybe (a, SizeChange) -> Bool
smallers [Maybe (Int, SizeChange)]
args'
        smallers :: Maybe (a, SizeChange) -> Bool
smallers (Just (a
_, SizeChange
Smaller)) = Bool
True
        smallers Maybe (a, SizeChange)
_ = Bool
False

-- If any route along the multipath leads to infinite descent, we're fine.
-- Try a route beginning with every argument.
--   If we reach a point we've been to before, but with a smaller value,
--   that means there is an infinitely descending path from that argument.

checkMP :: IState -> Name -> Int -> MultiPath -> Totality
checkMP :: IState -> Name -> Int -> [SCGEntry] -> Totality
checkMP IState
ist Name
topfn Int
i [SCGEntry]
mp = if Int
i forall a. Ord a => a -> a -> Bool
> Int
0
                     then let paths :: [Totality]
paths = (forall a b. (a -> b) -> [a] -> [b]
map (Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
0 [] [SCGEntry]
mp) [Int
0..Int
iforall a. Num a => a -> a -> a
-Int
1]) in
--                               trace ("Paths " ++ show paths) $
                               [Totality] -> Totality
collapse [Totality]
paths
                     else Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
0 [] [SCGEntry]
mp Int
0
  where
    mkBig :: (a, b) -> (a, b)
mkBig (a
e, b
d) = (a
e, b
10000)

    tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
    tryPath :: Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
desc [((SCGEntry, Int), Int)]
path [] Int
_ = [Int] -> Totality
Total []
--     tryPath desc path ((UN "believe_me", _) : _) arg
--             = Partial BelieveMe
    -- if we get to a constructor, it's fine as long as it's strictly positive
    tryPath Int
desc [((SCGEntry, Int), Int)]
path ((Name
f, [Maybe (Int, SizeChange)]
_) : [SCGEntry]
es) Int
arg
        | [TyDecl (DCon Int
_ Int
_ Bool
_) Term
_] <- Name -> Context -> [Def]
lookupDef Name
f (IState -> Context
tt_ctxt IState
ist)
            = case Name -> Context -> Maybe Totality
lookupTotalExact Name
f (IState -> Context
tt_ctxt IState
ist) of
                   Just (Total [Int]
_) -> Totality
Unchecked -- okay so far
                   Just (Partial PReason
_) -> PReason -> Totality
Partial ([Name] -> PReason
Other [Name
f])
                   Maybe Totality
x -> Totality
Unchecked -- An error elsewhere, set as Unchecked to make
                                  -- some progress
        | [TyDecl (TCon Int
_ Int
_) Term
_] <- Name -> Context -> [Def]
lookupDef Name
f (IState -> Context
tt_ctxt IState
ist)
            = [Int] -> Totality
Total []
    tryPath Int
desc [((SCGEntry, Int), Int)]
path (e :: SCGEntry
e@(Name
f, [Maybe (Int, SizeChange)]
args) : [SCGEntry]
es) Int
arg
        | [Total [Int]
a] <- Name -> Context -> [Totality]
lookupTotal Name
f (IState -> Context
tt_ctxt IState
ist) = [Int] -> Totality
Total [Int]
a
        | SCGEntry
e forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SCGEntry]
es Bool -> Bool -> Bool
&& forall a. [Maybe a] -> Bool
allNothing [Maybe (Int, SizeChange)]
args = PReason -> Totality
Partial ([Name] -> PReason
Mutual [Name
f])
    tryPath Int
desc [((SCGEntry, Int), Int)]
path (e :: SCGEntry
e@(Name
f, [Maybe (Int, SizeChange)]
nextargs) : [SCGEntry]
es) Int
arg
        | [Total [Int]
a] <- Name -> Context -> [Totality]
lookupTotal Name
f (IState -> Context
tt_ctxt IState
ist) = [Int] -> Totality
Total [Int]
a
        | [Partial PReason
_] <- Name -> Context -> [Totality]
lookupTotal Name
f (IState -> Context
tt_ctxt IState
ist) = PReason -> Totality
Partial ([Name] -> PReason
Other [Name
f])
        | Just Int
d <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (SCGEntry
e, Int
arg) [((SCGEntry, Int), Int)]
path
            = if Int
desc forall a. Num a => a -> a -> a
- Int
d forall a. Ord a => a -> a -> Bool
> Int
0 -- Now lower than when we were last here
                   then -- trace ("Descent " ++ show (desc - d) ++ " "
                        --      ++ show (path, e)) $
                        [Int] -> Totality
Total []
                   else PReason -> Totality
Partial ([Name] -> PReason
Mutual (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [((SCGEntry, Int), Int)]
path forall a. [a] -> [a] -> [a]
++ [Name
f]))
        | SCGEntry
e forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [((SCGEntry, Int), Int)]
path
           Bool -> Bool -> Bool
&& Bool -> Bool
not (Name
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [SCGEntry]
es)
              = PReason -> Totality
Partial ([Name] -> PReason
Mutual (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [((SCGEntry, Int), Int)]
path forall a. [a] -> [a] -> [a]
++ [Name
f]))
        | [Totality
Unchecked] <- Name -> Context -> [Totality]
lookupTotal Name
f (IState -> Context
tt_ctxt IState
ist) =
            let argspos :: [(Maybe (Int, SizeChange), Int)]
argspos = forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe (Int, SizeChange)]
nextargs [Int
0..]
                pathres :: [Totality]
pathres =
                  do (Maybe (Int, SizeChange)
a, Int
pos) <- [(Maybe (Int, SizeChange), Int)]
argspos
                     case Maybe (Int, SizeChange)
a of
                        Maybe (Int, SizeChange)
Nothing -> -- gone up, but if the
                                   -- rest definitely terminates without any
                                   -- cycles (including the path so far, which
                                   -- we take as inaccessible) the path is fine
                            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
0 (forall a b. (a -> b) -> [a] -> [b]
map forall {b} {a} {b}. Num b => (a, b) -> (a, b)
mkBig (((SCGEntry
e, Int
arg), Int
desc) forall a. a -> [a] -> [a]
: [((SCGEntry, Int), Int)]
path)) [SCGEntry]
es Int
pos
                        Just (Int
nextarg, SizeChange
sc) ->
                          if Int
nextarg forall a. Eq a => a -> a -> Bool
== Int
arg then
                            case SizeChange
sc of
                              SizeChange
Same -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
desc (((SCGEntry
e, Int
arg), Int
desc) forall a. a -> [a] -> [a]
: [((SCGEntry, Int), Int)]
path)
                                                       [SCGEntry]
es Int
pos
                              SizeChange
Smaller -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath (Int
descforall a. Num a => a -> a -> a
+Int
1)
                                                          (((SCGEntry
e, Int
arg), Int
desc) forall a. a -> [a] -> [a]
: [((SCGEntry, Int), Int)]
path)
                                                          [SCGEntry]
es
                                                          Int
pos
                              SizeChange
_ -> forall a. [Char] -> a -> a
trace ([Char]
"Shouldn't happen " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SCGEntry
e) forall a b. (a -> b) -> a -> b
$
                                      forall (m :: * -> *) a. Monad m => a -> m a
return (PReason -> Totality
Partial PReason
Itself)
                            else forall (m :: * -> *) a. Monad m => a -> m a
return Totality
Unchecked in
--                   trace (show (desc, argspos, path, es, pathres)) $
                   [Totality] -> Totality
collapse [Totality]
pathres

        | Bool
otherwise = Totality
Unchecked

allNothing :: [Maybe a] -> Bool
allNothing :: forall a. [Maybe a] -> Bool
allNothing [Maybe a]
xs = forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a b. [(Maybe a, b)] -> [(Maybe a, b)]
collapseNothing (forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe a]
xs [Integer
0..]))

collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
collapseNothing :: forall a b. [(Maybe a, b)] -> [(Maybe a, b)]
collapseNothing ((Maybe a
Nothing, b
t) : [(Maybe a, b)]
xs)
   = (forall a. Maybe a
Nothing, b
t) forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Maybe a
x, b
_) -> case Maybe a
x of
                                             Maybe a
Nothing -> Bool
False
                                             Maybe a
_ -> Bool
True) [(Maybe a, b)]
xs
collapseNothing ((Maybe a, b)
x : [(Maybe a, b)]
xs) = (Maybe a, b)
x forall a. a -> [a] -> [a]
: forall a b. [(Maybe a, b)] -> [(Maybe a, b)]
collapseNothing [(Maybe a, b)]
xs
collapseNothing [] = []

noPartial :: [Totality] -> Totality
noPartial :: [Totality] -> Totality
noPartial (Partial PReason
p : [Totality]
xs) = PReason -> Totality
Partial PReason
p
noPartial (Totality
_ : [Totality]
xs)         = [Totality] -> Totality
noPartial [Totality]
xs
noPartial []               = [Int] -> Totality
Total []

collapse :: [Totality] -> Totality
collapse :: [Totality] -> Totality
collapse [Totality]
xs = Totality -> [Totality] -> Totality
collapse' Totality
Unchecked [Totality]
xs
collapse' :: Totality -> [Totality] -> Totality
collapse' Totality
def (Total [Int]
r : [Totality]
xs)   = [Int] -> Totality
Total [Int]
r
collapse' Totality
def (Totality
Unchecked : [Totality]
xs) = Totality -> [Totality] -> Totality
collapse' Totality
def [Totality]
xs
collapse' Totality
def (Totality
d : [Totality]
xs)         = Totality -> [Totality] -> Totality
collapse' Totality
d [Totality]
xs
-- collapse' Unchecked []         = Total []
collapse' Totality
def []               = Totality
def

-- totalityCheckBlock :: Idris ()
-- totalityCheckBlock = do
--          ist <- getIState
--          -- Do totality checking after entire mutual block
--          mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n
--                          ctxt' <- do ctxt <- getContext
--                                      tclift $ simplifyCasedef n (getErasureInfo ist) ctxt
--                          setContext ctxt')
--                  (map snd (idris_totcheck ist))
--          mapM_ buildSCG (idris_totcheck ist)
--          mapM_ checkDeclTotality (idris_totcheck ist)
--          clear_totcheck