{-# LANGUAGE FlexibleContexts, PatternGuards #-}
module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
mkPatTm) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Elab.Utils
import Idris.Error
import Control.Monad
import Control.Monad.State.Strict
import Data.Char
import Data.List
import Data.Maybe
mkPatTm :: PTerm -> Idris Term
mkPatTm :: PTerm -> Idris Term
mkPatTm PTerm
t = do IState
i <- Idris IState
getIState
let timp :: PTerm
timp = Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
addImpl' Bool
True [] [] [] IState
i PTerm
t
StateT Int (StateT IState (ExceptT Err IO)) Term
-> Int -> Idris Term
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
timp) Int
0
where
toTT :: Maybe Type -> PTerm -> StateT Int Idris Term
toTT :: Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
ty (PRef FC
_ [FC]
_ Name
n)
= do IState
i <- Idris IState -> StateT Int (StateT IState (ExceptT Err IO)) IState
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
i) of
Just (TyDecl NameType
nt Term
_) -> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n Term
forall n. TT n
Erased
Maybe Def
_ -> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased
toTT Maybe Term
ty (PApp FC
_ t :: PTerm
t@(PRef FC
_ [FC]
_ Name
n) [PArg]
args)
= do IState
i <- Idris IState -> StateT Int (StateT IState (ExceptT Err IO)) IState
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
let aTys :: [Maybe Term]
aTys = case Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
i) of
Just Term
nty -> ((Name, Term) -> Maybe Term) -> [(Name, Term)] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term)
-> ((Name, Term) -> Term) -> (Name, Term) -> Maybe Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Term) -> Term
forall a b. (a, b) -> b
snd) (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
nty)
Maybe Term
Nothing -> (PArg -> Maybe Term) -> [PArg] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Term -> PArg -> Maybe Term
forall a b. a -> b -> a
const Maybe Term
forall a. Maybe a
Nothing) [PArg]
args
[Term]
args' <- (Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> [Maybe Term]
-> [PTerm]
-> StateT Int (StateT IState (ExceptT Err IO)) [Term]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT [Maybe Term]
aTys ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
args)
Term
t' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
t
Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
t' [Term]
args'
toTT Maybe Term
ty (PApp FC
_ PTerm
t [PArg]
args)
= do Term
t' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
t
[Term]
args' <- (PArg -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> [PArg] -> StateT Int (StateT IState (ExceptT Err IO)) [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing (PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> (PArg -> PTerm)
-> PArg
-> StateT Int (StateT IState (ExceptT Err IO)) Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PArg -> PTerm
forall t. PArg' t -> t
getTm) [PArg]
args
Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
t' [Term]
args'
toTT Maybe Term
ty (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
_ PTerm
r)
= do Term
l' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
l
Term
r' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
r
Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
sigmaCon Term
forall n. TT n
Erased) [Term
forall n. TT n
Erased, Term
forall n. TT n
Erased, Term
l', Term
r']
toTT Maybe Term
ty (PPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
r)
= do Term
l' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
l
Term
r' <- Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT Maybe Term
forall a. Maybe a
Nothing PTerm
r
Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
pairCon Term
forall n. TT n
Erased) [Term
forall n. TT n
Erased, Term
forall n. TT n
Erased, Term
l', Term
r']
toTT (Just Term
ty) (PAlternative [(Name, Name)]
_ PAltType
_ [PTerm]
as)
| (Term
hd, [Term]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ty
= do IState
i <- Idris IState -> StateT Int (StateT IState (ExceptT Err IO)) IState
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
case Bool -> Env -> Term -> Term -> IState -> [PTerm] -> [PTerm]
pruneByType Bool
True [] Term
hd Term
ty IState
i [PTerm]
as of
[PTerm
a] -> Maybe Term
-> PTerm -> StateT Int (StateT IState (ExceptT Err IO)) Term
toTT (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
ty) PTerm
a
[PTerm]
_ -> Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Err -> Idris Term
forall a. Err -> Idris a
ierror (Err -> Idris Term) -> Err -> Idris Term
forall a b. (a -> b) -> a -> b
$ [Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts ((PTerm -> Name) -> [PTerm] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Name
getAltName [PTerm]
as)
toTT Maybe Term
Nothing (PAlternative [(Name, Name)]
_ PAltType
_ [PTerm]
as)
= Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall (m :: * -> *) a. Monad m => m a -> StateT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term)
-> Idris Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a b. (a -> b) -> a -> b
$ Err -> Idris Term
forall a. Err -> Idris a
ierror (Err -> Idris Term) -> Err -> Idris Term
forall a b. (a -> b) -> a -> b
$ [Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts ((PTerm -> Name) -> [PTerm] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Name
getAltName [PTerm]
as)
toTT Maybe Term
ty PTerm
_
= do Int
v <- StateT Int (StateT IState (ExceptT Err IO)) Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int (StateT IState (ExceptT Err IO)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
Term -> StateT Int (StateT IState (ExceptT Err IO)) Term
forall a. a -> StateT Int (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound (Int -> String -> Name
sMN Int
v String
"imp") Term
forall n. TT n
Erased)
getAltName :: PTerm -> Name
getAltName (PApp FC
_ (PRef FC
_ [FC]
_ (UN Text
l)) [PArg
_, PArg
_, PArg
arg])
| Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" = PTerm -> Name
getAltName (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
arg)
getAltName (PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg]
_) = Name
n
getAltName (PRef FC
_ [FC]
_ Name
n) = Name
n
getAltName (PApp FC
_ PTerm
h [PArg]
_) = PTerm -> Name
getAltName PTerm
h
getAltName (PHidden PTerm
h) = PTerm -> Name
getAltName PTerm
h
getAltName PTerm
x = String -> Name
sUN String
"_"
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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
genClauses FC
fc Name
n [([Name], Term)]
lhs_tms [PTerm]
given
= do IState
i <- Idris IState
getIState
let lhs_given :: [([Name], Term, Term)]
lhs_given = (([Name], Term) -> PTerm -> ([Name], Term, Term))
-> [([Name], Term)] -> [PTerm] -> [([Name], Term, Term)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders [([Name], Term)]
lhs_tms
((PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> PTerm -> PTerm
stripUnmatchable IState
i) ((PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PTerm
flattenArgs [PTerm]
given))
Int -> String -> Idris ()
logCoverage Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Building coverage tree for:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" ((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
given)
Int -> String -> Idris ()
logCoverage Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Building coverage tree for:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" ((([Name], Term, Term) -> String)
-> [([Name], Term, Term)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ([Name], Term, Term) -> String
forall a. Show a => a -> String
show [([Name], Term, Term)]
lhs_given)
Int -> String -> Idris ()
logCoverage Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"From terms:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" ((([Name], Term) -> String) -> [([Name], Term)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ([Name], Term) -> String
forall a. Show a => a -> String
show [([Name], Term)]
lhs_tms)
let givenpos :: [Int]
givenpos = [[Int]] -> [Int]
mergePos ((PTerm -> [Int]) -> [PTerm] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> [Int]
getGivenPos [PTerm]
given)
([Name]
cns, SC
ctree_in) <-
case Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
False (String -> SC
forall t. String -> SC' t
UnmatchedCase String
"Undefined") Bool
False
([Int] -> Phase
CoverageCheck [Int]
givenpos) FC
emptyFC [] []
[([Name], Term, Term)]
lhs_given
([Int] -> ErasureInfo
forall a b. a -> b -> a
const []) of
OK (CaseDef [Name]
cns SC
ctree_in [Term]
_) ->
([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
cns, SC
ctree_in)
Error Err
e -> TC ([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC)
forall a. TC a -> Idris a
tclift (TC ([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC))
-> TC ([Name], SC) -> StateT IState (ExceptT Err IO) ([Name], SC)
forall a b. (a -> b) -> a -> b
$ Err -> TC ([Name], SC)
forall a. Err -> TC a
tfail (Err -> TC ([Name], SC)) -> Err -> TC ([Name], SC)
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc Err
e
let ctree :: SC
ctree = SC -> SC
trimOverlapping (IState -> SC -> SC
addMissingCons IState
i SC
ctree_in)
let ([Term]
coveredas, [Term]
missingas) = Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses (IState -> Context
tt_ctxt IState
i) Name
n [Name]
cns SC
ctree
let covered :: [PTerm]
covered = (Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (\Term
t -> IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
t Bool
True Bool
True) [Term]
coveredas
let missing :: [PTerm]
missing = (PTerm -> Bool) -> [PTerm] -> [PTerm]
forall a. (a -> Bool) -> [a] -> [a]
filter (\PTerm
x -> PTerm
x PTerm -> [PTerm] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [PTerm]
covered) ([PTerm] -> [PTerm]) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> a -> b
$
(Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (\Term
t -> IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
t Bool
True Bool
True) [Term]
missingas
Int -> String -> Idris ()
logCoverage Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Coverage from case tree for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
ctree
Int -> String -> Idris ()
logCoverage Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show ([PTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PTerm]
missing) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" missing clauses for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
Int -> String -> Idris ()
logCoverage Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Missing clauses:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
missing)
Int -> String -> Idris ()
logCoverage Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Covered clauses:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
covered)
[PTerm] -> Idris [PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
missing
where
flattenArgs :: PTerm -> PTerm
flattenArgs (PApp FC
fc (PApp FC
_ PTerm
f [PArg]
as) [PArg]
as')
= PTerm -> PTerm
flattenArgs (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f ([PArg]
as [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ [PArg]
as'))
flattenArgs PTerm
t = PTerm
t
getGivenPos :: PTerm -> [Int]
getGivenPos :: PTerm -> [Int]
getGivenPos (PApp FC
_ PTerm
_ [PArg]
pargs) = Int -> [PTerm] -> [Int]
forall {a}. Num a => a -> [PTerm] -> [a]
getGiven Int
0 ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
pargs)
where
getGiven :: a -> [PTerm] -> [a]
getGiven a
i (PTerm
Placeholder : [PTerm]
tms) = a -> [PTerm] -> [a]
getGiven (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) [PTerm]
tms
getGiven a
i (PTerm
_ : [PTerm]
tms) = a
i a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a -> [PTerm] -> [a]
getGiven (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) [PTerm]
tms
getGiven a
i [] = []
getGivenPos PTerm
_ = []
mergePos :: [[Int]] -> [Int]
mergePos :: [[Int]] -> [Int]
mergePos [] = []
mergePos [[Int]
x] = [Int]
x
mergePos ([Int]
x : [[Int]]
xs) = [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Int]
x ([[Int]] -> [Int]
mergePos [[Int]]
xs)
removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
removePlaceholders ([Name]
ns, Term
tm) PTerm
ptm = ([Name]
ns, Term -> PTerm -> Term
forall {n}. TT n -> PTerm -> TT n
rp Term
tm PTerm
ptm, Term
forall n. TT n
Erased)
where
rp :: TT n -> PTerm -> TT n
rp TT n
Erased PTerm
Placeholder = TT n
forall n. TT n
Erased
rp TT n
tm PTerm
Placeholder = TT n -> TT n
forall n. TT n -> TT n
Inferred TT n
tm
rp TT n
tm (PApp FC
_ PTerm
pf [PArg]
pargs)
| (TT n
tf, [TT n]
targs) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm
= let tf' :: TT n
tf' = TT n -> PTerm -> TT n
rp TT n
tf PTerm
pf
targs' :: [TT n]
targs' = (TT n -> PTerm -> TT n) -> [TT n] -> [PTerm] -> [TT n]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TT n -> PTerm -> TT n
rp [TT n]
targs ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
pargs) in
TT n -> [TT n] -> TT n
forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf' [TT n]
targs'
rp TT n
tm (PPair FC
_ [FC]
_ PunInfo
_ PTerm
pl PTerm
pr)
| (TT n
tf, [TT n
tyl, TT n
tyr, TT n
tl, TT n
tr]) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm
= let tl' :: TT n
tl' = TT n -> PTerm -> TT n
rp TT n
tl PTerm
pl
tr' :: TT n
tr' = TT n -> PTerm -> TT n
rp TT n
tr PTerm
pr in
TT n -> [TT n] -> TT n
forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf [TT n
forall n. TT n
Erased, TT n
forall n. TT n
Erased, TT n
tl', TT n
tr']
rp TT n
tm (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
pl PTerm
pt PTerm
pr)
| (TT n
tf, [TT n
tyl, TT n
tyr, TT n
tl, TT n
tr]) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm
= let tl' :: TT n
tl' = TT n -> PTerm -> TT n
rp TT n
tl PTerm
pl
tr' :: TT n
tr' = TT n -> PTerm -> TT n
rp TT n
tr PTerm
pr in
TT n -> [TT n] -> TT n
forall n. TT n -> [TT n] -> TT n
mkApp TT n
tf [TT n
forall n. TT n
Erased, TT n
forall n. TT n
Erased, TT n
tl', TT n
tr']
rp TT n
tm PTerm
_ = TT n
tm
mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
mkNewClauses Context
ctxt Name
fn [Name]
ns SC
sc
= (([Term] -> Term) -> [[Term]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> [Term] -> Term
mkPlApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
fn Term
forall n. TT n
Erased)) ([[Term]] -> [Term]) -> [[Term]] -> [Term]
forall a b. (a -> b) -> a -> b
$
Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
True ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
ns) SC
sc,
([Term] -> Term) -> [[Term]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> [Term] -> Term
mkPlApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
fn Term
forall n. TT n
Erased)) ([[Term]] -> [Term]) -> [[Term]] -> [Term]
forall a b. (a -> b) -> a -> b
$
Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
False ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
ns) SC
sc)
where
mkPlApp :: Term -> [Term] -> Term
mkPlApp Term
f [Term]
args = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
f ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
erasePs [Term]
args)
erasePs :: Term -> Term
erasePs ap :: Term
ap@(App AppStatus Name
t Term
f Term
a)
| (Term
f, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
f ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
erasePs [Term]
args)
erasePs (P NameType
_ Name
n Term
_) | Bool -> Bool
not (Name -> Context -> Bool
isConName Name
n Context
ctxt) = Term
forall n. TT n
Erased
erasePs Term
tm = Term
tm
mkFromSC :: Bool -> [Term] -> SC -> [[Term]]
mkFromSC Bool
cov [Term]
args SC
sc = State [[Term]] [[Term]] -> [[Term]] -> [[Term]]
forall s a. State s a -> s -> a
evalState (Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args SC
sc) []
mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args (STerm Term
_)
= if Bool
cov then [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args] else [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mkFromSC' Bool
cov [Term]
args (UnmatchedCase String
_)
= if Bool
cov then [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Term]
args]
mkFromSC' Bool
cov [Term]
args SC
ImpossibleCase = [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mkFromSC' Bool
cov [Term]
args (Case CaseType
_ Name
x [CaseAlt' Term]
alts)
= do [[Term]]
done <- State [[Term]] [[Term]]
forall s (m :: * -> *). MonadState s m => m s
get
if ([Term]
args [Term] -> [[Term]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Term]]
done)
then [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
else do [[[Term]]]
alts' <- (CaseAlt' Term -> State [[Term]] [[Term]])
-> [CaseAlt' Term] -> StateT [[Term]] Identity [[[Term]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> [Term] -> Name -> CaseAlt' Term -> State [[Term]] [[Term]]
mkFromAlt Bool
cov [Term]
args Name
x) [CaseAlt' Term]
alts
[[Term]] -> StateT [[Term]] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
args [Term] -> [[Term]] -> [[Term]]
forall a. a -> [a] -> [a]
: [[Term]]
done)
[[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[[Term]]] -> [[Term]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Term]]]
alts')
mkFromSC' Bool
cov [Term]
args SC
_ = [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> State [[Term]] [[Term]]
mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt' Term -> State [[Term]] [[Term]]
mkFromAlt Bool
cov [Term]
args Name
x (ConCase Name
c Int
t [Name]
conargs SC
sc)
= let argrep :: Term
argrep = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> Bool -> NameType
DCon Int
t ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Bool
False) Name
c Term
forall n. TT n
Erased)
((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
conargs)
args' :: [Term]
args' = (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
x Term
argrep) [Term]
args in
Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args' SC
sc
mkFromAlt Bool
cov [Term]
args Name
x (ConstCase Const
c SC
sc)
= let argrep :: TT n
argrep = Const -> TT n
forall n. Const -> TT n
Constant Const
c
args' :: [Term]
args' = (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
x Term
forall n. TT n
argrep) [Term]
args in
Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args' SC
sc
mkFromAlt Bool
cov [Term]
args Name
x (DefaultCase SC
sc)
= Bool -> [Term] -> SC -> State [[Term]] [[Term]]
mkFromSC' Bool
cov [Term]
args SC
sc
mkFromAlt Bool
cov [Term]
_ Name
_ CaseAlt' Term
_ = [[Term]] -> State [[Term]] [[Term]]
forall a. a -> StateT [[Term]] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as'
| consts :: [Const]
consts@(Const
n:[Const]
_) <- (CaseAlt' Term -> Maybe Const) -> [CaseAlt' Term] -> [Const]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe CaseAlt' Term -> Maybe Const
forall {t}. CaseAlt' t -> Maybe Const
collectConsts [CaseAlt' Term]
as
= let missing :: [Const]
missing = [Const] -> [Const]
forall a. Eq a => [a] -> [a]
nub ((Const -> Const) -> [Const] -> [Const]
forall a b. (a -> b) -> [a] -> [b]
map Const -> Const
nextConst [Const]
consts) [Const] -> [Const] -> [Const]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Const]
consts in
(CaseAlt' Term -> State Int (CaseAlt' Term))
-> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt ([Const] -> [CaseAlt' Term] -> [CaseAlt' Term]
forall {t}. [Const] -> [CaseAlt' t] -> [CaseAlt' t]
addCons [Const]
missing [CaseAlt' Term]
as)
addMissingAlts p
n [CaseAlt' Term]
as = (CaseAlt' Term -> State Int (CaseAlt' Term))
-> [CaseAlt' Term] -> StateT Int Identity [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> State Int (CaseAlt' Term)
addMissingAlt [CaseAlt' Term]
as
addCases :: [Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases [Name]
missing [] = [CaseAlt' t] -> m [CaseAlt' t]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
addCases [Name]
missing (DefaultCase SC' t
rhs : [CaseAlt' t]
rest)
= do [Maybe (CaseAlt' t)]
missing' <- (Name -> m (Maybe (CaseAlt' t)))
-> [Name] -> m [Maybe (CaseAlt' t)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (SC' t -> Name -> m (Maybe (CaseAlt' t))
forall {m :: * -> *} {t}.
MonadState Int m =>
SC' t -> Name -> m (Maybe (CaseAlt' t))
genMissingAlt SC' t
rhs) [Name]
missing
[CaseAlt' t] -> m [CaseAlt' t]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe (CaseAlt' t) -> Maybe (CaseAlt' t))
-> [Maybe (CaseAlt' t)] -> [CaseAlt' t]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Maybe (CaseAlt' t) -> Maybe (CaseAlt' t)
forall a. a -> a
id [Maybe (CaseAlt' t)]
missing' [CaseAlt' t] -> [CaseAlt' t] -> [CaseAlt' t]
forall a. [a] -> [a] -> [a]
++ [CaseAlt' t]
rest)
addCases [Name]
missing (CaseAlt' t
c : [CaseAlt' t]
rest)
= ([CaseAlt' t] -> [CaseAlt' t]) -> m [CaseAlt' t] -> m [CaseAlt' t]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (CaseAlt' t
c CaseAlt' t -> [CaseAlt' t] -> [CaseAlt' t]
forall a. a -> [a] -> [a]
:) (m [CaseAlt' t] -> m [CaseAlt' t])
-> m [CaseAlt' t] -> m [CaseAlt' t]
forall a b. (a -> b) -> a -> b
$ [Name] -> [CaseAlt' t] -> m [CaseAlt' t]
addCases [Name]
missing [CaseAlt' t]
rest
addCons :: [Const] -> [CaseAlt' t] -> [CaseAlt' t]
addCons [Const]
missing [] = []
addCons [Const]
missing (DefaultCase SC' t
rhs : [CaseAlt' t]
rest)
= (Const -> CaseAlt' t) -> [Const] -> [CaseAlt' t]
forall a b. (a -> b) -> [a] -> [b]
map (SC' t -> Const -> CaseAlt' t
forall {t}. SC' t -> Const -> CaseAlt' t
genMissingConAlt SC' t
rhs) [Const]
missing [CaseAlt' t] -> [CaseAlt' t] -> [CaseAlt' t]
forall a. [a] -> [a] -> [a]
++ [CaseAlt' t]
rest
addCons [Const]
missing (CaseAlt' t
c : [CaseAlt' t]
rest) = CaseAlt' t
c CaseAlt' t -> [CaseAlt' t] -> [CaseAlt' t]
forall a. a -> [a] -> [a]
: [Const] -> [CaseAlt' t] -> [CaseAlt' t]
addCons [Const]
missing [CaseAlt' t]
rest
genMissingAlt :: SC' t -> Name -> m (Maybe (CaseAlt' t))
genMissingAlt SC' t
rhs Name
n
| Just (TyDecl (DCon Int
tag Int
arity Bool
_) Term
ty) <- Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
ist)
= do Int
name <- m Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
name Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
arity)
let args :: [Int]
args = (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int
name Int -> Int -> Int
forall a. Num a => a -> a -> a
+) [Int
0..Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t)))
-> Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
forall a b. (a -> b) -> a -> b
$ CaseAlt' t -> Maybe (CaseAlt' t)
forall a. a -> Maybe a
Just (CaseAlt' t -> Maybe (CaseAlt' t))
-> CaseAlt' t -> Maybe (CaseAlt' t)
forall a b. (a -> b) -> a -> b
$ Name -> Int -> [Name] -> SC' t -> CaseAlt' t
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
tag ((Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Int -> String -> Name
sMN Int
i String
"m") [Int]
args) SC' t
rhs
| Bool
otherwise = Maybe (CaseAlt' t) -> m (Maybe (CaseAlt' t))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (CaseAlt' t)
forall a. Maybe a
Nothing
genMissingConAlt :: SC' t -> Const -> CaseAlt' t
genMissingConAlt SC' t
rhs Const
n = Const -> SC' t -> CaseAlt' t
forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
n SC' t
rhs
collectCons :: CaseAlt' t -> Maybe Name
collectCons (ConCase Name
n Int
i [Name]
args SC' t
sc) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
collectCons CaseAlt' t
_ = Maybe Name
forall a. Maybe a
Nothing
collectConsts :: CaseAlt' t -> Maybe Const
collectConsts (ConstCase Const
c SC' t
sc) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
collectConsts CaseAlt' t
_ = Maybe Const
forall a. Maybe a
Nothing
getConType :: Name -> Maybe Name
getConType Name
n = do Term
ty <- Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist)
case Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> Term
forall n. TT n -> TT n
getRetTy (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
ty)) of
(P NameType
_ Name
tyn Term
_, [Term]
_) -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
tyn
(Term, [Term])
_ -> Maybe Name
forall a. Maybe a
Nothing
nextConst :: Const -> Const
nextConst (I Int
c) = Int -> Const
I (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
nextConst (BI Integer
c) = Integer -> Const
BI (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
nextConst (Fl Double
c) = Double -> Const
Fl (Double
c Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
1)
nextConst (B8 Word8
c) = Word8 -> Const
B8 (Word8
c Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1)
nextConst (B16 Word16
c) = Word16 -> Const
B16 (Word16
c Word16 -> Word16 -> Word16
forall a. Num a => a -> a -> a
+ Word16
1)
nextConst (B32 Word32
c) = Word32 -> Const
B32 (Word32
c Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
+ Word32
1)
nextConst (B64 Word64
c) = Word64 -> Const
B64 (Word64
c Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
nextConst (Ch Char
c) = Char -> Const
Ch (Int -> Char
chr (Int -> Char) -> Int -> Char
forall a b. (a -> b) -> a -> b
$ Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
nextConst (Str String
c) = String -> Const
Str (String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")
nextConst Const
o = Const
o
addMissingConsSt IState
ist SC
sc = SC -> State Int SC
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SC
sc
trimOverlapping :: SC -> SC
trimOverlapping :: SC -> SC
trimOverlapping SC
sc = [(Name, (Name, [Name]))] -> [(Name, [Name])] -> SC -> SC
trim [] [] SC
sc
where
trim :: [(Name, (Name, [Name]))] ->
[(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 a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just Term
y' -> Term -> Term -> State [(Name, Term)] Bool
checkRec Term
tm Term
y'
where
isCon :: TT n -> Bool
isCon TT n
tm
| (P NameType
yt n
_ TT n
_, [TT n]
_) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm,
NameType -> Bool
conType NameType
yt = Bool
True
isCon (Constant Const
_) = Bool
True
isCon TT n
_ = Bool
False
conType :: NameType -> Bool
conType (DCon Int
_ Int
_ Bool
_) = Bool
True
conType (TCon Int
_ Int
_) = Bool
True
conType NameType
_ = Bool
False
checkRec Term
tm (P NameType
Bound Name
y Term
_)
| Term -> Bool
forall {n}. TT n -> Bool
isCon Term
tm = do [(Name, Term)]
nmap <- StateT [(Name, Term)] Identity [(Name, Term)]
forall s (m :: * -> *). MonadState s m => m s
get
case Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
y [(Name, Term)]
nmap of
Maybe Term
Nothing -> do [(Name, Term)] -> StateT [(Name, Term)] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
y, Term
tm) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
nmap)
Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just Term
x' -> Term -> Term -> State [(Name, Term)] Bool
checkRec Term
tm Term
x'
where
isCon :: TT n -> Bool
isCon TT n
tm
| (P NameType
yt n
_ TT n
_, [TT n]
_) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm,
NameType -> Bool
conType NameType
yt = Bool
True
isCon (Constant Const
_) = Bool
True
isCon TT n
_ = Bool
False
conType :: NameType -> Bool
conType (DCon Int
_ Int
_ Bool
_) = Bool
True
conType (TCon Int
_ Int
_) = Bool
True
conType NameType
_ = Bool
False
checkRec (App AppStatus Name
_ Term
f Term
a) p :: Term
p@(P NameType
_ Name
_ Term
_) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
p
checkRec (App AppStatus Name
_ Term
f Term
a) p :: Term
p@(Constant Const
_) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
p
checkRec p :: Term
p@(P NameType
_ Name
_ Term
_) (App AppStatus Name
_ Term
f Term
a) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
p Term
f
checkRec p :: Term
p@(Constant Const
_) (App AppStatus Name
_ Term
f Term
a) = Term -> Term -> State [(Name, Term)] Bool
checkRec Term
p Term
f
checkRec fa :: Term
fa@(App AppStatus Name
_ Term
_ Term
_) fa' :: Term
fa'@(App AppStatus Name
_ Term
_ Term
_)
| (Term
f, [Term]
as) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fa,
(Term
f', [Term]
as') <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fa'
= if ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as')
then Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
f'
else do Bool
fok <- Term -> Term -> State [(Name, Term)] Bool
checkRec Term
f Term
f'
Bool
argok <- [Term] -> [Term] -> State [(Name, Term)] Bool
checkRecs (Term
f Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
as) (Term
f Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
as')
Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Term -> Bool
forall {n}. TT n -> Bool
conType Term
f then Bool
fok Bool -> Bool -> Bool
&& Bool
argok
else Bool
fok Bool -> Bool -> Bool
|| Bool
argok)
where
checkRecs :: [Term] -> [Term] -> State [(Name, Term)] Bool
checkRecs [] [] = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRecs (Term
a : [Term]
as) (Term
b : [Term]
bs) = do Bool
aok <- Term -> Term -> State [(Name, Term)] Bool
checkRec Term
a Term
b
Bool
asok <- [Term] -> [Term] -> State [(Name, Term)] Bool
checkRecs [Term]
as [Term]
bs
Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
aok Bool -> Bool -> Bool
&& Bool
asok)
conType :: TT n -> Bool
conType (P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_) = Bool
True
conType (P (TCon Int
_ Int
_) n
_ TT n
_) = Bool
True
conType (Constant Const
_) = Bool
True
conType TT n
_ = Bool
False
checkRec (P NameType
xt Name
x Term
_) (P NameType
yt Name
y Term
_)
| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
| NameType -> NameType -> Bool
ntRec NameType
xt NameType
yt = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
where
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 a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (Constant Const
_) (P NameType
Ref Name
_ Term
_) = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec (TType UExp
_) (TType UExp
_) = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkRec Term
_ Term
_ = Bool -> State [(Name, Term)] Bool
forall a. a -> StateT [(Name, Term)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False