-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Christian Sternagel

{-# LANGUAGE FlexibleContexts#-}
module Data.Rewriting.Term.Parse (
    fromString,
    parse,
    parseIO,
    parseFun,
    parseVar,
    parseWST,
) where

import Data.Rewriting.Utils.Parse (lex, par, ident)
import Prelude hiding (lex)
import Control.Monad
import Data.Rewriting.Term.Type
import Text.Parsec hiding (parse)
import Text.Parsec.Prim (runP)

-- | 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" []]
parseIO :: [String] -> String -> IO (Term String String)
parseIO :: [String] -> String -> IO (Term String String)
parseIO [String]
xs String
input = case [String] -> String -> Either ParseError (Term String String)
fromString [String]
xs String
input of
    Left ParseError
err -> do { String -> IO ()
putStr String
"parse error at "; ParseError -> IO ()
forall a. Show a => a -> IO ()
print ParseError
err; IO (Term String String)
forall a. IO a
forall (m :: * -> *) a. MonadPlus m => m a
mzero }
    Right Term String String
t  -> Term String String -> IO (Term String String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term String String
t

-- | @fromString xs s@ parsers a term from the string @s@, where elements of @xs@
-- are considered as variables.
fromString :: [String] -> String -> Either ParseError (Term String String)
fromString :: [String] -> String -> Either ParseError (Term String String)
fromString [String]
xs = Parsec String () (Term String String)
-> () -> String -> String -> Either ParseError (Term String String)
forall s t u a.
Stream s Identity t =>
Parsec s u a -> u -> String -> s -> Either ParseError a
runP ([String] -> Parsec String () (Term String String)
forall s (m :: * -> *) u.
Stream s m Char =>
[String] -> ParsecT s u m (Term String String)
parseWST [String]
xs) () String
""


-- | @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@.
parse :: Stream s m Char => ParsecT s u m f -> ParsecT s u m v
    -> ParsecT s u m (Term f v)
parse :: forall s (m :: * -> *) u f v.
Stream s m Char =>
ParsecT s u m f -> ParsecT s u m v -> ParsecT s u m (Term f v)
parse ParsecT s u m f
fun ParsecT s u m v
var = ParsecT s u m (Term f v)
term ParsecT s u m (Term f v) -> String -> ParsecT s u m (Term f v)
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"term" where
    term :: ParsecT s u m (Term f v)
term = ParsecT s u m (Term f v) -> ParsecT s u m (Term f v)
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ((v -> Term f v) -> ParsecT s u m v -> ParsecT s u m (Term f v)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM v -> Term f v
forall f v. v -> Term f v
Var ParsecT s u m v
var) ParsecT s u m (Term f v)
-> ParsecT s u m (Term f v) -> ParsecT s u m (Term f v)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (f -> [Term f v] -> Term f v)
-> ParsecT s u m f
-> ParsecT s u m [Term f v]
-> ParsecT s u m (Term f v)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f -> [Term f v] -> Term f v
forall f v. f -> [Term f v] -> Term f v
Fun ParsecT s u m f
fun ParsecT s u m [Term f v]
args
    args :: ParsecT s u m [Term f v]
args =  ParsecT s u m [Term f v] -> ParsecT s u m [Term f v]
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
par (ParsecT s u m (Term f v)
-> ParsecT s u m Char -> ParsecT s u m [Term f v]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy ParsecT s u m (Term f v)
term (ParsecT s u m Char -> ParsecT s u m Char
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (ParsecT s u m Char -> ParsecT s u m Char)
-> ParsecT s u m Char -> ParsecT s u m Char
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
',')) ParsecT s u m [Term f v]
-> ParsecT s u m [Term f v] -> ParsecT s u m [Term f v]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Term f v] -> ParsecT s u m [Term f v]
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return []


-- | @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 'Data.Char.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@.

-- change name?
parseWST :: Stream s m Char => [String] -> ParsecT s u m (Term String String)
parseWST :: forall s (m :: * -> *) u.
Stream s m Char =>
[String] -> ParsecT s u m (Term String String)
parseWST [String]
xs = ParsecT s u m String
-> ParsecT s u m String -> ParsecT s u m (Term String String)
forall s (m :: * -> *) u f v.
Stream s m Char =>
ParsecT s u m f -> ParsecT s u m v -> ParsecT s u m (Term f v)
parse (ParsecT s u m String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m String -> ParsecT s u m String
parseFun ParsecT s u m String
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m String
identWST) (ParsecT s u m String -> [String] -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m String -> [String] -> ParsecT s u m String
parseVar ParsecT s u m String
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m String
identWST [String]
xs)

-- | @parseFun ident@ parses function symbols defined by @ident@.
parseFun :: Stream s m Char => ParsecT s u m String -> ParsecT s u m String
parseFun :: forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m String -> ParsecT s u m String
parseFun ParsecT s u m String
id = ParsecT s u m String -> ParsecT s u m String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex ParsecT s u m String
id ParsecT s u m String -> String -> ParsecT s u m String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"function symbol"

-- | @parseVar ident vars@ parses variables as defined by @ident@ and with the
-- additional requirement that the result is a member of @vars@.
parseVar :: Stream s m Char =>
    ParsecT s u m String -> [String] -> ParsecT s u m String
parseVar :: forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m String -> [String] -> ParsecT s u m String
parseVar ParsecT s u m String
id [String]
xs =  do { String
x <- ParsecT s u m String -> ParsecT s u m String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex ParsecT s u m String
id; Bool -> ParsecT s u m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (String
x String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
xs); String -> ParsecT s u m String
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
x }
              ParsecT s u m String -> String -> ParsecT s u m String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"variable"

identWST :: Stream s m Char => ParsecT s u m String
-- COMMENT: according to http://www.lri.fr/~marche/tpdb/format.html '"' and some
-- reserved strings are also not allowed, but I don't see the point
identWST :: forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m String
identWST = String -> [String] -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> [String] -> ParsecT s u m String
ident String
"()," []