idris-0.9.5: src/Idris/Coverage.hs
{-# LANGUAGE PatternGuards #-}
module Idris.Coverage where
import Core.TT
import Core.Evaluate
import Core.CaseTree
import Idris.AbsSyntax
import Idris.Delaborate
import Idris.Error
import Data.List
import Data.Either
import Data.Maybe
import Debug.Trace
import Control.Monad.State
-- Generate the LHSes which are missing from a case tree
-- Eliminate the ones which cannot be well typed
genMissing :: Name -> [Name] -> SC -> Idris [PTerm]
genMissing fn args sc
= do sc' <- expandTree sc
logLvl 5 $ "Checking missing cases for " ++
show fn ++ "\n" ++ (show sc')
(got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'
return $ filter (\x -> not (x `elem` got)) missing
-- Make a term to feed to the pattern matcher from a LHS declared impossible
-- (we can't type check it, but we need the case analysis to check for
-- covering...)
mkPatTm :: PTerm -> Idris Term
mkPatTm t = do i <- get
let timp = addImpl' True [] i t
evalStateT (toTT timp) 0
where
toTT (PRef _ n) = do i <- lift $ get
case lookupDef Nothing n (tt_ctxt i) of
[TyDecl nt _] -> return $ P nt n Erased
_ -> return $ P Ref n Erased
toTT (PApp _ t args) = do t' <- toTT t
args' <- mapM (toTT . getTm) args
return $ mkApp t' args'
toTT _ = do v <- get
put (v + 1)
return (P Bound (MN v "imp") Erased)
mkPTerm :: Name -> [TT Name] -> Idris PTerm
mkPTerm f args = do i <- get
let fapp = mkApp (P Bound f Erased) (map eraseName args)
return $ delab i fapp
where eraseName (App f a) = App (eraseName f) (eraseName a)
eraseName (P _ (MN _ _) _) = Erased
eraseName t = t
gm :: Name -> [TT Name] -> SC -> Idris ([PTerm], [PTerm])
gm fn args (Case n alts) = do m <- mapM (gmAlt fn args n) alts
let (got, missing) = unzip m
return (concat got, concat missing)
gm fn args (STerm tm) = do logLvl 3 ("Covered: " ++ show args)
t <- mkPTerm fn args
return ([t], [])
gm fn args ImpossibleCase = do logLvl 3 ("Impossible: " ++ show args)
t <- mkPTerm fn args
return ([], [])
gm fn args (UnmatchedCase _) = do logLvl 3 ("Missing: " ++ show args)
t <- mkPTerm fn args
return ([], [t])
gmAlt fn args n (ConCase cn t cargs sc)
= do let args' = map (subst n (mkApp (P Bound cn Erased)
(map (\x -> P Bound x Erased) cargs)))
args
gm fn args' sc
gmAlt fn args n (ConstCase c sc)
= do let args' = map (subst n (Constant c)) args
gm fn args' sc
gmAlt fn args n (DefaultCase sc)
= do gm fn args sc
getDefault (DefaultCase sc : _) = sc
getDefault (_ : cs) = getDefault cs
getDefault [] = UnmatchedCase ""
dropDefault (DefaultCase sc : rest) = dropDefault rest
dropDefault (c : cs) = c : dropDefault cs
dropDefault [] = []
expandTree :: SC -> Idris SC
expandTree (Case n alts) = do i <- get
as <- expandAlts i (dropDefault alts)
(getDefault alts)
alts' <- mapM expandTreeA as
return (Case n alts')
where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc
return (ConCase n i ns sc')
expandTreeA (ConstCase i sc) = do sc' <- expandTree sc
return (ConstCase i sc')
expandTreeA (DefaultCase sc) = do sc' <- expandTree sc
return (DefaultCase sc')
expandTree t = return t
expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]
expandAlts i all@(ConstCase c _ : alts) def
= return $ all ++ [DefaultCase def]
expandAlts i all@(ConCase n _ _ _ : alts) def
| (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
= do let tyn = getTy n (tt_ctxt i)
case lookupCtxt Nothing tyn (idris_datatypes i) of
(TI ns _ : _) -> do let ps = map mkPat ns
return $ addAlts ps (altsFor all) all
_ -> return all
where
altsFor [] = []
altsFor (ConCase n _ _ _ : alts) = n : altsFor alts
altsFor (_ : alts) = altsFor alts
addAlts [] got alts = alts
addAlts ((n, arity) : ps) got alts
| n `elem` got = addAlts ps got alts
| otherwise = addAlts ps got (alts ++
[ConCase n (-1) (argList arity) def])
argList i = take i (map (\x -> (MN x "ign")) [0..])
getTy n ctxt
= case lookupTy Nothing n ctxt of
(t : _) -> case unApply (getRetTy t) of
(P _ tyn _, _) -> tyn
x -> error $ "Can't happen getTy 1 " ++ show (n, x)
_ -> error "Can't happen getTy 2"
mkPat x = case lookupCtxt Nothing x (idris_implicits i) of
(pargs : _)
-> (x, length pargs)
_ -> error "Can't happen - genAll"
expandAlts i alts def = return alts
-- OLD STUFF: probably broken...
-- Given a list of LHSs, generate a extra clauses which cover the remaining
-- cases. The ones which haven't been provided are marked 'absurd' so that the
-- checker will make sure they can't happen.
-- This will only work after the given clauses have been typechecked and the
-- names are fully explicit!
genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]
genClauses fc n xs given
= do i <- getIState
let lhss = map (getLHS i) xs
let argss = transpose lhss
let all_args = map (genAll i) argss
logLvl 7 $ "COVERAGE of " ++ show n
logLvl 10 $ show argss ++ "\n" ++ show all_args
logLvl 10 $ "Original: \n" ++
showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
let parg = case lookupCtxt Nothing n (idris_implicits i) of
(p : _) -> p
_ -> repeat (pexp Placeholder)
let tryclauses = mkClauses parg all_args
let new = mnub i $ filter (noMatch i) tryclauses
logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
return new
-- return (map (\t -> PClause n t [] PImpossible []) new)
where getLHS i term
| (f, args) <- unApply term = map (\t -> delab' i t True) args
| otherwise = []
lhsApp (PClause _ _ l _ _ _) = l
lhsApp (PWith _ _ l _ _ _) = l
mnub i [] = []
mnub i (x : xs) =
if (any (\t -> case matchClause i x t of
Right _ -> True
Left _ -> False) xs) then mnub i xs
else x : mnub i xs
noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of
Right _ -> False
Left miss -> True) xs
mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
mkClauses parg args
| all (== [Placeholder]) args = []
mkClauses parg args
= do args' <- mkArg args
let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
return tm
where
mkArg :: [[PTerm]] -> [[PTerm]]
mkArg [] = return []
mkArg (a : as) = do a' <- a
as' <- mkArg as
return (a':as')
-- FIXME: Just look for which one is the deepest, then generate all
-- possibilities up to that depth.
genAll :: IState -> [PTerm] -> [PTerm]
genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
[] -> [Placeholder]
xs -> xs
where
conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i)
conForm (PRef fc n) = isConName Nothing n (tt_ctxt i)
conForm _ = False
otherPats :: PTerm -> [PTerm]
otherPats o@(PRef fc n) = ops fc n [] o
otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
otherPats arg = return Placeholder
ops fc n xs o
| (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
= do xs' <- mapM otherPats (map getTm xs)
let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
let tyn = getTy n (tt_ctxt i)
case lookupCtxt Nothing tyn (idris_datatypes i) of
(TI ns _ : _) -> p : map (mkPat fc) (ns \\ [n])
_ -> [p]
ops fc n arg o = return Placeholder
getTy n ctxt = case lookupTy Nothing n ctxt of
(t : _) -> case unApply (getRetTy t) of
(P _ tyn _, _) -> tyn
x -> error $ "Can't happen getTy 1 " ++ show (n, x)
_ -> error "Can't happen getTy 2"
mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of
(pargs : _)
-> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
_ -> error "Can't happen - genAll"
upd p' p = p { getTm = p' }
-- Check if, in a given type n, the constructor cn : ty is strictly positive,
-- and update the context accordingly
checkPositive :: Name -> (Name, Type) -> Idris ()
checkPositive n (cn, ty)
= do let p = cp ty
i <- getIState
let tot = if p then Total (args ty) else Partial NotPositive
let ctxt' = setTotal cn tot (tt_ctxt i)
putIState (i { tt_ctxt = ctxt' })
logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot
addIBC (IBCTotal cn tot)
where
args t = [0..length (getArgTys t)-1]
cp (Bind n (Pi aty) sc) = posArg aty && cp sc
cp t = True
posArg (Bind _ (Pi nty) sc)
| (P _ n' _, args) <- unApply nty
= n /= n' && posArg sc
posArg t = True
-- Totality checking - check for structural recursion
-- (no mutual definitions yet)
data LexOrder = LexXX | LexEQ | LexLT
deriving (Show, Eq, Ord)
calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
calcProd i fc n pats = do patsprod <- mapM prodRec pats
if (and patsprod)
then return Productive
else return (Partial NotProductive)
where
-- every application of n must be in an argument of a coinductive
-- constructor
prodRec :: ([Name], Term, Term) -> Idris Bool
prodRec (_, _, tm) = prod False tm
prod ok ap@(App _ _)
| (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
| (P _ f ty, args) <- unApply ap
= let co = cotype ty in
if f == n
then do argsprod <- mapM (prod co) args
return (and (ok : argsprod) )
else do argsprod <- mapM (prod co) args
return (and argsprod)
prod ok (App f a) = liftM2 (&&) (prod False f) (prod False a)
prod ok (Bind _ (Let t v) sc) = liftM2 (&&) (prod False v) (prod False v)
prod ok (Bind _ b sc) = prod ok sc
prod ok t = return True
cotype ty
| (P _ t _, _) <- unApply (getRetTy ty)
= case lookupCtxt Nothing t (idris_datatypes i) of
[TI _ True] -> True
_ -> False
| otherwise = False
calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
-> Idris Totality
calcTotality path fc n pats
= do i <- get
let opts = case lookupCtxt Nothing n (idris_flags i) of
[fs] -> fs
_ -> []
case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
(failure : _) -> return failure
_ -> if (Coinductive `elem` opts)
then calcProd i fc n pats
else checkSizeChange n
where
checkLHS i (P _ fn _)
= case lookupTotal fn (tt_ctxt i) of
[Partial _] -> return (Partial (Other [fn]))
_ -> Nothing
checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)
checkLHS _ _ = Nothing
checkTotality :: [Name] -> FC -> Name -> Idris Totality
checkTotality path fc n
| n `elem` path = return (Partial (Mutual (n : path)))
| otherwise = do
t <- getTotality n
updateContext (simplifyCasedef n)
ctxt <- getContext
i <- getIState
let opts = case lookupCtxt Nothing n (idris_flags i) of
[fs] -> fs
_ -> []
t' <- case t of
Unchecked ->
case lookupDef Nothing n ctxt of
[CaseOp _ _ _ pats _ _ _ _] ->
do t' <- if AssertTotal `elem` opts
then return $ Total []
else calcTotality path fc n pats
setTotality n t'
addIBC (IBCTotal n t')
-- if it's not total, it can't reduce, to keep
-- typechecking decidable
case t' of
-- FIXME: Put this back when we can handle mutually recursive things
-- p@(Partial _) ->
-- do setAccessibility n Frozen
-- addIBC (IBCAccess n Frozen)
-- logLvl 5 $ "HIDDEN: "
-- ++ show n ++ show p
_ -> return ()
return t'
_ -> return $ Total []
x -> return x
case t' of
Total _ -> return t'
Productive -> return t'
e -> do w <- cmdOptSet WarnPartial
if TotalFn `elem` opts
then totalityError t'
else do when (w && not (PartialFn `elem` opts)) $
warnPartial n t'
return t'
where
totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
warnPartial n t
= do i <- get
case lookupDef Nothing n (tt_ctxt i) of
[x] -> do
iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t
-- ++ "\n" ++ show x
-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
-- iputStrLn (show cg)
checkDeclTotality :: (FC, Name) -> Idris Totality
checkDeclTotality (fc, n)
= do logLvl 2 $ "Checking " ++ show n ++ " for totality"
buildSCG (fc, n)
checkTotality [] fc n
-- Calculate the size change graph for this definition
-- SCG for a function f consists of a list of:
-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
-- where g is a function called
-- a1 ... an are the arguments of f in positions 1..n of g
-- sizechange1 ... sizechange2 is how their size has changed wrt the input
-- to f
-- Nothing, if the argument is unrelated to the input
buildSCG :: (FC, Name) -> Idris ()
buildSCG (_, n) = do
ist <- get
case lookupCtxt Nothing n (idris_callgraph ist) of
[cg] -> case lookupDef Nothing n (tt_ctxt ist) of
[CaseOp _ _ _ _ args sc _ _] ->
do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n"
++ show sc
let newscg = buildSCG' ist sc args
logLvl 5 $ show newscg
addToCG n ( cg { scg = newscg } )
buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
buildSCG' ist sc args = nub $ scg sc (zip args args)
(zip args (zip args (repeat Same)))
where
scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
[(Name, (Name, SizeChange))] -> -- orig to new, and relationship
[SCGEntry]
scg (Case x alts) vars szs
= let x' = findTL x vars in
concatMap (scgAlt x' vars szs) alts
where
findTL x vars
| Just x' <- lookup x vars
= if x' `elem` args then x'
else findTL x' vars
| otherwise = x
scg (STerm tm) vars szs = scgTerm tm vars szs
scg _ _ _ = []
-- how the arguments relate - either Smaller or Unknown
argRels :: Name -> [(Name, SizeChange)]
argRels n = let ctxt = tt_ctxt ist
[ty] = lookupTy Nothing n ctxt -- must exist!
P _ nty _ = fst (unApply (getRetTy ty))
args = map snd (getArgTys ty) in
map (getRel nty) (map (fst . unApply . getRetTy) args)
where
getRel ty (P _ n' _) | n' == ty = (n, Smaller)
getRel ty _ = (n, Unknown)
scgAlt x vars szs (ConCase n _ args sc)
-- all args smaller than top variable of x in sc
-- (as long as they are in the same type family)
| Just tvar <- lookup x vars
= let arel = argRels n
szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel
++ szs
vars' = zip args (repeat tvar) ++ vars in
scg sc vars' szs'
| otherwise = scg sc vars szs
scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
scgAlt x vars szs (DefaultCase sc) = scg sc vars szs
scgTerm f@(App _ _) vars szs
| (P _ (UN "lazy") _, [_, arg]) <- unApply f
= scgTerm arg vars szs
| (P _ fn _, args) <- unApply f
= let rest = concatMap (\x -> scgTerm x vars szs) args in
case lookup fn vars of
Just _ -> rest
Nothing -> (fn, map (mkChange szs) args) : rest
scgTerm (App f a) vars szs
= scgTerm f vars szs ++ scgTerm a vars szs
scgTerm (Bind n (Let t v) e) vars szs
= scgTerm v vars szs ++ scgTerm e vars szs
scgTerm (Bind n _ e) vars szs
= scgTerm e ((n, n) : vars) szs
scgTerm (P _ fn _) vars szs
= case lookup fn vars of
Just _ -> []
Nothing -> [(fn, [])]
scgTerm _ _ _ = []
mkChange :: [(Name, (Name, SizeChange))] -> Term
-> Maybe (Int, SizeChange)
mkChange szs tm
| (P _ (UN "lazy") _, [_, arg]) <- unApply tm = mkChange szs arg
| (P _ n ty, _) <- unApply tm -- get higher order args too
= do sc <- lookup n szs
case sc of
(_, Unknown) -> Nothing
(o, sc) -> do i <- getArgPos 0 o args
return (i, sc)
mkChange _ _ = Nothing
getArgPos :: Int -> Name -> [Name] -> Maybe Int
getArgPos i n [] = Nothing
getArgPos i n (x : xs) | n == x = Just i
| otherwise = getArgPos (i + 1) n xs
checkSizeChange :: Name -> Idris Totality
checkSizeChange n = do
ist <- get
case lookupCtxt Nothing n (idris_callgraph ist) of
[cg] -> do let ms = mkMultiPaths ist [] (scg cg)
logLvl 6 ("Multipath for " ++ show n ++ ":\n" ++
"from " ++ show (scg cg) ++ "\n" ++
showSep "\n" (map show ms))
logLvl 6 (show cg)
-- every multipath must have an infinitely descending
-- thread, then the function terminates
-- also need to checks functions called are all total
-- (Unchecked is okay as we'll spot problems here)
let tot = map (checkMP ist (length (argsdef cg))) ms
logLvl 3 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
return (noPartial tot)
type MultiPath = [SCGEntry]
mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
mkMultiPaths ist path [] = [reverse path]
mkMultiPaths ist path cg
= concat (map extend cg)
where extend (nextf, args)
| (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
| otherwise
= case lookupCtxt Nothing nextf (idris_callgraph ist) of
[ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
_ -> [ reverse ((nextf, args) : path) ]
-- do (nextf, args) <- cg
-- if ((nextf, args) `elem` path)
-- then return (reverse ((nextf, args) : path))
-- else case lookupCtxt Nothing nextf (idris_callgraph ist) of
-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
-- _ -> return (reverse ((nextf, args) : path))
-- If any route along the multipath leads to infinite descent, we're fine.
-- Try a route beginning with every argument.
-- If we reach a point we've been to before, but with a smaller value,
-- that means there is an infinitely descending path.
checkMP :: IState -> Int -> MultiPath -> Totality
checkMP ist i mp = if i > 0
then collapse (map (tryPath 0 [] mp) [0..i-1])
else tryPath 0 [] mp 0
where
tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
tryPath desc path [] _ = Total []
-- if we get to a constructor, it's fine as long as it's strictly positive
tryPath desc path ((f, _) :es) arg
| [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
= case lookupTotal f (tt_ctxt ist) of
[Total _] -> Total []
[Partial _] -> Partial (Other [f])
x -> error (show x)
| [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
= Total []
-- tryPath desc path (e@(f, []) : es) arg
-- | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
-- tryPath (-10000) ((e, desc) : path) es 0
tryPath desc path (e@(f, nextargs) : es) arg
| Just d <- lookup e path
= if (desc - d) > 0
then Total []
else Partial (Mutual (map (fst . fst) path ++ [f]))
| [Unchecked] <- lookupTotal f (tt_ctxt ist) =
let argspos = zip nextargs [0..] in
collapse' (Partial (Mutual (map (fst . fst) path ++ [f]))) $
do (arg, pos) <- argspos
case arg of
Nothing -> -- don't know, but it's okay if the
-- rest definitely terminates without
-- any cycles with route so far
map (tryPath (-10000) ((e, desc):path) es)
[0..length nextargs - 1]
Just (nextarg, sc) ->
case sc of
Same -> return $ tryPath desc ((e, desc):path)
es
nextarg
Smaller -> return $ tryPath (desc+1)
((e, desc):path)
es
nextarg
_ -> trace ("Shouldn't happen " ++ show e) $
return (Partial Itself)
| [Total _] <- lookupTotal f (tt_ctxt ist) = Total []
| [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
| otherwise = Total []
noPartial (Partial p : xs) = Partial p
noPartial (_ : xs) = noPartial xs
noPartial [] = Total []
collapse xs = collapse' (Partial Itself) xs
collapse' def (Total r : xs) = Total r
collapse' def (d : xs) = collapse' d xs
collapse' def [] = def