{-# LANGUAGE FlexibleContexts, PatternGuards #-}
module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
mkPatTm) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Elab.Utils
import Idris.Error
import Control.Monad.State.Strict
import Data.Char
import Data.List
import Data.Maybe
mkPatTm :: PTerm -> Idris Term
mkPatTm :: PTerm -> Idris Term
mkPatTm PTerm
t = do IState
i <- Idris IState
getIState
let timp :: PTerm
timp = Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
addImpl' Bool
True [] [] [] IState
i PTerm
t
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) Int
0
where
toTT :: Maybe Type -> PTerm -> StateT Int Idris Term
toTT :: Maybe Term -> PTerm -> StateT Int Idris Term
toTT Maybe Term
ty (PRef FC
_ [FC]
_ 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 NameType
nt Term
_) -> 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
Maybe Def
_ -> 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 Maybe Term
ty (PApp FC
_ t :: PTerm
t@(PRef FC
_ [FC]
_ Name
n) [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 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 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 Maybe Term
ty (PApp FC
_ PTerm
t [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 Maybe Term
ty (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
_ 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 Maybe Term
ty (PPair FC
_ [FC]
_ PunInfo
_ PTerm
l 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 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 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
[PTerm
a] -> Maybe Term -> PTerm -> StateT Int Idris Term
toTT (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
ty) PTerm
a
[PTerm]
_ -> 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 Maybe Term
Nothing (PAlternative [(Name, Name)]
_ PAltType
_ [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 Maybe Term
ty PTerm
_
= 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
+ Int
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 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
"_"
genClauses :: FC -> Name -> [([Name], Term)] ->
[PTerm] -> Idris [PTerm]
genClauses :: FC -> Name -> [([Name], Term)] -> [PTerm] -> Idris [PTerm]
genClauses FC
fc Name
n [([Name], Term)]
lhs_tms [] = [PTerm] -> Idris [PTerm]
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 (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 (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 (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
_ = []
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 (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' Bool
cov [Term]
args (UnmatchedCase String
_)
= 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' Bool
cov [Term]
args SC
ImpossibleCase = [[Term]] -> State [[Term]] [[Term]]
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 (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' Bool
cov [Term]
args SC
_ = [[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 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 (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 (m :: * -> *) a. Monad m => a -> m a
return []
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
| 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)
= 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@(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)
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)
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 (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)
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 [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 (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 (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
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 (m :: * -> *) a. Monad m => a -> m a
return SC
sc
trimOverlapping :: SC -> SC
trimOverlapping :: SC -> SC
trimOverlapping SC
sc = [(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [] [] SC
sc
where
trim :: [(Name, (Name, [Name]))] ->
[(Name, [Name])] ->
SC -> SC
trim :: [(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [(Name, (Name, [Name]))]
mustbes [(Name, [Name])]
nots (Case CaseType
t Name
vn [CaseAlt' Term]
alts)
| Just (Name
c, [Name]
args) <- 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)
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
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
recoverableCoverage Context
ctxt (At FC
_ Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage Context
ctxt (Elaborating String
_ Name
_ Maybe Term
_ Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage Context
ctxt (ElaboratingArg Name
_ Name
_ [(Name, Name)]
_ Err
e) = Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
e
recoverableCoverage Context
_ Err
_ = Bool
False
checkRec :: Term -> Term -> State [(Name, Term)] Bool
checkRec :: Term -> Term -> State [(Name, Term)] Bool
checkRec (P NameType
Bound Name
x Term
_) Term
tm
| 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 (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 (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 (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 (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 (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 (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 NameType
x NameType
y | NameType
Ref <- NameType
x = Bool
True
| NameType
Ref <- NameType
y = Bool
True
| NameType
Bound <- NameType
x = Bool
True
| NameType
Bound <- NameType
y = Bool
True
| Bool
otherwise = Bool
False
checkRec (P NameType
Ref Name
_ Term
_) (Constant Const
_) = Bool -> State [(Name, Term)] Bool
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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (TType UExp
_) (TType UExp
_) = Bool -> State [(Name, Term)] Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec Term
_ Term
_ = Bool -> State [(Name, Term)] Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False