{-# 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 :: Bool
separate = Bool
False
              , rules :: [Rule (Term Identifier Identifier)]
rules = (Rule [Identifier] -> Rule (Term Identifier Identifier))
-> [Rule [Identifier]] -> [Rule (Term Identifier Identifier)]
forall a b. (a -> b) -> [a] -> [b]
map Rule [Identifier] -> Rule (Term Identifier Identifier)
convert_srs_rule ([Rule [Identifier]] -> [Rule (Term Identifier Identifier)])
-> [Rule [Identifier]] -> [Rule (Term Identifier Identifier)]
forall a b. (a -> b) -> a -> b
$ SRS Identifier -> [Rule [Identifier]]
forall s r. RS s r -> [Rule r]
rules SRS Identifier
s
              , signature :: [Identifier]
signature = (Identifier -> Identifier) -> [Identifier] -> [Identifier]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Identifier -> Identifier
set_arity Int
1) ([Identifier] -> [Identifier]) -> [Identifier] -> [Identifier]
forall a b. (a -> b) -> a -> b
$ SRS Identifier -> [Identifier]
forall s r. RS s r -> [s]
signature SRS Identifier
s
              }

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

convert_srs_rule :: Rule [Identifier] -> Rule (Term Identifier Identifier)
convert_srs_rule Rule [Identifier]
u =
    let v :: Identifier
v = Int -> Text -> Identifier
mk Int
0 Text
"x"
        handle :: [Identifier] -> Term Identifier Identifier
handle = Identifier -> [Identifier] -> Term Identifier Identifier
forall v s. 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 :: Term Identifier Identifier
lhs = [Identifier] -> Term Identifier Identifier
handle ([Identifier] -> Term Identifier Identifier)
-> [Identifier] -> Term Identifier Identifier
forall a b. (a -> b) -> a -> b
$ Rule [Identifier] -> [Identifier]
forall a. Rule a -> a
lhs Rule [Identifier]
u
          , rhs :: Term Identifier Identifier
rhs = [Identifier] -> Term Identifier Identifier
handle ([Identifier] -> Term Identifier Identifier)
-> [Identifier] -> Term Identifier Identifier
forall a b. (a -> b) -> a -> b
$ Rule [Identifier] -> [Identifier]
forall a. Rule a -> a
rhs Rule [Identifier]
u
          }

trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )
trs2srs :: 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])
forall a s. Eq a => Rule (Term a s) -> Maybe (Rule [s])
convert_trs_rule
    SRS s -> Maybe (SRS s)
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 :: Bool
separate = Bool
True , rules :: [Rule [s]]
rules = [Rule [s]]
us }

convert_trs_rule :: Rule (Term a s) -> Maybe (Rule [s])
convert_trs_rule Rule (Term a s)
u = do
      ( [s]
left_spine, a
left_base ) <- Term a s -> Maybe ([s], a)
forall v s. Term v s -> Maybe ([s], v)
spine (Term a s -> Maybe ([s], a)) -> Term a s -> Maybe ([s], a)
forall a b. (a -> b) -> a -> b
$ Rule (Term a s) -> Term a s
forall a. Rule a -> a
lhs Rule (Term a s)
u
      ( [s]
right_spine, a
right_base ) <- Term a s -> Maybe ([s], a)
forall v s. Term v s -> Maybe ([s], v)
spine (Term a s -> Maybe ([s], a)) -> Term a s -> Maybe ([s], a)
forall a b. (a -> b) -> a -> b
$ Rule (Term a s) -> Term a s
forall a. Rule a -> a
rhs Rule (Term a s)
u
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ a
left_base a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
right_base
      Rule [s] -> Maybe (Rule [s])
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 a s)
u { lhs :: [s]
lhs = [s]
left_spine, rhs :: [s]
rhs = [s]
right_spine }

unspine :: v -> [s] -> Term v s
unspine :: v -> [s] -> Term v s
unspine v
v = (s -> Term v s -> Term v s) -> Term v s -> [s] -> Term v s
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 :: Term v s -> Maybe ( [s], v )
spine :: 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 (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. Term v s -> Maybe ([s], v)
spine Term v s
arg
      ([s], v) -> Maybe ([s], v)
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 (m :: * -> *) a. Monad m => a -> m a
return ( [] , v
v )