{-|
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
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
               StateT Int (StateT IState (ExceptT Err IO)) Term
-> Int -> Idris Term
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 Maybe Term
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 <- Idris IState -> StateT Int (StateT IState (ExceptT Err IO)) IState
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
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
_) -> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n Term
forall n. TT n
Erased
                 Maybe Def
_ -> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased
    toTT Maybe Term
ty (PApp FC
_ t :: PTerm
t@(PRef FC
_ [FC]
_ Name
n) [PArg]
args)
       = do IState
i <- Idris IState -> StateT Int (StateT IState (ExceptT Err IO)) IState
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
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 -> ((Name, Term) -> Maybe Term) -> [(Name, Term)] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term)
-> ((Name, Term) -> Term) -> (Name, Term) -> Maybe Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Term) -> Term
forall a b. (a, b) -> b
snd) (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
nty)
                              Maybe Term
Nothing -> (PArg -> Maybe Term) -> [PArg] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Term -> PArg -> Maybe Term
forall a b. a -> b -> a
const Maybe Term
forall a. Maybe a
Nothing) [PArg]
args
            [Term]
args' <- (Maybe Term
 -> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> [Maybe Term]
-> [PTerm]
-> StateT Int (StateT IState (ExceptT Err IO)) [Term]
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 ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
args)
            Term
t' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
t
            Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
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 Maybe Term
forall a. Maybe a
Nothing PTerm
t
            [Term]
args' <- (PArg -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> [PArg] -> StateT Int (StateT IState (ExceptT Err IO)) [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing (PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> (PArg -> PTerm)
-> PArg
-> StateT Int (StateT IState (ExceptT Err IO)) Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PArg -> PTerm
forall t. PArg' t -> t
getTm) [PArg]
args
            Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
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 Maybe Term
forall a. Maybe a
Nothing PTerm
l
            Term
r' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
r
            Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
sigmaCon Term
forall n. TT n
Erased) [Term
forall n. TT n
Erased, Term
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 Maybe Term
forall a. Maybe a
Nothing PTerm
l
            Term
r' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
r
            Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
pairCon Term
forall n. TT n
Erased) [Term
forall n. TT n
Erased, Term
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]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ty
          = do IState
i <- Idris IState -> StateT Int (StateT IState (ExceptT Err IO)) IState
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
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 (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
ty) PTerm
a
                    [PTerm]
_ -> Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Err -> Idris Term
forall a. Err -> Idris a
ierror (Err -> Idris Term) -> Err -> Idris Term
forall a b. (a -> b) -> a -> b
$ [Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts ((PTerm -> Name) -> [PTerm] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Name
getAltName [PTerm]
as)
    toTT Maybe Term
Nothing (PAlternative [(Name, Name)]
_ PAltType
_ [PTerm]
as)
                    = Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Err -> Idris Term
forall a. Err -> Idris a
ierror (Err -> Idris Term) -> Err -> Idris Term
forall a b. (a -> b) -> a -> b
$ [Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts ((PTerm -> Name) -> [PTerm] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Name
getAltName [PTerm]
as)
    toTT Maybe Term
ty PTerm
_
       = do Int
v <- StateT Int (StateT IState (ExceptT Err IO)) Int
forall s (m :: * -> *). MonadState s m => m s
get
            Int -> StateT Int (StateT IState (ExceptT Err IO)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound (Int -> String -> Name
sMN Int
v String
"imp") Term
forall n. TT n
Erased)

    getAltName :: PTerm -> Name
getAltName (PApp FC
_ (PRef FC
_ [FC]
_ (UN Text
l)) [PArg
_, PArg
_, PArg
arg])
             | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" = PTerm -> Name
getAltName (PArg -> PTerm
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 [] = [PTerm] -> Idris [PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
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 = (([Name], Term) -> PTerm -> ([Name], Term, Term))
-> [([Name], Term)] -> [PTerm] -> [([Name], Term, Term)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders [([Name], Term)]
lhs_tms
                            ((PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> PTerm -> PTerm
stripUnmatchable IState
i) ((PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PTerm
flattenArgs [PTerm]
given))

        Int -> String -> Idris ()
logCoverage Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Building coverage tree for:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" ((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
given)
        Int -> String -> Idris ()
logCoverage Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Building coverage tree for:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" ((([Name], Term, Term) -> String)
-> [([Name], Term, Term)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ([Name], Term, Term) -> String
forall a. Show a => a -> String
show [([Name], Term, Term)]
lhs_given)
        Int -> String -> Idris ()
logCoverage Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"From terms:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" ((([Name], Term) -> String) -> [([Name], Term)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ([Name], Term) -> String
forall a. Show a => a -> String
show [([Name], Term)]
lhs_tms)
        let givenpos :: [Int]
givenpos = [[Int]] -> [Int]
mergePos ((PTerm -> [Int]) -> [PTerm] -> [[Int]]
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 (String -> SC
forall t. String -> SC' t
UnmatchedCase String
"Undefined") Bool
False
                              ([Int] -> Phase
CoverageCheck [Int]
givenpos) FC
emptyFC [] []
                              [([Name], Term, Term)]
lhs_given
                              ([Int] -> ErasureInfo
forall a b. a -> b -> a
const []) of
                           OK (CaseDef [Name]
cns SC
ctree_in [Term]
_) ->
                              ([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
cns, SC
ctree_in)
                           Error Err
e -> TC ([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC)
forall a. TC a -> Idris a
tclift (TC ([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC))
-> TC ([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC)
forall a b. (a -> b) -> a -> b
$ Err -> TC ([Name], SC)
forall a. Err -> TC a
tfail (Err -> TC ([Name], SC)) -> Err -> TC ([Name], SC)
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
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 = (Term -> PTerm) -> [Term] -> [PTerm]
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 = (PTerm -> Bool) -> [PTerm] -> [PTerm]
forall a. (a -> Bool) -> [a] -> [a]
filter (\PTerm
x -> PTerm
x PTerm -> [PTerm] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [PTerm]
covered) ([PTerm] -> [PTerm]) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> a -> b
$
                          (Term -> PTerm) -> [Term] -> [PTerm]
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Coverage from case tree for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
ctree
        Int -> String -> Idris ()
logCoverage Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show ([PTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PTerm]
missing) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" missing clauses for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
        Int -> String -> Idris ()
logCoverage Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Missing clauses:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
                              ((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
missing)
        Int -> String -> Idris ()
logCoverage Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Covered clauses:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
                              ((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
covered)
        [PTerm] -> Idris [PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
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 [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ [PArg]
as'))
        flattenArgs PTerm
t = PTerm
t

getGivenPos :: PTerm -> [Int]
getGivenPos :: PTerm -> [Int]
getGivenPos (PApp FC
_ PTerm
_ [PArg]
pargs) = Int -> [PTerm] -> [Int]
forall {a}. Num a => a -> [PTerm] -> [a]
getGiven Int
0 ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
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 a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) [PTerm]
tms
    getGiven a
i (PTerm
_ : [PTerm]
tms) = a
i a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a -> [PTerm] -> [a]
getGiven (a
i a -> a -> a
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) = [Int] -> [Int] -> [Int]
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, Term -> PTerm -> Term
forall {n}. TT n -> PTerm -> TT n
rp Term
tm PTerm
ptm, Term
forall n. TT n
Erased)
  where
    rp :: TT n -> PTerm -> TT n
rp TT n
Erased PTerm
Placeholder = TT n
forall n. TT n
Erased
    rp TT n
tm PTerm
Placeholder = TT n -> TT n
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) <- TT n -> (TT n, [TT n])
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' = (TT n -> PTerm -> TT n) -> [TT n] -> [PTerm] -> [TT n]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TT n -> PTerm -> TT n
rp [TT n]
targs ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
pargs) in
                 TT n -> [TT n] -> TT n
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]) <- TT n -> (TT n, [TT n])
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
                 TT n -> [TT n] -> TT n
forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf [TT n
forall n. TT n
Erased, TT n
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]) <- TT n -> (TT n, [TT n])
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
                 TT n -> [TT n] -> TT n
forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf [TT n
forall n. TT n
Erased, TT n
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
     = (([Term] -> Term) -> [[Term]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> [Term] -> Term
mkPlApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
fn Term
forall n. TT n
Erased)) ([[Term]] -> [Term]) -> [[Term]] -> [Term]
forall a b. (a -> b) -> a -> b
$
            Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
True ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
ns) SC
sc,
        ([Term] -> Term) -> [[Term]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> [Term] -> Term
mkPlApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
fn Term
forall n. TT n
Erased)) ([[Term]] -> [Term]) -> [[Term]] -> [Term]
forall a b. (a -> b) -> a -> b
$
            Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
False ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
ns) SC
sc)
  where
    mkPlApp :: Term -> [Term] -> Term
mkPlApp Term
f [Term]
args = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
f ((Term -> Term) -> [Term] -> [Term]
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
f ((Term -> Term) -> [Term] -> [Term]
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) = Term
forall n. TT n
Erased
    erasePs Term
tm = Term
tm

    mkFromSC :: Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
cov [Term]
args SC
sc = State [[Term]] [[Term]] -> [[Term]] -> [[Term]]
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 [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args] else [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- leaf of provided case
    mkFromSC' Bool
cov [Term]
args (UnmatchedCase String
_)
        = if Bool
cov then [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args] -- leaf of missing case
    mkFromSC' Bool
cov [Term]
args SC
ImpossibleCase = [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    mkFromSC' Bool
cov [Term]
args (Case CaseType
_ Name
x [CaseAlt' Term]
alts)
       = do [[Term]]
done <- State [[Term]] [[Term]]
forall s (m :: * -> *). MonadState s m => m s
get
            if ([Term]
args [Term] -> [[Term]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Term]]
done)
               then [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
               else do [[[Term]]]
alts' <- (CaseAlt' Term -> State [[Term]] [[Term]])
-> [CaseAlt' Term] -> StateT [[Term]] Identity [[[Term]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> [Term] -> Name -> CaseAlt' Term -> State [[Term]] [[Term]]
mkFromAlt Bool
cov [Term]
args Name
x) [CaseAlt' Term]
alts
                       [[Term]] -> StateT [[Term]] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
args [Term] -> [[Term]] -> [[Term]]
forall a. a -> [a] -> [a]
: [[Term]]
done)
                       [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[[Term]]] -> [[Term]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Term]]]
alts')
    mkFromSC' Bool
cov [Term]
args SC
_ = [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
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 = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> Bool -> NameType
DCon Int
t ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Bool
False) Name
c Term
forall n. TT n
Erased)
                            ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
conargs)
             args' :: [Term]
args' = (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Term -> Term -> Term
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 = Const -> TT n
forall n. Const -> TT n
Constant Const
c
             args' :: [Term]
args' = (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
x Term
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
_ = [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
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 = State Int SC -> Int -> 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) = ([CaseAlt' Term] -> SC)
-> StateT Int Identity [CaseAlt' Term] -> State Int SC
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
n) (Name -> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
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)
         = (SC -> CaseAlt' Term) -> State Int SC -> State Int (CaseAlt' Term)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Name -> Int -> [Name] -> SC -> CaseAlt' Term
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)
         = (SC -> CaseAlt' Term) -> State Int SC -> State Int (CaseAlt' Term)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Name -> [Name] -> SC -> CaseAlt' Term
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)
         = (SC -> CaseAlt' Term) -> State Int SC -> State Int (CaseAlt' Term)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Const -> SC -> CaseAlt' Term
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)
         = (SC -> CaseAlt' Term) -> State Int SC -> State Int (CaseAlt' Term)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Name -> SC -> CaseAlt' Term
forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n) (IState -> SC -> State Int SC
addMissingConsSt IState
ist SC
sc)
    addMissingAlt (DefaultCase SC
sc)
         = (SC -> CaseAlt' Term) -> State Int SC -> State Int (CaseAlt' Term)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SC -> CaseAlt' Term
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]
_) <- (CaseAlt' Term -> Maybe Name) -> [CaseAlt' Term] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe CaseAlt' Term -> Maybe Name
forall {t}. CaseAlt' t -> Maybe Name
collectCons [CaseAlt' Term]
as,
           Just Name
tyn <- Name -> Maybe Name
getConType Name
n,
           Just TypeInfo
ti <- Name -> Ctxt TypeInfo -> Maybe TypeInfo
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 [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
cons in
                   do [CaseAlt' Term]
as' <- [Name] -> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
forall {m :: * -> *} {t}.
MonadState Int m =>
[Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases [Name]
missing [CaseAlt' Term]
as
                      (CaseAlt' Term -> State Int (CaseAlt' Term))
-> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as'
         | consts :: [Const]
consts@(Const
n:[Const]
_) <- (CaseAlt' Term -> Maybe Const) -> [CaseAlt' Term] -> [Const]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe CaseAlt' Term -> Maybe Const
forall {t}. CaseAlt' t -> Maybe Const
collectConsts [CaseAlt' Term]
as
             = let missing :: [Const]
missing = [Const] -> [Const]
forall a. Eq a => [a] -> [a]
nub ((Const -> Const) -> [Const] -> [Const]
forall a b. (a -> b) -> [a] -> [b]
map Const -> Const
nextConst [Const]
consts) [Const] -> [Const] -> [Const]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Const]
consts in
                   (CaseAlt' Term -> State Int (CaseAlt' Term))
-> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt ([Const] -> [CaseAlt' Term] -> [CaseAlt' Term]
forall {t}. [Const] -> [CaseAlt' t] -> [CaseAlt' t]
addCons [Const]
missing [CaseAlt' Term]
as)
    addMissingAlts p
n [CaseAlt' Term]
as = (CaseAlt' Term -> State Int (CaseAlt' Term))
-> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as

    addCases :: [Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases [Name]
missing [] = [CaseAlt' t] -> m [CaseAlt' t]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    addCases [Name]
missing (DefaultCase SC' t
rhs : [CaseAlt' t]
rest)
       = do [Maybe (CaseAlt' t)]
missing' <- (Name -> m (Maybe (CaseAlt' t)))
-> [Name] -> m [Maybe (CaseAlt' t)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (SC' t -> Name -> m (Maybe (CaseAlt' t))
forall {m :: * -> *} {t}.
MonadState Int m =>
SC' t -> Name -> m (Maybe (CaseAlt' t))
genMissingAlt SC' t
rhs) [Name]
missing
            [CaseAlt' t] -> m [CaseAlt' t]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe (CaseAlt' t) -> Maybe (CaseAlt' t))
-> [Maybe (CaseAlt' t)] -> [CaseAlt' t]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Maybe (CaseAlt' t) -> Maybe (CaseAlt' t)
forall a. a -> a
id [Maybe (CaseAlt' t)]
missing' [CaseAlt' t] -> [CaseAlt' t] -> [CaseAlt' t]
forall a. [a] -> [a] -> [a]
++ [CaseAlt' t]
rest)
    addCases [Name]
missing (CaseAlt' t
c : [CaseAlt' t]
rest)
       = ([CaseAlt' t] -> [CaseAlt' t]) -> m [CaseAlt' t] -> m [CaseAlt' t]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (CaseAlt' t
c CaseAlt' t -> [CaseAlt' t] -> [CaseAlt' t]
forall a. a -> [a] -> [a]
:) (m [CaseAlt' t] -> m [CaseAlt' t])
-> m [CaseAlt' t] -> m [CaseAlt' t]
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)
       = (Const -> CaseAlt' t) -> [Const] -> [CaseAlt' t]
forall a b. (a -> b) -> [a] -> [b]
map (SC' t -> Const -> CaseAlt' t
forall {t}. SC' t -> Const -> CaseAlt' t
genMissingConAlt SC' t
rhs) [Const]
missing [CaseAlt' t] -> [CaseAlt' t] -> [CaseAlt' t]
forall a. [a] -> [a] -> [a]
++ [CaseAlt' t]
rest
    addCons [Const]
missing (CaseAlt' t
c : [CaseAlt' t]
rest) = CaseAlt' t
c CaseAlt' t -> [CaseAlt' t] -> [CaseAlt' t]
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 <- m Int
forall s (m :: * -> *). MonadState s m => m s
get
                  Int -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
name Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
arity)
                  let args :: [Int]
args = (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int
name Int -> Int -> Int
forall a. Num a => a -> a -> a
+) [Int
0..Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
                  Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t)))
-> Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
forall a b. (a -> b) -> a -> b
$ CaseAlt' t -> Maybe (CaseAlt' t)
forall a. a -> Maybe a
Just (CaseAlt' t -> Maybe (CaseAlt' t))
-> CaseAlt' t -> Maybe (CaseAlt' t)
forall a b. (a -> b) -> a -> b
$ Name -> Int -> [Name] -> SC' t -> CaseAlt' t
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
tag ((Int -> Name) -> [Int] -> [Name]
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 = Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (CaseAlt' t)
forall a. Maybe a
Nothing

    genMissingConAlt :: SC' t -> Const -> CaseAlt' t
genMissingConAlt SC' t
rhs Const
n = Const -> SC' t -> CaseAlt' t
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) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
    collectCons CaseAlt' t
_ = Maybe Name
forall a. Maybe a
Nothing

    collectConsts :: CaseAlt' t -> Maybe Const
collectConsts (ConstCase Const
c SC' t
sc) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
    collectConsts CaseAlt' t
_ = Maybe Const
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 Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> Term
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]
_) -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
tyn
                           (Term, [Term])
_ -> Maybe Name
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    nextConst (BI Integer
c) = Integer -> Const
BI (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
    nextConst (Fl Double
c) = Double -> Const
Fl (Double
c Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
1)
    nextConst (B8 Word8
c) = Word8 -> Const
B8 (Word8
c Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1)
    nextConst (B16 Word16
c) = Word16 -> Const
B16 (Word16
c Word16 -> Word16 -> Word16
forall a. Num a => a -> a -> a
+ Word16
1)
    nextConst (B32 Word32
c) = Word32 -> Const
B32 (Word32
c Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
+ Word32
1)
    nextConst (B64 Word64
c) = Word64 -> Const
B64 (Word64
c Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
    nextConst (Ch Char
c) = Char -> Const
Ch (Int -> Char
chr (Int -> Char) -> Int -> Char
forall a b. (a -> b) -> a -> b
$ Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    nextConst (Str String
c) = String -> Const
Str (String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")
    nextConst Const
o = Const
o

addMissingConsSt IState
ist SC
sc = SC -> State Int SC
forall a. a -> StateT Int Identity a
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) <- Name -> [(Name, (Name, [Name]))] -> Maybe (Name, [Name])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
vn [(Name, (Name, [Name]))]
mustbes
            = CaseType -> Name -> [CaseAlt' Term] -> SC
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 <- Name -> [(Name, [Name])] -> Maybe [Name]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
vn [(Name, [Name])]
nots
            = let alts' :: [CaseAlt' Term]
alts' = (CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> [CaseAlt' Term]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Name] -> CaseAlt' Term -> Bool
forall {t :: * -> *} {t}.
Foldable t =>
t Name -> CaseAlt' t -> Bool
notConMatch [Name]
cantbe) [CaseAlt' Term]
alts in
                  CaseType -> Name -> [CaseAlt' Term] -> SC
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 = CaseType -> Name -> [CaseAlt' Term] -> SC
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)
        = Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
t [Name]
args ([(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim (Name
-> (Name, [Name])
-> [(Name, (Name, [Name]))]
-> [(Name, (Name, [Name]))]
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) CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term]
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)
        = Name -> [Name] -> SC -> CaseAlt' Term
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) CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term]
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)
        = Const -> SC -> CaseAlt' Term
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) CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term]
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)
        = Name -> SC -> CaseAlt' Term
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) CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term]
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)
        = SC -> CaseAlt' Term
forall t. SC' t -> CaseAlt' t
DefaultCase ([(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [(Name, (Name, [Name]))]
cs [(Name, [Name])]
nots SC
sc) CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term]
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
cn = [Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
c Int
t [Name]
args ([(Name, Name)] -> SC -> SC
substNames ([Name] -> [Name] -> [(Name, Name)]
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 Name -> t Name -> Bool
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) (a, b) -> [(a, b)] -> [(a, b)]
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = ((Name
n, [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub (Name
cn Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
cbs)) (Name, [Name]) -> [(Name, [Name])] -> [(Name, [Name])]
forall a. a -> [a] -> [a]
: [(Name, [Name])]
nots)
          | Bool
otherwise = ((Name
n, [Name]
cbs) (Name, [Name]) -> [(Name, [Name])] -> [(Name, [Name])]
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 (Term -> Term -> Bool
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 (TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
topx, TT a -> (TT a, [TT a])
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 a -> a -> Bool
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 (Term -> Term -> Bool
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 (TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
topx, TT a -> (TT a, [TT a])
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 a -> a -> Bool
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
          State [(Name, Term)] Bool -> [(Name, Term)] -> Bool
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
          State [(Name, Term)] Bool -> [(Name, Term)] -> Bool
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
   | Term -> Bool
forall {n}. TT n -> Bool
isCon Term
tm = do [(Name, Term)]
nmap <- StateT [(Name, Term)] Identity [(Name, Term)]
forall s (m :: * -> *). MonadState s m => m s
get
                   case Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, Term)]
nmap of
                        Maybe Term
Nothing -> do [(Name, Term)] -> StateT [(Name, Term)] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
x, Term
tm) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
nmap)
                                      Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
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]
_) <- TT 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
_)
   | Term -> Bool
forall {n}. TT n -> Bool
isCon Term
tm = do [(Name, Term)]
nmap <- StateT [(Name, Term)] Identity [(Name, Term)]
forall s (m :: * -> *). MonadState s m => m s
get
                   case Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
y [(Name, Term)]
nmap of
                        Maybe Term
Nothing -> do [(Name, Term)] -> StateT [(Name, Term)] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
y, Term
tm) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
nmap)
                                      Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
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]
_) <- TT 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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fa,
      (Term
f', [Term]
as') <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fa'
         = if ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Term] -> Int
forall a. [a] -> Int
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 Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
as) (Term
f Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
as')
                      Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Term -> Bool
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 [] [] = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
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
                                     Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
   | NameType -> NameType -> Bool
ntRec NameType
xt NameType
yt = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
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
_) = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (Constant Const
_) (P NameType
Ref Name
_ Term
_) = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (TType UExp
_) (TType UExp
_) = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec Term
_ Term
_ = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False