{-# LANGUAGE PatternGuards #-}
module Idris.Transforms(
transformPats
, transformPatsWith
, applyTransRulesWith
, applyTransRules
) where
import Idris.AbsSyntax
import Idris.Core.TT
transformPats :: IState -> [Either Term (Term, Term)] ->
[Either Term (Term, Term)]
transformPats :: IState -> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
transformPats ist :: IState
ist ps :: [Either Term (Term, Term)]
ps = (Either Term (Term, Term) -> Either Term (Term, Term))
-> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map Either Term (Term, Term) -> Either Term (Term, Term)
forall a a. Either a (a, Term) -> Either a (a, Term)
tClause [Either Term (Term, Term)]
ps where
tClause :: Either a (a, Term) -> Either a (a, Term)
tClause (Left t :: a
t) = a -> Either a (a, Term)
forall a b. a -> Either a b
Left a
t
tClause (Right (lhs :: a
lhs, rhs :: Term
rhs))
= let rhs' :: Term
rhs' = IState -> Term -> Term
applyTransRules IState
ist Term
rhs in
(a, Term) -> Either a (a, Term)
forall a b. b -> Either a b
Right (a
lhs, Term
rhs')
transformPatsWith :: [(Term, Term)] -> [Either Term (Term, Term)] ->
[Either Term (Term, Term)]
transformPatsWith :: [(Term, Term)]
-> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
transformPatsWith rs :: [(Term, Term)]
rs ps :: [Either Term (Term, Term)]
ps = (Either Term (Term, Term) -> Either Term (Term, Term))
-> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map Either Term (Term, Term) -> Either Term (Term, Term)
forall a a. Either a (a, Term) -> Either a (a, Term)
tClause [Either Term (Term, Term)]
ps where
tClause :: Either a (a, Term) -> Either a (a, Term)
tClause (Left t :: a
t) = a -> Either a (a, Term)
forall a b. a -> Either a b
Left a
t
tClause (Right (lhs :: a
lhs, rhs :: Term
rhs))
= let rhs' :: Term
rhs' = [(Term, Term)] -> Term -> Term
applyTransRulesWith [(Term, Term)]
rs Term
rhs in
(a, Term) -> Either a (a, Term)
forall a b. b -> Either a b
Right (a
lhs, Term
rhs')
applyTransRules :: IState -> Term -> Term
applyTransRules :: IState -> Term -> Term
applyTransRules ist :: IState
ist tm :: Term
tm = Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [] (IState -> Ctxt [(Term, Term)]
idris_transforms IState
ist) (Term -> Term
forall n. TT n -> TT n
vToP Term
tm)
applyTransRulesWith :: [(Term, Term)] -> Term -> Term
applyTransRulesWith :: [(Term, Term)] -> Term -> Term
applyTransRulesWith rules :: [(Term, Term)]
rules tm :: Term
tm
= Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
rules Ctxt [(Term, Term)]
forall k a. Map k a
emptyContext (Term -> Term
forall n. TT n -> TT n
vToP Term
tm)
applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll extra :: [(Term, Term)]
extra ts :: Ctxt [(Term, Term)]
ts ap :: Term
ap@(App s :: AppStatus Name
s f :: Term
f a :: Term
a)
| (P _ fn :: Name
fn ty :: Term
ty, args :: [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap
= let rules :: [(Term, Term)]
rules = case Name -> Ctxt [(Term, Term)] -> Maybe [(Term, Term)]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
fn Ctxt [(Term, Term)]
ts of
Just r :: [(Term, Term)]
r -> [(Term, Term)]
extra [(Term, Term)] -> [(Term, Term)] -> [(Term, Term)]
forall a. [a] -> [a] -> [a]
++ [(Term, Term)]
r
Nothing -> [(Term, Term)]
extra
ap' :: Term
ap' = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s ([(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
f) ([(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
a) in
case [(Term, Term)]
rules of
[] -> Term
ap'
rs :: [(Term, Term)]
rs -> case [(Term, Term)] -> Term -> Maybe Term
applyFnRules [(Term, Term)]
rs Term
ap of
Just tm' :: Term
tm'@(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)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
f')
([(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
a')
Just tm' :: Term
tm' -> Term
tm'
_ -> AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s ([(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
f)
([(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
a)
applyAll extra :: [(Term, Term)]
extra ts :: Ctxt [(Term, Term)]
ts (Bind n :: Name
n b :: Binder Term
b sc :: Term
sc) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((Term -> Term) -> Binder Term -> Binder Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts) Binder Term
b)
([(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
applyAll [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
sc)
applyAll extra :: [(Term, Term)]
extra ts :: Ctxt [(Term, Term)]
ts t :: Term
t = Term
t
applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
applyFnRules [] tm :: Term
tm = Maybe Term
forall a. Maybe a
Nothing
applyFnRules (r :: (Term, Term)
r : rs :: [(Term, Term)]
rs) tm :: Term
tm | Just tm' :: Term
tm' <- (Term, Term) -> Term -> Maybe Term
applyRule (Term, Term)
r Term
tm = Term -> Maybe Term
forall a. a -> Maybe a
Just Term
tm'
| Bool
otherwise = [(Term, Term)] -> Term -> Maybe Term
applyFnRules [(Term, Term)]
rs Term
tm
applyRule :: (Term, Term) -> Term -> Maybe Term
applyRule :: (Term, Term) -> Term -> Maybe Term
applyRule (lhs :: Term
lhs, rhs :: Term
rhs) tm :: Term
tm
| Just ms :: [(Name, Term)]
ms <- Term -> Term -> Maybe [(Name, Term)]
matchTerm Term
lhs Term
tm
= Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ [(Name, Term)] -> Term -> Term
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
depat [(Name, Term)]
ms Term
rhs
| Bool
otherwise = Maybe Term
forall a. Maybe a
Nothing
where depat :: [(n, TT n)] -> TT n -> TT n
depat ms :: [(n, TT n)]
ms (Bind n :: n
n (PVar _ t :: TT n
t) sc :: TT n
sc)
= case n -> [(n, TT n)] -> Maybe (TT n)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup n
n [(n, TT n)]
ms of
Just tm :: TT n
tm -> [(n, TT n)] -> TT n -> TT n
depat [(n, TT n)]
ms (n -> TT n -> TT n -> TT n
forall n. Eq n => n -> TT n -> TT n -> TT n
subst n
n TT n
tm TT n
sc)
_ -> [(n, TT n)] -> TT n -> TT n
depat [(n, TT n)]
ms TT n
sc
depat ms :: [(n, TT n)]
ms tm :: TT n
tm = TT n
tm
matchTerm :: Term -> Term -> Maybe [(Name, Term)]
matchTerm :: Term -> Term -> Maybe [(Name, Term)]
matchTerm lhs :: Term
lhs tm :: Term
tm = [Name] -> Term -> Term -> Maybe [(Name, Term)]
matchVars [] Term
lhs Term
tm
where
matchVars :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
matchVars acc :: [Name]
acc (Bind n :: Name
n (PVar _ t :: Term
t) sc :: Term
sc) tm :: Term
tm
= [Name] -> Term -> Term -> Maybe [(Name, Term)]
matchVars (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
acc) (Term -> Term -> Term
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
t) Term
sc) Term
tm
matchVars acc :: [Name]
acc sc :: Term
sc tm :: Term
tm
=
[Name] -> Term -> Term -> Maybe [(Name, Term)]
doMatch [Name]
acc Term
sc Term
tm
doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
doMatch ns :: [Name]
ns (P _ n :: Name
n _) tm :: Term
tm
| Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns = [(Name, Term)] -> Maybe [(Name, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name
n, Term
tm)]
doMatch ns :: [Name]
ns (App _ f :: Term
f a :: Term
a) (App _ f' :: Term
f' a' :: Term
a')
= do [(Name, Term)]
fm <- [Name] -> Term -> Term -> Maybe [(Name, Term)]
doMatch [Name]
ns Term
f Term
f'
[(Name, Term)]
am <- [Name] -> Term -> Term -> Maybe [(Name, Term)]
doMatch [Name]
ns Term
a Term
a'
[(Name, Term)] -> Maybe [(Name, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Term)]
fm [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
am)
doMatch ns :: [Name]
ns x :: Term
x y :: Term
y | Term -> Term
forall n. TT n -> TT n
vToP Term
x Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term -> Term
forall n. TT n -> TT n
vToP Term
y = [(Name, Term)] -> Maybe [(Name, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = Maybe [(Name, Term)]
forall a. Maybe a
Nothing