{-|
Module      : Idris.Coverage
Description : Clause generation for coverage checking

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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

-- | Generate a pattern from an 'impossible' LHS.
--
-- We need this to eliminate the pattern clauses which have been
-- provided explicitly from new clause generation.
--
-- This takes a type directed approach to disambiguating names. If we
-- can't immediately disambiguate by looking at the expected type, it's an
-- error (we can't do this the usual way of trying it to see what type checks
-- since the whole point of an impossible case is that it won't type check!)
mkPatTm :: PTerm -> Idris Term
mkPatTm :: PTerm -> Idris Term
mkPatTm PTerm
t = do IState
i <- Idris IState
getIState
               let timp :: PTerm
timp = Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
addImpl' Bool
True [] [] [] IState
i PTerm
t
               forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing PTerm
timp) Int
0
  where
    toTT :: Maybe Type -> PTerm -> StateT Int Idris Term
    toTT :: Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
ty (PRef FC
_ [FC]
_ Name
n)
       = do IState
i <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
            case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
i) of
                 Just (TyDecl NameType
nt Term
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n forall n. TT n
Erased
                 Maybe Def
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n forall n. TT n
Erased
    toTT Maybe Term
ty (PApp FC
_ t :: PTerm
t@(PRef FC
_ [FC]
_ Name
n) [PArg]
args)
       = do IState
i <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
            let aTys :: [Maybe Term]
aTys = case Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
i) of
                              Just Term
nty -> forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall n. TT n -> [(n, TT n)]
getArgTys Term
nty)
                              Maybe Term
Nothing -> forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) [PArg]
args
            [Term]
args' <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT [Maybe Term]
aTys (forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
args)
            Term
t' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing PTerm
t
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. TT n -> [TT n] -> TT n
mkApp Term
t' [Term]
args'
    toTT Maybe Term
ty (PApp FC
_ PTerm
t [PArg]
args)
       = do Term
t' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing PTerm
t
            [Term]
args' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PArg' t -> t
getTm) [PArg]
args
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. TT n -> [TT n] -> TT n
mkApp Term
t' [Term]
args'
    toTT Maybe Term
ty (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
_ PTerm
r)
       = do Term
l' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing PTerm
l
            Term
r' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing PTerm
r
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
sigmaCon forall n. TT n
Erased) [forall n. TT n
Erased, forall n. TT n
Erased, Term
l', Term
r']
    toTT Maybe Term
ty (PPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
r)
       = do Term
l' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing PTerm
l
            Term
r' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT forall a. Maybe a
Nothing PTerm
r
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
pairCon forall n. TT n
Erased) [forall n. TT n
Erased, forall n. TT n
Erased, Term
l', Term
r']
    -- For alternatives, pick the first and drop the namespaces. It doesn't
    -- really matter which is taken since matching will ignore the namespace.
    toTT (Just Term
ty) (PAlternative [(Name, Name)]
_ PAltType
_ [PTerm]
as)
       | (Term
hd, [Term]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ty
          = do IState
i <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
               case Bool -> Env -> Term -> Term -> IState -> [PTerm] -> [PTerm]
pruneByType Bool
True [] Term
hd Term
ty IState
i [PTerm]
as of
                    [PTerm
a] -> Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT (forall a. a -> Maybe a
Just Term
ty) PTerm
a
                    [PTerm]
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. [Name] -> Err' t
CantResolveAlts (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Name
getAltName [PTerm]
as)
    toTT Maybe Term
Nothing (PAlternative [(Name, Name)]
_ PAltType
_ [PTerm]
as)
                    = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. [Name] -> Err' t
CantResolveAlts (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Name
getAltName [PTerm]
as)
    toTT Maybe Term
ty PTerm
_
       = do Int
v <- forall s (m :: * -> *). MonadState s m => m s
get
            forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v forall a. Num a => a -> a -> a
+ Int
1)
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound (Int -> String -> Name
sMN Int
v String
"imp") forall n. TT n
Erased)

    getAltName :: PTerm -> Name
getAltName (PApp FC
_ (PRef FC
_ [FC]
_ (UN Text
l)) [PArg
_, PArg
_, PArg
arg])
             | Text
l forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" = PTerm -> Name
getAltName (forall t. PArg' t -> t
getTm PArg
arg)
    getAltName (PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg]
_) = Name
n
    getAltName (PRef FC
_ [FC]
_ Name
n) = Name
n
    getAltName (PApp FC
_ PTerm
h [PArg]
_) = PTerm -> Name
getAltName PTerm
h
    getAltName (PHidden PTerm
h) = PTerm -> Name
getAltName PTerm
h
    getAltName PTerm
x = String -> Name
sUN String
"_" -- should never happen here

-- | 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 -> [([Name], Term)] -> -- (Argument names, LHS)
              [PTerm] -> Idris [PTerm]
-- No clauses (only valid via elab reflection). We should probably still do
-- a check here somehow, e.g. that one of the arguments is an obviously
-- empty type. In practice, this should only really be used for Void elimination.
genClauses :: FC -> Name -> [([Name], Term)] -> [PTerm] -> Idris [PTerm]
genClauses FC
fc Name
n [([Name], Term)]
lhs_tms [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
genClauses FC
fc Name
n [([Name], Term)]
lhs_tms [PTerm]
given
   = do IState
i <- Idris IState
getIState

        let lhs_given :: [([Name], Term, Term)]
lhs_given = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders [([Name], Term)]
lhs_tms
                            (forall a b. (a -> b) -> [a] -> [b]
map (IState -> PTerm -> PTerm
stripUnmatchable IState
i) (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PTerm
flattenArgs [PTerm]
given))

        Int -> String -> Idris ()
logCoverage Int
5 forall a b. (a -> b) -> a -> b
$ String
"Building coverage tree for:\n" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
given)
        Int -> String -> Idris ()
logCoverage Int
10 forall a b. (a -> b) -> a -> b
$ String
"Building coverage tree for:\n" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [([Name], Term, Term)]
lhs_given)
        Int -> String -> Idris ()
logCoverage Int
10 forall a b. (a -> b) -> a -> b
$ String
"From terms:\n" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [([Name], Term)]
lhs_tms)
        let givenpos :: [Int]
givenpos = [[Int]] -> [Int]
mergePos (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> [Int]
getGivenPos [PTerm]
given)

        ([Name]
cns, SC
ctree_in) <-
                         case Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
False (forall t. String -> SC' t
UnmatchedCase String
"Undefined") Bool
False
                              ([Int] -> Phase
CoverageCheck [Int]
givenpos) FC
emptyFC [] []
                              [([Name], Term, Term)]
lhs_given
                              (forall a b. a -> b -> a
const []) of
                           OK (CaseDef [Name]
cns SC
ctree_in [Term]
_) ->
                              forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
cns, SC
ctree_in)
                           Error Err
e -> forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc Err
e

        let ctree :: SC
ctree = SC -> SC
trimOverlapping (IState -> SC -> SC
addMissingCons IState
i SC
ctree_in)
        let ([Term]
coveredas, [Term]
missingas) = Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses (IState -> Context
tt_ctxt IState
i) Name
n [Name]
cns SC
ctree
        let covered :: [PTerm]
covered = forall a b. (a -> b) -> [a] -> [b]
map (\Term
t -> IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
t Bool
True Bool
True) [Term]
coveredas
        let missing :: [PTerm]
missing = forall a. (a -> Bool) -> [a] -> [a]
filter (\PTerm
x -> PTerm
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [PTerm]
covered) forall a b. (a -> b) -> a -> b
$
                          forall a b. (a -> b) -> [a] -> [b]
map (\Term
t -> IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
t Bool
True Bool
True) [Term]
missingas

        Int -> String -> Idris ()
logCoverage Int
5 forall a b. (a -> b) -> a -> b
$ String
"Coverage from case tree for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SC
ctree
        Int -> String -> Idris ()
logCoverage Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PTerm]
missing) forall a. [a] -> [a] -> [a]
++ String
" missing clauses for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
        Int -> String -> Idris ()
logCoverage Int
3 forall a b. (a -> b) -> a -> b
$ String
"Missing clauses:\n" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
                              (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
missing)
        Int -> String -> Idris ()
logCoverage Int
10 forall a b. (a -> b) -> a -> b
$ String
"Covered clauses:\n" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
                              (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
covered)
        forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
missing
    where
        flattenArgs :: PTerm -> PTerm
flattenArgs (PApp FC
fc (PApp FC
_ PTerm
f [PArg]
as) [PArg]
as')
             = PTerm -> PTerm
flattenArgs (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f ([PArg]
as forall a. [a] -> [a] -> [a]
++ [PArg]
as'))
        flattenArgs PTerm
t = PTerm
t

getGivenPos :: PTerm -> [Int]
getGivenPos :: PTerm -> [Int]
getGivenPos (PApp FC
_ PTerm
_ [PArg]
pargs) = forall {a}. Num a => a -> [PTerm] -> [a]
getGiven Int
0 (forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
pargs)
  where
    getGiven :: a -> [PTerm] -> [a]
getGiven a
i (PTerm
Placeholder : [PTerm]
tms) = a -> [PTerm] -> [a]
getGiven (a
i forall a. Num a => a -> a -> a
+ a
1) [PTerm]
tms
    getGiven a
i (PTerm
_ : [PTerm]
tms) = a
i forall a. a -> [a] -> [a]
: a -> [PTerm] -> [a]
getGiven (a
i forall a. Num a => a -> a -> a
+ a
1) [PTerm]
tms
    getGiven a
i [] = []
getGivenPos PTerm
_ = []

-- Return a list of Ints which are in every list
mergePos :: [[Int]] -> [Int]
mergePos :: [[Int]] -> [Int]
mergePos [] = []
mergePos [[Int]
x] = [Int]
x
mergePos ([Int]
x : [[Int]]
xs) = forall a. Eq a => [a] -> [a] -> [a]
intersect [Int]
x ([[Int]] -> [Int]
mergePos [[Int]]
xs)

removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders ([Name]
ns, Term
tm) PTerm
ptm = ([Name]
ns, forall {n}. TT n -> PTerm -> TT n
rp Term
tm PTerm
ptm, forall n. TT n
Erased)
  where
    rp :: TT n -> PTerm -> TT n
rp TT n
Erased PTerm
Placeholder = forall n. TT n
Erased
    rp TT n
tm PTerm
Placeholder = forall n. TT n -> TT n
Inferred TT n
tm
    rp TT n
tm (PApp FC
_ PTerm
pf [PArg]
pargs)
       | (TT n
tf, [TT n]
targs) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm
           = let tf' :: TT n
tf' = TT n -> PTerm -> TT n
rp TT n
tf PTerm
pf
                 targs' :: [TT n]
targs' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TT n -> PTerm -> TT n
rp [TT n]
targs (forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
pargs) in
                 forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf' [TT n]
targs'
    rp TT n
tm (PPair FC
_ [FC]
_ PunInfo
_ PTerm
pl PTerm
pr)
       | (TT n
tf, [TT n
tyl, TT n
tyr, TT n
tl, TT n
tr]) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm
           = let tl' :: TT n
tl' = TT n -> PTerm -> TT n
rp TT n
tl PTerm
pl
                 tr' :: TT n
tr' = TT n -> PTerm -> TT n
rp TT n
tr PTerm
pr in
                 forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf [forall n. TT n
Erased, forall n. TT n
Erased, TT n
tl', TT n
tr']
    rp TT n
tm (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
pl PTerm
pt PTerm
pr)
       | (TT n
tf, [TT n
tyl, TT n
tyr, TT n
tl, TT n
tr]) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm
           = let tl' :: TT n
tl' = TT n -> PTerm -> TT n
rp TT n
tl PTerm
pl
                 tr' :: TT n
tr' = TT n -> PTerm -> TT n
rp TT n
tr PTerm
pr in
                 forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf [forall n. TT n
Erased, forall n. TT n
Erased, TT n
tl', TT n
tr']
    rp TT n
tm PTerm
_ = TT n
tm

mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses Context
ctxt Name
fn [Name]
ns SC
sc
     = (forall a b. (a -> b) -> [a] -> [b]
map (Term -> [Term] -> Term
mkPlApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
fn forall n. TT n
Erased)) forall a b. (a -> b) -> a -> b
$
            Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
True (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n forall n. TT n
Erased) [Name]
ns) SC
sc,
        forall a b. (a -> b) -> [a] -> [b]
map (Term -> [Term] -> Term
mkPlApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
fn forall n. TT n
Erased)) forall a b. (a -> b) -> a -> b
$
            Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
False (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n forall n. TT n
Erased) [Name]
ns) SC
sc)
  where
    mkPlApp :: Term -> [Term] -> Term
mkPlApp Term
f [Term]
args = forall n. TT n -> [TT n] -> TT n
mkApp Term
f (forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
erasePs [Term]
args)

    erasePs :: Term -> Term
erasePs ap :: Term
ap@(App AppStatus Name
t Term
f Term
a)
        | (Term
f, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap = forall n. TT n -> [TT n] -> TT n
mkApp Term
f (forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
erasePs [Term]
args)
    erasePs (P NameType
_ Name
n Term
_) | Bool -> Bool
not (Name -> Context -> Bool
isConName Name
n Context
ctxt) = forall n. TT n
Erased
    erasePs Term
tm = Term
tm

    mkFromSC :: Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
cov [Term]
args SC
sc = forall s a. State s a -> s -> a
evalState (Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args SC
sc) []

    mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]
    mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args (STerm Term
_)
        = if Bool
cov then forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args] else forall (m :: * -> *) a. Monad m => a -> m a
return [] -- leaf of provided case
    mkFromSC' Bool
cov [Term]
args (UnmatchedCase String
_)
        = if Bool
cov then forall (m :: * -> *) a. Monad m => a -> m a
return [] else forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args] -- leaf of missing case
    mkFromSC' Bool
cov [Term]
args SC
ImpossibleCase = forall (m :: * -> *) a. Monad m => a -> m a
return []
    mkFromSC' Bool
cov [Term]
args (Case CaseType
_ Name
x [CaseAlt' Term]
alts)
       = do [[Term]]
done <- forall s (m :: * -> *). MonadState s m => m s
get
            if ([Term]
args forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Term]]
done)
               then forall (m :: * -> *) a. Monad m => a -> m a
return []
               else do [[[Term]]]
alts' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> [Term] -> Name -> CaseAlt' Term -> State [[Term]] [[Term]]
mkFromAlt Bool
cov [Term]
args Name
x) [CaseAlt' Term]
alts
                       forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
args forall a. a -> [a] -> [a]
: [[Term]]
done)
                       forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Term]]]
alts')
    mkFromSC' Bool
cov [Term]
args SC
_ = forall (m :: * -> *) a. Monad m => a -> m a
return [] -- Should never happen

    mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> State [[Term]] [[Term]]
    mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt' Term -> State [[Term]] [[Term]]
mkFromAlt Bool
cov [Term]
args Name
x (ConCase Name
c Int
t [Name]
conargs SC
sc)
       = let argrep :: Term
argrep = forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> Bool -> NameType
DCon Int
t (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Bool
False) Name
c forall n. TT n
Erased)
                            (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n forall n. TT n
Erased) [Name]
conargs)
             args' :: [Term]
args' = forall a b. (a -> b) -> [a] -> [b]
map (forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
x Term
argrep) [Term]
args in
             Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args' SC
sc
    mkFromAlt Bool
cov [Term]
args Name
x (ConstCase Const
c SC
sc)
       = let argrep :: TT n
argrep = forall n. Const -> TT n
Constant Const
c
             args' :: [Term]
args' = forall a b. (a -> b) -> [a] -> [b]
map (forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
x forall n. TT n
argrep) [Term]
args in
             Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args' SC
sc
    mkFromAlt Bool
cov [Term]
args Name
x (DefaultCase SC
sc)
       = Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args SC
sc
    mkFromAlt Bool
cov [Term]
_ Name
_ CaseAlt' Term
_ = forall (m :: * -> *) a. Monad m => a -> m a
return []

-- Modify the generated case tree (the case tree builder doesn't have access
-- to the context, so can't do this itself).
-- Replaces any missing cases with explicit cases for the missing constructors
addMissingCons :: IState -> SC -> SC
addMissingCons :: IState -> SC -> SC
addMissingCons IState
ist SC
sc = forall s a. State s a -> s -> a
evalState (IState -> SC -> State Int SC
addMissingConsSt IState
ist SC
sc) Int
0

addMissingConsSt :: IState -> SC -> State Int SC
addMissingConsSt :: IState -> SC -> State Int SC
addMissingConsSt IState
ist (Case CaseType
t Name
n [CaseAlt' Term]
alts) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
n) (forall {p}.
p -> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
addMissingAlts Name
n [CaseAlt' Term]
alts)
  where
    addMissingAlt :: CaseAlt -> State Int CaseAlt
    addMissingAlt :: CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt (ConCase Name
n Int
i [Name]
ns SC
sc)
         = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
i [Name]
ns) (IState -> SC -> State Int SC
addMissingConsSt IState
ist SC
sc)
    addMissingAlt (FnCase Name
n [Name]
ns SC
sc)
         = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
n [Name]
ns) (IState -> SC -> State Int SC
addMissingConsSt IState
ist SC
sc)
    addMissingAlt (ConstCase Const
c SC
sc)
         = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c) (IState -> SC -> State Int SC
addMissingConsSt IState
ist SC
sc)
    addMissingAlt (SucCase Name
n SC
sc)
         = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n) (IState -> SC -> State Int SC
addMissingConsSt IState
ist SC
sc)
    addMissingAlt (DefaultCase SC
sc)
         = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall t. SC' t -> CaseAlt' t
DefaultCase (IState -> SC -> State Int SC
addMissingConsSt IState
ist SC
sc)

    addMissingAlts :: p -> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
addMissingAlts p
argn [CaseAlt' Term]
as
--          | any hasDefault as = map addMissingAlt as
         | cons :: [Name]
cons@(Name
n:[Name]
_) <- forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {t}. CaseAlt' t -> Maybe Name
collectCons [CaseAlt' Term]
as,
           Just Name
tyn <- Name -> Maybe Name
getConType Name
n,
           Just TypeInfo
ti <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tyn (IState -> Ctxt TypeInfo
idris_datatypes IState
ist)
             -- If we've fallen through on this argument earlier, then the
             -- things which were matched in other cases earlier can't be missing
             -- cases now
             = let missing :: [Name]
missing = TypeInfo -> [Name]
con_names TypeInfo
ti forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
cons in
                   do [CaseAlt' Term]
as' <- forall {m :: * -> *} {t}.
MonadState Int m =>
[Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases [Name]
missing [CaseAlt' Term]
as
                      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as'
         | consts :: [Const]
consts@(Const
n:[Const]
_) <- forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {t}. CaseAlt' t -> Maybe Const
collectConsts [CaseAlt' Term]
as
             = let missing :: [Const]
missing = forall a. Eq a => [a] -> [a]
nub (forall a b. (a -> b) -> [a] -> [b]
map Const -> Const
nextConst [Const]
consts) forall a. Eq a => [a] -> [a] -> [a]
\\ [Const]
consts in
                   forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt (forall {t}. [Const] -> [CaseAlt' t] -> [CaseAlt' t]
addCons [Const]
missing [CaseAlt' Term]
as)
    addMissingAlts p
n [CaseAlt' Term]
as = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as

    addCases :: [Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases [Name]
missing [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    addCases [Name]
missing (DefaultCase SC' t
rhs : [CaseAlt' t]
rest)
       = do [Maybe (CaseAlt' t)]
missing' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {m :: * -> *} {t}.
MonadState Int m =>
SC' t -> Name -> m (Maybe (CaseAlt' t))
genMissingAlt SC' t
rhs) [Name]
missing
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a. a -> a
id [Maybe (CaseAlt' t)]
missing' forall a. [a] -> [a] -> [a]
++ [CaseAlt' t]
rest)
    addCases [Name]
missing (CaseAlt' t
c : [CaseAlt' t]
rest)
       = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (CaseAlt' t
c forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ [Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases [Name]
missing [CaseAlt' t]
rest

    addCons :: [Const] -> [CaseAlt' t] -> [CaseAlt' t]
addCons [Const]
missing [] = []
    addCons [Const]
missing (DefaultCase SC' t
rhs : [CaseAlt' t]
rest)
       = forall a b. (a -> b) -> [a] -> [b]
map (forall {t}. SC' t -> Const -> CaseAlt' t
genMissingConAlt SC' t
rhs) [Const]
missing forall a. [a] -> [a] -> [a]
++ [CaseAlt' t]
rest
    addCons [Const]
missing (CaseAlt' t
c : [CaseAlt' t]
rest) = CaseAlt' t
c forall a. a -> [a] -> [a]
: [Const] -> [CaseAlt' t] -> [CaseAlt' t]
addCons [Const]
missing [CaseAlt' t]
rest

    genMissingAlt :: SC' t -> Name -> m (Maybe (CaseAlt' t))
genMissingAlt SC' t
rhs Name
n
         | Just (TyDecl (DCon Int
tag Int
arity Bool
_) Term
ty) <- Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
ist)
             = do Int
name <- forall s (m :: * -> *). MonadState s m => m s
get
                  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
name forall a. Num a => a -> a -> a
+ Int
arity)
                  let args :: [Int]
args = forall a b. (a -> b) -> [a] -> [b]
map (Int
name forall a. Num a => a -> a -> a
+) [Int
0..Int
arityforall a. Num a => a -> a -> a
-Int
1]
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
tag (forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Int -> String -> Name
sMN Int
i String
"m") [Int]
args) SC' t
rhs
         | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

    genMissingConAlt :: SC' t -> Const -> CaseAlt' t
genMissingConAlt SC' t
rhs Const
n = forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
n SC' t
rhs

    collectCons :: CaseAlt' t -> Maybe Name
collectCons (ConCase Name
n Int
i [Name]
args SC' t
sc) = forall a. a -> Maybe a
Just Name
n
    collectCons CaseAlt' t
_ = forall a. Maybe a
Nothing

    collectConsts :: CaseAlt' t -> Maybe Const
collectConsts (ConstCase Const
c SC' t
sc) = forall a. a -> Maybe a
Just Const
c
    collectConsts CaseAlt' t
_ = forall a. Maybe a
Nothing

    getConType :: Name -> Maybe Name
getConType Name
n = do Term
ty <- Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist)
                      case forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
getRetTy (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
ty)) of
                           (P NameType
_ Name
tyn Term
_, [Term]
_) -> forall a. a -> Maybe a
Just Name
tyn
                           (Term, [Term])
_ -> forall a. Maybe a
Nothing

    -- for every constant in a term (at any level) take next one to make sure
    -- that constants which are not explicitly handled are covered
    nextConst :: Const -> Const
nextConst (I Int
c) = Int -> Const
I (Int
c forall a. Num a => a -> a -> a
+ Int
1)
    nextConst (BI Integer
c) = Integer -> Const
BI (Integer
c forall a. Num a => a -> a -> a
+ Integer
1)
    nextConst (Fl Double
c) = Double -> Const
Fl (Double
c forall a. Num a => a -> a -> a
+ Double
1)
    nextConst (B8 Word8
c) = Word8 -> Const
B8 (Word8
c forall a. Num a => a -> a -> a
+ Word8
1)
    nextConst (B16 Word16
c) = Word16 -> Const
B16 (Word16
c forall a. Num a => a -> a -> a
+ Word16
1)
    nextConst (B32 Word32
c) = Word32 -> Const
B32 (Word32
c forall a. Num a => a -> a -> a
+ Word32
1)
    nextConst (B64 Word64
c) = Word64 -> Const
B64 (Word64
c forall a. Num a => a -> a -> a
+ Word64
1)
    nextConst (Ch Char
c) = Char -> Const
Ch (Int -> Char
chr forall a b. (a -> b) -> a -> b
$ Char -> Int
ord Char
c forall a. Num a => a -> a -> a
+ Int
1)
    nextConst (Str String
c) = String -> Const
Str (String
c forall a. [a] -> [a] -> [a]
++ String
"'")
    nextConst Const
o = Const
o

addMissingConsSt IState
ist SC
sc = forall (m :: * -> *) a. Monad m => a -> m a
return SC
sc

trimOverlapping :: SC -> SC
trimOverlapping :: SC -> SC
trimOverlapping SC
sc = [(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [] [] SC
sc
  where
    trim :: [(Name, (Name, [Name]))] -> -- Variable - constructor+args already matched
            [(Name, [Name])] -> -- Variable - constructors which it can't be
            SC -> SC
    trim :: [(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [(Name, (Name, [Name]))]
mustbes [(Name, [Name])]
nots (Case CaseType
t Name
vn [CaseAlt' Term]
alts)
       | Just (Name
c, [Name]
args) <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
vn [(Name, (Name, [Name]))]
mustbes
            = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
vn ([(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
mustbes [(Name, [Name])]
nots Name
vn ((Name, [Name]) -> [CaseAlt' Term] -> [CaseAlt' Term]
substMatch (Name
c, [Name]
args) [CaseAlt' Term]
alts))
       | Just [Name]
cantbe <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
vn [(Name, [Name])]
nots
            = let alts' :: [CaseAlt' Term]
alts' = forall a. (a -> Bool) -> [a] -> [a]
filter (forall {t :: * -> *} {t}.
Foldable t =>
t Name -> CaseAlt' t -> Bool
notConMatch [Name]
cantbe) [CaseAlt' Term]
alts in
                  forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
vn ([(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
mustbes [(Name, [Name])]
nots Name
vn [CaseAlt' Term]
alts')
       | Bool
otherwise = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
vn ([(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
mustbes [(Name, [Name])]
nots Name
vn [CaseAlt' Term]
alts)
    trim [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots SC
sc = SC
sc

    trimAlts :: [(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn [] = []
    trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn (ConCase Name
cn Int
t [Name]
args SC
sc : [CaseAlt' Term]
rest)
        = forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
t [Name]
args ([(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim (forall {a} {b}. a -> b -> [(a, b)] -> [(a, b)]
addMatch Name
vn (Name
cn, [Name]
args) [(Name, (Name, [Name]))]
cs) [(Name, [Name])]
nots SC
sc) forall a. a -> [a] -> [a]
:
            [(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
cs (Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
addCantBe Name
vn Name
cn [(Name, [Name])]
nots) Name
vn [CaseAlt' Term]
rest
    trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn (FnCase Name
n [Name]
ns SC
sc : [CaseAlt' Term]
rest)
        = forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
n [Name]
ns ([(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots SC
sc) forall a. a -> [a] -> [a]
: [(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn [CaseAlt' Term]
rest
    trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn (ConstCase Const
c SC
sc : [CaseAlt' Term]
rest)
        = forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c ([(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots SC
sc) forall a. a -> [a] -> [a]
: [(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn [CaseAlt' Term]
rest
    trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn (SucCase Name
n SC
sc : [CaseAlt' Term]
rest)
        = forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n ([(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots SC
sc) forall a. a -> [a] -> [a]
: [(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn [CaseAlt' Term]
rest
    trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn (DefaultCase SC
sc : [CaseAlt' Term]
rest)
        = forall t. SC' t -> CaseAlt' t
DefaultCase ([(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots SC
sc) forall a. a -> [a] -> [a]
: [(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots Name
vn [CaseAlt' Term]
rest

    substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]
    substMatch :: (Name, [Name]) -> [CaseAlt' Term] -> [CaseAlt' Term]
substMatch (Name, [Name])
ca [] = []
    substMatch (Name
c,[Name]
args) (ConCase Name
cn Int
t [Name]
args' SC
sc : [CaseAlt' Term]
_)
        | Name
c forall a. Eq a => a -> a -> Bool
== Name
cn = [forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
c Int
t [Name]
args ([(Name, Name)] -> SC -> SC
substNames (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args' [Name]
args) SC
sc)]
    substMatch (Name, [Name])
ca (CaseAlt' Term
_:[CaseAlt' Term]
cs) = (Name, [Name]) -> [CaseAlt' Term] -> [CaseAlt' Term]
substMatch (Name, [Name])
ca [CaseAlt' Term]
cs

    substNames :: [(Name, Name)] -> SC -> SC
substNames [] SC
sc = SC
sc
    substNames ((Name
n, Name
n') : [(Name, Name)]
ns) SC
sc
       = [(Name, Name)] -> SC -> SC
substNames [(Name, Name)]
ns (Name -> Name -> SC -> SC
substSC Name
n Name
n' SC
sc)

    notConMatch :: t Name -> CaseAlt' t -> Bool
notConMatch t Name
cs (ConCase Name
cn Int
t [Name]
args SC' t
sc) = Name
cn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t Name
cs
    notConMatch t Name
cs CaseAlt' t
_ = Bool
True

    addMatch :: a -> b -> [(a, b)] -> [(a, b)]
addMatch a
vn b
cn [(a, b)]
cs = (a
vn, b
cn) forall a. a -> [a] -> [a]
: [(a, b)]
cs

    addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
    addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
addCantBe Name
vn Name
cn [] = [(Name
vn, [Name
cn])]
    addCantBe Name
vn Name
cn ((Name
n, [Name]
cbs) : [(Name, [Name])]
nots)
          | Name
vn forall a. Eq a => a -> a -> Bool
== Name
n = ((Name
n, forall a. Eq a => [a] -> [a]
nub (Name
cn forall a. a -> [a] -> [a]
: [Name]
cbs)) forall a. a -> [a] -> [a]
: [(Name, [Name])]
nots)
          | Bool
otherwise = ((Name
n, [Name]
cbs) forall a. a -> [a] -> [a]
: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
addCantBe Name
vn Name
cn [(Name, [Name])]
nots)

-- | Does this error result rule out a case as valid when coverage checking?
validCoverageCase :: Context -> Err -> Bool
validCoverageCase :: Context -> Err -> Bool
validCoverageCase Context
ctxt (CantUnify Bool
_ (Term
topx, Maybe Provenance
_) (Term
topy, Maybe Provenance
_) Err
e [(Name, Term)]
_ Int
_)
    = let topx' :: Term
topx' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topx
          topy' :: Term
topy' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topy in
          Bool -> Bool
not (forall {a}. Eq a => TT a -> TT a -> Bool
sameFam Term
topx' Term
topy' Bool -> Bool -> Bool
|| Bool -> Bool
not (Context -> Err -> Bool
validCoverageCase Context
ctxt Err
e))
  where sameFam :: TT a -> TT a -> Bool
sameFam TT a
topx TT a
topy
            = case (forall n. TT n -> (TT n, [TT n])
unApply TT a
topx, forall n. TT n -> (TT n, [TT n])
unApply TT a
topy) of
                   ((P NameType
_ a
x TT a
_, [TT a]
_), (P NameType
_ a
y TT a
_, [TT a]
_)) -> a
x forall a. Eq a => a -> a -> Bool
== a
y
                   ((TT a, [TT a]), (TT a, [TT a]))
_ -> Bool
False
validCoverageCase Context
ctxt (InfiniteUnify Name
_ Term
_ [(Name, Term)]
_) = Bool
False
validCoverageCase Context
ctxt (CantConvert Term
topx Term
topy [(Name, Term)]
_)
    = let topx' :: Term
topx' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topx
          topy' :: Term
topy' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topy in
          Bool -> Bool
not (forall {a}. Eq a => TT a -> TT a -> Bool
sameFam Term
topx' Term
topy')
  where sameFam :: TT a -> TT a -> Bool
sameFam TT a
topx TT a
topy
            = case (forall n. TT n -> (TT n, [TT n])
unApply TT a
topx, forall n. TT n -> (TT n, [TT n])
unApply TT a
topy) of
                   ((P NameType
_ a
x TT a
_, [TT a]
_), (P NameType
_ a
y TT a
_, [TT a]
_)) -> a
x forall a. Eq a => a -> a -> Bool
== a
y
                   ((TT a, [TT a]), (TT a, [TT a]))
_ -> Bool
False
validCoverageCase Context
ctxt (At FC
_ Err
e) = Context -> Err -> Bool
validCoverageCase Context
ctxt Err
e
validCoverageCase Context
ctxt (Elaborating String
_ Name
_ Maybe Term
_ Err
e) = Context -> Err -> Bool
validCoverageCase Context
ctxt Err
e
validCoverageCase Context
ctxt (ElaboratingArg Name
_ Name
_ [(Name, Name)]
_ Err
e) = Context -> Err -> Bool
validCoverageCase Context
ctxt Err
e
validCoverageCase Context
ctxt Err
_ = Bool
True

-- | Check whether an error is recoverable in the sense needed for
-- coverage checking.
recoverableCoverage :: Context -> Err -> Bool
recoverableCoverage :: Context -> Err -> Bool
recoverableCoverage Context
ctxt (CantUnify Bool
r (Term
topx, Maybe Provenance
_) (Term
topy, Maybe Provenance
_) Err
e [(Name, Term)]
_ Int
_)
    = let topx' :: Term
topx' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topx
          topy' :: Term
topy' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topy in
          forall s a. State s a -> s -> a
evalState (Term -> Term -> State [(Name, Term)] Bool
checkRec Term
topx' Term
topy') []
recoverableCoverage Context
ctxt (CantConvert Term
topx Term
topy [(Name, Term)]
_)
    = let topx' :: Term
topx' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topx
          topy' :: Term
topy' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
topy in
          forall s a. State s a -> s -> a
evalState (Term -> Term -> State [(Name, Term)] Bool
checkRec Term
topx' Term
topy') []
recoverableCoverage Context
ctxt (InfiniteUnify Name
_ Term
_ [(Name, Term)]
_) = Bool
False -- always unrecoverable
recoverableCoverage Context
ctxt (At FC
_ Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage Context
ctxt (Elaborating String
_ Name
_ Maybe Term
_ Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage Context
ctxt (ElaboratingArg Name
_ Name
_ [(Name, Name)]
_ Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage Context
_ Err
_ = Bool
False

-- different notion of recoverable than in unification, since we
-- have no metavars -- just looking to see if a constructor is failing
-- to unify with a function that may be reduced later, or if any
-- variables need to have two different constructor forms

-- The state is a mapping of name to what it has failed to unify
-- with
checkRec :: Term -> Term -> State [(Name, Term)] Bool
checkRec :: Term -> Term -> State [(Name, Term)] Bool
checkRec (P NameType
Bound Name
x Term
_) Term
tm
   | forall {n}. TT n -> Bool
isCon Term
tm = do [(Name, Term)]
nmap <- forall s (m :: * -> *). MonadState s m => m s
get
                   case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, Term)]
nmap of
                        Maybe Term
Nothing -> do forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
x, Term
tm) forall a. a -> [a] -> [a]
: [(Name, Term)]
nmap)
                                      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                        Just Term
y' -> Term -> Term -> State [(Name, Term)] Bool
checkRec Term
tm Term
y'
 where
   isCon :: TT n -> Bool
isCon TT n
tm
       | (P NameType
yt n
_ TT n
_, [TT n]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm,
         NameType -> Bool
conType NameType
yt = Bool
True
   isCon (Constant Const
_) = Bool
True
   isCon TT n
_ = Bool
False

   conType :: NameType -> Bool
conType (DCon Int
_ Int
_ Bool
_) = Bool
True
   conType (TCon Int
_ Int
_) = Bool
True
   conType NameType
_ = Bool
False

checkRec Term
tm (P NameType
Bound Name
y Term
_)
   | forall {n}. TT n -> Bool
isCon Term
tm = do [(Name, Term)]
nmap <- forall s (m :: * -> *). MonadState s m => m s
get
                   case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
y [(Name, Term)]
nmap of
                        Maybe Term
Nothing -> do forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
y, Term
tm) forall a. a -> [a] -> [a]
: [(Name, Term)]
nmap)
                                      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                        Just Term
x' -> Term -> Term -> State [(Name, Term)] Bool
checkRec Term
tm Term
x'
 where
   isCon :: TT n -> Bool
isCon TT n
tm
       | (P NameType
yt n
_ TT n
_, [TT n]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm,
         NameType -> Bool
conType NameType
yt = Bool
True
   isCon (Constant Const
_) = Bool
True
   isCon TT n
_ = Bool
False

   conType :: NameType -> Bool
conType (DCon Int
_ Int
_ Bool
_) = Bool
True
   conType (TCon Int
_ Int
_) = Bool
True
   conType NameType
_ = Bool
False

checkRec (App AppStatus Name
_ Term
f Term
a) p :: Term
p@(P NameType
_ Name
_ Term
_) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
p
checkRec (App AppStatus Name
_ Term
f Term
a) p :: Term
p@(Constant Const
_) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
p
checkRec p :: Term
p@(P NameType
_ Name
_ Term
_) (App AppStatus Name
_ Term
f Term
a) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
p Term
f
checkRec p :: Term
p@(Constant Const
_) (App AppStatus Name
_ Term
f Term
a) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
p Term
f
checkRec fa :: Term
fa@(App AppStatus Name
_ Term
_ Term
_) fa' :: Term
fa'@(App AppStatus Name
_ Term
_ Term
_)
    | (Term
f, [Term]
as) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fa,
      (Term
f', [Term]
as') <- forall n. TT n -> (TT n, [TT n])
unApply Term
fa'
         = if (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as')
              then Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
f'
              -- Same function but different args is recoverable,
              -- and vice versa, if it's an ordinary function
              -- If a constructor, everything has to be recoverable
              else do Bool
fok <- Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
f'
                      Bool
argok <- [Term] -> [Term] -> State [(Name, Term)] Bool
checkRecs (Term
f forall a. a -> [a] -> [a]
: [Term]
as) (Term
f forall a. a -> [a] -> [a]
: [Term]
as')
                      forall (m :: * -> *) a. Monad m => a -> m a
return (if forall {n}. TT n -> Bool
conType Term
f then Bool
fok Bool -> Bool -> Bool
&& Bool
argok
                                           else Bool
fok Bool -> Bool -> Bool
|| Bool
argok)
  where
    checkRecs :: [Term] -> [Term] -> State [(Name, Term)] Bool
checkRecs [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    checkRecs (Term
a : [Term]
as) (Term
b : [Term]
bs) = do Bool
aok <- Term -> Term -> State [(Name, Term)] Bool
checkRec Term
a Term
b
                                     Bool
asok <- [Term] -> [Term] -> State [(Name, Term)] Bool
checkRecs [Term]
as [Term]
bs
                                     forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
aok Bool -> Bool -> Bool
&& Bool
asok)
    conType :: TT n -> Bool
conType (P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_) = Bool
True
    conType (P (TCon Int
_ Int
_) n
_ TT n
_) = Bool
True
    conType (Constant Const
_) = Bool
True
    conType TT n
_ = Bool
False

checkRec (P NameType
xt Name
x Term
_) (P NameType
yt Name
y Term
_)
   | Name
x forall a. Eq a => a -> a -> Bool
== Name
y = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
   | NameType -> NameType -> Bool
ntRec NameType
xt NameType
yt = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
 where
    -- If either name is a reference or a bound variable, then further
    -- development may fix the error, so consider it recoverable.
    -- If both names are constructors, and the name is different, then
    -- it's not recoverable
    ntRec :: NameType -> NameType -> Bool
ntRec NameType
x NameType
y | NameType
Ref <- NameType
x = Bool
True
              | NameType
Ref <- NameType
y = Bool
True
              | NameType
Bound <- NameType
x = Bool
True
              | NameType
Bound <- NameType
y = Bool
True
              | Bool
otherwise = Bool
False -- name is different, unrecoverable
-- A function reference against a constant might be recoverable if we get to
-- reduce the function
checkRec (P NameType
Ref Name
_ Term
_) (Constant Const
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (Constant Const
_) (P NameType
Ref Name
_ Term
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (TType UExp
_) (TType UExp
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec Term
_ Term
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False