module TPDB.Mirror where

import TPDB.Data
import TPDB.Convert

import Control.Monad ( forM, guard )

-- | if input is SRS, reverse lhs and rhs of each rule
mirror :: TRS Identifier s 
       -> Maybe ( TRS Identifier s )
mirror :: TRS Identifier s -> Maybe (TRS Identifier s)
mirror TRS Identifier s
trs = do
    [Rule (Term Identifier s)]
us <- [Rule (Term Identifier s)]
-> (Rule (Term Identifier s) -> Maybe (Rule (Term Identifier s)))
-> Maybe [Rule (Term Identifier s)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (TRS Identifier s -> [Rule (Term Identifier s)]
forall s r. RS s r -> [Rule r]
rules TRS Identifier s
trs) ((Rule (Term Identifier s) -> Maybe (Rule (Term Identifier s)))
 -> Maybe [Rule (Term Identifier s)])
-> (Rule (Term Identifier s) -> Maybe (Rule (Term Identifier s)))
-> Maybe [Rule (Term Identifier s)]
forall a b. (a -> b) -> a -> b
$ \ Rule (Term Identifier s)
u -> do
      ( [s]
left_spine, Identifier
left_base ) <- Term Identifier s -> Maybe ([s], Identifier)
forall v s. Term v s -> Maybe ([s], v)
spine (Term Identifier s -> Maybe ([s], Identifier))
-> Term Identifier s -> Maybe ([s], Identifier)
forall a b. (a -> b) -> a -> b
$ Rule (Term Identifier s) -> Term Identifier s
forall a. Rule a -> a
lhs Rule (Term Identifier s)
u
      ( [s]
right_spine, Identifier
right_base ) <- Term Identifier s -> Maybe ([s], Identifier)
forall v s. Term v s -> Maybe ([s], v)
spine (Term Identifier s -> Maybe ([s], Identifier))
-> Term Identifier s -> Maybe ([s], Identifier)
forall a b. (a -> b) -> a -> b
$ Rule (Term Identifier s) -> Term Identifier s
forall a. Rule a -> a
rhs Rule (Term Identifier s)
u
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Identifier
left_base Identifier -> Identifier -> Bool
forall a. Eq a => a -> a -> Bool
== Identifier
right_base 
      Rule (Term Identifier s) -> Maybe (Rule (Term Identifier s))
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term Identifier s) -> Maybe (Rule (Term Identifier s)))
-> Rule (Term Identifier s) -> Maybe (Rule (Term Identifier s))
forall a b. (a -> b) -> a -> b
$ Rule (Term Identifier s)
u { lhs :: Term Identifier s
lhs = Identifier -> [s] -> Term Identifier s
forall v s. v -> [s] -> Term v s
unspine Identifier
left_base ([s] -> Term Identifier s) -> [s] -> Term Identifier s
forall a b. (a -> b) -> a -> b
$ [s] -> [s]
forall a. [a] -> [a]
reverse [s]
left_spine
                 , rhs :: Term Identifier s
rhs = Identifier -> [s] -> Term Identifier s
forall v s. v -> [s] -> Term v s
unspine Identifier
right_base ([s] -> Term Identifier s) -> [s] -> Term Identifier s
forall a b. (a -> b) -> a -> b
$ [s] -> [s]
forall a. [a] -> [a]
reverse [s]
right_spine
                 }
    TRS Identifier s -> Maybe (TRS Identifier s)
forall (m :: * -> *) a. Monad m => a -> m a
return (TRS Identifier s -> Maybe (TRS Identifier s))
-> TRS Identifier s -> Maybe (TRS Identifier s)
forall a b. (a -> b) -> a -> b
$ TRS Identifier s
trs { rules :: [Rule (Term Identifier s)]
rules = [Rule (Term Identifier s)]
us }