{-# 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 :: 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']
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
"_"
genClauses :: FC -> Name -> [([Name], Term)] ->
[PTerm] -> Idris [PTerm]
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
_ = []
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 []
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]
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 []
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 []
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
| 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)
= 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
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]))] ->
[(Name, [Name])] ->
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)
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
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
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
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'
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
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
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