{-# 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
import Control.Monad.State.Strict
import Data.Either
import Data.List
import Data.Maybe
import Debug.Trace
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
done)
= do IState
i <- StateT IState (ExceptT Err IO) IState
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 = Name -> [Char]
forall a. Show a => a -> [Char]
show Name
top [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Totality -> [Char]
forall a. Show a => a -> [Char]
show Totality
tot [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" due to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n
IState -> Idris ()
putIState IState
i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
IBCWrite -> Idris ()
addIBC (FC -> [Char] -> IBCWrite
IBCTotCheckErr FC
fc [Char]
msg)
[Partial (Other [Name]
ns)] ->
(Name -> Idris ()) -> [Name] -> Idris ()
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 Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
done) Name
top) [Name]
ns
[Totality]
x -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkAllCovering FC
_ [Name]
_ Name
_ Name
_ = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkIfGuarded :: Name -> Idris ()
checkIfGuarded :: Name -> Idris ()
checkIfGuarded Name
n
= do IState
i <- StateT IState (ExceptT Err IO) IState
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 = ([Name], SC) -> [Name]
forall a b. (a, b) -> a
fst (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cases) in
if [Name] -> IState -> SC -> Bool
forall {t :: * -> *}. Foldable t => t Name -> IState -> SC -> Bool
allGuarded [Name]
gnames IState
i (([Name], SC) -> SC
forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cases))
then
Name -> FnOpt -> Idris ()
addFnOpt Name
n FnOpt
AllGuarded
else () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe Def
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 Name -> Ctxt [FnOpt] -> Maybe [FnOpt]
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 FnOpt -> [FnOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
fs
allGuarded :: t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i (STerm Term
t)
| (P NameType
_ Name
fn Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t,
Name -> IState -> Bool
guard Name
fn IState
i
= [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Term -> Bool) -> [Term] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> Term -> Bool
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) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> [Bool]
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) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> [Bool]
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 Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Name -> IState -> Bool
guard Name
fn IState
i Bool -> Bool -> Bool
|| Name
fn Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
names
= [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Term -> Bool) -> [Term] -> [Bool]
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
checkPositive :: [Name]
-> (Name, Type)
-> Idris Totality
checkPositive :: [Name] -> (Name, Term) -> Idris Totality
checkPositive [Name]
mut_ns (Name
cn, Term
ty')
= do IState
i <- StateT IState (ExceptT Err IO) 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 (Term -> [Int]
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 = ctxt' })
Int -> [Char] -> Idris ()
logCoverage Int
5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Constructor " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
cn [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Totality -> [Char]
forall a. Show a => a -> [Char]
show Totality
tot [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" with " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Char]
forall a. Show a => a -> [Char]
show [Name]
mut_ns
IBCWrite -> Idris ()
addIBC (Name -> Totality -> IBCWrite
IBCTotal Name
cn Totality
tot)
Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
tot
where
args :: TT n -> [Int]
args TT n
t = [Int
0..[(n, TT n)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (TT n -> [(n, TT n)]
forall n. TT n -> [(n, TT n)]
getArgTys TT n
t)Int -> Int -> Int
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t,
Name
n' Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
mut_ns = (Term -> Bool) -> [Term] -> Bool
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 = (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Name
x -> Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
mut_ns) (Term -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Term
arg)
posParams :: IState -> Term -> Bool
posParams IState
ist Term
t | (P NameType
_ Name
n Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t
= case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
Just TypeInfo
ti -> [Int] -> Int -> [Term] -> Bool
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 -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Term -> Bool) -> [Term] -> [Bool]
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 t -> t t -> Bool
forall a. Eq a => a -> t a -> Bool
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 t -> t -> t
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 t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [Term]
ps
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 <- StateT IState (ExceptT Err IO) IState
getIState
case (Term -> Maybe Totality) -> [Term] -> [Totality]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (IState -> Term -> Maybe Totality
checkLHS IState
i) ((([Name], Term, Term) -> Term) -> [([Name], Term, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ ([Name]
_, Term
l, Term
r) -> Term
l) [([Name], Term, Term)]
pats) of
(Totality
failure : [Totality]
_) -> Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
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
_) -> Totality -> Maybe Totality
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (PReason -> Totality
Partial ([Name] -> PReason
Other [Name
fn]))
Maybe Totality
_ -> Maybe Totality
forall a. Maybe a
Nothing
checkLHS IState
i (App AppStatus Name
_ Term
f Term
a) = Maybe Totality -> Maybe Totality -> Maybe Totality
forall a. Maybe a -> Maybe a -> Maybe 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
_ = Maybe Totality
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
path = Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PReason -> Totality
Partial ([Name] -> PReason
Mutual (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
path)))
| Bool
otherwise = do
Totality
t <- Name -> Idris Totality
getTotality Name
n
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
Context
ctxt' <- do Context
ctxt <- StateT IState (ExceptT Err IO) Context
getContext
TC Context -> StateT IState (ExceptT Err IO) Context
forall a. TC a -> Idris a
tclift (TC Context -> StateT IState (ExceptT Err IO) Context)
-> TC Context -> StateT IState (ExceptT Err IO) Context
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 <- StateT IState (ExceptT Err IO) IState
getIState
let opts :: [FnOpt]
opts = case Name -> Ctxt [FnOpt] -> [[FnOpt]]
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 FnOpt -> [FnOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts
then Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Totality -> Idris Totality) -> Totality -> Idris Totality
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 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Set to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Totality -> [Char]
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')
Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
[TyDecl (DCon Int
_ Int
_ Bool
_) Term
ty] ->
case Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> Term
forall n. TT n -> TT n
getRetTy Term
ty) of
(P NameType
_ Name
tyn Term
_, [Term]
_) -> do
let ms :: [Name]
ms = case Name -> Ctxt TypeInfo -> [TypeInfo]
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])
_-> Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Totality -> Idris Totality) -> Totality -> Idris Totality
forall a b. (a -> b) -> a -> b
$ [Int] -> Totality
Total []
[Def]
_ -> Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Totality -> Idris Totality) -> Totality -> Idris Totality
forall a b. (a -> b) -> a -> b
$ [Int] -> Totality
Total []
Totality
x -> Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
x
case Totality
t' of
Total [Int]
_ -> Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
Totality
Productive -> Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
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 FnOpt -> [FnOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts
then do Totality -> Idris ()
forall {p}. Show p => p -> Idris ()
totalityError Totality
t'; Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
else do Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
w Bool -> Bool -> Bool
&& Bool -> Bool
not (FnOpt
PartialFn FnOpt -> [FnOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
Name -> Totality -> Idris ()
forall {a}. Show a => Name -> a -> Idris ()
warnPartial Name
n Totality
t'
Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
where
totalityError :: p -> Idris ()
totalityError p
t = do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let msg :: [Char]
msg = Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ p -> [Char]
forall a. Show a => a -> [Char]
show p
t
IState -> Idris ()
putIState IState
i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
IBCWrite -> Idris ()
addIBC (FC -> [Char] -> IBCWrite
IBCTotCheckErr FC
fc [Char]
msg)
warnPartial :: Name -> a -> Idris ()
warnPartial Name
n a
t
= do IState
i <- StateT IState (ExceptT Err IO) 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 (OutputDoc -> Idris ())
-> ([Char] -> OutputDoc) -> [Char] -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> Err -> OutputDoc
pprintErr IState
i (Err -> OutputDoc) -> ([Char] -> Err) -> [Char] -> OutputDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Err
forall t. [Char] -> Err' t
Msg ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Warning - " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
t
checkDeclTotality :: (FC, Name) -> Idris Totality
checkDeclTotality :: (FC, Name) -> Idris Totality
checkDeclTotality (FC
fc, Name
n)
= do Int -> [Char] -> Idris ()
logCoverage Int
2 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Checking " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for totality"
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let opts :: [FnOpt]
opts = case Name -> Ctxt [FnOpt] -> Maybe [FnOpt]
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]
_ -> []
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
CoveringFn FnOpt -> [FnOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
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
Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t
verifyTotality :: (FC, Name) -> Idris ()
verifyTotality :: (FC, Name) -> Idris ()
verifyTotality (FC
fc, Name
n)
= do Int -> [Char] -> Idris ()
logCoverage Int
2 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Checking " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'s descendents are total"
IState
ist <- StateT IState (ExceptT Err IO) 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 -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Set in verify to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Totality -> [Char]
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
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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
((Name, [[Name]]) -> Name) -> [(Name, [[Name]])] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [[Name]]) -> Name
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 [] [] = Maybe [Name]
forall a. Maybe a
Nothing
getPartial IState
ist [Name]
bad [] = [Name] -> Maybe [Name]
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 Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
bad) [Name]
ns
Maybe Totality
_ -> IState -> [Name] -> [Name] -> Maybe [Name]
getPartial IState
ist [Name]
bad [Name]
ns
buildSCG :: (FC, Name) -> Idris ()
buildSCG :: (FC, Name) -> Idris ()
buildSCG (FC
_, Name
n) = do
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
case Name -> Ctxt CGInfo -> Maybe CGInfo
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 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Building SCG for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" from\n"
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Either Term (Term, Term)] -> [Char]
forall a. Show a => a -> [Char]
show [Either Term (Term, Term)]
pats [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SC -> [Char]
forall a. Show a => a -> [Char]
show SC
sc
let newscg :: [SCGEntry]
newscg = IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
buildSCG' IState
ist Name
n ([Either Term (Term, Term)] -> [(Term, Term)]
forall a b. [Either a b] -> [b]
rights [Either Term (Term, Term)]
pats) [Name]
args
Int -> [Char] -> Idris ()
logCoverage Int
5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"SCG is: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SCGEntry] -> [Char]
forall a. Show a => a -> [Char]
show [SCGEntry]
newscg
Name -> CGInfo -> Idris ()
addToCG Name
n ( CGInfo
cg { scg = newscg } )
Maybe Def
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe CGInfo
_ -> Int -> [Char] -> Idris ()
logCoverage Int
5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Could not build SCG for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
delazy :: Term -> Term
delazy = Bool -> Term -> Term
delazy' Bool
False
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]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t,
Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Force" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty Text -> Text -> Bool
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]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t,
Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Delay" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty Text -> Text -> Bool
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]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t,
Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Delayed" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty Text -> Text -> Bool
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) = AppStatus Name -> Term -> Term -> Term
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) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
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 -> [Char] -> [Char]
[Guardedness] -> [Char] -> [Char]
Guardedness -> [Char]
(Int -> Guardedness -> [Char] -> [Char])
-> (Guardedness -> [Char])
-> ([Guardedness] -> [Char] -> [Char])
-> Show Guardedness
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Guardedness -> [Char] -> [Char]
showsPrec :: Int -> Guardedness -> [Char] -> [Char]
$cshow :: Guardedness -> [Char]
show :: Guardedness -> [Char]
$cshowList :: [Guardedness] -> [Char] -> [Char]
showList :: [Guardedness] -> [Char] -> [Char]
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 = [SCGEntry] -> [SCGEntry]
forall a. Eq a => [a] -> [a]
nub ([SCGEntry] -> [SCGEntry]) -> [SCGEntry] -> [SCGEntry]
forall a b. (a -> b) -> a -> b
$ ((Term, Term) -> [SCGEntry]) -> [(Term, Term)] -> [SCGEntry]
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) = Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> Term
forall n. TT n -> TT n
dePat Term
lhs') in
[Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [] Guardedness
Toplevel (Term -> Term
forall n. TT n -> TT n
dePat Term
rhs') (Term -> [Name]
forall {a}. TT a -> [a]
patvars Term
lhs')
([Term] -> [Int] -> [(Term, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
pargs [Int
0..])
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
| (P NameType
_ (UN Text
at) Term
_, [Term
_, Term
_]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Text
at Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"assert_total" = []
| (P NameType
_ Name
n Term
_, [Term]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Just [FnOpt]
opts <- Name -> Ctxt [FnOpt] -> Maybe [FnOpt]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [FnOpt]
idris_flags IState
ist),
FnOpt
AssertTotal FnOpt -> [FnOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts = []
| (P NameType
_ (UN Text
del) Term
_, [Term
_,Term
_,Term
arg]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Guardedness
Guarded <- Guardedness
guarded,
Text
del Text -> Text -> Bool
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) <- Term -> (Term, [Term])
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
=
(Term -> [SCGEntry]) -> [Term] -> [SCGEntry]
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]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Name
ifthenelse Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [[Char]] -> Name
sNS ([Char] -> Name
sUN [Char]
"ifThenElse") [[Char]
"Bool", [Char]
"Prelude"]
= [Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Term
t [Name]
pvs [(Term, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Name -> Bool
caseName Name
n Bool -> Bool -> Bool
&& Name
n Name -> Name -> Bool
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))
= (Term -> [SCGEntry]) -> [Term] -> [SCGEntry]
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 [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
if Name
n Name -> [Name] -> Bool
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 Name -> [Name] -> [Name]
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Guardedness
Delayed <- Guardedness
guarded
= (Term -> [SCGEntry]) -> [Term] -> [SCGEntry]
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Bool -> Bool
not (Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
pvs)
= 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
Name -> [Term] -> [(Term, Int)] -> [SCGEntry]
forall {a}.
Name -> [Term] -> [(Term, a)] -> [(Name, [Maybe (a, SizeChange)])]
mkChange Name
n [Term]
args [(Term, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
(Term -> [SCGEntry]) -> [Term] -> [SCGEntry]
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 [SCGEntry] -> [SCGEntry] -> [SCGEntry]
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 [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
[Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Term
v [Name]
pvs [(Term, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
[Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded (Term -> Term -> Term
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 (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
t) [Name]
pvs [(Term, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
[Name]
-> Guardedness -> Term -> [Name] -> [(Term, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Term
e (Name
n Name -> [Name] -> [Name]
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
pvs) = [(Name
f, [])]
findCalls [Name]
_ Guardedness
_ Term
_ [Name]
_ [(Term, Int)]
_ = []
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) ->
((Term, Term) -> [SCGEntry]) -> [(Term, Term)] -> [SCGEntry]
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) ([Either Term (Term, Term)] -> [(Term, Term)]
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) = Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> Term
forall n. TT n -> TT n
dePat Term
lhs')
newpargs :: [Maybe (Term, Int)]
newpargs = [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
newPArg [Term]
args [(Term, Int)]
pargs
csubs :: [(Term, Term)]
csubs = [Term] -> [Term] -> [(Term, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
pargs_case [Term]
args
newrhs :: Term
newrhs = [(Term, Term)] -> Term -> Term
forall {n}. Eq n => [(TT n, TT n)] -> TT n -> TT n
doCaseSubs [(Term, Term)]
csubs (Term -> Term
forall n. TT n -> TT n
dePat Term
rhs')
pargs' :: [(Term, Int)]
pargs' = [(Term, Int)]
pargs [(Term, Int)] -> [(Term, Int)] -> [(Term, Int)]
forall a. [a] -> [a] -> [a]
++ [Maybe (Term, Int)] -> [Term] -> [(Term, Int)]
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 (TT n -> TT n -> [(TT n, TT n)] -> [(TT n, TT n)]
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) (TT n -> TT n -> TT n -> TT n
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)
= (TT n -> TT n -> TT n -> TT n
forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm TT n
x TT n
x' TT n
l, TT n -> TT n -> TT n -> TT n
forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm TT n
x TT n
x' TT n
r) (TT n, TT n) -> [(TT n, TT n)] -> [(TT n, TT n)]
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) (a, b) -> [(a, b)] -> [(a, b)]
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 Term -> [(Term, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Term
t [(Term, Int)]
pargs of
Just Int
i -> (Term, Int) -> Maybe (Term, Int)
forall a. a -> Maybe a
Just (Term
t, Int
i) Maybe (Term, Int) -> [Maybe (Term, Int)] -> [Maybe (Term, Int)]
forall a. a -> [a] -> [a]
: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
newPArg [Term]
ts [(Term, Int)]
pargs
Maybe Int
Nothing -> Maybe (Term, Int)
forall a. Maybe a
Nothing Maybe (Term, Int) -> [Maybe (Term, Int)] -> [Maybe (Term, Int)]
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] -> Integer -> Term -> [Maybe a] -> [Maybe a]
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 Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
: t -> TT n -> [Maybe a] -> [Maybe a]
expand (t
i t -> t -> t
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) [] = Maybe a
forall a. Maybe a
Nothing Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
: t -> TT n -> [Maybe a] -> [Maybe a]
expand (t
i t -> t -> t
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, Name -> [Maybe (a, SizeChange)] -> [Maybe (a, SizeChange)]
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) = Term -> [(Term, a)] -> Maybe (a, SizeChange)
forall {a}. Term -> [(Term, a)] -> Maybe (a, SizeChange)
checkSize Term
a [(Term, a)]
pargs Maybe (a, SizeChange)
-> [Maybe (a, SizeChange)] -> [Maybe (a, SizeChange)]
forall a. a -> [a] -> [a]
: [Term] -> [Maybe (a, SizeChange)]
sizes [Term]
as
checkSize :: Term -> [(Term, a)] -> Maybe (a, SizeChange)
checkSize Term
a ((Term
p, a
i) : [(Term, a)]
ps)
| Term
a Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
p = (a, SizeChange) -> Maybe (a, SizeChange)
forall a. a -> Maybe a
Just (a
i, SizeChange
Same)
| (P NameType
_ (UN Text
as) Term
_, [Term
_,Term
_,Term
arg,Term
_]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
a,
Text
as Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"assert_smaller" Bool -> Bool -> Bool
&& Term
arg Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
p
= (a, SizeChange) -> Maybe (a, SizeChange)
forall a. a -> Maybe a
Just (a
i, SizeChange
Smaller)
| Maybe Term -> Term -> (Term, Maybe Term) -> Bool
smaller Maybe Term
forall a. Maybe a
Nothing Term
a (Term
p, Maybe Term
forall a. Maybe a
Nothing) = (a, SizeChange) -> Maybe (a, SizeChange)
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 [] = Maybe (a, SizeChange)
forall a. Maybe a
Nothing
smaller :: Maybe Term -> Term -> (Term, Maybe Term) -> Bool
smaller Maybe Term
_ Term
_ (Term
Erased, Maybe Term
_) = Bool
False
smaller (Just Term
tyn) Term
a (Term
t, Just Term
tyt) | Term
a Term -> Term -> Bool
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
_)
| (P (DCon Int
_ Int
_ Bool
_) (UN Text
d) Term
_, [P NameType
_ (UN Text
reason) Term
_, Term
_, Term
_]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Text
d Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Delay" Bool -> Bool -> Bool
&& Text
reason Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt [Char]
"Infinite"
= Bool
False
| (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap
= let tyn :: Term
tyn = Name -> Term
getType Name
n in
((Term, Maybe Term) -> Bool) -> [(Term, Maybe Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Term -> Term -> (Term, Maybe Term) -> Bool
smaller (Maybe Term
ty Maybe Term -> Maybe Term -> Maybe Term
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Maybe Term
forall a. a -> Maybe a
Just Term
tyn) Term
a)
([Term] -> [Maybe Term] -> [(Term, Maybe Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
args (((Name, Term) -> Maybe Term) -> [(Name, Term)] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Maybe Term
forall {a} {a}. (a, a) -> Maybe a
toJust (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
tyn)))
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) = a -> Maybe a
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)
dePat :: TT n -> TT n
dePat (Bind n
x (PVar RigCount
_ TT n
ty) TT n
sc) = TT n -> TT n
dePat (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
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 a -> [a] -> [a]
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 Name -> Ctxt [FnOpt] -> Maybe [FnOpt]
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 FnOpt -> [FnOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 <- StateT IState (ExceptT Err IO) IState
getIState
case Name -> Ctxt CGInfo -> [CGInfo]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"from " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SCGEntry] -> [Char]
forall a. Show a => a -> [Char]
show (CGInfo -> [SCGEntry]
scg CGInfo
cg) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
Int -> [Char]
forall a. Show a => a -> [Char]
show ([[SCGEntry]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[SCGEntry]]
ms) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char] -> [[Char]] -> [Char]
showSep [Char]
"\n" (([SCGEntry] -> [Char]) -> [[SCGEntry]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map [SCGEntry] -> [Char]
forall a. Show a => a -> [Char]
show [[SCGEntry]]
ms))
Int -> [Char] -> Idris ()
logCoverage Int
6 (CGInfo -> [Char]
forall a. Show a => a -> [Char]
show CGInfo
cg)
let tot :: [Totality]
tot = ([SCGEntry] -> Totality) -> [[SCGEntry]] -> [Totality]
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 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Generated " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Totality] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Totality]
tot) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" paths"
Int -> [Char] -> Idris ()
logCoverage Int
5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Paths for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" yield " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
([Char] -> [[Char]] -> [Char]
showSep [Char]
"\n" ((([SCGEntry], Totality) -> [Char])
-> [([SCGEntry], Totality)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([SCGEntry], Totality) -> [Char]
forall a. Show a => a -> [Char]
show ([[SCGEntry]] -> [Totality] -> [([SCGEntry], Totality)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[SCGEntry]]
ms [Totality]
tot)))
Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Totality] -> Totality
noPartial [Totality]
tot)
[] -> do Int -> [Char] -> Idris ()
logCoverage Int
5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Char]
"No paths for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n
Totality -> Idris Totality
forall a. a -> StateT IState (ExceptT Err IO) a
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] -> Term -> Int
forall n. TT n -> Int
arity (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
ty)
[Term]
_ -> [Char] -> Int
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 [] = [[SCGEntry] -> [SCGEntry]
forall a. [a] -> [a]
reverse [SCGEntry]
path]
mkMultiPaths IState
ist [SCGEntry]
path [SCGEntry]
cg = (SCGEntry -> [[SCGEntry]]) -> [SCGEntry] -> [[SCGEntry]]
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 = [ [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a]
reverse ((Name
nextf, [Maybe (Int, SizeChange)]
args) SCGEntry -> [SCGEntry] -> [SCGEntry]
forall a. a -> [a] -> [a]
: [SCGEntry]
path) ]
| [Totality
Unchecked] <- Name -> Context -> [Totality]
lookupTotal Name
nextf (IState -> Context
tt_ctxt IState
ist)
= case Name -> Ctxt CGInfo -> [CGInfo]
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) SCGEntry -> [SCGEntry] -> [SCGEntry]
forall a. a -> [a] -> [a]
: [SCGEntry]
path) (CGInfo -> [SCGEntry]
scg CGInfo
ncg)
[CGInfo]
_ -> [ [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a]
reverse ((Name
nextf, [Maybe (Int, SizeChange)]
args) SCGEntry -> [SCGEntry] -> [SCGEntry]
forall a. a -> [a] -> [a]
: [SCGEntry]
path) ]
| Bool
otherwise = [ [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a]
reverse ((Name
nextf, [Maybe (Int, SizeChange)]
args) SCGEntry -> [SCGEntry] -> [SCGEntry]
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 SCGEntry -> SCGEntry -> Bool
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
g Bool -> Bool -> Bool
&& Bool -> Bool
not ([Maybe (Int, SizeChange)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Maybe (Int, SizeChange) -> Bool)
-> [Maybe (Int, SizeChange)] -> [Maybe (Int, SizeChange)]
forall a. (a -> Bool) -> [a] -> [a]
filter Maybe (Int, SizeChange) -> Bool
forall {a}. Maybe (a, SizeChange) -> Bool
smallers [Maybe (Int, SizeChange)]
args))
Bool -> Bool -> Bool
&& (Maybe (Int, SizeChange) -> Bool)
-> [Maybe (Int, SizeChange)] -> [Maybe (Int, SizeChange)]
forall a. (a -> Bool) -> [a] -> [a]
filter Maybe (Int, SizeChange) -> Bool
forall {a}. Maybe (a, SizeChange) -> Bool
smallers [Maybe (Int, SizeChange)]
args [Maybe (Int, SizeChange)] -> [Maybe (Int, SizeChange)] -> Bool
forall a. Eq a => a -> a -> Bool
== (Maybe (Int, SizeChange) -> Bool)
-> [Maybe (Int, SizeChange)] -> [Maybe (Int, SizeChange)]
forall a. (a -> Bool) -> [a] -> [a]
filter Maybe (Int, SizeChange) -> Bool
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
checkMP :: IState -> Name -> Int -> MultiPath -> Totality
checkMP :: IState -> Name -> Int -> [SCGEntry] -> Totality
checkMP IState
ist Name
topfn Int
i [SCGEntry]
mp = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
then let paths :: [Totality]
paths = ((Int -> Totality) -> [Int] -> [Totality]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
0 [] [SCGEntry]
mp) [Int
0..Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]) in
[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 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
Just (Partial PReason
_) -> PReason -> Totality
Partial ([Name] -> PReason
Other [Name
f])
Maybe Totality
x -> Totality
Unchecked
| [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 SCGEntry -> [SCGEntry] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SCGEntry]
es Bool -> Bool -> Bool
&& [Maybe (Int, SizeChange)] -> 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 <- (SCGEntry, Int) -> [((SCGEntry, Int), Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (SCGEntry
e, Int
arg) [((SCGEntry, Int), Int)]
path
= if Int
desc Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
then
[Int] -> Totality
Total []
else PReason -> Totality
Partial ([Name] -> PReason
Mutual ((((SCGEntry, Int), Int) -> Name)
-> [((SCGEntry, Int), Int)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (SCGEntry -> Name
forall a b. (a, b) -> a
fst (SCGEntry -> Name)
-> (((SCGEntry, Int), Int) -> SCGEntry)
-> ((SCGEntry, Int), Int)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SCGEntry, Int) -> SCGEntry
forall a b. (a, b) -> a
fst ((SCGEntry, Int) -> SCGEntry)
-> (((SCGEntry, Int), Int) -> (SCGEntry, Int))
-> ((SCGEntry, Int), Int)
-> SCGEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SCGEntry, Int), Int) -> (SCGEntry, Int)
forall a b. (a, b) -> a
fst) [((SCGEntry, Int), Int)]
path [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
f]))
| SCGEntry
e SCGEntry -> [SCGEntry] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (((SCGEntry, Int), Int) -> SCGEntry)
-> [((SCGEntry, Int), Int)] -> [SCGEntry]
forall a b. (a -> b) -> [a] -> [b]
map ((SCGEntry, Int) -> SCGEntry
forall a b. (a, b) -> a
fst ((SCGEntry, Int) -> SCGEntry)
-> (((SCGEntry, Int), Int) -> (SCGEntry, Int))
-> ((SCGEntry, Int), Int)
-> SCGEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SCGEntry, Int), Int) -> (SCGEntry, Int)
forall a b. (a, b) -> a
fst) [((SCGEntry, Int), Int)]
path
Bool -> Bool -> Bool
&& Bool -> Bool
not (Name
f Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (SCGEntry -> Name) -> [SCGEntry] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map SCGEntry -> Name
forall a b. (a, b) -> a
fst [SCGEntry]
es)
= PReason -> Totality
Partial ([Name] -> PReason
Mutual ((((SCGEntry, Int), Int) -> Name)
-> [((SCGEntry, Int), Int)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (SCGEntry -> Name
forall a b. (a, b) -> a
fst (SCGEntry -> Name)
-> (((SCGEntry, Int), Int) -> SCGEntry)
-> ((SCGEntry, Int), Int)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SCGEntry, Int) -> SCGEntry
forall a b. (a, b) -> a
fst ((SCGEntry, Int) -> SCGEntry)
-> (((SCGEntry, Int), Int) -> (SCGEntry, Int))
-> ((SCGEntry, Int), Int)
-> SCGEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SCGEntry, Int), Int) -> (SCGEntry, Int)
forall a b. (a, b) -> a
fst) [((SCGEntry, Int), Int)]
path [Name] -> [Name] -> [Name]
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 = [Maybe (Int, SizeChange)]
-> [Int] -> [(Maybe (Int, SizeChange), Int)]
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 ->
Totality -> [Totality]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Totality -> [Totality]) -> Totality -> [Totality]
forall a b. (a -> b) -> a -> b
$ Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
0 ((((SCGEntry, Int), Int) -> ((SCGEntry, Int), Int))
-> [((SCGEntry, Int), Int)] -> [((SCGEntry, Int), Int)]
forall a b. (a -> b) -> [a] -> [b]
map ((SCGEntry, Int), Int) -> ((SCGEntry, Int), Int)
forall {b} {a} {b}. Num b => (a, b) -> (a, b)
mkBig (((SCGEntry
e, Int
arg), Int
desc) ((SCGEntry, Int), Int)
-> [((SCGEntry, Int), Int)] -> [((SCGEntry, Int), Int)]
forall a. a -> [a] -> [a]
: [((SCGEntry, Int), Int)]
path)) [SCGEntry]
es Int
pos
Just (Int
nextarg, SizeChange
sc) ->
if Int
nextarg Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arg then
case SizeChange
sc of
SizeChange
Same -> Totality -> [Totality]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Totality -> [Totality]) -> Totality -> [Totality]
forall a b. (a -> b) -> a -> b
$ Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath Int
desc (((SCGEntry
e, Int
arg), Int
desc) ((SCGEntry, Int), Int)
-> [((SCGEntry, Int), Int)] -> [((SCGEntry, Int), Int)]
forall a. a -> [a] -> [a]
: [((SCGEntry, Int), Int)]
path)
[SCGEntry]
es Int
pos
SizeChange
Smaller -> Totality -> [Totality]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Totality -> [Totality]) -> Totality -> [Totality]
forall a b. (a -> b) -> a -> b
$ Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath (Int
descInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
(((SCGEntry
e, Int
arg), Int
desc) ((SCGEntry, Int), Int)
-> [((SCGEntry, Int), Int)] -> [((SCGEntry, Int), Int)]
forall a. a -> [a] -> [a]
: [((SCGEntry, Int), Int)]
path)
[SCGEntry]
es
Int
pos
SizeChange
_ -> [Char] -> [Totality] -> [Totality]
forall a. [Char] -> a -> a
trace ([Char]
"Shouldn't happen " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SCGEntry -> [Char]
forall a. Show a => a -> [Char]
show SCGEntry
e) ([Totality] -> [Totality]) -> [Totality] -> [Totality]
forall a b. (a -> b) -> a -> b
$
Totality -> [Totality]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (PReason -> Totality
Partial PReason
Itself)
else Totality -> [Totality]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
Unchecked in
[Totality] -> Totality
collapse [Totality]
pathres
| Bool
otherwise = Totality
Unchecked
allNothing :: [Maybe a] -> Bool
allNothing :: forall a. [Maybe a] -> Bool
allNothing [Maybe a]
xs = [(Maybe a, Integer)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Maybe a, Integer)] -> [(Maybe a, Integer)]
forall a b. [(Maybe a, b)] -> [(Maybe a, b)]
collapseNothing ([Maybe a] -> [Integer] -> [(Maybe a, Integer)]
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)
= (Maybe a
forall a. Maybe a
Nothing, b
t) (Maybe a, b) -> [(Maybe a, b)] -> [(Maybe a, b)]
forall a. a -> [a] -> [a]
: ((Maybe a, b) -> Bool) -> [(Maybe a, b)] -> [(Maybe a, b)]
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 (Maybe a, b) -> [(Maybe a, b)] -> [(Maybe a, b)]
forall a. a -> [a] -> [a]
: [(Maybe a, b)] -> [(Maybe a, b)]
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' Totality
def [] = Totality
def