TPDB.Plain.Read

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

Documentation

trs :: Text -> Either String (TRS Identifier Identifier)

srs :: Text -> Either String (SRS Identifier)

class Reader a where

Methods

reader :: Parser a

Instances

Reader Identifier

Defined in TPDB.Plain.Read

Methods

reader :: Parser Identifier

Reader s => Reader [s]

Defined in TPDB.Plain.Read

Methods

reader :: Parser [s]

Reader u => Reader (Rule u)

Defined in TPDB.Plain.Read

Methods

reader :: Parser (Rule u)

Reader (SRS Identifier)

Defined in TPDB.Plain.Read

Methods

reader :: Parser (SRS Identifier)

Reader v => Reader (Term v Identifier)

Defined in TPDB.Plain.Read

Methods

reader :: Parser (Term v Identifier)

Reader (TRS Identifier Identifier)

Defined in TPDB.Plain.Read

Methods

reader :: Parser (TRS Identifier Identifier)

lexer :: GenTokenParser Text () Identity

warning: by definition, {}[] may appear in identifiers

data Declaration u

Constructors

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 -> Parser (Declaration u)

anylist :: ParsecT Text () Identity ()

repair_signature_srs :: Eq s1 => RS s2 [s1] -> RS s1 [s1]

make_srs :: Eq s => [Declaration [s]] -> SRS s

repair_signature_trs :: Ord s1 => RS s2 (Term v s1) -> RS s1 (Term v s1)

make_trs :: [Declaration (Term Identifier Identifier)] -> TRS Identifier Identifier

repair_variables :: (Monad m, Foldable t, Eq s) => t s -> m (Rule (Term v s)) -> m (Rule (Term s s))