-- | textual input,
-- cf. <http://www.lri.fr/~marche/tpdb/format.html>

{-# language PatternSignatures, TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-}

module TPDB.Plain.Read where

import TPDB.Data

import Text.Parsec (parse)

import qualified Data.Text.Lazy as T

import Text.Parsec.Text.Lazy as P
import Text.Parsec.Token
import Text.Parsec.Language
import Text.Parsec.Char
import Control.Applicative
-- import Text.Parsec.Combinator
import Data.Functor.Identity (Identity)

import TPDB.Pretty (pretty)
import TPDB.Plain.Write ()
import Data.Text ()
import Data.String (fromString)

import Control.Monad ( guard, void )
import Data.List ( nub )

trs :: T.Text -> Either String ( TRS Identifier Identifier )
trs :: Text -> Either String (TRS Identifier Identifier)
trs Text
s = case Parsec Text () (TRS Identifier Identifier)
-> String -> Text -> Either ParseError (TRS Identifier Identifier)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
Text.Parsec.parse Parsec Text () (TRS Identifier Identifier)
forall a. Reader a => Parser a
reader String
"input" Text
s of
    Left ParseError
err -> String -> Either String (TRS Identifier Identifier)
forall a b. a -> Either a b
Left (String -> Either String (TRS Identifier Identifier))
-> String -> Either String (TRS Identifier Identifier)
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
err
    Right TRS Identifier Identifier
t  -> TRS Identifier Identifier
-> Either String (TRS Identifier Identifier)
forall a b. b -> Either a b
Right TRS Identifier Identifier
t

srs :: T.Text -> Either String ( SRS Identifier )
srs :: Text -> Either String (SRS Identifier)
srs Text
s = case Parsec Text () (SRS Identifier)
-> String -> Text -> Either ParseError (SRS Identifier)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
Text.Parsec.parse Parsec Text () (SRS Identifier)
forall a. Reader a => Parser a
reader String
"input" Text
s of
    Left ParseError
err -> String -> Either String (SRS Identifier)
forall a b. a -> Either a b
Left (String -> Either String (SRS Identifier))
-> String -> Either String (SRS Identifier)
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
err
    Right SRS Identifier
t  -> SRS Identifier -> Either String (SRS Identifier)
forall a b. b -> Either a b
Right SRS Identifier
t

-- type Parser = Parsec ByteString () 

class Reader a where reader :: P.Parser a

-- | warning: by definition, {}[] may appear in identifiers
lexer :: GenTokenParser T.Text () Identity
lexer :: GenTokenParser Text () Identity
lexer = GenLanguageDef Text () Identity -> GenTokenParser Text () Identity
forall s (m :: * -> *) u.
Stream s m Char =>
GenLanguageDef s u m -> GenTokenParser s u m
makeTokenParser
    (GenLanguageDef Text () Identity
 -> GenTokenParser Text () Identity)
-> GenLanguageDef Text () Identity
-> GenTokenParser Text () Identity
forall a b. (a -> b) -> a -> b
$ LanguageDef
       { nestedComments :: Bool
nestedComments = Bool
True
       , opStart :: ParsecT Text () Identity Char
opStart        = String -> ParsecT Text () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
":!#$%&*+./<=>?@\\^|-~"
       , opLetter :: ParsecT Text () Identity Char
opLetter       = String -> ParsecT Text () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
":!#$%&*+./<=>?@\\^|-~"
       , reservedOpNames :: [String]
reservedOpNames = []
       , caseSensitive :: Bool
caseSensitive  = Bool
True
       , identStart :: ParsecT Text () Identity Char
identStart  = ParsecT Text () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT Text () Identity Char
-> ParsecT Text () Identity Char -> ParsecT Text () Identity Char
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> ParsecT Text () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
"_:!#$%&*+./<=>?@\\^|-~{}[]'"
       , identLetter :: ParsecT Text () Identity Char
identLetter = ParsecT Text () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT Text () Identity Char
-> ParsecT Text () Identity Char -> ParsecT Text () Identity Char
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> ParsecT Text () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
"_:!#$%&*+./<=>?@\\^|-~{}[]'"
       , commentLine :: String
commentLine = String
"" , commentStart :: String
commentStart = String
"" , commentEnd :: String
commentEnd = String
""
       , reservedNames :: [String]
reservedNames = [ String
"VAR", String
"THEORY", String
"STRATEGY", String
"RULES", String
"->", String
"->=" ]
       }

instance Reader Identifier where 
    reader :: Parser Identifier
reader = do
        String
i :: String <- GenTokenParser Text () Identity -> ParsecT Text () Identity String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
identifier GenTokenParser Text () Identity
lexer 
        Identifier -> Parser Identifier
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Identifier -> Parser Identifier)
-> Identifier -> Parser Identifier
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Identifier
mk Int
0 (Text -> Identifier) -> Text -> Identifier
forall a b. (a -> b) -> a -> b
$ String -> Text
forall a. IsString a => String -> a
fromString String
i

instance Reader s =>  Reader [s] where
    reader :: Parser [s]
reader = ParsecT Text () Identity s -> Parser [s]
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ParsecT Text () Identity s
forall a. Reader a => Parser a
reader

-- NOTE: this is dangerous since we read the variables as constants,
-- and this needs to be patched up later.
-- NOTE: this is more dangerous as we do not set the arity of identifiers
instance ( TermC v Identifier, Reader v ) => Reader ( Term v Identifier ) where
    reader :: Parser (Term v Identifier)
reader = do
        Identifier
f  <- Parser Identifier
forall a. Reader a => Parser a
reader 
        [Term v Identifier]
xs <- ( GenTokenParser Text () Identity
-> forall a.
   ParsecT Text () Identity a -> ParsecT Text () Identity a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
parens GenTokenParser Text () Identity
lexer (ParsecT Text () Identity [Term v Identifier]
 -> ParsecT Text () Identity [Term v Identifier])
-> ParsecT Text () Identity [Term v Identifier]
-> ParsecT Text () Identity [Term v Identifier]
forall a b. (a -> b) -> a -> b
$ GenTokenParser Text () Identity
-> forall a.
   ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m [a]
commaSep GenTokenParser Text () Identity
lexer Parser (Term v Identifier)
forall a. Reader a => Parser a
reader ) ParsecT Text () Identity [Term v Identifier]
-> ParsecT Text () Identity [Term v Identifier]
-> ParsecT Text () Identity [Term v Identifier]
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term v Identifier] -> ParsecT Text () Identity [Term v Identifier]
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Term v Identifier -> Parser (Term v Identifier)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term v Identifier -> Parser (Term v Identifier))
-> Term v Identifier -> Parser (Term v Identifier)
forall a b. (a -> b) -> a -> b
$ Identifier -> [Term v Identifier] -> Term v Identifier
forall v s. s -> [Term v s] -> Term v s
Node ( Identifier
f { arity = Prelude.length xs } ) [Term v Identifier]
xs

instance Reader u => Reader ( Rule u ) where
    reader :: Parser (Rule u)
reader = do
        u
l <- Parser u
forall a. Reader a => Parser a
reader
        Relation
rel <-  do GenTokenParser Text () Identity
-> String -> ParsecT Text () Identity ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser Text () Identity
lexer String
"->"  ; Relation -> ParsecT Text () Identity Relation
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Relation
Strict
          ParsecT Text () Identity Relation
-> ParsecT Text () Identity Relation
-> ParsecT Text () Identity Relation
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do GenTokenParser Text () Identity
-> String -> ParsecT Text () Identity ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser Text () Identity
lexer String
"->=" ; Relation -> ParsecT Text () Identity Relation
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Relation
Weak
          -- FIXME: for the moment, we do not parse this
          -- as it would deviate from published TPDB syntax
          -- <|> do reservedOp lexer "=" ; return Equal
        u
r <- Parser u
forall a. Reader a => Parser a
reader
        Rule u -> Parser (Rule u)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule u -> Parser (Rule u)) -> Rule u -> Parser (Rule u)
forall a b. (a -> b) -> a -> b
$ Rule { lhs :: u
lhs = u
l, relation :: Relation
relation = Relation
rel, top :: Bool
top = Bool
False, rhs :: u
rhs = u
r
                      , original_variable :: Maybe Identifier
original_variable = Maybe Identifier
forall a. Maybe a
Nothing
                      }

data Declaration u
     = Var_Declaration [ Identifier ]
     | Theory_Declaration 
     | Strategy_Declaration 
     | Rules_Declaration [ Rule u ]
     | Unknown_Declaration
       -- ^ this is super-ugly: a parenthesized, possibly nested, 
       -- possibly comma-separated, list of identifiers or strings

declaration :: Reader u => Bool -> P.Parser ( Declaration u )
declaration :: forall u. Reader u => Bool -> Parser (Declaration u)
declaration Bool
sep = GenTokenParser Text () Identity
-> forall a.
   ParsecT Text () Identity a -> ParsecT Text () Identity a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
parens GenTokenParser Text () Identity
lexer (ParsecT Text () Identity (Declaration u)
 -> ParsecT Text () Identity (Declaration u))
-> ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
forall a b. (a -> b) -> a -> b
$ 
           do GenTokenParser Text () Identity
-> String -> ParsecT Text () Identity ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser Text () Identity
lexer String
"VAR" ; [Identifier]
xs <- Parser Identifier -> ParsecT Text () Identity [Identifier]
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser Identifier
forall a. Reader a => Parser a
reader 
              Declaration u -> ParsecT Text () Identity (Declaration u)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Declaration u -> ParsecT Text () Identity (Declaration u))
-> Declaration u -> ParsecT Text () Identity (Declaration u)
forall a b. (a -> b) -> a -> b
$ [Identifier] -> Declaration u
forall u. [Identifier] -> Declaration u
Var_Declaration [Identifier]
xs
       ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do GenTokenParser Text () Identity
-> String -> ParsecT Text () Identity ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser Text () Identity
lexer String
"THEORY" 
              String -> ParsecT Text () Identity (Declaration u)
forall a. HasCallStack => String -> a
error String
"TPDB.Plain.Read: parser for THEORY decl. missing"
       ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do GenTokenParser Text () Identity
-> String -> ParsecT Text () Identity ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser Text () Identity
lexer String
"STRATEGY" 
              String -> ParsecT Text () Identity (Declaration u)
forall a. HasCallStack => String -> a
error String
"TPDB.Plain.Read: parser for THEORY decl. missing"
       ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do GenTokenParser Text () Identity
-> String -> ParsecT Text () Identity ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser Text () Identity
lexer String
"RULES" 
              [Rule u]
us <- if Bool
sep then do 
                        ParsecT Text () Identity (Rule u)
-> ParsecT Text () Identity [Rule u]
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (ParsecT Text () Identity (Rule u)
 -> ParsecT Text () Identity [Rule u])
-> ParsecT Text () Identity (Rule u)
-> ParsecT Text () Identity [Rule u]
forall a b. (a -> b) -> a -> b
$ do 
                            Rule u
u <- ParsecT Text () Identity (Rule u)
forall a. Reader a => Parser a
reader ; ParsecT Text () Identity String
-> ParsecT Text () Identity (Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (ParsecT Text () Identity String
 -> ParsecT Text () Identity (Maybe String))
-> ParsecT Text () Identity String
-> ParsecT Text () Identity (Maybe String)
forall a b. (a -> b) -> a -> b
$ GenTokenParser Text () Identity -> ParsecT Text () Identity String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
comma GenTokenParser Text () Identity
lexer
                            Rule u -> ParsecT Text () Identity (Rule u)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Rule u
u
                        -- yes, TPDB contains some trailing commas, e.g., z008
                        -- ( RULES a b -> b a , )
                    else ParsecT Text () Identity (Rule u)
-> ParsecT Text () Identity [Rule u]
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ParsecT Text () Identity (Rule u)
forall a. Reader a => Parser a
reader
              Declaration u -> ParsecT Text () Identity (Declaration u)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Declaration u -> ParsecT Text () Identity (Declaration u))
-> Declaration u -> ParsecT Text () Identity (Declaration u)
forall a b. (a -> b) -> a -> b
$ [Rule u] -> Declaration u
forall u. [Rule u] -> Declaration u
Rules_Declaration [Rule u]
us
       ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
-> ParsecT Text () Identity (Declaration u)
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do ParsecT Text () Identity ()
anylist ; Declaration u -> ParsecT Text () Identity (Declaration u)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration u
forall u. Declaration u
Unknown_Declaration

anylist :: ParsecT Text () Identity ()
anylist = ParsecT Text () Identity [[()]] -> ParsecT Text () Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void 
        (ParsecT Text () Identity [[()]] -> ParsecT Text () Identity ())
-> ParsecT Text () Identity [[()]] -> ParsecT Text () Identity ()
forall a b. (a -> b) -> a -> b
$ GenTokenParser Text () Identity
-> forall a.
   ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m [a]
commaSep GenTokenParser Text () Identity
lexer 
        (ParsecT Text () Identity [()] -> ParsecT Text () Identity [[()]])
-> ParsecT Text () Identity [()] -> ParsecT Text () Identity [[()]]
forall a b. (a -> b) -> a -> b
$ ParsecT Text () Identity () -> ParsecT Text () Identity [()]
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ( ParsecT Text () Identity String -> ParsecT Text () Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ( GenTokenParser Text () Identity -> ParsecT Text () Identity String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
identifier GenTokenParser Text () Identity
lexer ) ParsecT Text () Identity ()
-> ParsecT Text () Identity () -> ParsecT Text () Identity ()
forall a.
ParsecT Text () Identity a
-> ParsecT Text () Identity a -> ParsecT Text () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> GenTokenParser Text () Identity
-> forall a.
   ParsecT Text () Identity a -> ParsecT Text () Identity a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
parens GenTokenParser Text () Identity
lexer ParsecT Text () Identity ()
anylist )

instance Reader ( SRS Identifier ) where
    reader :: Parsec Text () (SRS Identifier)
reader = do 
        ParsecT Text () Identity Char -> ParsecT Text () Identity String
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ParsecT Text () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space
        [Declaration [Identifier]]
ds <- ParsecT Text () Identity (Declaration [Identifier])
-> ParsecT Text () Identity [Declaration [Identifier]]
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (ParsecT Text () Identity (Declaration [Identifier])
 -> ParsecT Text () Identity [Declaration [Identifier]])
-> ParsecT Text () Identity (Declaration [Identifier])
-> ParsecT Text () Identity [Declaration [Identifier]]
forall a b. (a -> b) -> a -> b
$ Bool -> ParsecT Text () Identity (Declaration [Identifier])
forall u. Reader u => Bool -> Parser (Declaration u)
declaration Bool
True
        SRS Identifier -> Parsec Text () (SRS Identifier)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SRS Identifier -> Parsec Text () (SRS Identifier))
-> SRS Identifier -> Parsec Text () (SRS Identifier)
forall a b. (a -> b) -> a -> b
$ [Declaration [Identifier]] -> SRS Identifier
forall s. Eq s => [Declaration [s]] -> SRS s
make_srs [Declaration [Identifier]]
ds

instance Reader ( TRS Identifier Identifier ) where
    reader :: Parsec Text () (TRS Identifier Identifier)
reader = do
        ParsecT Text () Identity Char -> ParsecT Text () Identity String
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ParsecT Text () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space
        [Declaration (Term Identifier Identifier)]
ds <- ParsecT Text () Identity (Declaration (Term Identifier Identifier))
-> ParsecT
     Text () Identity [Declaration (Term Identifier Identifier)]
forall a.
ParsecT Text () Identity a -> ParsecT Text () Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (ParsecT
   Text () Identity (Declaration (Term Identifier Identifier))
 -> ParsecT
      Text () Identity [Declaration (Term Identifier Identifier)])
-> ParsecT
     Text () Identity (Declaration (Term Identifier Identifier))
-> ParsecT
     Text () Identity [Declaration (Term Identifier Identifier)]
forall a b. (a -> b) -> a -> b
$ Bool
-> ParsecT
     Text () Identity (Declaration (Term Identifier Identifier))
forall u. Reader u => Bool -> Parser (Declaration u)
declaration Bool
False
        TRS Identifier Identifier
-> Parsec Text () (TRS Identifier Identifier)
forall a. a -> ParsecT Text () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TRS Identifier Identifier
 -> Parsec Text () (TRS Identifier Identifier))
-> TRS Identifier Identifier
-> Parsec Text () (TRS Identifier Identifier)
forall a b. (a -> b) -> a -> b
$ [Declaration (Term Identifier Identifier)]
-> TRS Identifier Identifier
make_trs [Declaration (Term Identifier Identifier)]
ds

repair_signature_srs :: RS s [s] -> RS s [s]
repair_signature_srs RS s [s]
sys = 
    let sig :: [s]
sig = [s] -> [s]
forall a. Eq a => [a] -> [a]
nub ([s] -> [s]) -> [s] -> [s]
forall a b. (a -> b) -> a -> b
$ do Rule [s]
u <- RS s [s] -> [Rule [s]]
forall s r. RS s r -> [Rule r]
rules RS s [s]
sys ; Rule [s] -> [s]
forall a. Rule a -> a
lhs Rule [s]
u [s] -> [s] -> [s]
forall a. [a] -> [a] -> [a]
++ Rule [s] -> [s]
forall a. Rule a -> a
rhs Rule [s]
u
    in  RS s [s]
sys { signature = sig }

make_srs :: Eq s => [ Declaration [s] ] -> SRS s
make_srs :: forall s. Eq s => [Declaration [s]] -> SRS s
make_srs [Declaration [s]]
ds = RS Any [s] -> RS s [s]
forall {s} {s}. Eq s => RS s [s] -> RS s [s]
repair_signature_srs (RS Any [s] -> RS s [s]) -> RS Any [s] -> RS s [s]
forall a b. (a -> b) -> a -> b
$
    let us :: [Rule [s]]
us = do Rules_Declaration [Rule [s]]
us <- [Declaration [s]]
ds ; [Rule [s]]
us        
    in  RS { rules :: [Rule [s]]
rules = [Rule [s]]
us, separate :: Bool
separate = Bool
True }

repair_signature_trs :: RS s (Term v s) -> RS s (Term v s)
repair_signature_trs RS s (Term v s)
sys = 
    let sig :: [s]
sig = [s] -> [s]
forall a. Eq a => [a] -> [a]
nub ([s] -> [s]) -> [s] -> [s]
forall a b. (a -> b) -> a -> b
$ do Rule (Term v s)
u <- RS s (Term v s) -> [Rule (Term v s)]
forall s r. RS s r -> [Rule r]
rules RS s (Term v s)
sys ; Term v s -> [s]
forall c v. (Ord c, TermC v Identifier) => Term v c -> [c]
lsyms ( Rule (Term v s) -> Term v s
forall a. Rule a -> a
lhs Rule (Term v s)
u ) [s] -> [s] -> [s]
forall a. [a] -> [a] -> [a]
++ Term v s -> [s]
forall c v. (Ord c, TermC v Identifier) => Term v c -> [c]
lsyms ( Rule (Term v s) -> Term v s
forall a. Rule a -> a
rhs Rule (Term v s)
u)
    in  RS s (Term v s)
sys { signature = sig }

make_trs :: [ Declaration ( Term Identifier Identifier ) ] 
         -> TRS Identifier Identifier
make_trs :: [Declaration (Term Identifier Identifier)]
-> TRS Identifier Identifier
make_trs [Declaration (Term Identifier Identifier)]
ds = RS Any (Term Identifier Identifier) -> TRS Identifier Identifier
forall {s} {s} {v}. Ord s => RS s (Term v s) -> RS s (Term v s)
repair_signature_trs (RS Any (Term Identifier Identifier) -> TRS Identifier Identifier)
-> RS Any (Term Identifier Identifier) -> TRS Identifier Identifier
forall a b. (a -> b) -> a -> b
$
    let vs :: [Identifier]
vs = do Var_Declaration [Identifier]
vs <- [Declaration (Term Identifier Identifier)]
ds ; [Identifier]
vs
        us :: [Rule (Term Identifier Identifier)]
us = do Rules_Declaration [Rule (Term Identifier Identifier)]
us <- [Declaration (Term Identifier Identifier)]
ds ; [Rule (Term Identifier Identifier)]
us
        us' :: [Rule (Term Identifier Identifier)]
us' = [Identifier]
-> [Rule (Term Identifier Identifier)]
-> [Rule (Term Identifier Identifier)]
forall {m :: * -> *} {t :: * -> *} {s} {v}.
(Monad m, Foldable t, Eq s) =>
t s -> m (Rule (Term v s)) -> m (Rule (Term s s))
repair_variables [Identifier]
vs [Rule (Term Identifier Identifier)]
us
    in  RS { rules :: [Rule (Term Identifier Identifier)]
rules = [Rule (Term Identifier Identifier)]
us', separate :: Bool
separate = Bool
False }


repair_variables :: t s -> m (Rule (Term v s)) -> m (Rule (Term s s))
repair_variables t s
vars m (Rule (Term v s))
rules = do
    let xform :: Term v s -> Term s s
xform ( Node s
c [] ) | s
c s -> t s -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t s
vars = s -> Term s s
forall v s. v -> Term v s
Var s
c
        xform ( Node s
c [Term v s]
args ) = s -> [Term s s] -> Term s s
forall v s. s -> [Term v s] -> Term v s
Node s
c ( (Term v s -> Term s s) -> [Term v s] -> [Term s s]
forall a b. (a -> b) -> [a] -> [b]
map Term v s -> Term s s
xform [Term v s]
args )
    Rule (Term v s)
rule <- m (Rule (Term v s))
rules  
    Rule (Term s s) -> m (Rule (Term s s))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term s s) -> m (Rule (Term s s)))
-> Rule (Term s s) -> m (Rule (Term s s))
forall a b. (a -> b) -> a -> b
$ Rule (Term v s)
rule { lhs = xform $ lhs rule
                  , rhs = xform $ rhs rule
                  }