{-|
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 IState
ist [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 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 (a
lhs, 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 [(Term, Term)]
rs [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 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 (a
lhs, 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 IState
ist 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 [(Term, Term)]
rules 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 [(Term, Term)]
extra Ctxt [(Term, Term)]
ts ap :: Term
ap@(App AppStatus Name
s Term
f Term
a)
    | (P NameType
_ Name
fn Term
ty, [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 [(Term, Term)]
r -> [(Term, Term)]
extra [(Term, Term)] -> [(Term, Term)] -> [(Term, Term)]
forall a. [a] -> [a] -> [a]
++ [(Term, Term)]
r
                            Maybe [(Term, Term)]
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'
                    [(Term, Term)]
rs -> case [(Term, Term)] -> Term -> Maybe Term
applyFnRules [(Term, Term)]
rs Term
ap of
                                   Just tm' :: Term
tm'@(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)] -> 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 Term
tm' -> Term
tm'
                                   Maybe Term
_ -> 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 [(Term, Term)]
extra Ctxt [(Term, Term)]
ts (Bind Name
n Binder Term
b 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 [(Term, Term)]
extra Ctxt [(Term, Term)]
ts Term
t = Term
t

applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
applyFnRules [] Term
tm = Maybe Term
forall a. Maybe a
Nothing
applyFnRules ((Term, Term)
r : [(Term, Term)]
rs) Term
tm | Just 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 (Term
lhs, Term
rhs) Term
tm
    | Just [(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 [(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 -- no occurrence? Shouldn't happen
        depat [(n, TT n)]
ms TT n
tm = TT n
tm

matchTerm :: Term -> Term -> Maybe [(Name, Term)]
matchTerm :: Term -> Term -> Maybe [(Name, Term)]
matchTerm Term
lhs Term
tm = [Name] -> Term -> Term -> Maybe [(Name, Term)]
matchVars [] Term
lhs Term
tm
   where
      matchVars :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
matchVars [Name]
acc (Bind Name
n (PVar RigCount
_ Term
t) Term
sc) 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 [Name]
acc Term
sc 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 [Name]
ns (P NameType
_ Name
n Term
_) 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 [Name]
ns (App AppStatus Name
_ Term
f Term
a) (App AppStatus Name
_ Term
f' 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 [Name]
ns Term
x 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