term-rewriting-0.4.0.1: Term Rewriting Library

Data.Rewriting.Term.Parse

Synopsis

# Documentation

fromString xs s parsers a term from the string s, where elements of xs are considered as variables.

parse :: Stream s m Char => ParsecT s u m f -> ParsecT s u m v -> ParsecT s u m (Term f v) Source #

parse fun var is a parser for terms, where fun and var are parsers for function symbols and variables, respectively. The var parser has a higher priority than the fun parser. Hence, whenever var succeeds, the token is treated as a variable.

Note that the user has to take care of handling trailing white space in fun and var.

parseIO :: [String] -> String -> IO (Term String String) Source #

Like fromString, but the result is wrapped in the IO monad, making this function useful for interactive testing.

>>> parseIO ["x","y"] "f(x,c)"
Fun "f" [Var "x",Fun "c" []]


parseFun :: Stream s m Char => ParsecT s u m String -> ParsecT s u m String Source #

parseFun ident parses function symbols defined by ident.

parseVar :: Stream s m Char => ParsecT s u m String -> [String] -> ParsecT s u m String Source #

parseVar ident vars parses variables as defined by ident and with the additional requirement that the result is a member of vars.

parseWST :: Stream s m Char => [String] -> ParsecT s u m (Term String String) Source #

parseWST xs is a parser for terms following the conventions of the ancient ASCII input format of the termination competition: every Char that is neither a white space (according to isSpace) nor one of '(', ')', or ',', is considered a letter. An identifier is a non-empty sequence of letters and it is treated as variable iff it is contained in xs.