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

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Data.Rewriting.Problem.Parse (
  parseIO,
  parseFileIO,
  fromString,
  fromFile,
  fromCharStream,
  ProblemParseError (..)
  ) where

import Data.Rewriting.Utils.Parse (lex, par, ident)
import qualified Data.Rewriting.Problem.Type as Prob
import Data.Rewriting.Problem.Type (Problem)
import Data.Rewriting.Rule (Rule (..))
import qualified Data.Rewriting.Term as Term
import qualified Data.Rewriting.Rules as Rules

import Data.List (partition, union)
import Data.Maybe (isJust)
import Prelude hiding (lex, catch)
import Control.Exception (catch)
import Control.Monad (liftM, liftM2, liftM3, mzero)
import Text.Parsec hiding (parse)
import System.IO (readFile)

data ProblemParseError = UnknownParseError String
                       | UnsupportedStrategy String
                       | FileReadError IOError
                       | UnsupportedDeclaration String
                       | SomeParseError ParseError deriving (Int -> ProblemParseError -> ShowS
[ProblemParseError] -> ShowS
ProblemParseError -> String
(Int -> ProblemParseError -> ShowS)
-> (ProblemParseError -> String)
-> ([ProblemParseError] -> ShowS)
-> Show ProblemParseError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProblemParseError -> ShowS
showsPrec :: Int -> ProblemParseError -> ShowS
$cshow :: ProblemParseError -> String
show :: ProblemParseError -> String
$cshowList :: [ProblemParseError] -> ShowS
showList :: [ProblemParseError] -> ShowS
Show)

parseFileIO :: FilePath -> IO (Problem String String)
parseFileIO :: String -> IO (Problem String String)
parseFileIO String
file = do Either ProblemParseError (Problem String String)
r <- String -> IO (Either ProblemParseError (Problem String String))
fromFile String
file
                      case Either ProblemParseError (Problem String String)
r of
                        Left ProblemParseError
err -> do { String -> IO ()
putStrLn String
"following error occured:"; ProblemParseError -> IO ()
forall a. Show a => a -> IO ()
print ProblemParseError
err; IO (Problem String String)
forall a. IO a
forall (m :: * -> *) a. MonadPlus m => m a
mzero }
                        Right Problem String String
t  -> Problem String String -> IO (Problem String String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Problem String String
t

parseIO :: String -> IO (Problem String String)
parseIO :: String -> IO (Problem String String)
parseIO String
string = case String -> Either ProblemParseError (Problem String String)
fromString String
string of
                    Left ProblemParseError
err -> do { String -> IO ()
putStrLn String
"following error occured:"; ProblemParseError -> IO ()
forall a. Show a => a -> IO ()
print ProblemParseError
err; IO (Problem String String)
forall a. IO a
forall (m :: * -> *) a. MonadPlus m => m a
mzero }
                    Right Problem String String
t  -> Problem String String -> IO (Problem String String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Problem String String
t

fromFile :: FilePath -> IO (Either ProblemParseError (Problem String String))
fromFile :: String -> IO (Either ProblemParseError (Problem String String))
fromFile String
file = IO (Either ProblemParseError (Problem String String))
fromFile' IO (Either ProblemParseError (Problem String String))
-> (IOError
    -> IO (Either ProblemParseError (Problem String String)))
-> IO (Either ProblemParseError (Problem String String))
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (Either ProblemParseError (Problem String String)
-> IO (Either ProblemParseError (Problem String String))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ProblemParseError (Problem String String)
 -> IO (Either ProblemParseError (Problem String String)))
-> (IOError -> Either ProblemParseError (Problem String String))
-> IOError
-> IO (Either ProblemParseError (Problem String String))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemParseError
-> Either ProblemParseError (Problem String String)
forall a b. a -> Either a b
Left (ProblemParseError
 -> Either ProblemParseError (Problem String String))
-> (IOError -> ProblemParseError)
-> IOError
-> Either ProblemParseError (Problem String String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IOError -> ProblemParseError
FileReadError) where
  fromFile' :: IO (Either ProblemParseError (Problem String String))
fromFile' = String
-> String -> Either ProblemParseError (Problem String String)
forall s.
Stream s (Either ProblemParseError) Char =>
String -> s -> Either ProblemParseError (Problem String String)
fromCharStream String
sn (String -> Either ProblemParseError (Problem String String))
-> IO String
-> IO (Either ProblemParseError (Problem String String))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` String -> IO String
readFile String
file
  sn :: String
sn         = String
"<file " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"

fromString :: String -> Either ProblemParseError (Problem String String)
fromString :: String -> Either ProblemParseError (Problem String String)
fromString = String
-> String -> Either ProblemParseError (Problem String String)
forall s.
Stream s (Either ProblemParseError) Char =>
String -> s -> Either ProblemParseError (Problem String String)
fromCharStream String
"supplied string"

fromCharStream :: (Stream s (Either ProblemParseError) Char)
                   => SourceName -> s -> Either ProblemParseError (Problem String String)
fromCharStream :: forall s.
Stream s (Either ProblemParseError) Char =>
String -> s -> Either ProblemParseError (Problem String String)
fromCharStream String
sourcename s
input =
  case ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Problem String String)
-> Problem String String
-> String
-> s
-> Either
     ProblemParseError (Either ParseError (Problem String String))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> u -> String -> s -> m (Either ParseError a)
runParserT ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Problem String String)
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s (Problem String String)
parse Problem String String
forall {f} {v}. Problem f v
initialState String
sourcename s
input of
    Right (Left ParseError
e)  -> ProblemParseError
-> Either ProblemParseError (Problem String String)
forall a b. a -> Either a b
Left (ProblemParseError
 -> Either ProblemParseError (Problem String String))
-> ProblemParseError
-> Either ProblemParseError (Problem String String)
forall a b. (a -> b) -> a -> b
$ ParseError -> ProblemParseError
SomeParseError ParseError
e
    Right (Right Problem String String
p) -> Problem String String
-> Either ProblemParseError (Problem String String)
forall a b. b -> Either a b
Right Problem String String
p
    Left ProblemParseError
e          -> ProblemParseError
-> Either ProblemParseError (Problem String String)
forall a b. a -> Either a b
Left ProblemParseError
e
  where initialState :: Problem f v
initialState = Prob.Problem { startTerms :: StartTerms
Prob.startTerms = StartTerms
Prob.AllTerms ,
                                      strategy :: Strategy
Prob.strategy   = Strategy
Prob.Full ,
                                      theory :: Maybe [Theory f v]
Prob.theory     = Maybe [Theory f v]
forall a. Maybe a
Nothing ,
                                      rules :: RulesPair f v
Prob.rules      = Prob.RulesPair { strictRules :: [Rule f v]
Prob.strictRules = [],
                                                                         weakRules :: [Rule f v]
Prob.weakRules = [] } ,
                                      variables :: [v]
Prob.variables  = [] ,
                                      symbols :: [f]
Prob.symbols    = [] ,
                                      signature :: Maybe [(f, Int)]
Prob.signature  = Maybe [(f, Int)]
forall a. Maybe a
Nothing,
                                      comment :: Maybe String
Prob.comment    = Maybe String
forall a. Maybe a
Nothing }


type ParserState = Problem String String

type WSTParser s a = ParsecT s ParserState (Either ProblemParseError) a

modifyProblem :: (Problem String String -> Problem String String) -> WSTParser s ()
modifyProblem :: forall s.
(Problem String String -> Problem String String) -> WSTParser s ()
modifyProblem = (Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall (m :: * -> *) u s. Monad m => (u -> u) -> ParsecT s u m ()
modifyState

parsedVariables :: WSTParser s [String]
parsedVariables :: forall s. WSTParser s [String]
parsedVariables = Problem String String -> [String]
forall f v. Problem f v -> [v]
Prob.variables (Problem String String -> [String])
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Problem String String)
-> ParsecT
     s (Problem String String) (Either ProblemParseError) [String]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Problem String String)
forall (m :: * -> *) s u. Monad m => ParsecT s u m u
getState

parse :: (Stream s (Either ProblemParseError) Char) => WSTParser s (Problem String String)
parse :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s (Problem String String)
parse = ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT
     s (Problem String String) (Either ProblemParseError) [()]
-> ParsecT
     s (Problem String String) (Either ProblemParseError) [()]
forall a b.
ParsecT s (Problem String String) (Either ProblemParseError) a
-> ParsecT s (Problem String String) (Either ProblemParseError) b
-> ParsecT s (Problem String String) (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT s (Problem String String) (Either ProblemParseError) [()]
parseDecls ParsecT s (Problem String String) (Either ProblemParseError) [()]
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall a b.
ParsecT s (Problem String String) (Either ProblemParseError) a
-> ParsecT s (Problem String String) (Either ProblemParseError) b
-> ParsecT s (Problem String String) (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Problem String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Problem String String)
forall a b.
ParsecT s (Problem String String) (Either ProblemParseError) a
-> ParsecT s (Problem String String) (Either ProblemParseError) b
-> ParsecT s (Problem String String) (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Problem String String)
forall (m :: * -> *) s u. Monad m => ParsecT s u m u
getState where
  parseDecls :: ParsecT s (Problem String String) (Either ProblemParseError) [()]
parseDecls = ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT
     s (Problem String String) (Either ProblemParseError) [()]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT s (Problem String String) (Either ProblemParseError) ()
parseDecl
  parseDecl :: ParsecT s (Problem String String) (Either ProblemParseError) ()
parseDecl =  String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) [String]
-> ([String] -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall {s} {t}.
Stream s (Either ProblemParseError) Char =>
String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
"VAR"       ParsecT
  s (Problem String String) (Either ProblemParseError) [String]
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s [String]
vars       (\ [String]
e Problem String String
p -> Problem String String
p {Prob.variables = e `union` Prob.variables p})
           ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [Theory String String]
-> ([Theory String String]
    -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall {s} {t}.
Stream s (Either ProblemParseError) Char =>
String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
"THEORY"    ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  [Theory String String]
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s [Theory String String]
theory     (\ [Theory String String]
e Problem String String
p -> Problem String String
p {Prob.theory = maybeAppend Prob.theory e p})
           ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [(String, Int)]
-> ([(String, Int)]
    -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall {s} {t}.
Stream s (Either ProblemParseError) Char =>
String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
"SIG"       ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  [(String, Int)]
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s [(String, Int)]
signature  (\ [(String, Int)]
e Problem String String
p -> Problem String String
p {Prob.signature = maybeAppend Prob.signature e p})
           ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (RulesPair String String)
-> (RulesPair String String
    -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall {s} {t}.
Stream s (Either ProblemParseError) Char =>
String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
"RULES"     ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (RulesPair String String)
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s (RulesPair String String)
rules      (\ RulesPair String String
e Problem String String
p -> Problem String String
p {Prob.rules   = e, --FIXME multiple RULES blocks?
                                                        Prob.symbols = Rules.funsDL (Prob.allRules e) [] })
           ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) Strategy
-> (Strategy -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall {s} {t}.
Stream s (Either ProblemParseError) Char =>
String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
"STRATEGY"  ParsecT
  s (Problem String String) (Either ProblemParseError) Strategy
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s Strategy
strategy   (\ Strategy
e Problem String String
p -> Problem String String
p {Prob.strategy = e})
           ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) StartTerms
-> (StartTerms -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall {s} {t}.
Stream s (Either ProblemParseError) Char =>
String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
"STARTTERM" ParsecT
  s (Problem String String) (Either ProblemParseError) StartTerms
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s StartTerms
startterms (\ StartTerms
e Problem String String
p -> Problem String String
p {Prob.startTerms = e})
           ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> (String -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall {s} {t}.
Stream s (Either ProblemParseError) Char =>
String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
"COMMENT"   ParsecT s (Problem String String) (Either ProblemParseError) String
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s String
comment   (\ String
e Problem String String
p -> Problem String String
p {Prob.comment = maybeAppend Prob.comment e p}) ParsecT s (Problem String String) (Either ProblemParseError) ()
-> String
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"comment")
           ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
par ParsecT s (Problem String String) (Either ProblemParseError) String
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s String
comment ParsecT s (Problem String String) (Either ProblemParseError) String
-> (String
    -> ParsecT s (Problem String String) (Either ProblemParseError) ())
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall a b.
ParsecT s (Problem String String) (Either ProblemParseError) a
-> (a
    -> ParsecT s (Problem String String) (Either ProblemParseError) b)
-> ParsecT s (Problem String String) (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s.
(Problem String String -> Problem String String) -> WSTParser s ()
modifyProblem ((Problem String String -> Problem String String)
 -> ParsecT s (Problem String String) (Either ProblemParseError) ())
-> (String -> Problem String String -> Problem String String)
-> String
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ String
e Problem String String
p -> Problem String String
p {Prob.comment = maybeAppend Prob.comment e p}) ParsecT s (Problem String String) (Either ProblemParseError) ()
-> String
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"comment")
  decl :: String
-> ParsecT s (Problem String String) (Either ProblemParseError) t
-> (t -> Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
decl String
name ParsecT s (Problem String String) (Either ProblemParseError) t
p t -> Problem String String -> Problem String String
f = ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
par (ParsecT s (Problem String String) (Either ProblemParseError) ()
 -> ParsecT s (Problem String String) (Either ProblemParseError) ())
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall a b. (a -> b) -> a -> b
$ do
      ParsecT s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (ParsecT
   s (Problem String String) (Either ProblemParseError) String
 -> ParsecT
      s (Problem String String) (Either ProblemParseError) String)
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall a b. (a -> b) -> a -> b
$ String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
name
      t
r <- ParsecT s (Problem String String) (Either ProblemParseError) t
p
      (Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s.
(Problem String String -> Problem String String) -> WSTParser s ()
modifyProblem ((Problem String String -> Problem String String)
 -> ParsecT s (Problem String String) (Either ProblemParseError) ())
-> (Problem String String -> Problem String String)
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall a b. (a -> b) -> a -> b
$ t -> Problem String String -> Problem String String
f t
r) ParsecT s (Problem String String) (Either ProblemParseError) ()
-> String
-> ParsecT s (Problem String String) (Either ProblemParseError) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> (String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" block")
  maybeAppend :: (t -> Maybe [a]) -> [a] -> t -> Maybe [a]
maybeAppend t -> Maybe [a]
fld [a]
e t
p = [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ [a] -> ([a] -> [a]) -> Maybe [a] -> [a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] [a] -> [a]
forall a. a -> a
id (t -> Maybe [a]
fld t
p) [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
e

vars :: (Stream s (Either ProblemParseError) Char) => WSTParser s [String]
vars :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s [String]
vars = do [String]
vs <- ParsecT s (Problem String String) (Either ProblemParseError) String
-> WSTParser s [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (ParsecT
   s (Problem String String) (Either ProblemParseError) String
 -> ParsecT
      s (Problem String String) (Either ProblemParseError) String)
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall a b. (a -> b) -> a -> b
$ String
-> [String]
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> [String] -> ParsecT s u m String
ident String
"()," [])
          [String] -> WSTParser s [String]
forall a.
a -> ParsecT s (Problem String String) (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return [String]
vs

signature :: (Stream s (Either ProblemParseError) Char) => WSTParser s [(String,Int)]
signature :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s [(String, Int)]
signature = ParsecT
  s (Problem String String) (Either ProblemParseError) (String, Int)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [(String, Int)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT
  s (Problem String String) (Either ProblemParseError) (String, Int)
forall {u}. ParsecT s u (Either ProblemParseError) (String, Int)
fundecl
    where
        fundecl :: ParsecT s u (Either ProblemParseError) (String, Int)
fundecl = ParsecT s u (Either ProblemParseError) (String, Int)
-> ParsecT s u (Either ProblemParseError) (String, Int)
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
par (do
            String
f  <- ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (ParsecT s u (Either ProblemParseError) String
 -> ParsecT s u (Either ProblemParseError) String)
-> ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> [String] -> ParsecT s u m String
ident String
"()," []
            Int
ar <- ParsecT s u (Either ProblemParseError) Int
-> ParsecT s u (Either ProblemParseError) Int
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (String -> Int
forall a. Read a => String -> a
read (String -> Int)
-> ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT s u (Either ProblemParseError) Char
-> ParsecT s u (Either ProblemParseError) String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT s u (Either ProblemParseError) Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit)
            (String, Int)
-> ParsecT s u (Either ProblemParseError) (String, Int)
forall a. a -> ParsecT s u (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((String, Int)
 -> ParsecT s u (Either ProblemParseError) (String, Int))
-> (String, Int)
-> ParsecT s u (Either ProblemParseError) (String, Int)
forall a b. (a -> b) -> a -> b
$ (String
f,Int
ar))

theory :: (Stream s (Either ProblemParseError) Char) => WSTParser s [Prob.Theory String String]
theory :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s [Theory String String]
theory = ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Theory String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [Theory String String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Theory String String)
thdecl where
    thdecl :: ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Theory String String)
thdecl     = ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Theory String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
par ((ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  [Rule String String]
equations ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  [Rule String String]
-> ([Rule String String]
    -> ParsecT
         s
         (Problem String String)
         (Either ProblemParseError)
         (Theory String String))
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall a b.
ParsecT s (Problem String String) (Either ProblemParseError) a
-> (a
    -> ParsecT s (Problem String String) (Either ProblemParseError) b)
-> ParsecT s (Problem String String) (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Theory String String
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall a.
a -> ParsecT s (Problem String String) (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Theory String String
 -> ParsecT
      s
      (Problem String String)
      (Either ProblemParseError)
      (Theory String String))
-> ([Rule String String] -> Theory String String)
-> [Rule String String]
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Rule String String] -> Theory String String
forall f v. [Rule f v] -> Theory f v
Prob.Equations)
              ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Theory String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>     (ParsecT
  s (Problem String String) (Either ProblemParseError) [String]
forall {u}. ParsecT s u (Either ProblemParseError) [String]
idlist    ParsecT
  s (Problem String String) (Either ProblemParseError) [String]
-> ([String]
    -> ParsecT
         s
         (Problem String String)
         (Either ProblemParseError)
         (Theory String String))
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall a b.
ParsecT s (Problem String String) (Either ProblemParseError) a
-> (a
    -> ParsecT s (Problem String String) (Either ProblemParseError) b)
-> ParsecT s (Problem String String) (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (String
x:[String]
xs) -> Theory String String
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall a.
a -> ParsecT s (Problem String String) (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Theory String String
 -> ParsecT
      s
      (Problem String String)
      (Either ProblemParseError)
      (Theory String String))
-> Theory String String
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Theory String String)
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Theory String String
forall f v. String -> [f] -> Theory f v
Prob.SymbolProperty String
x [String]
xs))
    equations :: ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  [Rule String String]
equations  = ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  [Rule String String]
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [Rule String String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (do
        [String]
vs <- ParsecT
  s (Problem String String) (Either ProblemParseError) [String]
forall s. WSTParser s [String]
parsedVariables
        ParsecT s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (ParsecT
   s (Problem String String) (Either ProblemParseError) String
 -> ParsecT
      s (Problem String String) (Either ProblemParseError) String)
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall a b. (a -> b) -> a -> b
$ String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"EQUATIONS"
        ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Rule String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [Rule String String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT
   s
   (Problem String String)
   (Either ProblemParseError)
   (Rule String String)
 -> ParsecT
      s
      (Problem String String)
      (Either ProblemParseError)
      [Rule String String])
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Rule String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [Rule String String]
forall a b. (a -> b) -> a -> b
$ [String]
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Rule String String)
forall {s} {m :: * -> *} {u}.
Stream s m Char =>
[String] -> ParsecT s u m (Rule String String)
equation [String]
vs) ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  [Rule String String]
-> String
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [Rule String String]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
"EQUATIONS block"
    equation :: [String] -> ParsecT s u m (Rule String String)
equation [String]
vs = do
        Term String String
l <- [String] -> ParsecT s u m (Term String String)
forall s (m :: * -> *) u.
Stream s m Char =>
[String] -> ParsecT s u m (Term String String)
Term.parseWST [String]
vs
        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 -> ParsecT s u m String)
-> ParsecT s u m String -> ParsecT s u m String
forall a b. (a -> b) -> a -> b
$ String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"=="
        Term String String
r <- [String] -> ParsecT s u m (Term String String)
forall s (m :: * -> *) u.
Stream s m Char =>
[String] -> ParsecT s u m (Term String String)
Term.parseWST [String]
vs
        Rule String String -> ParsecT s u m (Rule String String)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule String String -> ParsecT s u m (Rule String String))
-> Rule String String -> ParsecT s u m (Rule String String)
forall a b. (a -> b) -> a -> b
$ Term String String -> Term String String -> Rule String String
forall f v. Term f v -> Term f v -> Rule f v
Rule Term String String
l Term String String
r
    idlist :: ParsecT s u (Either ProblemParseError) [String]
idlist      = ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT s u (Either ProblemParseError) String
 -> ParsecT s u (Either ProblemParseError) [String])
-> ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) [String]
forall a b. (a -> b) -> a -> b
$ (ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u a.
Stream s m Char =>
ParsecT s u m a -> ParsecT s u m a
lex (ParsecT s u (Either ProblemParseError) String
 -> ParsecT s u (Either ProblemParseError) String)
-> ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> [String] -> ParsecT s u m String
ident String
"()," [])

rules :: (Stream s (Either ProblemParseError) Char) => WSTParser s (Prob.RulesPair String String)
rules :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s (RulesPair String String)
rules = do [String]
vs <- WSTParser s [String]
forall s. WSTParser s [String]
parsedVariables
           [(Bool, Rule String String)]
rs <- ParsecT
  s
  (Problem String String)
  (Either ProblemParseError)
  (Bool, Rule String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [(Bool, Rule String String)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT
   s
   (Problem String String)
   (Either ProblemParseError)
   (Bool, Rule String String)
 -> ParsecT
      s
      (Problem String String)
      (Either ProblemParseError)
      [(Bool, Rule String String)])
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Bool, Rule String String)
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     [(Bool, Rule String String)]
forall a b. (a -> b) -> a -> b
$ [String]
-> ParsecT
     s
     (Problem String String)
     (Either ProblemParseError)
     (Bool, Rule String String)
forall {s} {m :: * -> *} {u}.
Stream s m Char =>
[String] -> ParsecT s u m (Bool, Rule String String)
rule [String]
vs
           let ([(Bool, Rule String String)]
s,[(Bool, Rule String String)]
w) = ((Bool, Rule String String) -> Bool)
-> [(Bool, Rule String String)]
-> ([(Bool, Rule String String)], [(Bool, Rule String String)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool, Rule String String) -> Bool
forall a b. (a, b) -> a
fst [(Bool, Rule String String)]
rs
           RulesPair String String -> WSTParser s (RulesPair String String)
forall a.
a -> ParsecT s (Problem String String) (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return Prob.RulesPair { strictRules :: [Rule String String]
Prob.strictRules = ((Bool, Rule String String) -> Rule String String)
-> [(Bool, Rule String String)] -> [Rule String String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, Rule String String) -> Rule String String
forall a b. (a, b) -> b
snd [(Bool, Rule String String)]
s ,
                                   weakRules :: [Rule String String]
Prob.weakRules   = ((Bool, Rule String String) -> Rule String String)
-> [(Bool, Rule String String)] -> [Rule String String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, Rule String String) -> Rule String String
forall a b. (a, b) -> b
snd [(Bool, Rule String String)]
w }
  where rule :: [String] -> ParsecT s u m (Bool, Rule String String)
rule [String]
vs = do Term String String
l <- [String] -> ParsecT s u m (Term String String)
forall s (m :: * -> *) u.
Stream s m Char =>
[String] -> ParsecT s u m (Term String String)
Term.parseWST [String]
vs
                     String
sep <- 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 -> ParsecT s u m String)
-> ParsecT s u m String -> ParsecT s u m String
forall a b. (a -> b) -> a -> b
$ (ParsecT s u m String -> ParsecT s u m String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s u m String -> ParsecT s u m String)
-> ParsecT s u m String -> ParsecT s u m String
forall a b. (a -> b) -> a -> b
$ String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"->=") ParsecT s u m String
-> ParsecT s u m String -> ParsecT s u m String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"->"
                     Term String String
r <- [String] -> ParsecT s u m (Term String String)
forall s (m :: * -> *) u.
Stream s m Char =>
[String] -> ParsecT s u m (Term String String)
Term.parseWST [String]
vs
                     (Bool, Rule String String)
-> ParsecT s u m (Bool, Rule String String)
forall a. a -> ParsecT s u m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
sep String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"->", Rule {lhs :: Term String String
lhs = Term String String
l, rhs :: Term String String
rhs = Term String String
r})

strategy :: (Stream s (Either ProblemParseError) Char) => WSTParser s Prob.Strategy
strategy :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s Strategy
strategy = ParsecT
  s (Problem String String) (Either ProblemParseError) Strategy
forall {u}. ParsecT s u (Either ProblemParseError) Strategy
innermost ParsecT
  s (Problem String String) (Either ProblemParseError) Strategy
-> ParsecT
     s (Problem String String) (Either ProblemParseError) Strategy
-> ParsecT
     s (Problem String String) (Either ProblemParseError) Strategy
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT
  s (Problem String String) (Either ProblemParseError) Strategy
forall {u}. ParsecT s u (Either ProblemParseError) Strategy
outermost where
  innermost :: ParsecT s u (Either ProblemParseError) Strategy
innermost = String -> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"INNERMOST" ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) Strategy
-> ParsecT s u (Either ProblemParseError) Strategy
forall a b.
ParsecT s u (Either ProblemParseError) a
-> ParsecT s u (Either ProblemParseError) b
-> ParsecT s u (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Strategy -> ParsecT s u (Either ProblemParseError) Strategy
forall a. a -> ParsecT s u (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return Strategy
Prob.Innermost
  outermost :: ParsecT s u (Either ProblemParseError) Strategy
outermost = String -> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"OUTERMOST" ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) Strategy
-> ParsecT s u (Either ProblemParseError) Strategy
forall a b.
ParsecT s u (Either ProblemParseError) a
-> ParsecT s u (Either ProblemParseError) b
-> ParsecT s u (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Strategy -> ParsecT s u (Either ProblemParseError) Strategy
forall a. a -> ParsecT s u (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return Strategy
Prob.Outermost

startterms :: (Stream s (Either ProblemParseError) Char) => WSTParser s Prob.StartTerms
startterms :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s StartTerms
startterms = ParsecT
  s (Problem String String) (Either ProblemParseError) StartTerms
forall {u}. ParsecT s u (Either ProblemParseError) StartTerms
basic ParsecT
  s (Problem String String) (Either ProblemParseError) StartTerms
-> ParsecT
     s (Problem String String) (Either ProblemParseError) StartTerms
-> ParsecT
     s (Problem String String) (Either ProblemParseError) StartTerms
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT
  s (Problem String String) (Either ProblemParseError) StartTerms
forall {u}. ParsecT s u (Either ProblemParseError) StartTerms
terms where
  basic :: ParsecT s u (Either ProblemParseError) StartTerms
basic = String -> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"CONSTRUCTOR-BASED" ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) StartTerms
-> ParsecT s u (Either ProblemParseError) StartTerms
forall a b.
ParsecT s u (Either ProblemParseError) a
-> ParsecT s u (Either ProblemParseError) b
-> ParsecT s u (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StartTerms -> ParsecT s u (Either ProblemParseError) StartTerms
forall a. a -> ParsecT s u (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return StartTerms
Prob.BasicTerms
  terms :: ParsecT s u (Either ProblemParseError) StartTerms
terms = String -> ParsecT s u (Either ProblemParseError) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"FULL" ParsecT s u (Either ProblemParseError) String
-> ParsecT s u (Either ProblemParseError) StartTerms
-> ParsecT s u (Either ProblemParseError) StartTerms
forall a b.
ParsecT s u (Either ProblemParseError) a
-> ParsecT s u (Either ProblemParseError) b
-> ParsecT s u (Either ProblemParseError) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StartTerms -> ParsecT s u (Either ProblemParseError) StartTerms
forall a. a -> ParsecT s u (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return StartTerms
Prob.AllTerms

comment :: (Stream s (Either ProblemParseError) Char) => WSTParser s String
comment :: forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s String
comment = ParsecT s (Problem String String) (Either ProblemParseError) String
withpars ParsecT s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> ShowS)
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 String -> ShowS
forall a. [a] -> [a] -> [a]
(++) ParsecT s (Problem String String) (Either ProblemParseError) String
forall {u}. ParsecT s u (Either ProblemParseError) String
idents ParsecT s (Problem String String) (Either ProblemParseError) String
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s String
comment ParsecT s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall a.
a -> ParsecT s (Problem String String) (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
""
  where idents :: ParsecT s u (Either ProblemParseError) String
idents = ParsecT s u (Either ProblemParseError) Char
-> ParsecT s u (Either ProblemParseError) String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many1 (String -> ParsecT s u (Either ProblemParseError) Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
noneOf String
"()")
        withpars :: ParsecT s (Problem String String) (Either ProblemParseError) String
withpars = do Char
_ <- Char
-> ParsecT
     s (Problem String String) (Either ProblemParseError) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'('
                      String
pre <- ParsecT s (Problem String String) (Either ProblemParseError) String
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s String
comment
                      Char
_ <- Char
-> ParsecT
     s (Problem String String) (Either ProblemParseError) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')'
                      String
suf <- ParsecT s (Problem String String) (Either ProblemParseError) String
forall s.
Stream s (Either ProblemParseError) Char =>
WSTParser s String
comment
                      String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall a.
a -> ParsecT s (Problem String String) (Either ProblemParseError) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
 -> ParsecT
      s (Problem String String) (Either ProblemParseError) String)
-> String
-> ParsecT
     s (Problem String String) (Either ProblemParseError) String
forall a b. (a -> b) -> a -> b
$ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
pre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
suf