{-# language OverloadedStrings #-}

module TPDB.Convert where

import TPDB.Data
import Control.Monad ( forM, guard )

srs2trs :: SRS Identifier -> TRS Identifier Identifier
srs2trs :: SRS Identifier -> TRS Identifier Identifier
srs2trs SRS Identifier
s = SRS Identifier
s { separate = False
              , rules = map convert_srs_rule $ rules s
              , signature = map (set_arity 1) $ signature s
              }

set_arity :: Int -> Identifier -> Identifier
set_arity Int
a Identifier
s = Identifier
s { arity = a }

convert_srs_rule :: Rule [Identifier] -> Rule (Term Identifier Identifier)
convert_srs_rule Rule [Identifier]
u =
    let v :: Identifier
v = case Rule [Identifier] -> Maybe Identifier
forall a. Rule a -> Maybe Identifier
original_variable Rule [Identifier]
u of
          Maybe Identifier
Nothing -> Int -> Text -> Identifier
mk Int
0 Text
"x" -- RISKY
          Just Identifier
v -> Identifier
v
        handle :: [Identifier] -> Term Identifier Identifier
handle = Identifier -> [Identifier] -> Term Identifier Identifier
forall v s. (() :: Constraint) => v -> [s] -> Term v s
unspine Identifier
v ([Identifier] -> Term Identifier Identifier)
-> ([Identifier] -> [Identifier])
-> [Identifier]
-> Term Identifier Identifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Identifier -> Identifier) -> [Identifier] -> [Identifier]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Identifier -> Identifier
set_arity Int
1)
    in  Rule [Identifier]
u { lhs = handle $ lhs u
          , rhs = handle $ rhs u
          }

trs2srs :: (Eq v, TermC v s, v ~ Identifier) => TRS v s -> Maybe ( SRS s )
trs2srs :: forall v s.
(Eq v, () :: Constraint, v ~ Identifier) =>
TRS v s -> Maybe (SRS s)
trs2srs TRS v s
t = do
    [Rule [s]]
us <- [Rule (Term v s)]
-> (Rule (Term v s) -> Maybe (Rule [s])) -> Maybe [Rule [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
t ) Rule (Term v s) -> Maybe (Rule [s])
Rule (Term Identifier s) -> Maybe (Rule [s])
forall {s}. Rule (Term Identifier s) -> Maybe (Rule [s])
convert_trs_rule
    SRS s -> Maybe (SRS s)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SRS s -> Maybe (SRS s)) -> SRS s -> Maybe (SRS s)
forall a b. (a -> b) -> a -> b
$ TRS v s
t { separate = True , rules = us }

convert_trs_rule :: Rule (Term Identifier s) -> Maybe (Rule [s])
convert_trs_rule Rule (Term Identifier s)
u = do
      ( [s]
left_spine, Identifier
left_base ) <- Term Identifier s -> Maybe ([s], Identifier)
forall v s. (() :: Constraint) => 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. (() :: Constraint) => 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 [s] -> Maybe (Rule [s])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule [s] -> Maybe (Rule [s])) -> Rule [s] -> Maybe (Rule [s])
forall a b. (a -> b) -> a -> b
$ Rule (Term Identifier s)
u
        { lhs = left_spine, rhs = right_spine
        , original_variable = Just left_base
        }

unspine :: TermC v s => v -> [s] -> Term v s
unspine :: forall v s. (() :: Constraint) => v -> [s] -> Term v s
unspine v
v = (s -> Term v s -> Term v s) -> Term v s -> [s] -> Term v s
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (  \ s
c Term v s
t -> s -> [Term v s] -> Term v s
forall v s. s -> [Term v s] -> Term v s
Node s
c [ Term v s
t ] ) ( v -> Term v s
forall v s. v -> Term v s
Var v
v )

-- | success iff term consists of unary symbols
-- and the lowest node is a variable
spine :: TermC v s => Term v s -> Maybe ( [s], v )
spine :: forall v s. (() :: Constraint) => Term v s -> Maybe ([s], v)
spine Term v s
t = case Term v s
t of
    Node s
f [Term v s]
args -> do
      [ Term v s
arg ] <- [Term v s] -> Maybe [Term v s]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Term v s]
args
      ( [s]
sp, v
base ) <- Term v s -> Maybe ([s], v)
forall v s. (() :: Constraint) => Term v s -> Maybe ([s], v)
spine Term v s
arg
      ([s], v) -> Maybe ([s], v)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ( s
f s -> [s] -> [s]
forall a. a -> [a] -> [a]
: [s]
sp, v
base )
    Var v
v -> ([s], v) -> Maybe ([s], v)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [] , v
v )