{-|
Module      : Idris.Transforms
Description : A collection of transformations.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# 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 -- not a clause, leave it alone
  tClause (Right (lhs :: a
lhs, rhs :: Term
rhs)) -- apply transforms on 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 -- not a clause, leave it alone
  tClause (Right (lhs :: a
lhs, rhs :: Term
rhs)) -- apply transforms on 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')

-- | Work on explicitly named terms, so we don't have to manipulate de
-- Bruijn indices
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)

-- | Work on explicitly named terms, so we don't have to manipulate de
-- Bruijn indices
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
--          = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
--                   "\n" ++ show rhs
--                   ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
          = 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
-- ASSUMPTION: The names in the transformation rule bindings cannot occur
-- in the term being transformed.
-- (In general, this would not be true, but when we elaborate transformation
-- rules we mangle the names so that it is true. While this feels a bit
-- hacky, it's much easier to think about than mangling de Bruijn indices).
  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 -- no occurrence? Shouldn't happen
        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
          = -- trace (show acc ++ ": " ++ show (sc, 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