{-# 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.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
/= :: PEArgType -> PEArgType -> Bool
$c/= :: PEArgType -> PEArgType -> Bool
== :: PEArgType -> PEArgType -> Bool
$c== :: 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
showList :: [PEArgType] -> ShowS
$cshowList :: [PEArgType] -> ShowS
show :: PEArgType -> String
$cshow :: PEArgType -> String
showsPrec :: Int -> PEArgType -> ShowS
$cshowsPrec :: Int -> 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 ctxt :: Context
ctxt ns_in :: [(Name, Maybe Int)]
ns_in tms :: [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)
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 ((n :: a
n, Just x :: a
x) : ns :: [(a, Maybe a)]
ns)
| Just (Just y :: 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 (n :: (a, Maybe a)
n : ns :: [(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 n :: t
n ((m :: t
m, _) : ns :: [(t, b)]
ns) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
m = [(t, b)]
ns
drop n :: t
n (x :: (t, b)
x : ns :: [(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 n :: t
n [] = []
peClause :: Either a (a, Term) -> Maybe (Either a (a, Term))
peClause (Left t :: 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 (lhs :: a
lhs, rhs :: Term
rhs))
= let (rhs' :: Term
rhs', reductions :: [(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 (t :: * -> *) a. Foldable t => t a -> Int
length [Either Term (Term, Term)]
tms Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 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 (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 (n :: Name
n, Nothing) | Name -> Context -> Bool
isTCDict Name
n Context
ctxt = (Name
n, 2)
toLimit (n :: Name
n, Nothing) = (Name
n, 65536)
toLimit (n :: Name
n, Just l :: b
l) = (Name
n, b
l)
checkProgress :: [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress ns :: [(a, Maybe a)]
ns [] = () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkProgress ns :: [(a, Maybe a)]
ns ((n :: a
n, r :: a
r) : rs :: [(a, a)]
rs)
| Just (Just start :: 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
<= 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 args :: [(PEArgType, Term)]
args ty :: Term
ty = let (t :: Term
t, args' :: [((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 :: * -> *).
(MonadState [((PEArgType, TT n), Name)] m, Eq n) =>
[(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 ((ExplicitS, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rc :: RigCount
rc _ t :: TT n
t _) sc :: 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 _, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rc :: RigCount
rc _ t :: TT n
t _) sc :: 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 ((ConstraintS, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rc :: RigCount
rc _ t :: TT n
t _) sc :: 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 ((UnifiedD, _) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi _ _ t :: TT n
t _) sc :: TT n
sc)
= [(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc
st (_ : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: TT n
t k :: TT n
k) sc :: 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 _ t :: TT n
t = TT n
t
unifyEq :: [(PEArgType, TT n)] -> Term -> m Term
unifyEq (imp :: (PEArgType, TT n)
imp@(ImplicitD _, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: Term
t k :: Term
k) sc :: 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 n' :: 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 (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')
_ -> 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 (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 (x :: (PEArgType, TT n)
x : xs :: [(PEArgType, TT n)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: Term
t k :: Term
k) sc :: 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 (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 xs :: [(PEArgType, TT n)]
xs t :: 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 "_"))))
Term -> m Term
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 ist :: IState
ist args :: [(PEArgType, Term)]
args ty :: 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 ((ExplicitD, v :: b
v) : xs :: [(PEArgType, b)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig _ t :: Term
t k :: Term
k) sc :: 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 ((ConstraintD, v :: b
v) : xs :: [(PEArgType, b)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig _ t :: Term
t k :: Term
k) sc :: 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 _, v :: b
v) : xs :: [(PEArgType, b)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig _ t :: Term
t k :: Term
k) sc :: 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 (_ : xs :: [(PEArgType, b)]
xs) t :: Term
t
= [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
t
mkty [] t :: Term
t = IState -> Term -> PTerm
delab IState
ist Term
t
generaliseIn :: Term -> Term
generaliseIn tm :: 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) 0
gen :: Term -> m Term
gen tm :: Term
tm | (P _ fn :: Name
fn _, args :: [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
+ 1)
Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound (Int -> String -> Name
sMN Int
nm "spec") Term
forall n. TT n
Erased)
gen (App s :: AppStatus Name
s f :: Term
f a :: 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
gen Term
a
gen tm :: Term
tm = Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm
interfaceConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool
interfaceConstraint :: IState -> Term -> Bool
interfaceConstraint ist :: IState
ist v :: Term
v
| (P _ c :: Name
c _, args :: [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
[_] -> Bool
True
_ -> Bool
False
| Bool
otherwise = Bool
False
concreteInterface :: IState -> TT Name -> Bool
concreteInterface :: IState -> Term -> Bool
concreteInterface ist :: IState
ist v :: Term
v
| Bool -> Bool
not (IState -> Term -> Bool
interfaceConstraint IState
ist Term
v) = Bool
False
| (P _ c :: Name
c _, args :: [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 _) = Bool
True
concrete tm :: Term
tm | (P _ n :: Name
n _, args :: [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 -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
concrete [Term]
args
_ -> 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 ist :: IState
ist d :: [(Term, Term)]
d ns :: [(PEArgType, Term)]
ns newname :: Name
newname sname :: Name
sname lhs :: PTerm
lhs rhs :: 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 ap :: TT n
ap = case TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
ap of
(_, args :: [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 _ [] = Bool
True
dynArgs ((ImplicitS _, _) : ns :: [(PEArgType, b)]
ns) (a :: TT n
a : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs ((ConstraintS, _) : ns :: [(PEArgType, b)]
ns) (a :: TT n
a : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs ((ExplicitS, _) : ns :: [(PEArgType, b)]
ns) (a :: TT n
a : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs (_ : ns :: [(PEArgType, b)]
ns) (V _ : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs (_ : ns :: [(PEArgType, b)]
ns) (P _ _ _ : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
dynArgs _ _ = Bool
False
mkNewPats ist :: IState
ist d :: [(Term, Term)]
d ns :: [(PEArgType, Term)]
ns newname :: Name
newname sname :: Name
sname lhs :: PTerm
lhs rhs :: 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 (oldlhs :: Term
oldlhs, oldrhs :: Term
oldrhs)
= let (_, as :: [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 _ [] _ = []
mkLHSargs sub :: [(Name, Term)]
sub ((ExplicitD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ImplicitD n :: Name
n, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ConstraintD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((UnifiedD, _) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [Term]
as)
= [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
mkLHSargs sub :: [(Name, Term)]
sub ((ImplicitS _, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ExplicitS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ConstraintS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub _ [] = []
extend :: TT a -> b -> [(a, b)] -> [(a, b)]
extend (P _ n :: a
n _) t :: b
t sub :: [(a, b)]
sub = (a
n, b
t) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
sub
extend _ _ sub :: [(a, b)]
sub = [(a, b)]
sub
mkRHSargs :: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs ((ExplicitS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) as :: [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 ((ExplicitD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: PArg' PTerm
a : as :: [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 n :: Name
n, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: PArg' PTerm
a : as :: [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 n :: Name
n, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) as :: [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 ((ConstraintD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: PArg' PTerm
a : as :: [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 ((ConstraintS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) as :: [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 (_ : ns :: [(PEArgType, Term)]
ns) as :: [PArg' PTerm]
as = [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
mkRHSargs _ _ = []
mkPE_TermDecl :: IState
-> Name
-> Name
-> PTerm
-> [(PEArgType, Term)]
-> PEDecl
mkPE_TermDecl :: IState -> Name -> Name -> PTerm -> [(PEArgType, Term)] -> PEDecl
mkPE_TermDecl ist :: IState
ist newname :: Name
newname sname :: Name
sname specty :: PTerm
specty ns :: [(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
Nothing -> PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs [(PTerm
lhs, PTerm
rhs)] Bool
True
Just d :: ([([(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 (ps :: [(a, a, b)]
ps, _) = ((a, a, b) -> (a, b)) -> [(a, a, b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(_, lhs :: a
lhs, rhs :: b
rhs) -> (a
lhs, b
rhs)) [(a, a, b)]
ps
eraseRet :: PTerm -> PTerm
eraseRet (PPi p :: Plicity
p n :: Name
n fc :: FC
fc ty :: PTerm
ty sc :: PTerm
sc) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
ty (PTerm -> PTerm
eraseRet PTerm
sc)
eraseRet _ = PTerm
Placeholder
getDepNames :: PTerm -> [Name]
getDepNames (PPi _ n :: Name
n _ _ sc :: PTerm
sc)
| Name
n Name -> [Name] -> 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 tm :: PTerm
tm = []
mkp :: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [] = []
mkp ((ExplicitD, tm :: Term
tm) : tms :: [(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 n :: Name
n, tm :: Term
tm) : tms :: [(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 (_ : tms :: [(PEArgType, Term)]
tms) = [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms
eraseDeps :: t Name -> PTerm -> PTerm
eraseDeps ns :: t Name
ns tm :: 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 ns :: t Name
ns (PApp fc :: FC
fc t :: PTerm
t as :: [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 ns :: t Name
ns t :: PTerm
t = PTerm
t
deImpArg :: t Name -> PArg' PTerm -> PArg' PTerm
deImpArg ns :: t Name
ns a :: PArg' PTerm
a | PArg' PTerm -> Name
forall t. PArg' t -> Name
pname PArg' PTerm
a Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ns = PArg' PTerm
a { getTm :: PTerm
getTm = PTerm
Placeholder }
| Bool
otherwise = PArg' PTerm
a
getSpecApps :: IState
-> [Name]
-> Term
-> [(Name, [(PEArgType, Term)])]
getSpecApps :: IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])]
getSpecApps ist :: IState
ist env :: [Name]
env tm :: 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 env :: p
env True imp :: PArg' t
imp tm :: Term
tm n :: a
n
| Just n :: 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 env :: p
env False imp :: PArg' t
imp tm :: Term
tm n :: a
n
| Just nm :: 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]
++ "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]
++ "arg")) Term
forall n. TT n
Erased))
imparg :: PArg' t -> Maybe Name
imparg (PExp _ _ _ _) = Maybe Name
forall a. Maybe a
Nothing
imparg (PConstraint _ _ _ _) = Maybe Name
forall a. Maybe a
Nothing
imparg arg :: 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 _ _ _ _) = Bool
True
constrarg arg :: PArg' t
arg = Bool
False
buildApp :: p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp env :: p
env [] [] _ _ = []
buildApp env :: p
env (s :: Bool
s:ss :: [Bool]
ss) (i :: PArg' t
i:is :: [PArg' t]
is) (a :: Term
a:as :: [Term]
as) (n :: a
n:ns :: [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 env :: [Name]
env tm :: Term
tm@(App _ f :: Term
f a :: Term
a) | (P _ n :: Name
n _, args :: [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 statics :: [Bool]
statics, Just imps :: [PArg' PTerm]
imps) ->
if ([Bool] -> 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 (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 [0..] of
args :: [(PEArgType, Term)]
args -> [(Name
n, [(PEArgType, Term)]
args)]
else []
_ -> []
ga env :: [Name]
env (Bind n :: Name
n (Let rc :: RigCount
rc t :: Term
t v :: Term
v) sc :: 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 env :: [Name]
env (Bind n :: Name
n t :: Binder Term
t sc :: Term
sc) = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
ga env :: [Name]
env t :: Term
t = []
specialisable :: Context -> Name -> Bool
specialisable :: Context -> Name -> Bool
specialisable ctxt :: Context
ctxt n :: Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (CaseOp _ _ _ _ _ cds :: CaseDefs
cds) ->
SC -> Bool
noOverlap (([Name], SC) -> SC
forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cds))
_ -> Bool
False
noOverlap :: SC -> Bool
noOverlap :: SC -> Bool
noOverlap (Case _ _ [DefaultCase sc :: SC
sc]) = SC -> Bool
noOverlap SC
sc
noOverlap (Case _ _ alts :: [CaseAlt' Term]
alts) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
alts
noOverlap _ = Bool
True
noOverlapAlts :: [CaseAlt' Term] -> Bool
noOverlapAlts (ConCase _ _ _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest)
= [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
noOverlapAlts (FnCase _ _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest
noOverlapAlts (ConstCase _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest)
= [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
noOverlapAlts (SucCase _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest)
= [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
noOverlapAlts (DefaultCase _ : _) = Bool
False
noOverlapAlts _ = Bool
True