{-# 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 t :: 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 Idris Term -> Int -> Idris Term
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
timp) 0
where
toTT :: Maybe Type -> PTerm -> StateT Int Idris Term
toTT :: Maybe Term -> PTerm -> StateT Int Idris Term
toTT ty :: Maybe Term
ty (PRef _ _ n :: Name
n)
= do IState
i <- Idris IState -> StateT Int Idris IState
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 nt :: NameType
nt _) -> Term -> StateT Int Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int Idris Term) -> Term -> StateT Int Idris 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
_ -> Term -> StateT Int Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int Idris Term) -> Term -> StateT Int Idris 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 ty :: Maybe Term
ty (PApp _ t :: PTerm
t@(PRef _ _ n :: Name
n) args :: [PArg]
args)
= do IState
i <- Idris IState -> StateT Int Idris IState
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 nty :: 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)
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 Idris Term)
-> [Maybe Term] -> [PTerm] -> StateT Int Idris [Term]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Maybe Term -> PTerm -> StateT Int Idris 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 Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
t
Term -> StateT Int Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int Idris Term) -> Term -> StateT Int Idris 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 ty :: Maybe Term
ty (PApp _ t :: PTerm
t args :: [PArg]
args)
= do Term
t' <- Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
t
[Term]
args' <- (PArg -> StateT Int Idris Term)
-> [PArg] -> StateT Int Idris [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing (PTerm -> StateT Int Idris Term)
-> (PArg -> PTerm) -> PArg -> StateT Int Idris Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PArg -> PTerm
forall t. PArg' t -> t
getTm) [PArg]
args
Term -> StateT Int Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int Idris Term) -> Term -> StateT Int Idris 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 ty :: Maybe Term
ty (PDPair _ _ _ l :: PTerm
l _ r :: PTerm
r)
= do Term
l' <- Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
l
Term
r' <- Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
r
Term -> StateT Int Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int Idris Term) -> Term -> StateT Int Idris 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 ty :: Maybe Term
ty (PPair _ _ _ l :: PTerm
l r :: PTerm
r)
= do Term
l' <- Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
l
Term
r' <- Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
r
Term -> StateT Int Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int Idris Term) -> Term -> StateT Int Idris 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']
toTT (Just ty :: Term
ty) (PAlternative _ _ as :: [PTerm]
as)
| (hd :: Term
hd, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ty
= do IState
i <- Idris IState -> StateT Int Idris IState
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
[a :: PTerm
a] -> Maybe Term -> PTerm -> StateT Int Idris Term
toTT (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
ty) PTerm
a
_ -> Idris Term -> StateT Int Idris Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Term -> StateT Int Idris Term)
-> Idris Term -> StateT Int Idris 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 Nothing (PAlternative _ _ as :: [PTerm]
as)
= Idris Term -> StateT Int Idris Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Term -> StateT Int Idris Term)
-> Idris Term -> StateT Int Idris 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 ty :: Maybe Term
ty _
= do Int
v <- StateT Int Idris Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Idris ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
Term -> StateT Int Idris Term
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 "imp") Term
forall n. TT n
Erased)
getAltName :: PTerm -> Name
getAltName (PApp _ (PRef _ _ (UN l :: Text
l)) [_, _, arg :: PArg
arg])
| Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Delay" = PTerm -> Name
getAltName (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
arg)
getAltName (PApp _ (PRef _ _ n :: Name
n) _) = Name
n
getAltName (PRef _ _ n :: Name
n) = Name
n
getAltName (PApp _ h :: PTerm
h _) = PTerm -> Name
getAltName PTerm
h
getAltName (PHidden h :: PTerm
h) = PTerm -> Name
getAltName PTerm
h
getAltName x :: PTerm
x = String -> Name
sUN "_"
genClauses :: FC -> Name -> [([Name], Term)] ->
[PTerm] -> Idris [PTerm]
genClauses :: FC -> Name -> [([Name], Term)] -> [PTerm] -> Idris [PTerm]
genClauses fc :: FC
fc n :: Name
n lhs_tms :: [([Name], Term)]
lhs_tms [] = [PTerm] -> Idris [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return []
genClauses fc :: FC
fc n :: Name
n lhs_tms :: [([Name], Term)]
lhs_tms given :: [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 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Building coverage tree for:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep "\n" ((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
given)
Int -> String -> Idris ()
logCoverage 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Building coverage tree for:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep "\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 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "From terms:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep "\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)
(cns :: [Name]
cns, ctree_in :: 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 "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 cns :: [Name]
cns ctree_in :: SC
ctree_in _) ->
([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
cns, SC
ctree_in)
Error e :: 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 (coveredas :: [Term]
coveredas, missingas :: [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 (\t :: 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 (\x :: 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 (\t :: Term
t -> IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
t Bool
True Bool
True) [Term]
missingas
Int -> String -> Idris ()
logCoverage 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
ctree
Int -> String -> Idris ()
logCoverage 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show ([PTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PTerm]
missing) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 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 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Missing clauses:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep "\n"
((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
missing)
Int -> String -> Idris ()
logCoverage 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Covered clauses:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep "\n"
((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
covered)
[PTerm] -> Idris [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
missing
where
flattenArgs :: PTerm -> PTerm
flattenArgs (PApp fc :: FC
fc (PApp _ f :: PTerm
f as :: [PArg]
as) 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 t :: PTerm
t = PTerm
t
getGivenPos :: PTerm -> [Int]
getGivenPos :: PTerm -> [Int]
getGivenPos (PApp _ _ pargs :: [PArg]
pargs) = Int -> [PTerm] -> [Int]
forall a. Num a => a -> [PTerm] -> [a]
getGiven 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 i :: a
i (Placeholder : tms :: [PTerm]
tms) = a -> [PTerm] -> [a]
getGiven (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) [PTerm]
tms
getGiven i :: a
i (_ : tms :: [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
+ 1) [PTerm]
tms
getGiven i :: a
i [] = []
getGivenPos _ = []
mergePos :: [[Int]] -> [Int]
mergePos :: [[Int]] -> [Int]
mergePos [] = []
mergePos [x :: [Int]
x] = [Int]
x
mergePos (x :: [Int]
x : xs :: [[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 (ns :: [Name]
ns, tm :: Term
tm) ptm :: 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 Erased Placeholder = TT n
forall n. TT n
Erased
rp tm :: TT n
tm Placeholder = TT n -> TT n
forall n. TT n -> TT n
Inferred TT n
tm
rp tm :: TT n
tm (PApp _ pf :: PTerm
pf pargs :: [PArg]
pargs)
| (tf :: TT n
tf, targs :: [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 tm :: TT n
tm (PPair _ _ _ pl :: PTerm
pl pr :: PTerm
pr)
| (tf :: TT n
tf, [tyl :: TT n
tyl, tyr :: TT n
tyr, tl :: TT n
tl, tr :: 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 tm :: TT n
tm (PDPair _ _ _ pl :: PTerm
pl pt :: PTerm
pt pr :: PTerm
pr)
| (tf :: TT n
tf, [tyl :: TT n
tyl, tyr :: TT n
tyr, tl :: TT n
tl, tr :: 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 tm :: TT n
tm _ = TT n
tm
mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses ctxt :: Context
ctxt fn :: Name
fn ns :: [Name]
ns sc :: 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 (\n :: 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 (\n :: 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 f :: Term
f args :: [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 t :: AppStatus Name
t f :: Term
f a :: Term
a)
| (f :: Term
f, args :: [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 _ n :: Name
n _) | Bool -> Bool
not (Name -> Context -> Bool
isConName Name
n Context
ctxt) = Term
forall n. TT n
Erased
erasePs tm :: Term
tm = Term
tm
mkFromSC :: Bool -> [Term] -> SC -> [[Term]]
mkFromSC cov :: Bool
cov args :: [Term]
args sc :: 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' cov :: Bool
cov args :: [Term]
args (STerm _)
= if Bool
cov then [[Term]] -> State [[Term]] [[Term]]
forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args] else [[Term]] -> State [[Term]] [[Term]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
mkFromSC' cov :: Bool
cov args :: [Term]
args (UnmatchedCase _)
= if Bool
cov then [[Term]] -> State [[Term]] [[Term]]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else [[Term]] -> State [[Term]] [[Term]]
forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args]
mkFromSC' cov :: Bool
cov args :: [Term]
args ImpossibleCase = [[Term]] -> State [[Term]] [[Term]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
mkFromSC' cov :: Bool
cov args :: [Term]
args (Case _ x :: Name
x alts :: [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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Term]]
done)
then [[Term]] -> State [[Term]] [[Term]]
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)
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 (m :: * -> *) a. Monad m => a -> m a
return ([[[Term]]] -> [[Term]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Term]]]
alts')
mkFromSC' cov :: Bool
cov args :: [Term]
args _ = [[Term]] -> State [[Term]] [[Term]]
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 cov :: Bool
cov args :: [Term]
args x :: Name
x (ConCase c :: Name
c t :: Int
t conargs :: [Name]
conargs sc :: 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 (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 (\n :: 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 cov :: Bool
cov args :: [Term]
args x :: Name
x (ConstCase c :: Const
c sc :: 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 cov :: Bool
cov args :: [Term]
args x :: Name
x (DefaultCase sc :: SC
sc)
= Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args SC
sc
mkFromAlt cov :: Bool
cov _ _ _ = [[Term]] -> State [[Term]] [[Term]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
addMissingCons :: IState -> SC -> SC
addMissingCons :: IState -> SC -> SC
addMissingCons ist :: IState
ist sc :: 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) 0
addMissingConsSt :: IState -> SC -> State Int SC
addMissingConsSt :: IState -> SC -> State Int SC
addMissingConsSt ist :: IState
ist (Case t :: CaseType
t n :: Name
n alts :: [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 n :: Name
n i :: Int
i ns :: [Name]
ns sc :: 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 n :: Name
n ns :: [Name]
ns sc :: 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 c :: Const
c sc :: 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 n :: Name
n sc :: 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)
= (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 argn :: p
argn as :: [CaseAlt' Term]
as
| cons :: [Name]
cons@(n :: Name
n:_) <- (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 tyn :: Name
tyn <- Name -> Maybe Name
getConType Name
n,
Just ti :: TypeInfo
ti <- Name -> Ctxt TypeInfo -> Maybe TypeInfo
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 [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)
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as'
| consts :: [Const]
consts@(n :: Const
n:_) <- (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)
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 n :: p
n as :: [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)
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as
addCases :: [Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases missing :: [Name]
missing [] = [CaseAlt' t] -> m [CaseAlt' t]
forall (m :: * -> *) a. Monad m => a -> m a
return []
addCases missing :: [Name]
missing (DefaultCase rhs :: SC' t
rhs : rest :: [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)
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 (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 missing :: [Name]
missing (c :: CaseAlt' t
c : rest :: [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 missing :: [Const]
missing [] = []
addCons missing :: [Const]
missing (DefaultCase rhs :: SC' t
rhs : rest :: [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 missing :: [Const]
missing (c :: CaseAlt' t
c : rest :: [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 rhs :: SC' t
rhs n :: Name
n
| Just (TyDecl (DCon tag :: Int
tag arity :: Int
arity _) ty :: 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
+) [0..Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]
Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
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 (\i :: Int
i -> Int -> String -> Name
sMN Int
i "m") [Int]
args) SC' t
rhs
| Bool
otherwise = Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (CaseAlt' t)
forall a. Maybe a
Nothing
genMissingConAlt :: SC' t -> Const -> CaseAlt' t
genMissingConAlt rhs :: SC' t
rhs n :: 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 n :: Name
n i :: Int
i args :: [Name]
args sc :: SC' t
sc) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
collectCons _ = Maybe Name
forall a. Maybe a
Nothing
collectConsts :: CaseAlt' t -> Maybe Const
collectConsts (ConstCase c :: Const
c sc :: SC' t
sc) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
collectConsts _ = Maybe Const
forall a. Maybe a
Nothing
getConType :: Name -> Maybe Name
getConType n :: 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 _ tyn :: Name
tyn _, _) -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
tyn
_ -> Maybe Name
forall a. Maybe a
Nothing
nextConst :: Const -> Const
nextConst (I c :: Int
c) = Int -> Const
I (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
nextConst (BI c :: Integer
c) = Integer -> Const
BI (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)
nextConst (Fl c :: Double
c) = Double -> Const
Fl (Double
c Double -> Double -> Double
forall a. Num a => a -> a -> a
+ 1)
nextConst (B8 c :: Word8
c) = Word8 -> Const
B8 (Word8
c Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ 1)
nextConst (B16 c :: Word16
c) = Word16 -> Const
B16 (Word16
c Word16 -> Word16 -> Word16
forall a. Num a => a -> a -> a
+ 1)
nextConst (B32 c :: Word32
c) = Word32 -> Const
B32 (Word32
c Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
+ 1)
nextConst (B64 c :: Word64
c) = Word64 -> Const
B64 (Word64
c Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ 1)
nextConst (Ch c :: 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
+ 1)
nextConst (Str c :: String
c) = String -> Const
Str (String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'")
nextConst o :: Const
o = Const
o
addMissingConsSt ist :: IState
ist sc :: SC
sc = SC -> State Int SC
forall (m :: * -> *) a. Monad m => a -> m a
return SC
sc
trimOverlapping :: SC -> SC
trimOverlapping :: SC -> SC
trimOverlapping sc :: 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 mustbes :: [(Name, (Name, [Name]))]
mustbes nots :: [(Name, [Name])]
nots (Case t :: CaseType
t vn :: Name
vn alts :: [CaseAlt' Term]
alts)
| Just (c :: Name
c, args :: [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 cantbe :: [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 cs :: [(Name, (Name, [Name]))]
cs nots :: [(Name, [Name])]
nots sc :: SC
sc = SC
sc
trimAlts :: [(Name, (Name, [Name]))]
-> [(Name, [Name])] -> Name -> [CaseAlt' Term] -> [CaseAlt' Term]
trimAlts cs :: [(Name, (Name, [Name]))]
cs nots :: [(Name, [Name])]
nots vn :: Name
vn [] = []
trimAlts cs :: [(Name, (Name, [Name]))]
cs nots :: [(Name, [Name])]
nots vn :: Name
vn (ConCase cn :: Name
cn t :: Int
t args :: [Name]
args sc :: SC
sc : rest :: [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 cs :: [(Name, (Name, [Name]))]
cs nots :: [(Name, [Name])]
nots vn :: Name
vn (FnCase n :: Name
n ns :: [Name]
ns sc :: SC
sc : rest :: [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 cs :: [(Name, (Name, [Name]))]
cs nots :: [(Name, [Name])]
nots vn :: Name
vn (ConstCase c :: Const
c sc :: SC
sc : rest :: [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 cs :: [(Name, (Name, [Name]))]
cs nots :: [(Name, [Name])]
nots vn :: Name
vn (SucCase n :: Name
n sc :: SC
sc : rest :: [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 cs :: [(Name, (Name, [Name]))]
cs nots :: [(Name, [Name])]
nots vn :: Name
vn (DefaultCase sc :: SC
sc : rest :: [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 ca :: (Name, [Name])
ca [] = []
substMatch (c :: Name
c,args :: [Name]
args) (ConCase cn :: Name
cn t :: Int
t args' :: [Name]
args' sc :: SC
sc : _)
| 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 ca :: (Name, [Name])
ca (_:cs :: [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
sc
substNames ((n :: Name
n, n' :: Name
n') : ns :: [(Name, Name)]
ns) sc :: 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 cs :: t Name
cs (ConCase cn :: Name
cn t :: Int
t args :: [Name]
args sc :: 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 cs :: t Name
cs _ = Bool
True
addMatch :: a -> b -> [(a, b)] -> [(a, b)]
addMatch vn :: a
vn cn :: b
cn cs :: [(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 vn :: Name
vn cn :: Name
cn [] = [(Name
vn, [Name
cn])]
addCantBe vn :: Name
vn cn :: Name
cn ((n :: Name
n, cbs :: [Name]
cbs) : nots :: [(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)
validCoverageCase :: Context -> Err -> Bool
validCoverageCase :: Context -> Err -> Bool
validCoverageCase ctxt :: Context
ctxt (CantUnify _ (topx :: Term
topx, _) (topy :: Term
topy, _) e :: Err
e _ _)
= 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 topx :: TT a
topx topy :: 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 _ x :: a
x _, _), (P _ y :: a
y _, _)) -> a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
_ -> Bool
False
validCoverageCase ctxt :: Context
ctxt (InfiniteUnify _ _ _) = Bool
False
validCoverageCase ctxt :: Context
ctxt (CantConvert topx :: Term
topx topy :: Term
topy _)
= 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 topx :: TT a
topx topy :: 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 _ x :: a
x _, _), (P _ y :: a
y _, _)) -> a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
_ -> Bool
False
validCoverageCase ctxt :: Context
ctxt (At _ e :: Err
e) = Context -> Err -> Bool
validCoverageCase Context
ctxt Err
e
validCoverageCase ctxt :: Context
ctxt (Elaborating _ _ _ e :: Err
e) = Context -> Err -> Bool
validCoverageCase Context
ctxt Err
e
validCoverageCase ctxt :: Context
ctxt (ElaboratingArg _ _ _ e :: Err
e) = Context -> Err -> Bool
validCoverageCase Context
ctxt Err
e
validCoverageCase ctxt :: Context
ctxt _ = Bool
True
recoverableCoverage :: Context -> Err -> Bool
recoverableCoverage :: Context -> Err -> Bool
recoverableCoverage ctxt :: Context
ctxt (CantUnify r :: Bool
r (topx :: Term
topx, _) (topy :: Term
topy, _) e :: Err
e _ _)
= 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 ctxt :: Context
ctxt (CantConvert topx :: Term
topx topy :: Term
topy _)
= 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 ctxt :: Context
ctxt (InfiniteUnify _ _ _) = Bool
False
recoverableCoverage ctxt :: Context
ctxt (At _ e :: Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage ctxt :: Context
ctxt (Elaborating _ _ _ e :: Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage ctxt :: Context
ctxt (ElaboratingArg _ _ _ e :: Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage _ _ = Bool
False
checkRec :: Term -> Term -> State [(Name, Term)] Bool
checkRec :: Term -> Term -> State [(Name, Term)] Bool
checkRec (P Bound x :: Name
x _) tm :: 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
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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just y' :: Term
y' -> Term -> Term -> State [(Name, Term)] Bool
checkRec Term
tm Term
y'
where
isCon :: TT n -> Bool
isCon tm :: TT n
tm
| (P yt :: NameType
yt _ _, _) <- 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 _) = Bool
True
isCon _ = Bool
False
conType :: NameType -> Bool
conType (DCon _ _ _) = Bool
True
conType (TCon _ _) = Bool
True
conType _ = Bool
False
checkRec tm :: Term
tm (P Bound y :: Name
y _)
| 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
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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just x' :: Term
x' -> Term -> Term -> State [(Name, Term)] Bool
checkRec Term
tm Term
x'
where
isCon :: TT n -> Bool
isCon tm :: TT n
tm
| (P yt :: NameType
yt _ _, _) <- 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 _) = Bool
True
isCon _ = Bool
False
conType :: NameType -> Bool
conType (DCon _ _ _) = Bool
True
conType (TCon _ _) = Bool
True
conType _ = Bool
False
checkRec (App _ f :: Term
f a :: Term
a) p :: Term
p@(P _ _ _) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
p
checkRec (App _ f :: Term
f a :: Term
a) p :: Term
p@(Constant _) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
p
checkRec p :: Term
p@(P _ _ _) (App _ f :: Term
f a :: Term
a) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
p Term
f
checkRec p :: Term
p@(Constant _) (App _ f :: Term
f a :: Term
a) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
p Term
f
checkRec fa :: Term
fa@(App _ _ _) fa' :: Term
fa'@(App _ _ _)
| (f :: Term
f, as :: [Term]
as) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fa,
(f' :: Term
f', as' :: [Term]
as') <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fa'
= if ([Term] -> 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 (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 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 (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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRecs (a :: Term
a : as :: [Term]
as) (b :: Term
b : bs :: [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 (m :: * -> *) a. Monad m => a -> m a
return (Bool
aok Bool -> Bool -> Bool
&& Bool
asok)
conType :: TT n -> Bool
conType (P (DCon _ _ _) _ _) = Bool
True
conType (P (TCon _ _) _ _) = Bool
True
conType (Constant _) = Bool
True
conType _ = Bool
False
checkRec (P xt :: NameType
xt x :: Name
x _) (P yt :: NameType
yt y :: Name
y _)
| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = Bool -> State [(Name, Term)] Bool
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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
where
ntRec :: NameType -> NameType -> Bool
ntRec x :: NameType
x y :: 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 Ref _ _) (Constant _) = Bool -> State [(Name, Term)] Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (Constant _) (P Ref _ _) = Bool -> State [(Name, Term)] Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (TType _) (TType _) = Bool -> State [(Name, Term)] Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec _ _ = Bool -> State [(Name, Term)] Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False