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

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

-- | Work on explicitly named terms, so we don't have to manipulate de
-- Bruijn indices
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
--          = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
--                   "\n" ++ show rhs
--                   ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
          = 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
-- 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 :: 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
          = -- trace (show acc ++ ": " ++ show (sc, 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