-- 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.Substitution.Parse (
    fromString,
    parse,
    parseIO
) where

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


parse :: (Ord v) =>
    Parsec String u f -> Parsec String u v -> Parsec String u (Subst f v)
parse :: forall v u f.
Ord v =>
Parsec String u f
-> Parsec String u v -> Parsec String u (Subst f v)
parse Parsec String u f
fun Parsec String u v
var = ParsecT String u Identity (Subst f v)
-> ParsecT String u Identity (Subst f v)
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
par (ParsecT String u Identity (Subst f v)
 -> ParsecT String u Identity (Subst f v))
-> ParsecT String u Identity (Subst f v)
-> ParsecT String u Identity (Subst f v)
forall a b. (a -> b) -> a -> b
$ ([(v, Term f v)] -> Subst f v)
-> ParsecT String u Identity [(v, Term f v)]
-> ParsecT String u Identity (Subst f v)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Map v (Term f v) -> Subst f v
forall v f v'. Map v (Term f v') -> GSubst v f v'
fromMap (Map v (Term f v) -> Subst f v)
-> ([(v, Term f v)] -> Map v (Term f v))
-> [(v, Term f v)]
-> Subst f v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(v, Term f v)] -> Map v (Term f v)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList) ParsecT String u Identity [(v, Term f v)]
bindings where
    bindings :: ParsecT String u Identity [(v, Term f v)]
bindings = Parsec String u f
-> Parsec String u v -> Parsec String u (v, Term f v)
forall u f v.
Parsec String u f
-> Parsec String u v -> Parsec String u (v, Term f v)
binding Parsec String u f
fun Parsec String u v
var Parsec String u (v, Term f v)
-> ParsecT String u Identity Char
-> ParsecT String u Identity [(v, 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 String u Identity Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
',')


binding :: Parsec String u f -> Parsec String u v -> Parsec String u (v, Term f v)
binding :: forall u f v.
Parsec String u f
-> Parsec String u v -> Parsec String u (v, Term f v)
binding Parsec String u f
fun Parsec String u v
var = (v -> Term f v -> (v, Term f v))
-> Parsec String u v
-> ParsecT String u Identity (Term f v)
-> ParsecT String u Identity (v, Term f v)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) Parsec String u v
var (ParsecT String u Identity Char
forall {u}. ParsecT String u Identity Char
slash ParsecT String u Identity Char
-> ParsecT String u Identity (Term f v)
-> ParsecT String u Identity (Term f v)
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String u Identity (Term f v)
term) ParsecT String u Identity (v, Term f v)
-> String -> ParsecT String u Identity (v, Term f v)
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"binding" where
    slash :: ParsecT String u Identity Char
slash = ParsecT String u Identity Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (ParsecT String u Identity Char -> ParsecT String u Identity Char)
-> ParsecT String u Identity Char -> ParsecT String u Identity Char
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'/'
    term :: ParsecT String u Identity (Term f v)
term  = Parsec String u f
-> Parsec String u v -> ParsecT String u Identity (Term f v)
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)
Term.parse Parsec String u f
fun Parsec String u v
var


fromString :: [String] -> String -> Either ParseError (Subst String String)
fromString :: [String] -> String -> Either ParseError (Subst String String)
fromString [String]
xs = Parsec String () (Subst String String)
-> ()
-> String
-> String
-> Either ParseError (Subst String String)
forall s t u a.
Stream s Identity t =>
Parsec s u a -> u -> String -> s -> Either ParseError a
runP (Parsec String () String
-> Parsec String () String
-> Parsec String () (Subst String String)
forall v u f.
Ord v =>
Parsec String u f
-> Parsec String u v -> Parsec String u (Subst f v)
parse Parsec String () String
forall {u}. ParsecT String u Identity String
fun ([String] -> Parsec String () String
forall {u}. [String] -> ParsecT String u Identity String
var [String]
xs)) () String
"" where
    var :: [String] -> ParsecT String u Identity String
var = ParsecT String u Identity String
-> [String] -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m String -> [String] -> ParsecT s u m String
Term.parseVar (ParsecT String u Identity String
 -> [String] -> ParsecT String u Identity String)
-> ParsecT String u Identity String
-> [String]
-> ParsecT String u Identity String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> [String] -> ParsecT s u m String
ident String
"(),{}/" []
    fun :: ParsecT String u Identity String
fun = ParsecT String u Identity String
-> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m String -> ParsecT s u m String
Term.parseFun (ParsecT String u Identity String
 -> ParsecT String u Identity String)
-> ParsecT String u Identity String
-> ParsecT String u Identity String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> ParsecT String u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> [String] -> ParsecT s u m String
ident String
"(),{}"  []


parseIO :: [String] -> String -> IO (Subst String String)
parseIO :: [String] -> String -> IO (Subst String String)
parseIO [String]
xs String
input = case [String] -> String -> Either ParseError (Subst 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 (Subst String String)
forall a. IO a
forall (m :: * -> *) a. MonadPlus m => m a
mzero }
    Right Subst String String
t  -> Subst String String -> IO (Subst String String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Subst String String
t