{-# LANGUAGE FlexibleContexts, PatternGuards #-}
module Idris.PartialEval(
partial_eval, getSpecApps, specType
, mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)
, pe_app, pe_def, pe_clauses, pe_simple
) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Control.Monad
import Control.Monad.State
data PEArgType = ImplicitS Name
| ImplicitD Name
| ConstraintS
| ConstraintD
| ExplicitS
| ExplicitD
| UnifiedD
deriving (PEArgType -> PEArgType -> Bool
(PEArgType -> PEArgType -> Bool)
-> (PEArgType -> PEArgType -> Bool) -> Eq PEArgType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PEArgType -> PEArgType -> Bool
== :: PEArgType -> PEArgType -> Bool
$c/= :: PEArgType -> PEArgType -> Bool
/= :: PEArgType -> PEArgType -> Bool
Eq, Int -> PEArgType -> ShowS
[PEArgType] -> ShowS
PEArgType -> String
(Int -> PEArgType -> ShowS)
-> (PEArgType -> String)
-> ([PEArgType] -> ShowS)
-> Show PEArgType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PEArgType -> ShowS
showsPrec :: Int -> PEArgType -> ShowS
$cshow :: PEArgType -> String
show :: PEArgType -> String
$cshowList :: [PEArgType] -> ShowS
showList :: [PEArgType] -> ShowS
Show)
data PEDecl = PEDecl { PEDecl -> PTerm
pe_app :: PTerm,
PEDecl -> PTerm
pe_def :: PTerm,
PEDecl -> [(PTerm, PTerm)]
pe_clauses :: [(PTerm, PTerm)],
PEDecl -> Bool
pe_simple :: Bool
}
partial_eval :: Context
-> [(Name, Maybe Int)]
-> [Either Term (Term, Term)]
-> Maybe [Either Term (Term, Term)]
partial_eval :: Context
-> [(Name, Maybe Int)]
-> [Either Term (Term, Term)]
-> Maybe [Either Term (Term, Term)]
partial_eval Context
ctxt [(Name, Maybe Int)]
ns_in [Either Term (Term, Term)]
tms = (Either Term (Term, Term) -> Maybe (Either Term (Term, Term)))
-> [Either Term (Term, Term)] -> Maybe [Either Term (Term, 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 Either Term (Term, Term) -> Maybe (Either Term (Term, Term))
forall {a} {a}. Either a (a, Term) -> Maybe (Either a (a, Term))
peClause [Either Term (Term, Term)]
tms where
ns :: [(Name, Maybe Int)]
ns = [(Name, Maybe Int)] -> [(Name, Maybe Int)]
forall {a} {a}. (Eq a, Num a) => [(a, Maybe a)] -> [(a, Maybe a)]
squash [(Name, Maybe Int)]
ns_in
squash :: [(a, Maybe a)] -> [(a, Maybe a)]
squash ((a
n, Just a
x) : [(a, Maybe a)]
ns)
| Just (Just a
y) <- a -> [(a, Maybe a)] -> Maybe (Maybe a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Maybe a)]
ns
= [(a, Maybe a)] -> [(a, Maybe a)]
squash ((a
n, a -> Maybe a
forall a. a -> Maybe a
Just (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y)) (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
forall a. a -> [a] -> [a]
: a -> [(a, Maybe a)] -> [(a, Maybe a)]
forall {t} {b}. Eq t => t -> [(t, b)] -> [(t, b)]
drop a
n [(a, Maybe a)]
ns)
| Bool
otherwise = (a
n, a -> Maybe a
forall a. a -> Maybe a
Just a
x) (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
forall a. a -> [a] -> [a]
: [(a, Maybe a)] -> [(a, Maybe a)]
squash [(a, Maybe a)]
ns
squash ((a, Maybe a)
n : [(a, Maybe a)]
ns) = (a, Maybe a)
n (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
forall a. a -> [a] -> [a]
: [(a, Maybe a)] -> [(a, Maybe a)]
squash [(a, Maybe a)]
ns
squash [] = []
drop :: t -> [(t, b)] -> [(t, b)]
drop t
n ((t
m, b
_) : [(t, b)]
ns) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
m = [(t, b)]
ns
drop t
n ((t, b)
x : [(t, b)]
ns) = (t, b)
x (t, b) -> [(t, b)] -> [(t, b)]
forall a. a -> [a] -> [a]
: t -> [(t, b)] -> [(t, b)]
drop t
n [(t, b)]
ns
drop t
n [] = []
peClause :: Either a (a, Term) -> Maybe (Either a (a, Term))
peClause (Left a
t) = Either a (a, Term) -> Maybe (Either a (a, Term))
forall a. a -> Maybe a
Just (Either a (a, Term) -> Maybe (Either a (a, Term)))
-> Either a (a, Term) -> Maybe (Either a (a, Term))
forall a b. (a -> b) -> a -> b
$ a -> Either a (a, Term)
forall a b. a -> Either a b
Left a
t
peClause (Right (a
lhs, Term
rhs))
= let (Term
rhs', [(Name, Int)]
reductions) = Context -> Env -> [(Name, Int)] -> Term -> (Term, [(Name, Int)])
specialise Context
ctxt [] (((Name, Maybe Int) -> (Name, Int))
-> [(Name, Maybe Int)] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Maybe Int) -> (Name, Int)
forall {b}. Num b => (Name, Maybe b) -> (Name, b)
toLimit [(Name, Maybe Int)]
ns) Term
rhs in
do Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Either Term (Term, Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Term (Term, Term)]
tms Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (Maybe () -> Maybe ()) -> Maybe () -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [(Name, Maybe Int)] -> [(Name, Int)] -> Maybe ()
forall {a} {a}.
(Ord a, Num a, Eq a) =>
[(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(Name, Maybe Int)]
ns [(Name, Int)]
reductions
Either a (a, Term) -> Maybe (Either a (a, Term))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, Term) -> Either a (a, Term)
forall a b. b -> Either a b
Right (a
lhs, Term
rhs'))
toLimit :: (Name, Maybe b) -> (Name, b)
toLimit (Name
n, Maybe b
Nothing) | Name -> Context -> Bool
isTCDict Name
n Context
ctxt = (Name
n, b
2)
toLimit (Name
n, Maybe b
Nothing) = (Name
n, b
65536)
toLimit (Name
n, Just b
l) = (Name
n, b
l)
checkProgress :: [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(a, Maybe a)]
ns [] = () -> Maybe ()
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkProgress [(a, Maybe a)]
ns ((a
n, a
r) : [(a, a)]
rs)
| Just (Just a
start) <- a -> [(a, Maybe a)] -> Maybe (Maybe a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Maybe a)]
ns
= if a
start a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
1 Bool -> Bool -> Bool
|| a
r a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
start then [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(a, Maybe a)]
ns [(a, a)]
rs else Maybe ()
forall a. Maybe a
Nothing
| Bool
otherwise = [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(a, Maybe a)]
ns [(a, a)]
rs
specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])
specType :: [(PEArgType, Term)] -> Term -> (Term, [(PEArgType, Term)])
specType [(PEArgType, Term)]
args Term
ty = let (Term
t, [((PEArgType, Term), Name)]
args') = State [((PEArgType, Term), Name)] Term
-> [((PEArgType, Term), Name)]
-> (Term, [((PEArgType, Term), Name)])
forall s a. State s a -> s -> (a, s)
runState ([(PEArgType, Term)]
-> Term -> State [((PEArgType, Term), Name)] Term
forall {n} {m :: * -> *}.
(Eq n, MonadState [((PEArgType, TT n), Name)] m) =>
[(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, Term)]
args Term
ty) [] in
([(PEArgType, Term)] -> Term -> Term
forall {n}. [(PEArgType, TT n)] -> TT n -> TT n
st ((((PEArgType, Term), Name) -> (PEArgType, Term))
-> [((PEArgType, Term), Name)] -> [(PEArgType, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((PEArgType, Term), Name) -> (PEArgType, Term)
forall a b. (a, b) -> a
fst [((PEArgType, Term), Name)]
args') Term
t, (((PEArgType, Term), Name) -> (PEArgType, Term))
-> [((PEArgType, Term), Name)] -> [(PEArgType, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((PEArgType, Term), Name) -> (PEArgType, Term)
forall a b. (a, b) -> a
fst [((PEArgType, Term), Name)]
args')
where
st :: [(PEArgType, TT n)] -> TT n -> TT n
st ((PEArgType
ExplicitS, TT n
v) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rc Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
= n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT n
t TT n
v) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
st ((ImplicitS Name
_, TT n
v) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rc Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
= n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT n
t TT n
v) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
st ((PEArgType
ConstraintS, TT n
v) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rc Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
= n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT n
t TT n
v) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
st ((PEArgType
UnifiedD, TT n
_) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
= [(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc
st ((PEArgType, TT n)
_ : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rig Maybe ImplicitInfo
i TT n
t TT n
k) TT n
sc)
= n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> Maybe ImplicitInfo -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i TT n
t TT n
k) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
st [(PEArgType, TT n)]
_ TT n
t = TT n
t
unifyEq :: [(PEArgType, TT n)] -> Term -> m Term
unifyEq (imp :: (PEArgType, TT n)
imp@(ImplicitD Name
_, TT n
v) : [(PEArgType, TT n)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc)
= do [((PEArgType, TT n), Name)]
amap <- m [((PEArgType, TT n), Name)]
forall s (m :: * -> *). MonadState s m => m s
get
case (PEArgType, TT n) -> [((PEArgType, TT n), Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (PEArgType, TT n)
imp [((PEArgType, TT n), Name)]
amap of
Just Name
n' ->
do [((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
amap [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
forall a. [a] -> [a] -> [a]
++ [((PEArgType
UnifiedD, TT n
forall n. TT n
Erased), Name
n)])
Term
sc' <- [(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, TT n)]
xs (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
n (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n' Term
forall n. TT n
Erased) Term
sc)
Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc')
Maybe Name
_ -> do [((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
amap [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
forall a. [a] -> [a] -> [a]
++ [((PEArgType, TT n)
imp, Name
n)])
Term
sc' <- [(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, TT n)]
xs Term
sc
Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc')
unifyEq ((PEArgType, TT n)
x : [(PEArgType, TT n)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc)
= do [((PEArgType, TT n), Name)]
args <- m [((PEArgType, TT n), Name)]
forall s (m :: * -> *). MonadState s m => m s
get
[((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
args [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
forall a. [a] -> [a] -> [a]
++ [((PEArgType, TT n)
x, Name
n)])
Term
sc' <- [(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, TT n)]
xs Term
sc
Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc')
unifyEq [(PEArgType, TT n)]
xs Term
t = do [((PEArgType, TT n), Name)]
args <- m [((PEArgType, TT n), Name)]
forall s (m :: * -> *). MonadState s m => m s
get
[((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
args [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
forall a. [a] -> [a] -> [a]
++ ([(PEArgType, TT n)] -> [Name] -> [((PEArgType, TT n), Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(PEArgType, TT n)]
xs (Name -> [Name]
forall a. a -> [a]
repeat (String -> Name
sUN String
"_"))))
Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm
mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Term -> PTerm
mkPE_TyDecl IState
ist [(PEArgType, Term)]
args Term
ty = [(PEArgType, Term)] -> Term -> PTerm
forall {b}. [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, Term)]
args Term
ty
where
mkty :: [(PEArgType, b)] -> Term -> PTerm
mkty ((PEArgType
ExplicitD, b
v) : [(PEArgType, b)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
t Term
k) Term
sc)
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
n FC
NoFC (IState -> Term -> PTerm
delab IState
ist (Term -> Term
generaliseIn Term
t)) ([(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc)
mkty ((PEArgType
ConstraintD, b
v) : [(PEArgType, b)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
t Term
k) Term
sc)
| IState -> Term -> Bool
concreteInterface IState
ist Term
t = [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc
| IState -> Term -> Bool
interfaceConstraint IState
ist Term
t
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint Name
n FC
NoFC (IState -> Term -> PTerm
delab IState
ist (Term -> Term
generaliseIn Term
t)) ([(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc)
mkty ((ImplicitD Name
_, b
v) : [(PEArgType, b)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
t Term
k) Term
sc)
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
n FC
NoFC (IState -> Term -> PTerm
delab IState
ist (Term -> Term
generaliseIn Term
t)) ([(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc)
mkty ((PEArgType, b)
_ : [(PEArgType, b)]
xs) Term
t
= [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
t
mkty [] Term
t = IState -> Term -> PTerm
delab IState
ist Term
t
generaliseIn :: Term -> Term
generaliseIn Term
tm = State Int Term -> Int -> Term
forall s a. State s a -> s -> a
evalState (Term -> State Int Term
forall {m :: * -> *}. MonadState Int m => Term -> m Term
gen Term
tm) Int
0
gen :: Term -> m Term
gen Term
tm | (P NameType
_ Name
fn Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name -> Context -> Bool
isFnName Name
fn (IState -> Context
tt_ctxt IState
ist)
= do Int
nm <- m Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
Term -> m Term
forall a. a -> m 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
nm String
"spec") Term
forall n. TT n
Erased)
gen (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Term -> Term -> Term) -> m Term -> m (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
gen Term
f m (Term -> Term) -> m Term -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
gen Term
a
gen Term
tm = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm
interfaceConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool
interfaceConstraint :: IState -> Term -> Bool
interfaceConstraint IState
ist Term
v
| (P NameType
_ Name
c Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
v = case Name -> Ctxt InterfaceInfo -> [InterfaceInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
c (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
[InterfaceInfo
_] -> Bool
True
[InterfaceInfo]
_ -> Bool
False
| Bool
otherwise = Bool
False
concreteInterface :: IState -> TT Name -> Bool
concreteInterface :: IState -> Term -> Bool
concreteInterface IState
ist Term
v
| Bool -> Bool
not (IState -> Term -> Bool
interfaceConstraint IState
ist Term
v) = Bool
False
| (P NameType
_ Name
c Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
v = (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
concrete [Term]
args
| Bool
otherwise = Bool
False
where concrete :: Term -> Bool
concrete (Constant Const
_) = Bool
True
concrete Term
tm | (P NameType
_ Name
n Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm
= case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
[Term
_] -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
concrete [Term]
args
[Term]
_ -> Bool
False
| Bool
otherwise = Bool
False
mkNewPats :: IState
-> [(Term, Term)]
-> [(PEArgType, Term)]
-> Name
-> Name
-> PTerm
-> PTerm
-> PEDecl
mkNewPats :: IState
-> [(Term, Term)]
-> [(PEArgType, Term)]
-> Name
-> Name
-> PTerm
-> PTerm
-> PEDecl
mkNewPats IState
ist [(Term, Term)]
d [(PEArgType, Term)]
ns Name
newname Name
sname PTerm
lhs PTerm
rhs | (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
forall {n}. TT n -> Bool
dynVar (((Term, Term) -> Term) -> [(Term, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Term) -> Term
forall a b. (a, b) -> a
fst [(Term, Term)]
d)
= PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs [(PTerm
lhs, PTerm
rhs)] Bool
True
where dynVar :: TT n -> Bool
dynVar TT n
ap = case TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
ap of
(TT n
_, [TT n]
args) -> [(PEArgType, Term)] -> [TT n] -> Bool
forall {b} {n}. [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, Term)]
ns [TT n]
args
dynArgs :: [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
_ [] = Bool
True
dynArgs ((ImplicitS Name
_, b
_) : [(PEArgType, b)]
ns) (TT n
a : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs ((PEArgType
ConstraintS, b
_) : [(PEArgType, b)]
ns) (TT n
a : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs ((PEArgType
ExplicitS, b
_) : [(PEArgType, b)]
ns) (TT n
a : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs ((PEArgType, b)
_ : [(PEArgType, b)]
ns) (V Int
_ : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs ((PEArgType, b)
_ : [(PEArgType, b)]
ns) (P NameType
_ n
_ TT n
_ : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs [(PEArgType, b)]
_ [TT n]
_ = Bool
False
mkNewPats IState
ist [(Term, Term)]
d [(PEArgType, Term)]
ns Name
newname Name
sname PTerm
lhs PTerm
rhs =
PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs (((Term, Term) -> (PTerm, PTerm))
-> [(Term, Term)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Term) -> (PTerm, PTerm)
mkClause [(Term, Term)]
d) Bool
False
where
mkClause :: (Term, Term) -> (PTerm, PTerm)
mkClause :: (Term, Term) -> (PTerm, PTerm)
mkClause (Term
oldlhs, Term
oldrhs)
= let (Term
_, [Term]
as) = Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
oldlhs
lhsargs :: [PArg' PTerm]
lhsargs = [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [] [(PEArgType, Term)]
ns [Term]
as
lhs :: PTerm
lhs = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
emptyFC (FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
newname) [PArg' PTerm]
lhsargs
rhs :: PTerm
rhs = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
emptyFC (FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
sname)
([(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
lhsargs) in
(PTerm
lhs, PTerm
rhs)
mkLHSargs :: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
_ [] [Term]
_ = []
mkLHSargs [(Name, Term)]
sub ((PEArgType
ExplicitD, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
= PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist ([(Name, Term)] -> Term -> Term
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
mkLHSargs [(Name, Term)]
sub ((ImplicitD Name
n, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
= Name -> PTerm -> Bool -> PArg' PTerm
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist ([(Name, Term)] -> Term -> Term
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) Bool
True PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
mkLHSargs [(Name, Term)]
sub ((PEArgType
ConstraintD, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
= PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pconst (IState -> Term -> PTerm
delab IState
ist ([(Name, Term)] -> Term -> Term
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
mkLHSargs [(Name, Term)]
sub ((PEArgType
UnifiedD, Term
_) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
= [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
mkLHSargs [(Name, Term)]
sub ((ImplicitS Name
_, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
= [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs (Term -> Term -> [(Name, Term)] -> [(Name, Term)]
forall {a} {b}. TT a -> b -> [(a, b)] -> [(a, b)]
extend Term
a Term
t [(Name, Term)]
sub) [(PEArgType, Term)]
ns [Term]
as
mkLHSargs [(Name, Term)]
sub ((PEArgType
ExplicitS, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
= [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs (Term -> Term -> [(Name, Term)] -> [(Name, Term)]
forall {a} {b}. TT a -> b -> [(a, b)] -> [(a, b)]
extend Term
a Term
t [(Name, Term)]
sub) [(PEArgType, Term)]
ns [Term]
as
mkLHSargs [(Name, Term)]
sub ((PEArgType
ConstraintS, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
= [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs (Term -> Term -> [(Name, Term)] -> [(Name, Term)]
forall {a} {b}. TT a -> b -> [(a, b)] -> [(a, b)]
extend Term
a Term
t [(Name, Term)]
sub) [(PEArgType, Term)]
ns [Term]
as
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
_ [] = []
extend :: TT a -> b -> [(a, b)] -> [(a, b)]
extend (P NameType
_ a
n TT a
_) b
t [(a, b)]
sub = (a
n, b
t) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
sub
extend TT a
_ b
_ [(a, b)]
sub = [(a, b)]
sub
mkRHSargs :: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs ((PEArgType
ExplicitS, Term
t) : [(PEArgType, Term)]
ns) [PArg' PTerm]
as = PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist Term
t) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs ((PEArgType
ExplicitD, Term
t) : [(PEArgType, Term)]
ns) (PArg' PTerm
a : [PArg' PTerm]
as) = PArg' PTerm
a PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs ((ImplicitD Name
n, Term
t) : [(PEArgType, Term)]
ns) (PArg' PTerm
a : [PArg' PTerm]
as) = PArg' PTerm
a PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs ((ImplicitS Name
n, Term
t) : [(PEArgType, Term)]
ns) [PArg' PTerm]
as
= Name -> PTerm -> Bool -> PArg' PTerm
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist Term
t) Bool
True PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs ((PEArgType
ConstraintD, Term
t) : [(PEArgType, Term)]
ns) (PArg' PTerm
a : [PArg' PTerm]
as) = PArg' PTerm
a PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs ((PEArgType
ConstraintS, Term
t) : [(PEArgType, Term)]
ns) [PArg' PTerm]
as
= PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pconst (IState -> Term -> PTerm
delab IState
ist Term
t) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs ((PEArgType, Term)
_ : [(PEArgType, Term)]
ns) [PArg' PTerm]
as = [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs [(PEArgType, Term)]
_ [PArg' PTerm]
_ = []
mkPE_TermDecl :: IState
-> Name
-> Name
-> PTerm
-> [(PEArgType, Term)]
-> PEDecl
mkPE_TermDecl :: IState -> Name -> Name -> PTerm -> [(PEArgType, Term)] -> PEDecl
mkPE_TermDecl IState
ist Name
newname Name
sname PTerm
specty [(PEArgType, Term)]
ns
= let deps :: [Name]
deps = PTerm -> [Name]
getDepNames (PTerm -> PTerm
eraseRet PTerm
specty)
lhs :: PTerm
lhs = [Name] -> PTerm -> PTerm
forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
eraseDeps [Name]
deps (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
emptyFC (FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
newname) ([(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
ns)
rhs :: PTerm
rhs = [Name] -> PTerm -> PTerm
forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
eraseDeps [Name]
deps (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
IState -> Term -> PTerm
delab IState
ist (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
sname Term
forall n. TT n
Erased) (((PEArgType, Term) -> Term) -> [(PEArgType, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (PEArgType, Term) -> Term
forall a b. (a, b) -> b
snd [(PEArgType, Term)]
ns))
patdef :: Maybe ([([(Name, Term)], Term, Term)], [PTerm])
patdef =
Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> Maybe ([([(Name, Term)], Term, Term)], [PTerm])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
sname (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist)
newpats :: PEDecl
newpats = case Maybe ([([(Name, Term)], Term, Term)], [PTerm])
patdef of
Maybe ([([(Name, Term)], Term, Term)], [PTerm])
Nothing -> PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs [(PTerm
lhs, PTerm
rhs)] Bool
True
Just ([([(Name, Term)], Term, Term)], [PTerm])
d -> IState
-> [(Term, Term)]
-> [(PEArgType, Term)]
-> Name
-> Name
-> PTerm
-> PTerm
-> PEDecl
mkNewPats IState
ist (([([(Name, Term)], Term, Term)], [PTerm]) -> [(Term, Term)]
forall {a} {a} {b} {b}. ([(a, a, b)], b) -> [(a, b)]
getPats ([([(Name, Term)], Term, Term)], [PTerm])
d) [(PEArgType, Term)]
ns
Name
newname Name
sname PTerm
lhs PTerm
rhs in
PEDecl
newpats where
getPats :: ([(a, a, b)], b) -> [(a, b)]
getPats ([(a, a, b)]
ps, b
_) = ((a, a, b) -> (a, b)) -> [(a, a, b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
_, a
lhs, b
rhs) -> (a
lhs, b
rhs)) [(a, a, b)]
ps
eraseRet :: PTerm -> PTerm
eraseRet (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
sc) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
ty (PTerm -> PTerm
eraseRet PTerm
sc)
eraseRet PTerm
_ = PTerm
Placeholder
getDepNames :: PTerm -> [Name]
getDepNames (PPi Plicity
_ Name
n FC
_ PTerm
_ PTerm
sc)
| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PTerm -> [Name]
allNamesIn PTerm
sc = Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: PTerm -> [Name]
getDepNames PTerm
sc
| Bool
otherwise = PTerm -> [Name]
getDepNames PTerm
sc
getDepNames PTerm
tm = []
mkp :: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [] = []
mkp ((PEArgType
ExplicitD, Term
tm) : [(PEArgType, Term)]
tms) = PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist Term
tm) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms
mkp ((ImplicitD Name
n, Term
tm) : [(PEArgType, Term)]
tms) = Name -> PTerm -> Bool -> PArg' PTerm
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist Term
tm) Bool
True PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms
mkp ((PEArgType, Term)
_ : [(PEArgType, Term)]
tms) = [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms
eraseDeps :: t Name -> PTerm -> PTerm
eraseDeps t Name
ns PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT (t Name -> PTerm -> PTerm
forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
deImp t Name
ns) PTerm
tm
deImp :: t Name -> PTerm -> PTerm
deImp t Name
ns (PApp FC
fc PTerm
t [PArg' PTerm]
as) = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc PTerm
t ((PArg' PTerm -> PArg' PTerm) -> [PArg' PTerm] -> [PArg' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (t Name -> PArg' PTerm -> PArg' PTerm
forall {t :: * -> *}.
Foldable t =>
t Name -> PArg' PTerm -> PArg' PTerm
deImpArg t Name
ns) [PArg' PTerm]
as)
deImp t Name
ns PTerm
t = PTerm
t
deImpArg :: t Name -> PArg' PTerm -> PArg' PTerm
deImpArg t Name
ns PArg' PTerm
a | PArg' PTerm -> Name
forall t. PArg' t -> Name
pname PArg' PTerm
a Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ns = PArg' PTerm
a { getTm = Placeholder }
| Bool
otherwise = PArg' PTerm
a
getSpecApps :: IState
-> [Name]
-> Term
-> [(Name, [(PEArgType, Term)])]
getSpecApps :: IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])]
getSpecApps IState
ist [Name]
env Term
tm = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env (Term -> Term
forall n. TT n -> TT n
explicitNames Term
tm) where
staticArg :: p -> Bool -> PArg' t -> Term -> a -> (PEArgType, Term)
staticArg p
env Bool
True PArg' t
imp Term
tm a
n
| Just Name
n <- PArg' t -> Maybe Name
forall {t}. PArg' t -> Maybe Name
imparg PArg' t
imp = (Name -> PEArgType
ImplicitS Name
n, Term
tm)
| PArg' t -> Bool
forall {t}. PArg' t -> Bool
constrarg PArg' t
imp = (PEArgType
ConstraintS, Term
tm)
| Bool
otherwise = (PEArgType
ExplicitS, Term
tm)
staticArg p
env Bool
False PArg' t
imp Term
tm a
n
| Just Name
nm <- PArg' t -> Maybe Name
forall {t}. PArg' t -> Maybe Name
imparg PArg' t
imp = (Name -> PEArgType
ImplicitD Name
nm, (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"arg")) Term
forall n. TT n
Erased))
| PArg' t -> Bool
forall {t}. PArg' t -> Bool
constrarg PArg' t
imp = (PEArgType
ConstraintD, Term
tm)
| Bool
otherwise = (PEArgType
ExplicitD, (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"arg")) Term
forall n. TT n
Erased))
imparg :: PArg' t -> Maybe Name
imparg (PExp Int
_ [ArgOpt]
_ Name
_ t
_) = Maybe Name
forall a. Maybe a
Nothing
imparg (PConstraint Int
_ [ArgOpt]
_ Name
_ t
_) = Maybe Name
forall a. Maybe a
Nothing
imparg PArg' t
arg = Name -> Maybe Name
forall a. a -> Maybe a
Just (PArg' t -> Name
forall t. PArg' t -> Name
pname PArg' t
arg)
constrarg :: PArg' t -> Bool
constrarg (PConstraint Int
_ [ArgOpt]
_ Name
_ t
_) = Bool
True
constrarg PArg' t
arg = Bool
False
buildApp :: p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp p
env [] [] [Term]
_ [a]
_ = []
buildApp p
env (Bool
s:[Bool]
ss) (PArg' t
i:[PArg' t]
is) (Term
a:[Term]
as) (a
n:[a]
ns)
= let s' :: (PEArgType, Term)
s' = p -> Bool -> PArg' t -> Term -> a -> (PEArgType, Term)
forall {a} {p} {t}.
Show a =>
p -> Bool -> PArg' t -> Term -> a -> (PEArgType, Term)
staticArg p
env Bool
s PArg' t
i Term
a a
n
ss' :: [(PEArgType, Term)]
ss' = p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp p
env [Bool]
ss [PArg' t]
is [Term]
as [a]
ns in
((PEArgType, Term)
s' (PEArgType, Term) -> [(PEArgType, Term)] -> [(PEArgType, Term)]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)]
ss')
ga :: [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env tm :: Term
tm@(App AppStatus Name
_ Term
f Term
a) | (P NameType
_ Name
n Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) =
[Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env Term
f [(Name, [(PEArgType, Term)])]
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env Term
a [(Name, [(PEArgType, Term)])]
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a. [a] -> [a] -> [a]
++
case (Name -> Ctxt [Bool] -> Maybe [Bool]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
ist),
Name -> Ctxt [PArg' PTerm] -> Maybe [PArg' PTerm]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg' PTerm]
idris_implicits IState
ist)) of
(Just [Bool]
statics, Just [PArg' PTerm]
imps) ->
if ([Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
statics 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]
args Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
statics
Bool -> Bool -> Bool
&& Context -> Name -> Bool
specialisable (IState -> Context
tt_ctxt IState
ist) Name
n) then
case [Name]
-> [Bool]
-> [PArg' PTerm]
-> [Term]
-> [Integer]
-> [(PEArgType, Term)]
forall {a} {p} {t}.
Show a =>
p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp [Name]
env [Bool]
statics [PArg' PTerm]
imps [Term]
args [Integer
0..] of
[(PEArgType, Term)]
args -> [(Name
n, [(PEArgType, Term)]
args)]
else []
(Maybe [Bool], Maybe [PArg' PTerm])
_ -> []
ga [Name]
env (Bind Name
n (Let RigCount
rc Term
t Term
v) Term
sc) = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env Term
v [(Name, [(PEArgType, Term)])]
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
ga [Name]
env (Bind Name
n Binder Term
t Term
sc) = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
ga [Name]
env Term
t = []
specialisable :: Context -> Name -> Bool
specialisable :: Context -> Name -> Bool
specialisable Context
ctxt Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (CaseOp CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
cds) ->
SC -> Bool
noOverlap (([Name], SC) -> SC
forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cds))
Maybe Def
_ -> Bool
False
noOverlap :: SC -> Bool
noOverlap :: SC -> Bool
noOverlap (Case CaseType
_ Name
_ [DefaultCase SC
sc]) = SC -> Bool
noOverlap SC
sc
noOverlap (Case CaseType
_ Name
_ [CaseAlt' Term]
alts) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
alts
noOverlap SC
_ = Bool
True
noOverlapAlts :: [CaseAlt' Term] -> Bool
noOverlapAlts (ConCase Name
_ Int
_ [Name]
_ SC
sc : [CaseAlt' Term]
rest)
= [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
noOverlapAlts (FnCase Name
_ [Name]
_ SC
sc : [CaseAlt' Term]
rest) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest
noOverlapAlts (ConstCase Const
_ SC
sc : [CaseAlt' Term]
rest)
= [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
noOverlapAlts (SucCase Name
_ SC
sc : [CaseAlt' Term]
rest)
= [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
noOverlapAlts (DefaultCase SC
_ : [CaseAlt' Term]
_) = Bool
False
noOverlapAlts [CaseAlt' Term]
_ = Bool
True