{-# 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
checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering fc :: FC
fc done :: [Name]
done top :: Name
top n :: Name
n | Bool -> Bool
not (Name
n Name -> [Name] -> 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 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]
++ " 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]
++ " 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, [Char])]
idris_totcheckfail = (FC
fc, [Char]
msg) (FC, [Char]) -> [(FC, [Char])] -> [(FC, [Char])]
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 ns :: [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
x :: [Totality]
x -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkAllCovering _ _ _ _ = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkIfGuarded :: Name -> Idris ()
checkIfGuarded :: Name -> Idris ()
checkIfGuarded n :: 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 _ ty :: Type
ty _ _ _ cases :: 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 (m :: * -> *) a. Monad m => a -> m a
return ()
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
guard :: Name -> IState -> Bool
guard n :: Name
n ist :: 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 n :: Name
n ist :: 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
Nothing -> Bool
False
Just fs :: [FnOpt]
fs -> FnOpt
AllGuarded FnOpt -> [FnOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
fs
allGuarded :: t Name -> IState -> SC -> Bool
allGuarded names :: t Name
names i :: IState
i (STerm t :: Type
t)
| (P _ fn :: Name
fn _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t,
Name -> IState -> Bool
guard Name
fn IState
i
= [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Type -> Bool) -> [Type] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> Type -> Bool
forall (t :: * -> *).
Foldable t =>
t Name -> IState -> Type -> Bool
guardedTerm t Name
names IState
i) [Type]
args)
| Bool
otherwise = Bool
False
allGuarded names :: t Name
names i :: IState
i (ProjCase _ alts :: [CaseAlt' Type]
alts) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((CaseAlt' Type -> Bool) -> [CaseAlt' Type] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> CaseAlt' Type -> Bool
guardedAlt t Name
names IState
i) [CaseAlt' Type]
alts)
allGuarded names :: t Name
names i :: IState
i (Case _ _ alts :: [CaseAlt' Type]
alts) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((CaseAlt' Type -> Bool) -> [CaseAlt' Type] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> CaseAlt' Type -> Bool
guardedAlt t Name
names IState
i) [CaseAlt' Type]
alts)
allGuarded names :: t Name
names i :: IState
i _ = Bool
True
guardedTerm :: t Name -> IState -> Type -> Bool
guardedTerm names :: t Name
names i :: IState
i (P _ v :: Name
v _) = Name
v Name -> t Name -> 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 names :: t Name
names i :: IState
i (Bind n :: Name
n (Let rig :: RigCount
rig t :: Type
t v :: Type
v) sc :: Type
sc)
= t Name -> IState -> Type -> Bool
guardedTerm t Name
names IState
i Type
v Bool -> Bool -> Bool
&& t Name -> IState -> Type -> Bool
guardedTerm t Name
names IState
i Type
sc
guardedTerm names :: t Name
names i :: IState
i (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc) = Bool
False
guardedTerm names :: t Name
names i :: IState
i ap :: Type
ap@(App _ _ _)
| (P _ fn :: Name
fn _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Name -> IState -> Bool
guard Name
fn IState
i Bool -> Bool -> Bool
|| Name
fn Name -> t Name -> 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 ((Type -> Bool) -> [Type] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (t Name -> IState -> Type -> Bool
guardedTerm t Name
names IState
i) [Type]
args)
guardedTerm names :: t Name
names i :: IState
i (App _ f :: Type
f a :: Type
a) = Bool
False
guardedTerm names :: t Name
names i :: IState
i tm :: Type
tm = Bool
True
guardedAlt :: t Name -> IState -> CaseAlt' Type -> Bool
guardedAlt names :: t Name
names i :: IState
i (ConCase _ _ _ t :: SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
guardedAlt names :: t Name
names i :: IState
i (FnCase _ _ t :: SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
guardedAlt names :: t Name
names i :: IState
i (ConstCase _ t :: SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
guardedAlt names :: t Name
names i :: IState
i (SucCase _ t :: SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
guardedAlt names :: t Name
names i :: IState
i (DefaultCase t :: SC
t) = t Name -> IState -> SC -> Bool
allGuarded t Name
names IState
i SC
t
checkPositive :: [Name]
-> (Name, Type)
-> Idris Totality
checkPositive :: [Name] -> (Name, Type) -> Idris Totality
checkPositive mut_ns :: [Name]
mut_ns (cn :: Name
cn, ty' :: Type
ty')
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let ty :: Type
ty = Bool -> Type -> Type
delazy' Bool
True (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
i) [] Type
ty')
let p :: Bool
p = IState -> Type -> Bool
cp IState
i Type
ty
let tot :: Totality
tot = if Bool
p then [Int] -> Totality
Total (Type -> [Int]
forall n. TT n -> [Int]
args Type
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 5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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]
++ " 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]
++ " 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 (m :: * -> *) a. Monad m => a -> m a
return Totality
tot
where
args :: TT n -> [Int]
args t :: TT n
t = [0..[(n, TT n)] -> 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
-1]
cp :: IState -> Type -> Bool
cp i :: IState
i (Bind n :: Name
n (Pi _ _ aty :: Type
aty _) sc :: Type
sc)
= IState -> Type -> Bool
posArg IState
i Type
aty Bool -> Bool -> Bool
&& IState -> Type -> Bool
cp IState
i Type
sc
cp i :: IState
i t :: Type
t | (P _ n' :: Name
n' _ , args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t,
Name
n' Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
mut_ns = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noRec [Type]
args
cp i :: IState
i _ = Bool
True
posArg :: IState -> Type -> Bool
posArg ist :: IState
ist (Bind _ (Pi _ _ nty :: Type
nty _) sc :: Type
sc) = Type -> Bool
noRec Type
nty Bool -> Bool -> Bool
&& IState -> Type -> Bool
posArg IState
ist Type
sc
posArg ist :: IState
ist t :: Type
t = IState -> Type -> Bool
posParams IState
ist Type
t
noRec :: Type -> Bool
noRec arg :: Type
arg = (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\x :: Name
x -> Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
mut_ns) (Type -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Type
arg)
posParams :: IState -> Type -> Bool
posParams ist :: IState
ist t :: Type
t | (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
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 ti :: TypeInfo
ti -> [Int] -> Int -> [Type] -> Bool
forall (t :: * -> *) a.
(Foldable t, Eq a, Num a) =>
t a -> a -> [Type] -> Bool
checkParamsOK (TypeInfo -> [Int]
param_pos TypeInfo
ti) 0 [Type]
args
Nothing -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Type -> Bool) -> [Type] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Type -> Bool
posParams IState
ist) [Type]
args)
posParams ist :: IState
ist t :: Type
t = Type -> Bool
noRec Type
t
checkParamsOK :: t a -> a -> [Type] -> Bool
checkParamsOK ppos :: t a
ppos i :: a
i [] = Bool
True
checkParamsOK ppos :: t a
ppos i :: a
i (p :: Type
p : ps :: [Type]
ps)
| a
i a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ppos = t a -> a -> [Type] -> Bool
checkParamsOK t a
ppos (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) [Type]
ps
| Bool
otherwise = Type -> Bool
noRec Type
p Bool -> Bool -> Bool
&& t a -> a -> [Type] -> Bool
checkParamsOK t a
ppos (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) [Type]
ps
calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
calcTotality :: FC -> Name -> [([Name], Type, Type)] -> Idris Totality
calcTotality fc :: FC
fc n :: Name
n pats :: [([Name], Type, Type)]
pats
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
case (Type -> Maybe Totality) -> [Type] -> [Totality]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (IState -> Type -> Maybe Totality
checkLHS IState
i) ((([Name], Type, Type) -> Type) -> [([Name], Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, l :: Type
l, r :: Type
r) -> Type
l) [([Name], Type, Type)]
pats) of
(failure :: Totality
failure : _) -> Totality -> Idris Totality
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
failure
_ -> Name -> Idris Totality
checkSizeChange Name
n
where
checkLHS :: IState -> Type -> Maybe Totality
checkLHS i :: IState
i (P _ fn :: Name
fn _)
= case Name -> Context -> Maybe Totality
lookupTotalExact Name
fn (IState -> Context
tt_ctxt IState
i) of
Just (Partial _) -> Totality -> Maybe Totality
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 i :: IState
i (App _ f :: Type
f a :: Type
a) = Maybe Totality -> Maybe Totality -> Maybe Totality
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (IState -> Type -> Maybe Totality
checkLHS IState
i Type
f) (IState -> Type -> Maybe Totality
checkLHS IState
i Type
a)
checkLHS _ _ = Maybe Totality
forall a. Maybe a
Nothing
checkTotality :: [Name] -> FC -> Name -> Idris Totality
checkTotality :: [Name] -> FC -> Name -> Idris Totality
checkTotality path :: [Name]
path fc :: FC
fc n :: Name
n
| Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
path = Totality -> Idris Totality
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 <- Idris Context
getContext
TC Context -> Idris Context
forall a. TC a -> Idris a
tclift (TC Context -> Idris Context) -> TC Context -> Idris 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 <- Idris 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
[fs :: [FnOpt]
fs] -> [FnOpt]
fs
_ -> []
Totality
t' <- case Totality
t of
Unchecked ->
case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
[CaseOp _ _ _ _ pats :: [([Name], Type, Type)]
pats _] ->
do Totality
t' <- if FnOpt
AssertTotal FnOpt -> [FnOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts
then Totality -> Idris Totality
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], Type, Type)] -> Idris Totality
calcTotality FC
fc Name
n [([Name], Type, Type)]
pats
Int -> [Char] -> Idris ()
logCoverage 2 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
[TyDecl (DCon _ _ _) ty :: Type
ty] ->
case Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty) of
(P _ tyn :: Name
tyn _, _) -> 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 _ _ _ _ xs :: [Name]
xs@(_:_) _] -> [Name]
xs
ts :: [TypeInfo]
ts -> [Name
tyn]
[Name] -> (Name, Type) -> Idris Totality
checkPositive [Name]
ms (Name
n, Type
ty)
_-> Totality -> Idris Totality
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 -> Idris Totality
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 []
x :: Totality
x -> Totality -> Idris Totality
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
x
case Totality
t' of
Total _ -> Totality -> Idris Totality
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
Productive -> Totality -> Idris Totality
forall (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
e :: Totality
e -> do Bool
w <- Opt -> Idris Bool
cmdOptType Opt
WarnPartial
if FnOpt
TotalFn FnOpt -> [FnOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts
then do Totality -> Idris ()
forall a. Show a => a -> Idris ()
totalityError Totality
t'; Totality -> Idris Totality
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 (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 (m :: * -> *) a. Monad m => a -> m a
return Totality
t'
where
totalityError :: a -> Idris ()
totalityError t :: a
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]
++ " is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
t
IState -> Idris ()
putIState IState
i { idris_totcheckfail :: [(FC, [Char])]
idris_totcheckfail = (FC
fc, [Char]
msg) (FC, [Char]) -> [(FC, [Char])] -> [(FC, [Char])]
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 n :: Name
n t :: 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
[x :: 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
$ "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]
++ " 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
fc, n :: Name
n)
= do Int -> [Char] -> Idris ()
logCoverage 2 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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]
++ " 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 fs :: [FnOpt]
fs -> [FnOpt]
fs
_ -> []
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
CoveringFn FnOpt -> [FnOpt] -> 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 (m :: * -> *) a. Monad m => a -> m a
return Totality
t
verifyTotality :: (FC, Name) -> Idris ()
verifyTotality :: (FC, Name) -> Idris ()
verifyTotality (fc :: FC
fc, n :: Name
n)
= do Int -> [Char] -> Idris ()
logCoverage 2 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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]
++ "'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 _) -> 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
Nothing -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just bad :: [Name]
bad -> do let t' :: Totality
t' = PReason -> Totality
Partial ([Name] -> PReason
Other [Name]
bad)
Int -> [Char] -> Idris ()
logCoverage 2 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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')
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
getNames :: Context -> [Name]
getNames ctxt :: Context
ctxt = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (CaseOp _ _ _ _ _ defs :: CaseDefs
defs)
-> let (top :: [Name]
top, def :: 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)
_ -> []
getPartial :: IState -> [Name] -> [Name] -> Maybe [Name]
getPartial ist :: IState
ist [] [] = Maybe [Name]
forall a. Maybe a
Nothing
getPartial ist :: IState
ist bad :: [Name]
bad [] = [Name] -> Maybe [Name]
forall a. a -> Maybe a
Just [Name]
bad
getPartial ist :: IState
ist bad :: [Name]
bad (n :: Name
n : ns :: [Name]
ns)
= case Name -> Context -> Maybe Totality
lookupTotalExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Just (Partial _) -> IState -> [Name] -> [Name] -> Maybe [Name]
getPartial IState
ist (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
bad) [Name]
ns
_ -> IState -> [Name] -> [Name] -> Maybe [Name]
getPartial IState
ist [Name]
bad [Name]
ns
buildSCG :: (FC, Name) -> Idris ()
buildSCG :: (FC, Name) -> Idris ()
buildSCG (_, n :: 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 cg :: CGInfo
cg -> case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Just (CaseOp _ _ _ pats :: [Either Type (Type, Type)]
pats _ cd :: CaseDefs
cd) ->
let (args :: [Name]
args, sc :: SC
sc) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd in
do Int -> [Char] -> Idris ()
logCoverage 2 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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]
++ " from\n"
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Either Type (Type, Type)] -> [Char]
forall a. Show a => a -> [Char]
show [Either Type (Type, Type)]
pats [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "\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 -> [(Type, Type)] -> [Name] -> [SCGEntry]
buildSCG' IState
ist Name
n ([Either Type (Type, Type)] -> [(Type, Type)]
forall a b. [Either a b] -> [b]
rights [Either Type (Type, Type)]
pats) [Name]
args
Int -> [Char] -> Idris ()
logCoverage 5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 :: [SCGEntry]
scg = [SCGEntry]
newscg } )
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ -> Int -> [Char] -> Idris ()
logCoverage 5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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]
++ "\n"
delazy :: Type -> Type
delazy = Bool -> Type -> Type
delazy' Bool
False
delazy' :: Bool -> Type -> Type
delazy' all :: Bool
all t :: Type
t@(App _ f :: Type
f a :: Type
a)
| (P _ (UN l :: Text
l) _, [P _ (UN lty :: Text
lty) _, _, arg :: Type
arg]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t,
Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "Force" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char] -> Text
txt "Infinite") = Bool -> Type -> Type
delazy' Bool
all Type
arg
| (P _ (UN l :: Text
l) _, [P _ (UN lty :: Text
lty) _, _, arg :: Type
arg]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t,
Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "Delay" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char] -> Text
txt "Infinite") = Type -> Type
delazy Type
arg
| (P _ (UN l :: Text
l) _, [P _ (UN lty :: Text
lty) _, arg :: Type
arg]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t,
Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "Delayed" Bool -> Bool -> Bool
&& (Bool
all Bool -> Bool -> Bool
|| Text
lty Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char] -> Text
txt "Infinite") = Bool -> Type -> Type
delazy' Bool
all Type
arg
delazy' all :: Bool
all (App s :: AppStatus Name
s f :: Type
f a :: Type
a) = AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Bool -> Type -> Type
delazy' Bool
all Type
f) (Bool -> Type -> Type
delazy' Bool
all Type
a)
delazy' all :: Bool
all (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc) = Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((Type -> Type) -> Binder Type -> Binder Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Type -> Type
delazy' Bool
all) Binder Type
b) (Bool -> Type -> Type
delazy' Bool
all Type
sc)
delazy' all :: Bool
all t :: Type
t = Type
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
showList :: [Guardedness] -> [Char] -> [Char]
$cshowList :: [Guardedness] -> [Char] -> [Char]
show :: Guardedness -> [Char]
$cshow :: Guardedness -> [Char]
showsPrec :: Int -> Guardedness -> [Char] -> [Char]
$cshowsPrec :: Int -> Guardedness -> [Char] -> [Char]
Show
buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
buildSCG' :: IState -> Name -> [(Type, Type)] -> [Name] -> [SCGEntry]
buildSCG' ist :: IState
ist topfn :: Name
topfn pats :: [(Type, Type)]
pats args :: [Name]
args = [SCGEntry] -> [SCGEntry]
forall a. Eq a => [a] -> [a]
nub ([SCGEntry] -> [SCGEntry]) -> [SCGEntry] -> [SCGEntry]
forall a b. (a -> b) -> a -> b
$ ((Type, Type) -> [SCGEntry]) -> [(Type, Type)] -> [SCGEntry]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Type, Type) -> [SCGEntry]
scgPat [(Type, Type)]
pats where
scgPat :: (Type, Type) -> [SCGEntry]
scgPat (lhs :: Type
lhs, rhs :: Type
rhs) = let lhs' :: Type
lhs' = Type -> Type
delazy Type
lhs
rhs' :: Type
rhs' = Type -> Type
delazy Type
rhs
(_, pargs :: [Type]
pargs) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
dePat Type
lhs') in
[Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [] Guardedness
Toplevel (Type -> Type
forall n. TT n -> TT n
dePat Type
rhs') (Type -> [Name]
forall a. TT a -> [a]
patvars Type
lhs')
([Type] -> [Int] -> [(Type, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
pargs [0..])
findCalls :: [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls cases :: [Name]
cases Delayed ap :: Type
ap@(P _ n :: Name
n _) pvs :: [Name]
pvs args :: [(Type, Int)]
args = []
findCalls cases :: [Name]
cases guarded :: Guardedness
guarded ap :: Type
ap@(App _ f :: Type
f a :: Type
a) pvs :: [Name]
pvs pargs :: [(Type, Int)]
pargs
| (P _ (UN at :: Text
at) _, [_, _]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Text
at Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "assert_total" = []
| (P _ n :: Name
n _, _) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Just opts :: [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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
opts = []
| (P _ (UN del :: Text
del) _, [_,_,arg :: Type
arg]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Guardedness
Guarded <- Guardedness
guarded,
Text
del Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "Delay"
= [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Delayed Type
arg [Name]
pvs [(Type, Int)]
pargs
| (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
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
=
(Type -> [SCGEntry]) -> [Type] -> [SCGEntry]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\x :: Type
x -> [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Type
x [Name]
pvs [(Type, Int)]
pargs) [Type]
args
| (P _ ifthenelse :: Name
ifthenelse _, [_, _, t :: Type
t, e :: Type
e]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Name
ifthenelse Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [[Char]] -> Name
sNS ([Char] -> Name
sUN "ifThenElse") ["Bool", "Prelude"]
= [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Type
t [Name]
pvs [(Type, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
[Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Type
e [Name]
pvs [(Type, Int)]
pargs
| (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
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))
= (Type -> [SCGEntry]) -> [Type] -> [SCGEntry]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\x :: Type
x -> [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Type
x [Name]
pvs [(Type, Int)]
pargs) [Type]
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
-> [Type]
-> [Name]
-> [(Type, Int)]
-> [SCGEntry]
findCallsCase (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
cases) Guardedness
guarded Name
n [Type]
args [Name]
pvs [(Type, Int)]
pargs
else []
| (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Guardedness
Delayed <- Guardedness
guarded
= (Type -> [SCGEntry]) -> [Type] -> [SCGEntry]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\x :: Type
x -> [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Type
x [Name]
pvs [(Type, Int)]
pargs) [Type]
args
| (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Bool -> Bool
not (Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
pvs)
= let nguarded :: Guardedness
nguarded = case Guardedness
guarded of
Unguarded -> Guardedness
Unguarded
x :: 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 -> [Type] -> [(Type, Int)] -> [SCGEntry]
forall a.
Name -> [Type] -> [(Type, a)] -> [(Name, [Maybe (a, SizeChange)])]
mkChange Name
n [Type]
args [(Type, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
(Type -> [SCGEntry]) -> [Type] -> [SCGEntry]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\x :: Type
x -> [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
nguarded Type
x [Name]
pvs [(Type, Int)]
pargs) [Type]
args
where notPartial :: Maybe Totality -> Bool
notPartial (Just (Partial NotCovering)) = Bool
False
notPartial _ = Bool
True
findCalls cases :: [Name]
cases guarded :: Guardedness
guarded (App _ f :: Type
f a :: Type
a) pvs :: [Name]
pvs pargs :: [(Type, Int)]
pargs
= [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Type
f [Name]
pvs [(Type, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++ [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Type
a [Name]
pvs [(Type, Int)]
pargs
findCalls cases :: [Name]
cases guarded :: Guardedness
guarded (Bind n :: Name
n (Let rig :: RigCount
rig t :: Type
t v :: Type
v) e :: Type
e) pvs :: [Name]
pvs pargs :: [(Type, Int)]
pargs
= [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Type
t [Name]
pvs [(Type, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
[Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded Type
v [Name]
pvs [(Type, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
[Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
substV Type
v Type
e) [Name]
pvs [(Type, Int)]
pargs
findCalls cases :: [Name]
cases guarded :: Guardedness
guarded (Bind n :: Name
n t :: Binder Type
t e :: Type
e) pvs :: [Name]
pvs pargs :: [(Type, Int)]
pargs
= [Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
Unguarded (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
t) [Name]
pvs [(Type, Int)]
pargs [SCGEntry] -> [SCGEntry] -> [SCGEntry]
forall a. [a] -> [a] -> [a]
++
[Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
guarded Type
e (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
pvs) [(Type, Int)]
pargs
findCalls cases :: [Name]
cases guarded :: Guardedness
guarded (P _ f :: Name
f _ ) pvs :: [Name]
pvs pargs :: [(Type, Int)]
pargs
| Bool -> Bool
not (Name
f Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
pvs) = [(Name
f, [])]
findCalls _ _ _ _ _ = []
findCallsCase :: [Name]
-> Guardedness
-> Name
-> [Type]
-> [Name]
-> [(Type, Int)]
-> [SCGEntry]
findCallsCase cases :: [Name]
cases guarded :: Guardedness
guarded n :: Name
n args :: [Type]
args pvs :: [Name]
pvs pargs :: [(Type, Int)]
pargs
= case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Just (CaseOp _ _ _ pats :: [Either Type (Type, Type)]
pats _ cd :: CaseDefs
cd) ->
((Type, Type) -> [SCGEntry]) -> [(Type, Type)] -> [SCGEntry]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Name]
-> [Name]
-> [(Type, Int)]
-> [Type]
-> Guardedness
-> (Type, Type)
-> [SCGEntry]
fccPat [Name]
cases [Name]
pvs [(Type, Int)]
pargs [Type]
args Guardedness
guarded) ([Either Type (Type, Type)] -> [(Type, Type)]
forall a b. [Either a b] -> [b]
rights [Either Type (Type, Type)]
pats)
Nothing -> []
fccPat :: [Name]
-> [Name]
-> [(Type, Int)]
-> [Type]
-> Guardedness
-> (Type, Type)
-> [SCGEntry]
fccPat cases :: [Name]
cases pvs :: [Name]
pvs pargs :: [(Type, Int)]
pargs args :: [Type]
args g :: Guardedness
g (lhs :: Type
lhs, rhs :: Type
rhs)
= let lhs' :: Type
lhs' = Type -> Type
delazy Type
lhs
rhs' :: Type
rhs' = Type -> Type
delazy Type
rhs
(_, pargs_case :: [Type]
pargs_case) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
dePat Type
lhs')
newpargs :: [Maybe (Type, Int)]
newpargs = [Type] -> [(Type, Int)] -> [Maybe (Type, Int)]
newPArg [Type]
args [(Type, Int)]
pargs
csubs :: [(Type, Type)]
csubs = [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
pargs_case [Type]
args
newrhs :: Type
newrhs = [(Type, Type)] -> Type -> Type
forall n. Eq n => [(TT n, TT n)] -> TT n -> TT n
doCaseSubs [(Type, Type)]
csubs (Type -> Type
forall n. TT n -> TT n
dePat Type
rhs')
pargs' :: [(Type, Int)]
pargs' = [(Type, Int)]
pargs [(Type, Int)] -> [(Type, Int)] -> [(Type, Int)]
forall a. [a] -> [a] -> [a]
++ [Maybe (Type, Int)] -> [Type] -> [(Type, Int)]
forall a b a. [Maybe (a, b)] -> [a] -> [(a, b)]
addPArg [Maybe (Type, Int)]
newpargs [Type]
pargs_case in
[Name]
-> Guardedness -> Type -> [Name] -> [(Type, Int)] -> [SCGEntry]
findCalls [Name]
cases Guardedness
g Type
newrhs [Name]
pvs [(Type, Int)]
pargs'
where
doCaseSubs :: [(TT n, TT n)] -> TT n -> TT n
doCaseSubs [] tm :: TT n
tm = TT n
tm
doCaseSubs ((x :: TT n
x, x' :: TT n
x') : cs :: [(TT n, TT n)]
cs) tm :: 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 x :: TT n
x x' :: TT n
x' [] = []
subIn x :: TT n
x x' :: TT n
x' ((l :: TT n
l, r :: TT n
r) : cs :: [(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 (t :: a
t, i :: b
i) : ts :: [Maybe (a, b)]
ts) (t' :: a
t' : ts' :: [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 (Nothing : ts :: [Maybe (a, b)]
ts) (t' :: a
t' : ts' :: [a]
ts') = [Maybe (a, b)] -> [a] -> [(a, b)]
addPArg [Maybe (a, b)]
ts [a]
ts'
addPArg _ _ = []
newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
newPArg :: [Type] -> [(Type, Int)] -> [Maybe (Type, Int)]
newPArg (t :: Type
t : ts :: [Type]
ts) pargs :: [(Type, Int)]
pargs = case Type -> [(Type, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Type
t [(Type, Int)]
pargs of
Just i :: Int
i -> (Type, Int) -> Maybe (Type, Int)
forall a. a -> Maybe a
Just (Type
t, Int
i) Maybe (Type, Int) -> [Maybe (Type, Int)] -> [Maybe (Type, Int)]
forall a. a -> [a] -> [a]
: [Type] -> [(Type, Int)] -> [Maybe (Type, Int)]
newPArg [Type]
ts [(Type, Int)]
pargs
Nothing -> Maybe (Type, Int)
forall a. Maybe a
Nothing Maybe (Type, Int) -> [Maybe (Type, Int)] -> [Maybe (Type, Int)]
forall a. a -> [a] -> [a]
: [Type] -> [(Type, Int)] -> [Maybe (Type, Int)]
newPArg [Type]
ts [(Type, Int)]
pargs
newPArg [] pargs :: [(Type, Int)]
pargs = []
expandToArity :: Name -> [Maybe a] -> [Maybe a]
expandToArity n :: Name
n args :: [Maybe a]
args
= case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
[ty :: Type
ty] -> Integer -> Type -> [Maybe a] -> [Maybe a]
forall a n a. Num a => a -> TT n -> [Maybe a] -> [Maybe a]
expand 0 (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) [] Type
ty) [Maybe a]
args
_ -> [Maybe a]
args
where expand :: a -> TT n -> [Maybe a] -> [Maybe a]
expand i :: a
i (Bind n :: n
n (Pi _ _ _ _) sc :: TT n
sc) (x :: Maybe a
x : xs :: [Maybe a]
xs) = Maybe a
x Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
: a -> TT n -> [Maybe a] -> [Maybe a]
expand (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) TT n
sc [Maybe a]
xs
expand i :: a
i (Bind n :: n
n (Pi _ _ _ _) sc :: TT n
sc) [] = Maybe a
forall a. Maybe a
Nothing Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
: a -> TT n -> [Maybe a] -> [Maybe a]
expand (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) TT n
sc []
expand i :: a
i _ xs :: [Maybe a]
xs = [Maybe a]
xs
mkChange :: Name -> [Type] -> [(Type, a)] -> [(Name, [Maybe (a, SizeChange)])]
mkChange n :: Name
n args :: [Type]
args pargs :: [(Type, a)]
pargs = [(Name
n, Name -> [Maybe (a, SizeChange)] -> [Maybe (a, SizeChange)]
forall a. Name -> [Maybe a] -> [Maybe a]
expandToArity Name
n ([Type] -> [Maybe (a, SizeChange)]
sizes [Type]
args))]
where
sizes :: [Type] -> [Maybe (a, SizeChange)]
sizes [] = []
sizes (a :: Type
a : as :: [Type]
as) = Type -> [(Type, a)] -> Maybe (a, SizeChange)
forall a. Type -> [(Type, a)] -> Maybe (a, SizeChange)
checkSize Type
a [(Type, a)]
pargs Maybe (a, SizeChange)
-> [Maybe (a, SizeChange)] -> [Maybe (a, SizeChange)]
forall a. a -> [a] -> [a]
: [Type] -> [Maybe (a, SizeChange)]
sizes [Type]
as
checkSize :: Type -> [(Type, a)] -> Maybe (a, SizeChange)
checkSize a :: Type
a ((p :: Type
p, i :: a
i) : ps :: [(Type, a)]
ps)
| Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
p = (a, SizeChange) -> Maybe (a, SizeChange)
forall a. a -> Maybe a
Just (a
i, SizeChange
Same)
| (P _ (UN as :: Text
as) _, [_,_,arg :: Type
arg,_]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
a,
Text
as Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "assert_smaller" Bool -> Bool -> Bool
&& Type
arg Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
p
= (a, SizeChange) -> Maybe (a, SizeChange)
forall a. a -> Maybe a
Just (a
i, SizeChange
Smaller)
| Maybe Type -> Type -> (Type, Maybe Type) -> Bool
smaller Maybe Type
forall a. Maybe a
Nothing Type
a (Type
p, Maybe Type
forall a. Maybe a
Nothing) = (a, SizeChange) -> Maybe (a, SizeChange)
forall a. a -> Maybe a
Just (a
i, SizeChange
Smaller)
| Bool
otherwise = Type -> [(Type, a)] -> Maybe (a, SizeChange)
checkSize Type
a [(Type, a)]
ps
checkSize a :: Type
a [] = Maybe (a, SizeChange)
forall a. Maybe a
Nothing
smaller :: Maybe Type -> Type -> (Type, Maybe Type) -> Bool
smaller _ _ (Erased, _) = Bool
False
smaller (Just tyn :: Type
tyn) a :: Type
a (t :: Type
t, Just tyt :: Type
tyt) | Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t = Bool
True
smaller ty :: Maybe Type
ty a :: Type
a (ap :: Type
ap@(App _ f :: Type
f s :: Type
s), _)
| (P (DCon _ _ _) (UN d :: Text
d) _, [P _ (UN reason :: Text
reason) _, _, _]) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Text
d Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "Delay" Bool -> Bool -> Bool
&& Text
reason Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Text
txt "Infinite"
= Bool
False
| (P (DCon _ _ _) n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap
= let tyn :: Type
tyn = Name -> Type
getType Name
n in
((Type, Maybe Type) -> Bool) -> [(Type, Maybe Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Type -> Type -> (Type, Maybe Type) -> Bool
smaller (Maybe Type
ty Maybe Type -> Maybe Type -> Maybe Type
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Type -> Maybe Type
forall a. a -> Maybe a
Just Type
tyn) Type
a)
([Type] -> [Maybe Type] -> [(Type, Maybe Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
args (((Name, Type) -> Maybe Type) -> [(Name, Type)] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Maybe Type
forall a a. (a, a) -> Maybe a
toJust (Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys Type
tyn)))
smaller ty :: Maybe Type
ty (App _ f :: Type
f s :: Type
s) a :: (Type, Maybe Type)
a = Maybe Type -> Type -> (Type, Maybe Type) -> Bool
smaller Maybe Type
ty Type
f (Type, Maybe Type)
a
smaller _ _ _ = Bool
False
toJust :: (a, a) -> Maybe a
toJust (n :: a
n, t :: a
t) = a -> Maybe a
forall a. a -> Maybe a
Just a
t
getType :: Name -> Type
getType n :: Name
n = case Name -> Context -> Maybe Type
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Just ty :: Type
ty -> Type -> Type
delazy (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) [] Type
ty)
dePat :: TT n -> TT n
dePat (Bind x :: n
x (PVar _ ty :: TT n
ty) sc :: 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 t :: TT n
t = TT n
t
patvars :: TT a -> [a]
patvars (Bind x :: a
x (PVar _ _) sc :: TT a
sc) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: TT a -> [a]
patvars TT a
sc
patvars _ = []
allGuarded :: Name -> IState -> Bool
allGuarded n :: Name
n ist :: 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
Nothing -> Bool
False
Just fs :: [FnOpt]
fs -> FnOpt
AllGuarded FnOpt -> [FnOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FnOpt]
fs
checkSizeChange :: Name -> Idris Totality
checkSizeChange :: Name -> Idris Totality
checkSizeChange n :: 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
[cg :: CGInfo
cg] -> do let ms :: [[SCGEntry]]
ms = IState -> [SCGEntry] -> [SCGEntry] -> [[SCGEntry]]
mkMultiPaths IState
ist [] (CGInfo -> [SCGEntry]
scg CGInfo
cg)
Int -> [Char] -> Idris ()
logCoverage 5 ("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]
++ ":\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
"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]
++ "\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
Int -> [Char]
forall a. Show a => a -> [Char]
show ([[SCGEntry]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[SCGEntry]]
ms) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char] -> [[Char]] -> [Char]
showSep "\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 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 4 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Generated " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Totality] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Totality]
tot) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ " paths"
Int -> [Char] -> Idris ()
logCoverage 5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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]
++ " yield " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
([Char] -> [[Char]] -> [Char]
showSep "\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 (m :: * -> *) a. Monad m => a -> m a
return ([Totality] -> Totality
noPartial [Totality]
tot)
[] -> do Int -> [Char] -> Idris ()
logCoverage 5 ([Char] -> Idris ()) -> [Char] -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 (m :: * -> *) a. Monad m => a -> m a
return Totality
Unchecked
where getArity :: IState -> Name -> Int
getArity ist :: IState
ist n :: Name
n
= case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
[ty :: Type
ty] -> Type -> Int
forall n. TT n -> Int
arity (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) [] Type
ty)
_ -> [Char] -> Int
forall a. HasCallStack => [Char] -> a
error "Can't happen: checkSizeChange.getArity"
type MultiPath = [SCGEntry]
mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
mkMultiPaths :: IState -> [SCGEntry] -> [SCGEntry] -> [[SCGEntry]]
mkMultiPaths ist :: IState
ist path :: [SCGEntry]
path [] = [[SCGEntry] -> [SCGEntry]
forall a. [a] -> [a]
reverse [SCGEntry]
path]
mkMultiPaths ist :: IState
ist path :: [SCGEntry]
path cg :: [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 (nextf :: Name
nextf, args :: [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) ]
| [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
[ncg :: 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)
_ -> [ [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 f :: SCGEntry
f [] = Bool
False
inPath f :: SCGEntry
f (g :: SCGEntry
g : gs :: [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 (f :: Name
f, args :: [Maybe (Int, SizeChange)]
args) (g :: Name
g, args' :: [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 (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 (_, Smaller)) = Bool
True
smallers _ = Bool
False
checkMP :: IState -> Name -> Int -> MultiPath -> Totality
checkMP :: IState -> Name -> Int -> [SCGEntry] -> Totality
checkMP ist :: IState
ist topfn :: Name
topfn i :: Int
i mp :: [SCGEntry]
mp = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 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 0 [] [SCGEntry]
mp) [0..Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]) in
[Totality] -> Totality
collapse [Totality]
paths
else Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath 0 [] [SCGEntry]
mp 0
where
mkBig :: (a, b) -> (a, b)
mkBig (e :: a
e, d :: b
d) = (a
e, 10000)
tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
tryPath :: Int -> [((SCGEntry, Int), Int)] -> [SCGEntry] -> Int -> Totality
tryPath desc :: Int
desc path :: [((SCGEntry, Int), Int)]
path [] _ = [Int] -> Totality
Total []
tryPath desc :: Int
desc path :: [((SCGEntry, Int), Int)]
path ((f :: Name
f, _) : es :: [SCGEntry]
es) arg :: Int
arg
| [TyDecl (DCon _ _ _) _] <- 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 _) -> Totality
Unchecked
Just (Partial _) -> PReason -> Totality
Partial ([Name] -> PReason
Other [Name
f])
x :: Maybe Totality
x -> Totality
Unchecked
| [TyDecl (TCon _ _) _] <- Name -> Context -> [Def]
lookupDef Name
f (IState -> Context
tt_ctxt IState
ist)
= [Int] -> Totality
Total []
tryPath desc :: Int
desc path :: [((SCGEntry, Int), Int)]
path (e :: SCGEntry
e@(f :: Name
f, args :: [Maybe (Int, SizeChange)]
args) : es :: [SCGEntry]
es) arg :: Int
arg
| [Total a :: [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 (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 desc :: Int
desc path :: [((SCGEntry, Int), Int)]
path (e :: SCGEntry
e@(f :: Name
f, nextargs :: [Maybe (Int, SizeChange)]
nextargs) : es :: [SCGEntry]
es) arg :: Int
arg
| [Total a :: [Int]
a] <- Name -> Context -> [Totality]
lookupTotal Name
f (IState -> Context
tt_ctxt IState
ist) = [Int] -> Totality
Total [Int]
a
| [Partial _] <- Name -> Context -> [Totality]
lookupTotal Name
f (IState -> Context
tt_ctxt IState
ist) = PReason -> Totality
Partial ([Name] -> PReason
Other [Name
f])
| Just d :: 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
> 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 (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 (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]))
| [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 [0..]
pathres :: [Totality]
pathres =
do (a :: Maybe (Int, SizeChange)
a, pos :: Int
pos) <- [(Maybe (Int, SizeChange), Int)]
argspos
case Maybe (Int, SizeChange)
a of
Nothing ->
Totality -> [Totality]
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 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 (nextarg :: Int
nextarg, sc :: SizeChange
sc) ->
if Int
nextarg Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arg then
case SizeChange
sc of
Same -> Totality -> [Totality]
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
Smaller -> Totality -> [Totality]
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
+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
_ -> [Char] -> [Totality] -> [Totality]
forall a. [Char] -> a -> a
trace ("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 (m :: * -> *) a. Monad m => a -> m a
return (PReason -> Totality
Partial PReason
Itself)
else Totality -> [Totality]
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 :: [Maybe a] -> Bool
allNothing xs :: [Maybe a]
xs = [(Maybe a, Integer)] -> 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 [0..]))
collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
collapseNothing ((Nothing, t :: b
t) : xs :: [(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 (\ (x :: Maybe a
x, _) -> case Maybe a
x of
Nothing -> Bool
False
_ -> Bool
True) [(Maybe a, b)]
xs
collapseNothing (x :: (Maybe a, b)
x : xs :: [(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 p :: PReason
p : xs :: [Totality]
xs) = PReason -> Totality
Partial PReason
p
noPartial (_ : xs :: [Totality]
xs) = [Totality] -> Totality
noPartial [Totality]
xs
noPartial [] = [Int] -> Totality
Total []
collapse :: [Totality] -> Totality
collapse :: [Totality] -> Totality
collapse xs :: [Totality]
xs = Totality -> [Totality] -> Totality
collapse' Totality
Unchecked [Totality]
xs
collapse' :: Totality -> [Totality] -> Totality
collapse' def :: Totality
def (Total r :: [Int]
r : xs :: [Totality]
xs) = [Int] -> Totality
Total [Int]
r
collapse' def :: Totality
def (Unchecked : xs :: [Totality]
xs) = Totality -> [Totality] -> Totality
collapse' Totality
def [Totality]
xs
collapse' def :: Totality
def (d :: Totality
d : xs :: [Totality]
xs) = Totality -> [Totality] -> Totality
collapse' Totality
d [Totality]
xs
collapse' def :: Totality
def [] = Totality
def