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