{-# LANGUAGE FlexibleContexts, PatternGuards #-}
module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
mkPatTm) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Elab.Utils
import Idris.Error
import Control.Monad.State.Strict
import Data.Char
import Data.List
import Data.Maybe
mkPatTm :: PTerm -> Idris Term
mkPatTm t = do i <- getIState
let timp = addImpl' True [] [] [] i t
evalStateT (toTT Nothing timp) 0
where
toTT :: Maybe Type -> PTerm -> StateT Int Idris Term
toTT ty (PRef _ _ n)
= do i <- lift getIState
case lookupDefExact n (tt_ctxt i) of
Just (TyDecl nt _) -> return $ P nt n Erased
_ -> return $ P Ref n Erased
toTT ty (PApp _ t@(PRef _ _ n) args)
= do i <- lift getIState
let aTys = case lookupTyExact n (tt_ctxt i) of
Just nty -> map (Just . snd) (getArgTys nty)
Nothing -> map (const Nothing) args
args' <- zipWithM toTT aTys (map getTm args)
t' <- toTT Nothing t
return $ mkApp t' args'
toTT ty (PApp _ t args)
= do t' <- toTT Nothing t
args' <- mapM (toTT Nothing . getTm) args
return $ mkApp t' args'
toTT ty (PDPair _ _ _ l _ r)
= do l' <- toTT Nothing l
r' <- toTT Nothing r
return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
toTT ty (PPair _ _ _ l r)
= do l' <- toTT Nothing l
r' <- toTT Nothing r
return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
toTT (Just ty) (PAlternative _ _ as)
| (hd, _) <- unApply ty
= do i <- lift getIState
case pruneByType True [] hd ty i as of
[a] -> toTT (Just ty) a
_ -> lift $ ierror $ CantResolveAlts (map getAltName as)
toTT Nothing (PAlternative _ _ as)
= lift $ ierror $ CantResolveAlts (map getAltName as)
toTT ty _
= do v <- get
put (v + 1)
return (P Bound (sMN v "imp") Erased)
getAltName (PApp _ (PRef _ _ (UN l)) [_, _, arg])
| l == txt "Delay" = getAltName (getTm arg)
getAltName (PApp _ (PRef _ _ n) _) = n
getAltName (PRef _ _ n) = n
getAltName (PApp _ h _) = getAltName h
getAltName (PHidden h) = getAltName h
getAltName x = sUN "_"
genClauses :: FC -> Name -> [([Name], Term)] ->
[PTerm] -> Idris [PTerm]
genClauses fc n lhs_tms [] = return []
genClauses fc n lhs_tms given
= do i <- getIState
let lhs_given = zipWith removePlaceholders lhs_tms
(map (stripUnmatchable i) (map flattenArgs given))
logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map showTmImpls given)
logCoverage 10 $ "Building coverage tree for:\n" ++ showSep "\n" (map show lhs_given)
logCoverage 10 $ "From terms:\n" ++ showSep "\n" (map show lhs_tms)
let givenpos = mergePos (map getGivenPos given)
(cns, ctree_in) <-
case simpleCase False (UnmatchedCase "Undefined") False
(CoverageCheck givenpos) emptyFC [] []
lhs_given
(const []) of
OK (CaseDef cns ctree_in _) ->
return (cns, ctree_in)
Error e -> tclift $ tfail $ At fc e
let ctree = trimOverlapping (addMissingCons i ctree_in)
let (coveredas, missingas) = mkNewClauses (tt_ctxt i) n cns ctree
let covered = map (\t -> delab' i t True True) coveredas
let missing = filter (\x -> x `notElem` covered) $
map (\t -> delab' i t True True) missingas
logCoverage 5 $ "Coverage from case tree for " ++ show n ++ ": " ++ show ctree
logCoverage 2 $ show (length missing) ++ " missing clauses for " ++ show n
logCoverage 3 $ "Missing clauses:\n" ++ showSep "\n"
(map showTmImpls missing)
logCoverage 10 $ "Covered clauses:\n" ++ showSep "\n"
(map showTmImpls covered)
return missing
where
flattenArgs (PApp fc (PApp _ f as) as')
= flattenArgs (PApp fc f (as ++ as'))
flattenArgs t = t
getGivenPos :: PTerm -> [Int]
getGivenPos (PApp _ _ pargs) = getGiven 0 (map getTm pargs)
where
getGiven i (Placeholder : tms) = getGiven (i + 1) tms
getGiven i (_ : tms) = i : getGiven (i + 1) tms
getGiven i [] = []
getGivenPos _ = []
mergePos :: [[Int]] -> [Int]
mergePos [] = []
mergePos [x] = x
mergePos (x : xs) = intersect x (mergePos xs)
removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders (ns, tm) ptm = (ns, rp tm ptm, Erased)
where
rp Erased Placeholder = Erased
rp tm Placeholder = Inferred tm
rp tm (PApp _ pf pargs)
| (tf, targs) <- unApply tm
= let tf' = rp tf pf
targs' = zipWith rp targs (map getTm pargs) in
mkApp tf' targs'
rp tm (PPair _ _ _ pl pr)
| (tf, [tyl, tyr, tl, tr]) <- unApply tm
= let tl' = rp tl pl
tr' = rp tr pr in
mkApp tf [Erased, Erased, tl', tr']
rp tm (PDPair _ _ _ pl pt pr)
| (tf, [tyl, tyr, tl, tr]) <- unApply tm
= let tl' = rp tl pl
tr' = rp tr pr in
mkApp tf [Erased, Erased, tl', tr']
rp tm _ = tm
mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses ctxt fn ns sc
= (map (mkPlApp (P Ref fn Erased)) $
mkFromSC True (map (\n -> P Ref n Erased) ns) sc,
map (mkPlApp (P Ref fn Erased)) $
mkFromSC False (map (\n -> P Ref n Erased) ns) sc)
where
mkPlApp f args = mkApp f (map erasePs args)
erasePs ap@(App t f a)
| (f, args) <- unApply ap = mkApp f (map erasePs args)
erasePs (P _ n _) | not (isConName n ctxt) = Erased
erasePs tm = tm
mkFromSC cov args sc = evalState (mkFromSC' cov args sc) []
mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' cov args (STerm _)
= if cov then return [args] else return []
mkFromSC' cov args (UnmatchedCase _)
= if cov then return [] else return [args]
mkFromSC' cov args ImpossibleCase = return []
mkFromSC' cov args (Case _ x alts)
= do done <- get
if (args `elem` done)
then return []
else do alts' <- mapM (mkFromAlt cov args x) alts
put (args : done)
return (concat alts')
mkFromSC' cov args _ = return []
mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> State [[Term]] [[Term]]
mkFromAlt cov args x (ConCase c t conargs sc)
= let argrep = mkApp (P (DCon t (length args) False) c Erased)
(map (\n -> P Ref n Erased) conargs)
args' = map (subst x argrep) args in
mkFromSC' cov args' sc
mkFromAlt cov args x (ConstCase c sc)
= let argrep = Constant c
args' = map (subst x argrep) args in
mkFromSC' cov args' sc
mkFromAlt cov args x (DefaultCase sc)
= mkFromSC' cov args sc
mkFromAlt cov _ _ _ = return []
addMissingCons :: IState -> SC -> SC
addMissingCons ist sc = evalState (addMissingConsSt ist sc) 0
addMissingConsSt :: IState -> SC -> State Int SC
addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)
where
addMissingAlt :: CaseAlt -> State Int CaseAlt
addMissingAlt (ConCase n i ns sc)
= liftM (ConCase n i ns) (addMissingConsSt ist sc)
addMissingAlt (FnCase n ns sc)
= liftM (FnCase n ns) (addMissingConsSt ist sc)
addMissingAlt (ConstCase c sc)
= liftM (ConstCase c) (addMissingConsSt ist sc)
addMissingAlt (SucCase n sc)
= liftM (SucCase n) (addMissingConsSt ist sc)
addMissingAlt (DefaultCase sc)
= liftM DefaultCase (addMissingConsSt ist sc)
addMissingAlts argn as
| cons@(n:_) <- mapMaybe collectCons as,
Just tyn <- getConType n,
Just ti <- lookupCtxtExact tyn (idris_datatypes ist)
= let missing = con_names ti \\ cons in
do as' <- addCases missing as
mapM addMissingAlt as'
| consts@(n:_) <- mapMaybe collectConsts as
= let missing = nub (map nextConst consts) \\ consts in
mapM addMissingAlt (addCons missing as)
addMissingAlts n as = mapM addMissingAlt as
addCases missing [] = return []
addCases missing (DefaultCase rhs : rest)
= do missing' <- mapM (genMissingAlt rhs) missing
return (mapMaybe id missing' ++ rest)
addCases missing (c : rest)
= liftM (c :) $ addCases missing rest
addCons missing [] = []
addCons missing (DefaultCase rhs : rest)
= map (genMissingConAlt rhs) missing ++ rest
addCons missing (c : rest) = c : addCons missing rest
genMissingAlt rhs n
| Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)
= do name <- get
put (name + arity)
let args = map (name +) [0..arity-1]
return $ Just $ ConCase n tag (map (\i -> sMN i "m") args) rhs
| otherwise = return Nothing
genMissingConAlt rhs n = ConstCase n rhs
collectCons (ConCase n i args sc) = Just n
collectCons _ = Nothing
collectConsts (ConstCase c sc) = Just c
collectConsts _ = Nothing
getConType n = do ty <- lookupTyExact n (tt_ctxt ist)
case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of
(P _ tyn _, _) -> Just tyn
_ -> Nothing
nextConst (I c) = I (c + 1)
nextConst (BI c) = BI (c + 1)
nextConst (Fl c) = Fl (c + 1)
nextConst (B8 c) = B8 (c + 1)
nextConst (B16 c) = B16 (c + 1)
nextConst (B32 c) = B32 (c + 1)
nextConst (B64 c) = B64 (c + 1)
nextConst (Ch c) = Ch (chr $ ord c + 1)
nextConst (Str c) = Str (c ++ "'")
nextConst o = o
addMissingConsSt ist sc = return sc
trimOverlapping :: SC -> SC
trimOverlapping sc = trim [] [] sc
where
trim :: [(Name, (Name, [Name]))] ->
[(Name, [Name])] ->
SC -> SC
trim mustbes nots (Case t vn alts)
| Just (c, args) <- lookup vn mustbes
= Case t vn (trimAlts mustbes nots vn (substMatch (c, args) alts))
| Just cantbe <- lookup vn nots
= let alts' = filter (notConMatch cantbe) alts in
Case t vn (trimAlts mustbes nots vn alts')
| otherwise = Case t vn (trimAlts mustbes nots vn alts)
trim cs nots sc = sc
trimAlts cs nots vn [] = []
trimAlts cs nots vn (ConCase cn t args sc : rest)
= ConCase cn t args (trim (addMatch vn (cn, args) cs) nots sc) :
trimAlts cs (addCantBe vn cn nots) vn rest
trimAlts cs nots vn (FnCase n ns sc : rest)
= FnCase n ns (trim cs nots sc) : trimAlts cs nots vn rest
trimAlts cs nots vn (ConstCase c sc : rest)
= ConstCase c (trim cs nots sc) : trimAlts cs nots vn rest
trimAlts cs nots vn (SucCase n sc : rest)
= SucCase n (trim cs nots sc) : trimAlts cs nots vn rest
trimAlts cs nots vn (DefaultCase sc : rest)
= DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest
substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]
substMatch ca [] = []
substMatch (c,args) (ConCase cn t args' sc : _)
| c == cn = [ConCase c t args (substNames (zip args' args) sc)]
substMatch ca (_:cs) = substMatch ca cs
substNames [] sc = sc
substNames ((n, n') : ns) sc
= substNames ns (substSC n n' sc)
notConMatch cs (ConCase cn t args sc) = cn `notElem` cs
notConMatch cs _ = True
addMatch vn cn cs = (vn, cn) : cs
addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
addCantBe vn cn [] = [(vn, [cn])]
addCantBe vn cn ((n, cbs) : nots)
| vn == n = ((n, nub (cn : cbs)) : nots)
| otherwise = ((n, cbs) : addCantBe vn cn nots)
validCoverageCase :: Context -> Err -> Bool
validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
= let topx' = normalise ctxt [] topx
topy' = normalise ctxt [] topy in
not (sameFam topx' topy' || not (validCoverageCase ctxt e))
where sameFam topx topy
= case (unApply topx, unApply topy) of
((P _ x _, _), (P _ y _, _)) -> x == y
_ -> False
validCoverageCase ctxt (InfiniteUnify _ _ _) = False
validCoverageCase ctxt (CantConvert topx topy _)
= let topx' = normalise ctxt [] topx
topy' = normalise ctxt [] topy in
not (sameFam topx' topy')
where sameFam topx topy
= case (unApply topx, unApply topy) of
((P _ x _, _), (P _ y _, _)) -> x == y
_ -> False
validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e
validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e
validCoverageCase ctxt _ = True
recoverableCoverage :: Context -> Err -> Bool
recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
= let topx' = normalise ctxt [] topx
topy' = normalise ctxt [] topy in
evalState (checkRec topx' topy') []
recoverableCoverage ctxt (CantConvert topx topy _)
= let topx' = normalise ctxt [] topx
topy' = normalise ctxt [] topy in
evalState (checkRec topx' topy') []
recoverableCoverage ctxt (InfiniteUnify _ _ _) = False
recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
recoverableCoverage _ _ = False
checkRec :: Term -> Term -> State [(Name, Term)] Bool
checkRec (P Bound x _) tm
| isCon tm = do nmap <- get
case lookup x nmap of
Nothing -> do put ((x, tm) : nmap)
return True
Just y' -> checkRec tm y'
where
isCon tm
| (P yt _ _, _) <- unApply tm,
conType yt = True
isCon (Constant _) = True
isCon _ = False
conType (DCon _ _ _) = True
conType (TCon _ _) = True
conType _ = False
checkRec tm (P Bound y _)
| isCon tm = do nmap <- get
case lookup y nmap of
Nothing -> do put ((y, tm) : nmap)
return True
Just x' -> checkRec tm x'
where
isCon tm
| (P yt _ _, _) <- unApply tm,
conType yt = True
isCon (Constant _) = True
isCon _ = False
conType (DCon _ _ _) = True
conType (TCon _ _) = True
conType _ = False
checkRec (App _ f a) p@(P _ _ _) = checkRec f p
checkRec (App _ f a) p@(Constant _) = checkRec f p
checkRec p@(P _ _ _) (App _ f a) = checkRec p f
checkRec p@(Constant _) (App _ f a) = checkRec p f
checkRec fa@(App _ _ _) fa'@(App _ _ _)
| (f, as) <- unApply fa,
(f', as') <- unApply fa'
= if (length as /= length as')
then checkRec f f'
else do fok <- checkRec f f'
argok <- checkRecs (f : as) (f : as')
return (if conType f then fok && argok
else fok || argok)
where
checkRecs [] [] = return True
checkRecs (a : as) (b : bs) = do aok <- checkRec a b
asok <- checkRecs as bs
return (aok && asok)
conType (P (DCon _ _ _) _ _) = True
conType (P (TCon _ _) _ _) = True
conType (Constant _) = True
conType _ = False
checkRec (P xt x _) (P yt y _)
| x == y = return True
| ntRec xt yt = return True
where
ntRec x y | Ref <- x = True
| Ref <- y = True
| Bound <- x = True
| Bound <- y = True
| otherwise = False
checkRec (P Ref _ _) (Constant _) = return True
checkRec (Constant _) (P Ref _ _) = return True
checkRec (TType _) (TType _) = return True
checkRec _ _ = return False