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 :: (Eq v, TermC v s)
  => TRS v  s 
       -> Maybe ( TRS v s )
mirror :: forall v s. (Eq v, TermC v s) => TRS v s -> Maybe (TRS v s)
mirror TRS v s
trs = do
    [Rule (Term v s)]
us <- [Rule (Term v s)]
-> (Rule (Term v s) -> Maybe (Rule (Term v s)))
-> Maybe [Rule (Term v s)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (TRS v s -> [Rule (Term v s)]
forall s r. RS s r -> [Rule r]
rules TRS v s
trs) ((Rule (Term v s) -> Maybe (Rule (Term v s)))
 -> Maybe [Rule (Term v s)])
-> (Rule (Term v s) -> Maybe (Rule (Term v s)))
-> Maybe [Rule (Term v s)]
forall a b. (a -> b) -> a -> b
$ \ Rule (Term v s)
u -> do
      ( [s]
left_spine, v
left_base ) <- Term v s -> Maybe ([s], v)
forall v s. TermC v s => Term v s -> Maybe ([s], v)
spine (Term v s -> Maybe ([s], v)) -> Term v s -> Maybe ([s], v)
forall a b. (a -> b) -> a -> b
$ Rule (Term v s) -> Term v s
forall a. Rule a -> a
lhs Rule (Term v s)
u
      ( [s]
right_spine, v
right_base ) <- Term v s -> Maybe ([s], v)
forall v s. TermC v s => Term v s -> Maybe ([s], v)
spine (Term v s -> Maybe ([s], v)) -> Term v s -> Maybe ([s], v)
forall a b. (a -> b) -> a -> b
$ Rule (Term v s) -> Term v s
forall a. Rule a -> a
rhs Rule (Term v s)
u
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ v
left_base v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
right_base 
      Rule (Term v s) -> Maybe (Rule (Term v s))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term v s) -> Maybe (Rule (Term v s)))
-> Rule (Term v s) -> Maybe (Rule (Term v s))
forall a b. (a -> b) -> a -> b
$ Rule (Term v s)
u { lhs = unspine left_base $ reverse left_spine
                 , rhs = unspine right_base $ reverse right_spine
                 }
    TRS v s -> Maybe (TRS v s)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TRS v s -> Maybe (TRS v s)) -> TRS v s -> Maybe (TRS v s)
forall a b. (a -> b) -> a -> b
$ TRS v s
trs { rules = us }