{- |
Module      :  ./SoftFOL/DFGParser.hs
Description :  A parser for the SPASS Input Syntax
Copyright   :  (c) C. Immanuel Normann, Heng Jiang, C.Maeder, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

A parser for the SPASS Input Syntax taken from
<http://spass.mpi-sb.mpg.de/download/binaries/spass-input-syntax15.pdf >.
-}

module SoftFOL.DFGParser (parseSPASS) where

import SoftFOL.Sign

import Text.ParserCombinators.Parsec

import Common.AS_Annotation
import Common.Id
import Common.Lexer hiding (parens)
import Common.Parsec

import Control.Monad
import qualified Control.Monad.Fail as Fail

import Data.Char (isSpace)
import Data.Maybe
import qualified Data.Map as Map

-- * lexical matter

wordChar :: Parser Char
wordChar :: Parser Char
wordChar = Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum Parser Char -> Parser Char -> Parser Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Char] -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf "_"

anyWord :: Parser String
anyWord :: Parser [Char]
anyWord = do
    Char
c <- Parser Char
wordChar
    [Char]
r <- Parser Char -> Parser [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many Parser Char
wordChar
    Parser ()
whiteSpace
    [Char] -> Parser [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Parser [Char]) -> [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$ Char
c Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
r

reservedList :: [String]
reservedList :: [[Char]]
reservedList = ["end_of_list", "sort", "subsort", "predicate"]

identifierS :: Parser String
identifierS :: Parser [Char]
identifierS = Parser [Char] -> Parser [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$ Parser [Char]
anyWord Parser [Char] -> ([Char] -> Parser [Char]) -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    (\ s :: [Char]
s -> if [Char] -> [[Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Char]
s [[Char]]
reservedList then [Char] -> Parser [Char]
forall s (m :: * -> *) t u a.
Stream s m t =>
[Char] -> ParsecT s u m a
unexpected ([Char] -> Parser [Char]) -> [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
s else [Char] -> Parser [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
s)

identifierT :: Parser Token
identifierT :: Parser Token
identifierT = (Pos -> [Char] -> Token)
-> ParsecT [Char] () Identity Pos -> Parser [Char] -> Parser Token
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\ p :: Pos
p s :: [Char]
s -> [Char] -> Range -> Token
Token [Char]
s ([Pos] -> Range
Range [Pos
p])) ParsecT [Char] () Identity Pos
forall tok st. GenParser tok st Pos
getPos Parser [Char]
identifierS

arityT :: Parser Int
arityT :: Parser Int
arityT = ([Char] -> Int) -> Parser [Char] -> Parser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> Int
forall a. Read a => [Char] -> a
read (Parser [Char] -> Parser Int) -> Parser [Char] -> Parser Int
forall a b. (a -> b) -> a -> b
$ Parser Char -> Parser [Char]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit Parser [Char] -> Parser [Char] -> Parser [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser [Char] -> Parser [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try ([Char] -> Parser [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string "-1" Parser [Char] -> Parser () -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser Char -> Parser ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit)

commentLine :: Parser ()
commentLine :: Parser ()
commentLine = Parser [Char] -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (Parser [Char] -> Parser ()) -> Parser [Char] -> Parser ()
forall a b. (a -> b) -> a -> b
$ Char -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '%' Parser Char -> Parser [Char] -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Char -> Parser Char -> Parser [Char]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
newline

whiteSpace :: Parser ()
whiteSpace :: Parser ()
whiteSpace = Parser () -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser Char -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ((Char -> Bool) -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy Char -> Bool
isSpace) Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ()
commentLine

symbolT :: String -> Parser String
symbolT :: [Char] -> Parser [Char]
symbolT = (Parser [Char] -> Parser () -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
whiteSpace) (Parser [Char] -> Parser [Char])
-> ([Char] -> Parser [Char]) -> [Char] -> Parser [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Parser [Char]
forall st. [Char] -> CharParser st [Char]
tryString

keywordT :: String -> Parser String
keywordT :: [Char] -> Parser [Char]
keywordT s :: [Char]
s = Parser [Char] -> Parser [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try ([Char] -> Parser [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string [Char]
s Parser [Char] -> Parser () -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser Char -> Parser ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy Parser Char
wordChar) Parser [Char] -> Parser () -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
whiteSpace

dot :: Parser String
dot :: Parser [Char]
dot = [Char] -> Parser [Char]
symbolT "."

comma :: Parser String
comma :: Parser [Char]
comma = [Char] -> Parser [Char]
symbolT ","

commaSep :: Parser a -> Parser [a]
commaSep :: Parser a -> Parser [a]
commaSep p :: Parser a
p = Parser a -> Parser [Char] -> Parser [a]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
sepBy1 Parser a
p Parser [Char]
comma

parens :: Parser a -> Parser a
parens :: Parser a -> Parser a
parens p :: Parser a
p = [Char] -> Parser [Char]
symbolT "(" Parser [Char] -> Parser a -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a
p Parser a -> Parser [Char] -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< [Char] -> Parser [Char]
symbolT ")"

squares :: Parser a -> Parser a
squares :: Parser a -> Parser a
squares p :: Parser a
p = [Char] -> Parser [Char]
symbolT "[" Parser [Char] -> Parser a -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a
p Parser a -> Parser [Char] -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< [Char] -> Parser [Char]
symbolT "]"

parensDot :: Parser a -> Parser a
parensDot :: Parser a -> Parser a
parensDot p :: Parser a
p = [Char] -> Parser [Char]
symbolT "(" Parser [Char] -> Parser a -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a
p Parser a -> Parser [Char] -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< [Char] -> Parser [Char]
symbolT ")."

squaresDot :: Parser a -> Parser a
squaresDot :: Parser a -> Parser a
squaresDot p :: Parser a
p = [Char] -> Parser [Char]
symbolT "[" Parser [Char] -> Parser a -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a
p Parser a -> Parser [Char] -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< [Char] -> Parser [Char]
symbolT "]."

text :: Parser String
text :: Parser [Char]
text = ([Char] -> [Char]) -> Parser [Char] -> Parser [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
forall a. [a] -> [a]
reverse) (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$
    [Char] -> Parser [Char]
symbolT "{*" Parser [Char] -> Parser [Char] -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Char -> Parser [Char] -> Parser [Char]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar ([Char] -> Parser [Char]
symbolT "*}")

listOf :: String -> Parser String
listOf :: [Char] -> Parser [Char]
listOf = [Char] -> Parser [Char]
symbolT ([Char] -> Parser [Char])
-> ([Char] -> [Char]) -> [Char] -> Parser [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("list_of_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)

listOfDot :: String -> Parser String
listOfDot :: [Char] -> Parser [Char]
listOfDot = [Char] -> Parser [Char]
listOf ([Char] -> Parser [Char])
-> ([Char] -> [Char]) -> [Char] -> Parser [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ".")

endOfList :: Parser String
endOfList :: Parser [Char]
endOfList = [Char] -> Parser [Char]
symbolT "end_of_list."

mapTokensToData :: [(String, a)] -> Parser a
mapTokensToData :: [([Char], a)] -> Parser a
mapTokensToData ls :: [([Char], a)]
ls = [Parser a] -> Parser a
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((([Char], a) -> Parser a) -> [([Char], a)] -> [Parser a]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], a) -> Parser a
forall b. ([Char], b) -> ParsecT [Char] () Identity b
tokenToData [([Char], a)]
ls)
    where tokenToData :: ([Char], b) -> ParsecT [Char] () Identity b
tokenToData (s :: [Char]
s, t :: b
t) = [Char] -> Parser [Char]
keywordT [Char]
s Parser [Char]
-> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> ParsecT [Char] () Identity b
forall (m :: * -> *) a. Monad m => a -> m a
return b
t

{- * SPASS Problem
This is the main function of the module
-}

parseSPASS :: Parser SPProblem
parseSPASS :: Parser SPProblem
parseSPASS = Parser ()
whiteSpace Parser () -> Parser SPProblem -> Parser SPProblem
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser SPProblem
problem

problem :: Parser SPProblem
problem :: Parser SPProblem
problem = do
    [Char] -> Parser [Char]
symbolT "begin_problem"
    [Char]
i <- Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
parensDot Parser [Char]
identifierS
    SPDescription
dl <- Parser SPDescription
descriptionList
    SPLogicalPart
lp <- Parser SPLogicalPart
logicalPartP
    [SPSetting]
s <- Parser [SPSetting]
settingList
    [Char] -> Parser [Char]
symbolT "end_problem."
    Parser Char -> Parser [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar
    Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof
    SPProblem -> Parser SPProblem
forall (m :: * -> *) a. Monad m => a -> m a
return SPProblem :: [Char]
-> SPDescription -> SPLogicalPart -> [SPSetting] -> SPProblem
SPProblem
      { identifier :: [Char]
identifier = [Char]
i
      , description :: SPDescription
description = SPDescription
dl
      , logicalPart :: SPLogicalPart
logicalPart = SPLogicalPart
lp
      , settings :: [SPSetting]
settings = [SPSetting]
s}

-- ** SPASS Descriptions

{- | A description is mandatory for a SPASS problem. It has to specify
  at least a 'name', the name of the 'author', the 'status' (see also
  'SPLogState' below), and a (verbose) description. -}
descriptionList :: Parser SPDescription
descriptionList :: Parser SPDescription
descriptionList = do
    [Char] -> Parser [Char]
listOfDot "descriptions"
    [Char] -> Parser [Char]
keywordT "name"
    [Char]
n <- Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
parensDot Parser [Char]
text
    [Char] -> Parser [Char]
keywordT "author"
    [Char]
a <- Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
parensDot Parser [Char]
text
    Maybe [Char]
v <- Parser [Char] -> ParsecT [Char] () Identity (Maybe [Char])
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ([Char] -> Parser [Char]
keywordT "version" Parser [Char] -> Parser [Char] -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
parensDot Parser [Char]
text)
    Maybe [Char]
l <- Parser [Char] -> ParsecT [Char] () Identity (Maybe [Char])
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ([Char] -> Parser [Char]
keywordT "logic" Parser [Char] -> Parser [Char] -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
parensDot Parser [Char]
text)
    SPLogState
s <- [Char] -> Parser [Char]
keywordT "status" Parser [Char]
-> ParsecT [Char] () Identity SPLogState
-> ParsecT [Char] () Identity SPLogState
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] () Identity SPLogState
-> ParsecT [Char] () Identity SPLogState
forall a. Parser a -> Parser a
parensDot ([([Char], SPLogState)] -> ParsecT [Char] () Identity SPLogState
forall a. [([Char], a)] -> Parser a
mapTokensToData
      [ ("satisfiable", SPLogState
SPStateSatisfiable)
      , ("unsatisfiable", SPLogState
SPStateUnsatisfiable)
      , ("unknown", SPLogState
SPStateUnknown)])
    [Char] -> Parser [Char]
keywordT "description"
    [Char]
de <- Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
parensDot Parser [Char]
text
    Maybe [Char]
da <- Parser [Char] -> ParsecT [Char] () Identity (Maybe [Char])
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ([Char] -> Parser [Char]
keywordT "date" Parser [Char] -> Parser [Char] -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
parensDot Parser [Char]
text)
    Parser [Char]
endOfList
    SPDescription -> Parser SPDescription
forall (m :: * -> *) a. Monad m => a -> m a
return SPDescription :: [Char]
-> [Char]
-> Maybe [Char]
-> Maybe [Char]
-> SPLogState
-> [Char]
-> Maybe [Char]
-> SPDescription
SPDescription
      { name :: [Char]
name = [Char]
n
      , author :: [Char]
author = [Char]
a
      , version :: Maybe [Char]
version = Maybe [Char]
v
      , logic :: Maybe [Char]
logic = Maybe [Char]
l
      , status :: SPLogState
status = SPLogState
s
      , desc :: [Char]
desc = [Char]
de
      , date :: Maybe [Char]
date = Maybe [Char]
da }

-- ** SPASS Logical Parts

{- |
  A SPASS logical part consists of a symbol list, a declaration list, and a
  set of formula lists. Support for clause lists and proof lists hasn't
  been implemented yet.
-}
logicalPartP :: Parser SPLogicalPart
logicalPartP :: Parser SPLogicalPart
logicalPartP = do
    Maybe SPSymbolList
sl <- ParsecT [Char] () Identity SPSymbolList
-> ParsecT [Char] () Identity (Maybe SPSymbolList)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT [Char] () Identity SPSymbolList
symbolListP
    Maybe [SPDeclaration]
dl <- ParsecT [Char] () Identity [SPDeclaration]
-> ParsecT [Char] () Identity (Maybe [SPDeclaration])
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT [Char] () Identity [SPDeclaration]
declarationListP
    [SPFormulaList]
fs <- ParsecT [Char] () Identity SPFormulaList
-> ParsecT [Char] () Identity [SPFormulaList]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPFormulaList
formulaList
    [SPClauseList]
cl <- ParsecT [Char] () Identity SPClauseList
-> ParsecT [Char] () Identity [SPClauseList]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPClauseList
clauseList
    [SPProofList]
pl <- ParsecT [Char] () Identity SPProofList
-> ParsecT [Char] () Identity [SPProofList]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPProofList
proofList
    SPLogicalPart -> Parser SPLogicalPart
forall (m :: * -> *) a. Monad m => a -> m a
return SPLogicalPart :: Maybe SPSymbolList
-> Maybe [SPDeclaration]
-> [SPFormulaList]
-> [SPClauseList]
-> [SPProofList]
-> SPLogicalPart
SPLogicalPart
      { symbolList :: Maybe SPSymbolList
symbolList = Maybe SPSymbolList
sl
      , declarationList :: Maybe [SPDeclaration]
declarationList = Maybe [SPDeclaration]
dl
      , formulaLists :: [SPFormulaList]
formulaLists = [SPFormulaList]
fs
      , clauseLists :: [SPClauseList]
clauseLists = [SPClauseList]
cl
      , proofLists :: [SPProofList]
proofLists = [SPProofList]
pl }

-- *** Symbol List

{- |
  SPASS Symbol List
-}
symbolListP :: Parser SPSymbolList
symbolListP :: ParsecT [Char] () Identity SPSymbolList
symbolListP = do
    [Char] -> Parser [Char]
listOfDot "symbols"
    [SPSignSym]
fs <- GenParser Char () [SPSignSym] -> GenParser Char () [SPSignSym]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL ([Char] -> GenParser Char () [SPSignSym]
signSymFor "functions")
    [SPSignSym]
ps <- GenParser Char () [SPSignSym] -> GenParser Char () [SPSignSym]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL ([Char] -> GenParser Char () [SPSignSym]
signSymFor "predicates")
    [SPSignSym]
ss <- GenParser Char () [SPSignSym] -> GenParser Char () [SPSignSym]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL GenParser Char () [SPSignSym]
sortSymFor
    Parser [Char]
endOfList
    SPSymbolList -> ParsecT [Char] () Identity SPSymbolList
forall (m :: * -> *) a. Monad m => a -> m a
return SPSymbolList
emptySymbolList
      { functions :: [SPSignSym]
functions = [SPSignSym]
fs
      , predicates :: [SPSignSym]
predicates = [SPSignSym]
ps
      , sorts :: [SPSignSym]
sorts = [SPSignSym]
ss }

signSymFor :: String -> Parser [SPSignSym]
signSymFor :: [Char] -> GenParser Char () [SPSignSym]
signSymFor kind :: [Char]
kind = [Char] -> Parser [Char]
keywordT [Char]
kind Parser [Char]
-> GenParser Char () [SPSignSym] -> GenParser Char () [SPSignSym]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char () [SPSignSym] -> GenParser Char () [SPSignSym]
forall a. Parser a -> Parser a
squaresDot
    (Parser SPSignSym -> GenParser Char () [SPSignSym]
forall a. Parser a -> Parser [a]
commaSep (Parser SPSignSym -> GenParser Char () [SPSignSym])
-> Parser SPSignSym -> GenParser Char () [SPSignSym]
forall a b. (a -> b) -> a -> b
$ Parser SPSignSym -> Parser SPSignSym
forall a. Parser a -> Parser a
parens Parser SPSignSym
signSym Parser SPSignSym -> Parser SPSignSym -> Parser SPSignSym
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> SPSignSym) -> Parser Token -> Parser SPSignSym
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> SPSignSym
SPSimpleSignSym Parser Token
identifierT)

sortSymFor :: Parser [SPSignSym]
sortSymFor :: GenParser Char () [SPSignSym]
sortSymFor = [Char] -> Parser [Char]
keywordT "sorts" Parser [Char]
-> GenParser Char () [SPSignSym] -> GenParser Char () [SPSignSym]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char () [SPSignSym] -> GenParser Char () [SPSignSym]
forall a. Parser a -> Parser a
squaresDot
    (Parser SPSignSym -> GenParser Char () [SPSignSym]
forall a. Parser a -> Parser [a]
commaSep (Parser SPSignSym -> GenParser Char () [SPSignSym])
-> Parser SPSignSym -> GenParser Char () [SPSignSym]
forall a b. (a -> b) -> a -> b
$ (Token -> SPSignSym) -> Parser Token -> Parser SPSignSym
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> SPSignSym
SPSimpleSignSym Parser Token
identifierT)

signSym :: Parser SPSignSym
signSym :: Parser SPSignSym
signSym = do
    Token
s <- Parser Token
identifierT
    Parser [Char]
comma
    Int
a <- Parser Int
arityT
    SPSignSym -> Parser SPSignSym
forall (m :: * -> *) a. Monad m => a -> m a
return SPSignSym :: Token -> Int -> SPSignSym
SPSignSym {sym :: Token
sym = Token
s, arity :: Int
arity = Int
a}

functList :: Parser [SPIdentifier]
functList :: Parser [Token]
functList = Parser [Token] -> Parser [Token]
forall a. Parser a -> Parser a
squaresDot (Parser [Token] -> Parser [Token])
-> Parser [Token] -> Parser [Token]
forall a b. (a -> b) -> a -> b
$ Parser Token -> Parser [Token]
forall a. Parser a -> Parser [a]
commaSep Parser Token
identifierT

-- *** Formula List

{- |
  SPASS Formula List
-}
formulaList :: Parser SPFormulaList
formulaList :: ParsecT [Char] () Identity SPFormulaList
formulaList = do
    [Char] -> Parser [Char]
listOf "formulae"
    SPOriginType
ot <- Parser SPOriginType -> Parser SPOriginType
forall a. Parser a -> Parser a
parensDot (Parser SPOriginType -> Parser SPOriginType)
-> Parser SPOriginType -> Parser SPOriginType
forall a b. (a -> b) -> a -> b
$ [([Char], SPOriginType)] -> Parser SPOriginType
forall a. [([Char], a)] -> Parser a
mapTokensToData
      [ ("axioms", SPOriginType
SPOriginAxioms)
      , ("conjectures", SPOriginType
SPOriginConjectures)]
    [Named SPTerm]
fs <- ParsecT [Char] () Identity (Named SPTerm)
-> ParsecT [Char] () Identity [Named SPTerm]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT [Char] () Identity (Named SPTerm)
 -> ParsecT [Char] () Identity [Named SPTerm])
-> ParsecT [Char] () Identity (Named SPTerm)
-> ParsecT [Char] () Identity [Named SPTerm]
forall a b. (a -> b) -> a -> b
$ Bool -> ParsecT [Char] () Identity (Named SPTerm)
formula (Bool -> ParsecT [Char] () Identity (Named SPTerm))
-> Bool -> ParsecT [Char] () Identity (Named SPTerm)
forall a b. (a -> b) -> a -> b
$ case SPOriginType
ot of
      SPOriginAxioms -> Bool
True
      _ -> Bool
False
    Parser [Char]
endOfList
    SPFormulaList -> ParsecT [Char] () Identity SPFormulaList
forall (m :: * -> *) a. Monad m => a -> m a
return SPFormulaList :: SPOriginType -> [Named SPTerm] -> SPFormulaList
SPFormulaList { originType :: SPOriginType
originType = SPOriginType
ot, formulae :: [Named SPTerm]
formulae = [Named SPTerm]
fs }

clauseList :: Parser SPClauseList
clauseList :: ParsecT [Char] () Identity SPClauseList
clauseList = do
    [Char] -> Parser [Char]
listOf "clauses"
    (ot :: SPOriginType
ot, ct :: SPClauseType
ct) <- Parser (SPOriginType, SPClauseType)
-> Parser (SPOriginType, SPClauseType)
forall a. Parser a -> Parser a
parensDot (Parser (SPOriginType, SPClauseType)
 -> Parser (SPOriginType, SPClauseType))
-> Parser (SPOriginType, SPClauseType)
-> Parser (SPOriginType, SPClauseType)
forall a b. (a -> b) -> a -> b
$ do
        SPOriginType
ot <- [([Char], SPOriginType)] -> Parser SPOriginType
forall a. [([Char], a)] -> Parser a
mapTokensToData
          [ ("axioms", SPOriginType
SPOriginAxioms)
          , ("conjectures", SPOriginType
SPOriginConjectures)]
        Parser [Char]
comma
        SPClauseType
ct <- [([Char], SPClauseType)] -> Parser SPClauseType
forall a. [([Char], a)] -> Parser a
mapTokensToData [("cnf", SPClauseType
SPCNF), ("dnf", SPClauseType
SPDNF)]
        (SPOriginType, SPClauseType) -> Parser (SPOriginType, SPClauseType)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPOriginType
ot, SPClauseType
ct)
    [SPClause]
fs <- ParsecT [Char] () Identity SPClause
-> ParsecT [Char] () Identity [SPClause]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT [Char] () Identity SPClause
 -> ParsecT [Char] () Identity [SPClause])
-> ParsecT [Char] () Identity SPClause
-> ParsecT [Char] () Identity [SPClause]
forall a b. (a -> b) -> a -> b
$ SPClauseType -> Bool -> ParsecT [Char] () Identity SPClause
clause SPClauseType
ct (Bool -> ParsecT [Char] () Identity SPClause)
-> Bool -> ParsecT [Char] () Identity SPClause
forall a b. (a -> b) -> a -> b
$ case SPOriginType
ot of
      SPOriginAxioms -> Bool
True
      _ -> Bool
False
    Parser [Char]
endOfList
    SPClauseList -> ParsecT [Char] () Identity SPClauseList
forall (m :: * -> *) a. Monad m => a -> m a
return SPClauseList :: SPOriginType -> SPClauseType -> [SPClause] -> SPClauseList
SPClauseList
      { coriginType :: SPOriginType
coriginType = SPOriginType
ot
      , clauseType :: SPClauseType
clauseType = SPClauseType
ct
      , clauses :: [SPClause]
clauses = [SPClause]
fs }

clause :: SPClauseType -> Bool -> Parser SPClause
clause :: SPClauseType -> Bool -> ParsecT [Char] () Identity SPClause
clause ct :: SPClauseType
ct bool :: Bool
bool = [Char] -> Parser [Char]
keywordT "clause" Parser [Char]
-> ParsecT [Char] () Identity SPClause
-> ParsecT [Char] () Identity SPClause
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] () Identity SPClause
-> ParsecT [Char] () Identity SPClause
forall a. Parser a -> Parser a
parensDot (do
    NSPClause
sen <- SPClauseType -> Parser NSPClause
clauseFork SPClauseType
ct
    [Char]
cname <- Parser [Char] -> Parser [Char]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Parser [Char]
comma Parser [Char] -> Parser [Char] -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Char]
identifierS)
    SPClause -> ParsecT [Char] () Identity SPClause
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> NSPClause -> SPClause
forall a s. a -> s -> SenAttr s a
makeNamed [Char]
cname NSPClause
sen) { isAxiom :: Bool
isAxiom = Bool
bool })

clauseFork :: SPClauseType -> Parser NSPClause
clauseFork :: SPClauseType -> Parser NSPClause
clauseFork ct :: SPClauseType
ct = do
  termWsList1 :: TermWsList
termWsList1@(TWL ls :: [SPTerm]
ls b :: Bool
b) <- Parser TermWsList
termWsList
  do [Char] -> Parser [Char]
symbolT "||"
     TermWsList
termWsList2 <- Parser TermWsList
termWsList
     [Char] -> Parser [Char]
symbolT "->"
     TermWsList
termWsList3 <- Parser TermWsList
termWsList
     NSPClause -> Parser NSPClause
forall (m :: * -> *) a. Monad m => a -> m a
return (TermWsList -> TermWsList -> TermWsList -> NSPClause
BriefClause TermWsList
termWsList1 TermWsList
termWsList2 TermWsList
termWsList3)
    Parser NSPClause -> Parser NSPClause -> Parser NSPClause
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> case [SPTerm]
ls of
          [t :: SPTerm
t] | Bool -> Bool
not Bool
b -> SPClauseType -> SPTerm -> Parser NSPClause
forall (m :: * -> *).
MonadFail m =>
SPClauseType -> SPTerm -> m NSPClause
toNSPClause SPClauseType
ct SPTerm
t
          _ -> [Char] -> Parser NSPClause
forall s (m :: * -> *) t u a.
Stream s m t =>
[Char] -> ParsecT s u m a
unexpected "clause term"

toNSPClause :: Fail.MonadFail m => SPClauseType -> SPTerm -> m NSPClause
toNSPClause :: SPClauseType -> SPTerm -> m NSPClause
toNSPClause ct :: SPClauseType
ct t :: SPTerm
t = case SPTerm
t of
    SPQuantTerm q :: SPQuantSym
q vl :: [SPTerm]
vl l :: SPTerm
l | SPQuantSym
q SPQuantSym -> SPQuantSym -> Bool
forall a. Eq a => a -> a -> Bool
== SPQuantSym
SPForall Bool -> Bool -> Bool
&& SPClauseType
ct SPClauseType -> SPClauseType -> Bool
forall a. Eq a => a -> a -> Bool
== SPClauseType
SPCNF
        Bool -> Bool -> Bool
|| SPQuantSym
q SPQuantSym -> SPQuantSym -> Bool
forall a. Eq a => a -> a -> Bool
== SPQuantSym
SPExists Bool -> Bool -> Bool
&& SPClauseType
ct SPClauseType -> SPClauseType -> Bool
forall a. Eq a => a -> a -> Bool
== SPClauseType
SPDNF -> do
        NSPClauseBody
b <- SPClauseType -> SPTerm -> m NSPClauseBody
forall (m :: * -> *).
MonadFail m =>
SPClauseType -> SPTerm -> m NSPClauseBody
toClauseBody SPClauseType
ct SPTerm
l
        NSPClause -> m NSPClause
forall (m :: * -> *) a. Monad m => a -> m a
return (NSPClause -> m NSPClause) -> NSPClause -> m NSPClause
forall a b. (a -> b) -> a -> b
$ [SPTerm] -> NSPClauseBody -> NSPClause
QuanClause [SPTerm]
vl NSPClauseBody
b
    _ -> do
        NSPClauseBody
b <- SPClauseType -> SPTerm -> m NSPClauseBody
forall (m :: * -> *).
MonadFail m =>
SPClauseType -> SPTerm -> m NSPClauseBody
toClauseBody SPClauseType
ct SPTerm
t
        NSPClause -> m NSPClause
forall (m :: * -> *) a. Monad m => a -> m a
return (NSPClause -> m NSPClause) -> NSPClause -> m NSPClause
forall a b. (a -> b) -> a -> b
$ NSPClauseBody -> NSPClause
SimpleClause NSPClauseBody
b

termWsList :: Parser TermWsList
termWsList :: Parser TermWsList
termWsList = do
    [SPTerm]
twl <- ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity [SPTerm]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPTerm
term
    Maybe [Char]
p <- Parser [Char] -> ParsecT [Char] () Identity (Maybe [Char])
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ([Char] -> Parser [Char]
symbolT "+")
    TermWsList -> Parser TermWsList
forall (m :: * -> *) a. Monad m => a -> m a
return (TermWsList -> Parser TermWsList)
-> TermWsList -> Parser TermWsList
forall a b. (a -> b) -> a -> b
$ [SPTerm] -> Bool -> TermWsList
TWL [SPTerm]
twl (Bool -> TermWsList) -> Bool -> TermWsList
forall a b. (a -> b) -> a -> b
$ Maybe [Char] -> Bool
forall a. Maybe a -> Bool
isJust Maybe [Char]
p

formula :: Bool -> Parser (Named SoftFOL.Sign.SPTerm)
formula :: Bool -> ParsecT [Char] () Identity (Named SPTerm)
formula bool :: Bool
bool = [Char] -> Parser [Char]
keywordT "formula" Parser [Char]
-> ParsecT [Char] () Identity (Named SPTerm)
-> ParsecT [Char] () Identity (Named SPTerm)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] () Identity (Named SPTerm)
-> ParsecT [Char] () Identity (Named SPTerm)
forall a. Parser a -> Parser a
parensDot (do
     SPTerm
sen <- ParsecT [Char] () Identity SPTerm
term
     [Char]
fname <- Parser [Char] -> Parser [Char]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Parser [Char]
comma Parser [Char] -> Parser [Char] -> Parser [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Char]
identifierS)
     Named SPTerm -> ParsecT [Char] () Identity (Named SPTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> SPTerm -> Named SPTerm
forall a s. a -> s -> SenAttr s a
makeNamed [Char]
fname SPTerm
sen) { isAxiom :: Bool
isAxiom = Bool
bool })

declarationListP :: Parser [SPDeclaration]
declarationListP :: ParsecT [Char] () Identity [SPDeclaration]
declarationListP = do
    [Char] -> Parser [Char]
listOfDot "declarations"
    [SPDeclaration]
decl <- ParsecT [Char] () Identity SPDeclaration
-> ParsecT [Char] () Identity [SPDeclaration]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPDeclaration
declaration
    Parser [Char]
endOfList
    [SPDeclaration] -> ParsecT [Char] () Identity [SPDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return [SPDeclaration]
decl

declaration :: Parser SPDeclaration
declaration :: ParsecT [Char] () Identity SPDeclaration
declaration = do
    [Char] -> Parser [Char]
keywordT "sort"
    Token
sortName <- Parser Token
identifierT
    Bool
maybeFreely <- Bool
-> ParsecT [Char] () Identity Bool
-> ParsecT [Char] () Identity Bool
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Bool
False ([Char] -> Parser [Char]
keywordT "freely" Parser [Char]
-> ParsecT [Char] () Identity Bool
-> ParsecT [Char] () Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ParsecT [Char] () Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
    [Char] -> Parser [Char]
keywordT "generated by"
    [Token]
funList <- Parser [Token]
functList
    SPDeclaration -> ParsecT [Char] () Identity SPDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return SPGenDecl :: Token -> Bool -> [Token] -> SPDeclaration
SPGenDecl
      { sortSym :: Token
sortSym = Token
sortName
      , freelyGenerated :: Bool
freelyGenerated = Bool
maybeFreely
      , funcList :: [Token]
funcList = [Token]
funList }
  ParsecT [Char] () Identity SPDeclaration
-> ParsecT [Char] () Identity SPDeclaration
-> ParsecT [Char] () Identity SPDeclaration
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    [Char] -> Parser [Char]
keywordT "subsort"
    (s1 :: Token
s1, s2 :: Token
s2) <- Parser (Token, Token) -> Parser (Token, Token)
forall a. Parser a -> Parser a
parensDot (Parser (Token, Token) -> Parser (Token, Token))
-> Parser (Token, Token) -> Parser (Token, Token)
forall a b. (a -> b) -> a -> b
$ do
        Token
s1 <- Parser Token
identifierT
        Parser [Char]
comma
        Token
s2 <- Parser Token
identifierT
        (Token, Token) -> Parser (Token, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
s1, Token
s2)
    SPDeclaration -> ParsecT [Char] () Identity SPDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return SPSubsortDecl :: Token -> Token -> SPDeclaration
SPSubsortDecl { sortSymA :: Token
sortSymA = Token
s1, sortSymB :: Token
sortSymB = Token
s2 }
  ParsecT [Char] () Identity SPDeclaration
-> ParsecT [Char] () Identity SPDeclaration
-> ParsecT [Char] () Identity SPDeclaration
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    [Char] -> Parser [Char]
keywordT "predicate"
    (pn :: Token
pn, sl :: [Token]
sl) <- Parser (Token, [Token]) -> Parser (Token, [Token])
forall a. Parser a -> Parser a
parensDot (Parser (Token, [Token]) -> Parser (Token, [Token]))
-> Parser (Token, [Token]) -> Parser (Token, [Token])
forall a b. (a -> b) -> a -> b
$ do
        Token
pn <- Parser Token
identifierT
        Parser [Char]
comma
        [Token]
sl <- Parser Token -> Parser [Token]
forall a. Parser a -> Parser [a]
commaSep Parser Token
identifierT
        (Token, [Token]) -> Parser (Token, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
pn, [Token]
sl)
    SPDeclaration -> ParsecT [Char] () Identity SPDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return SPPredDecl :: Token -> [Token] -> SPDeclaration
SPPredDecl { predSym :: Token
predSym = Token
pn, sortSyms :: [Token]
sortSyms = [Token]
sl }
  ParsecT [Char] () Identity SPDeclaration
-> ParsecT [Char] () Identity SPDeclaration
-> ParsecT [Char] () Identity SPDeclaration
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    SPTerm
t <- ParsecT [Char] () Identity SPTerm
term
    Parser [Char]
dot
    SPDeclaration -> ParsecT [Char] () Identity SPDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return (SPDeclaration -> ParsecT [Char] () Identity SPDeclaration)
-> SPDeclaration -> ParsecT [Char] () Identity SPDeclaration
forall a b. (a -> b) -> a -> b
$ case SPTerm
t of
      SPQuantTerm SPForall tlist :: [SPTerm]
tlist tb :: SPTerm
tb ->
          SPTermDecl :: [SPTerm] -> SPTerm -> SPDeclaration
SPTermDecl { termDeclTermList :: [SPTerm]
termDeclTermList = [SPTerm]
tlist, termDeclTerm :: SPTerm
termDeclTerm = SPTerm
tb }
      _ -> SPTerm -> SPDeclaration
SPSimpleTermDecl SPTerm
t

-- | SPASS Proof List
proofList :: Parser SPProofList
proofList :: ParsecT [Char] () Identity SPProofList
proofList = do
    [Char] -> Parser [Char]
listOf "proof"
    Maybe (Maybe Token, Map SPKey SPValue)
pa <- ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
-> ParsecT
     [Char] () Identity (Maybe (Maybe Token, Map SPKey SPValue))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
 -> ParsecT
      [Char] () Identity (Maybe (Maybe Token, Map SPKey SPValue)))
-> ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
-> ParsecT
     [Char] () Identity (Maybe (Maybe Token, Map SPKey SPValue))
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
-> ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
forall a. Parser a -> Parser a
parensDot (ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
 -> ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue))
-> ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
-> ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
forall a b. (a -> b) -> a -> b
$ do
        Maybe Token
pt <- Parser Token -> ParsecT [Char] () Identity (Maybe Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe Parser Token
getproofType
        Map SPKey SPValue
assList <- Map SPKey SPValue
-> ParsecT [Char] () Identity (Map SPKey SPValue)
-> ParsecT [Char] () Identity (Map SPKey SPValue)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Map SPKey SPValue
forall k a. Map k a
Map.empty (Parser [Char]
comma Parser [Char]
-> ParsecT [Char] () Identity (Map SPKey SPValue)
-> ParsecT [Char] () Identity (Map SPKey SPValue)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] () Identity (Map SPKey SPValue)
assocList)
        (Maybe Token, Map SPKey SPValue)
-> ParsecT [Char] () Identity (Maybe Token, Map SPKey SPValue)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Token
pt, Map SPKey SPValue
assList)
    [SPProofStep]
steps <- ParsecT [Char] () Identity SPProofStep
-> ParsecT [Char] () Identity [SPProofStep]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPProofStep
proofStep
    Parser [Char]
endOfList
    SPProofList -> ParsecT [Char] () Identity SPProofList
forall (m :: * -> *) a. Monad m => a -> m a
return (SPProofList -> ParsecT [Char] () Identity SPProofList)
-> SPProofList -> ParsecT [Char] () Identity SPProofList
forall a b. (a -> b) -> a -> b
$ case Maybe (Maybe Token, Map SPKey SPValue)
pa of
      Nothing -> SPProofList :: Maybe Token -> Map SPKey SPValue -> [SPProofStep] -> SPProofList
SPProofList
        { proofType :: Maybe Token
proofType = Maybe Token
forall a. Maybe a
Nothing
        , plAssocList :: Map SPKey SPValue
plAssocList = Map SPKey SPValue
forall k a. Map k a
Map.empty
        , step :: [SPProofStep]
step = [SPProofStep]
steps}
      Just (pt :: Maybe Token
pt, mal :: Map SPKey SPValue
mal) -> SPProofList :: Maybe Token -> Map SPKey SPValue -> [SPProofStep] -> SPProofList
SPProofList
        { proofType :: Maybe Token
proofType = Maybe Token
pt
        , plAssocList :: Map SPKey SPValue
plAssocList = Map SPKey SPValue
mal
        , step :: [SPProofStep]
step = [SPProofStep]
steps}

getproofType :: Parser SPIdentifier
getproofType :: Parser Token
getproofType = Parser Token
identifierT

assocList :: Parser SPAssocList
assocList :: ParsecT [Char] () Identity (Map SPKey SPValue)
assocList = ([(SPKey, SPValue)] -> Map SPKey SPValue)
-> ParsecT [Char] () Identity [(SPKey, SPValue)]
-> ParsecT [Char] () Identity (Map SPKey SPValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(SPKey, SPValue)] -> Map SPKey SPValue
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (ParsecT [Char] () Identity [(SPKey, SPValue)]
 -> ParsecT [Char] () Identity (Map SPKey SPValue))
-> ParsecT [Char] () Identity [(SPKey, SPValue)]
-> ParsecT [Char] () Identity (Map SPKey SPValue)
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] () Identity [(SPKey, SPValue)]
-> ParsecT [Char] () Identity [(SPKey, SPValue)]
forall a. Parser a -> Parser a
squares (ParsecT [Char] () Identity [(SPKey, SPValue)]
 -> ParsecT [Char] () Identity [(SPKey, SPValue)])
-> ParsecT [Char] () Identity [(SPKey, SPValue)]
-> ParsecT [Char] () Identity [(SPKey, SPValue)]
forall a b. (a -> b) -> a -> b
$ Parser (SPKey, SPValue)
-> ParsecT [Char] () Identity [(SPKey, SPValue)]
forall a. Parser a -> Parser [a]
commaSep
  (Parser (SPKey, SPValue)
 -> ParsecT [Char] () Identity [(SPKey, SPValue)])
-> Parser (SPKey, SPValue)
-> ParsecT [Char] () Identity [(SPKey, SPValue)]
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] () Identity SPKey
-> ParsecT [Char] () Identity SPValue -> Parser (SPKey, SPValue)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair ParsecT [Char] () Identity SPKey
getKey (ParsecT [Char] () Identity SPValue -> Parser (SPKey, SPValue))
-> ParsecT [Char] () Identity SPValue -> Parser (SPKey, SPValue)
forall a b. (a -> b) -> a -> b
$ [Char] -> Parser [Char]
symbolT ":" Parser [Char]
-> ParsecT [Char] () Identity SPValue
-> ParsecT [Char] () Identity SPValue
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] () Identity SPValue
getValue

getKey :: Parser SPKey
getKey :: ParsecT [Char] () Identity SPKey
getKey = (SPTerm -> SPKey)
-> ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity SPKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SPTerm -> SPKey
PKeyTerm ParsecT [Char] () Identity SPTerm
term

getValue :: Parser SPValue
getValue :: ParsecT [Char] () Identity SPValue
getValue = (SPTerm -> SPValue)
-> ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity SPValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SPTerm -> SPValue
PValTerm ParsecT [Char] () Identity SPTerm
term

proofStep :: Parser SPProofStep
proofStep :: ParsecT [Char] () Identity SPProofStep
proofStep = do
    [Char] -> Parser [Char]
keywordT "step"
    (ref :: SPReference
ref, res :: SPResult
res, rule :: SPRuleAppl
rule, pl :: [SPParent]
pl, mal :: Map SPKey SPValue
mal) <- Parser
  (SPReference, SPResult, SPRuleAppl, [SPParent], Map SPKey SPValue)
-> Parser
     (SPReference, SPResult, SPRuleAppl, [SPParent], Map SPKey SPValue)
forall a. Parser a -> Parser a
parensDot Parser
  (SPReference, SPResult, SPRuleAppl, [SPParent], Map SPKey SPValue)
takeStep
    SPProofStep -> ParsecT [Char] () Identity SPProofStep
forall (m :: * -> *) a. Monad m => a -> m a
return SPProofStep :: SPReference
-> SPResult
-> SPRuleAppl
-> [SPParent]
-> Map SPKey SPValue
-> SPProofStep
SPProofStep
      { reference :: SPReference
reference = SPReference
ref
      , result :: SPResult
result = SPResult
res
      , ruleAppl :: SPRuleAppl
ruleAppl = SPRuleAppl
rule
      , parentList :: [SPParent]
parentList = [SPParent]
pl
      , stepAssocList :: Map SPKey SPValue
stepAssocList = Map SPKey SPValue
mal}
  where takeStep :: Parser
  (SPReference, SPResult, SPRuleAppl, [SPParent], Map SPKey SPValue)
takeStep = do
          SPReference
ref <- ParsecT [Char] () Identity SPReference
getReference
          Parser [Char]
comma
          SPResult
res <- ParsecT [Char] () Identity SPResult
getResult
          Parser [Char]
comma
          SPRuleAppl
rule <- ParsecT [Char] () Identity SPRuleAppl
getRuleAppl
          Parser [Char]
comma
          [SPParent]
pl <- Parser [SPParent]
getParentList
          Map SPKey SPValue
mal <- Map SPKey SPValue
-> ParsecT [Char] () Identity (Map SPKey SPValue)
-> ParsecT [Char] () Identity (Map SPKey SPValue)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Map SPKey SPValue
forall k a. Map k a
Map.empty (Parser [Char]
comma Parser [Char]
-> ParsecT [Char] () Identity (Map SPKey SPValue)
-> ParsecT [Char] () Identity (Map SPKey SPValue)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] () Identity (Map SPKey SPValue)
assocList)
          (SPReference, SPResult, SPRuleAppl, [SPParent], Map SPKey SPValue)
-> Parser
     (SPReference, SPResult, SPRuleAppl, [SPParent], Map SPKey SPValue)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPReference
ref, SPResult
res, SPRuleAppl
rule, [SPParent]
pl, Map SPKey SPValue
mal)

        getReference :: ParsecT [Char] () Identity SPReference
getReference = (SPTerm -> SPReference)
-> ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity SPReference
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SPTerm -> SPReference
PRefTerm ParsecT [Char] () Identity SPTerm
term
        getResult :: ParsecT [Char] () Identity SPResult
getResult = (SPTerm -> SPResult)
-> ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity SPResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SPTerm -> SPResult
PResTerm ParsecT [Char] () Identity SPTerm
term
        getRuleAppl :: ParsecT [Char] () Identity SPRuleAppl
getRuleAppl = do
          SPTerm
t <- ParsecT [Char] () Identity SPTerm
term
          let r :: SPRuleAppl
r = SPTerm -> SPRuleAppl
PRuleTerm SPTerm
t
          SPRuleAppl -> ParsecT [Char] () Identity SPRuleAppl
forall (m :: * -> *) a. Monad m => a -> m a
return (SPRuleAppl -> ParsecT [Char] () Identity SPRuleAppl)
-> SPRuleAppl -> ParsecT [Char] () Identity SPRuleAppl
forall a b. (a -> b) -> a -> b
$ case SPTerm
t of
            SPComplexTerm (SPCustomSymbol ide :: Token
ide) [] -> case [Char] -> [([Char], SPUserRuleAppl)] -> Maybe SPUserRuleAppl
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Token -> [Char]
tokStr Token
ide)
                ([([Char], SPUserRuleAppl)] -> Maybe SPUserRuleAppl)
-> [([Char], SPUserRuleAppl)] -> Maybe SPUserRuleAppl
forall a b. (a -> b) -> a -> b
$ (SPUserRuleAppl -> ([Char], SPUserRuleAppl))
-> [SPUserRuleAppl] -> [([Char], SPUserRuleAppl)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ z :: SPUserRuleAppl
z -> (SPUserRuleAppl -> [Char]
forall a. Show a => a -> [Char]
show SPUserRuleAppl
z, SPUserRuleAppl
z))
                [SPUserRuleAppl
GeR, SPUserRuleAppl
SpL,
                 SPUserRuleAppl
SpR, SPUserRuleAppl
EqF,
                 SPUserRuleAppl
Rew, SPUserRuleAppl
Obv,
                 SPUserRuleAppl
EmS, SPUserRuleAppl
SoR,
                 SPUserRuleAppl
EqR, SPUserRuleAppl
Mpm,
                 SPUserRuleAppl
SPm, SPUserRuleAppl
OPm,
                 SPUserRuleAppl
SHy, SPUserRuleAppl
OHy,
                 SPUserRuleAppl
URR, SPUserRuleAppl
Fac,
                 SPUserRuleAppl
Spt, SPUserRuleAppl
Inp,
                 SPUserRuleAppl
Con, SPUserRuleAppl
RRE,
                 SPUserRuleAppl
SSi, SPUserRuleAppl
ClR,
                 SPUserRuleAppl
UnC, SPUserRuleAppl
Ter] of
              Just u :: SPUserRuleAppl
u -> SPUserRuleAppl -> SPRuleAppl
PRuleUser SPUserRuleAppl
u
              Nothing -> SPRuleAppl
r
            _ -> SPRuleAppl
r
        getParentList :: Parser [SPParent]
getParentList = Parser [SPParent] -> Parser [SPParent]
forall a. Parser a -> Parser a
squares (Parser [SPParent] -> Parser [SPParent])
-> Parser [SPParent] -> Parser [SPParent]
forall a b. (a -> b) -> a -> b
$ Parser SPParent -> Parser [SPParent]
forall a. Parser a -> Parser [a]
commaSep Parser SPParent
getParent
        getParent :: Parser SPParent
getParent = (SPTerm -> SPParent)
-> ParsecT [Char] () Identity SPTerm -> Parser SPParent
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SPTerm -> SPParent
PParTerm ParsecT [Char] () Identity SPTerm
term

-- SPASS Settings.
settingList :: Parser [SPSetting]
settingList :: Parser [SPSetting]
settingList = ParsecT [Char] () Identity SPSetting -> Parser [SPSetting]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPSetting
setting

setting :: Parser SPSetting
setting :: ParsecT [Char] () Identity SPSetting
setting = do
    [Char] -> Parser [Char]
listOfDot "general_settings"
    [SPHypothesis]
entriesList <- ParsecT [Char] () Identity SPHypothesis
-> ParsecT [Char] () Identity [SPHypothesis]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPHypothesis
settingEntry
    Parser [Char]
endOfList
    SPSetting -> ParsecT [Char] () Identity SPSetting
forall (m :: * -> *) a. Monad m => a -> m a
return SPGeneralSettings :: [SPHypothesis] -> SPSetting
SPGeneralSettings {entries :: [SPHypothesis]
entries = [SPHypothesis]
entriesList}
  ParsecT [Char] () Identity SPSetting
-> ParsecT [Char] () Identity SPSetting
-> ParsecT [Char] () Identity SPSetting
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    [Char] -> Parser [Char]
listOf "settings"
    SPSettingLabel
slabel <- Parser SPSettingLabel -> Parser SPSettingLabel
forall a. Parser a -> Parser a
parensDot Parser SPSettingLabel
getLabel
    [Char] -> Parser [Char]
symbolT "{*"
    [SPSettingBody]
t <- ParsecT [Char] () Identity SPSettingBody
-> ParsecT [Char] () Identity [SPSettingBody]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] () Identity SPSettingBody
clauseFormulaRelation
    [Char] -> Parser [Char]
symbolT "*}"
    Parser [Char]
endOfList
    SPSetting -> ParsecT [Char] () Identity SPSetting
forall (m :: * -> *) a. Monad m => a -> m a
return SPSettings :: SPSettingLabel -> [SPSettingBody] -> SPSetting
SPSettings {settingName :: SPSettingLabel
settingName = SPSettingLabel
slabel, settingBody :: [SPSettingBody]
settingBody = [SPSettingBody]
t}

settingEntry :: Parser SPHypothesis
settingEntry :: ParsecT [Char] () Identity SPHypothesis
settingEntry = do
    [Char] -> Parser [Char]
keywordT "hypothesis"
    [Token]
slabels <- Parser [Token] -> Parser [Token]
forall a. Parser a -> Parser a
squaresDot (Parser Token -> Parser [Token]
forall a. Parser a -> Parser [a]
commaSep Parser Token
identifierT)
    SPHypothesis -> ParsecT [Char] () Identity SPHypothesis
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> SPHypothesis
SPHypothesis [Token]
slabels)

getLabel :: Parser SPSettingLabel
getLabel :: Parser SPSettingLabel
getLabel = [([Char], SPSettingLabel)] -> Parser SPSettingLabel
forall a. [([Char], a)] -> Parser a
mapTokensToData ([([Char], SPSettingLabel)] -> Parser SPSettingLabel)
-> [([Char], SPSettingLabel)] -> Parser SPSettingLabel
forall a b. (a -> b) -> a -> b
$ (SPSettingLabel -> ([Char], SPSettingLabel))
-> [SPSettingLabel] -> [([Char], SPSettingLabel)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ z :: SPSettingLabel
z -> (SPSettingLabel -> [Char]
showSettingLabel SPSettingLabel
z, SPSettingLabel
z))
    [SPSettingLabel
KIV, SPSettingLabel
LEM, SPSettingLabel
OTTER, SPSettingLabel
PROTEIN, SPSettingLabel
SATURATE, SPSettingLabel
ThreeTAP, SPSettingLabel
SETHEO, SPSettingLabel
SPASS]

-- SPASS Clause-Formula Relation

clauseFormulaRelation :: Parser SPSettingBody
clauseFormulaRelation :: ParsecT [Char] () Identity SPSettingBody
clauseFormulaRelation = do
    [Char] -> Parser [Char]
keywordT "set_ClauseFormulaRelation"
    [SPCRBIND]
cfr <- Parser [SPCRBIND] -> Parser [SPCRBIND]
forall a. Parser a -> Parser a
parensDot (Parser [SPCRBIND] -> Parser [SPCRBIND])
-> Parser [SPCRBIND] -> Parser [SPCRBIND]
forall a b. (a -> b) -> a -> b
$ (ParsecT [Char] () Identity SPCRBIND
 -> Parser [Char] -> Parser [SPCRBIND])
-> Parser [Char]
-> ParsecT [Char] () Identity SPCRBIND
-> Parser [SPCRBIND]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ParsecT [Char] () Identity SPCRBIND
-> Parser [Char] -> Parser [SPCRBIND]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
sepBy Parser [Char]
comma (ParsecT [Char] () Identity SPCRBIND -> Parser [SPCRBIND])
-> ParsecT [Char] () Identity SPCRBIND -> Parser [SPCRBIND]
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] () Identity SPCRBIND
-> ParsecT [Char] () Identity SPCRBIND
forall a. Parser a -> Parser a
parens (ParsecT [Char] () Identity SPCRBIND
 -> ParsecT [Char] () Identity SPCRBIND)
-> ParsecT [Char] () Identity SPCRBIND
-> ParsecT [Char] () Identity SPCRBIND
forall a b. (a -> b) -> a -> b
$ do
        [Char]
i1 <- Parser [Char]
identifierS
        Parser [Char]
comma
        [Char]
i2 <- Parser [Char]
identifierS
        SPCRBIND -> ParsecT [Char] () Identity SPCRBIND
forall (m :: * -> *) a. Monad m => a -> m a
return (SPCRBIND -> ParsecT [Char] () Identity SPCRBIND)
-> SPCRBIND -> ParsecT [Char] () Identity SPCRBIND
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> SPCRBIND
SPCRBIND [Char]
i1 [Char]
i2
    SPSettingBody -> ParsecT [Char] () Identity SPSettingBody
forall (m :: * -> *) a. Monad m => a -> m a
return ([SPCRBIND] -> SPSettingBody
SPClauseRelation [SPCRBIND]
cfr)
  ParsecT [Char] () Identity SPSettingBody
-> ParsecT [Char] () Identity SPSettingBody
-> ParsecT [Char] () Identity SPSettingBody
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    [Char]
t' <- Parser [Char]
identifierS
    [[Char]]
al <- Parser [[Char]] -> Parser [[Char]]
forall a. Parser a -> Parser a
parensDot (Parser [Char] -> Parser [[Char]]
forall a. Parser a -> Parser [a]
commaSep Parser [Char]
identifierS)
    SPSettingBody -> ParsecT [Char] () Identity SPSettingBody
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> [[Char]] -> SPSettingBody
SPFlag [Char]
t' [[Char]]
al)

-- *** Terms

{- |
  A SPASS Term.
-}

term :: Parser SPTerm
term :: ParsecT [Char] () Identity SPTerm
term = do
    Token
i <- Parser Token
identifierT
    let iStr :: [Char]
iStr = Token -> [Char]
tokStr Token
i
    case [Char] -> [([Char], SPSymbol)] -> Maybe SPSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
iStr [("true", SPSymbol
SPTrue), ("false", SPSymbol
SPFalse)] of
      Just s :: SPSymbol
s -> SPTerm -> ParsecT [Char] () Identity SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> ParsecT [Char] () Identity SPTerm)
-> SPTerm -> ParsecT [Char] () Identity SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> SPTerm
simpTerm SPSymbol
s
      Nothing -> do
        let s :: SPSymbol
s = Token -> SPSymbol
spSym Token
i
        SPTerm
-> ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity SPTerm
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (SPSymbol -> SPTerm
simpTerm SPSymbol
s) (ParsecT [Char] () Identity SPTerm
 -> ParsecT [Char] () Identity SPTerm)
-> ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity SPTerm
forall a b. (a -> b) -> a -> b
$ do
          (ts :: [SPTerm]
ts, as :: [SPTerm]
as@(a :: SPTerm
a : _)) <- Parser ([SPTerm], [SPTerm]) -> Parser ([SPTerm], [SPTerm])
forall a. Parser a -> Parser a
parens (Parser ([SPTerm], [SPTerm]) -> Parser ([SPTerm], [SPTerm]))
-> Parser ([SPTerm], [SPTerm]) -> Parser ([SPTerm], [SPTerm])
forall a b. (a -> b) -> a -> b
$ do
            [SPTerm]
ts <- ParsecT [Char] () Identity [SPTerm]
-> ParsecT [Char] () Identity [SPTerm]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (ParsecT [Char] () Identity [SPTerm]
-> ParsecT [Char] () Identity [SPTerm]
forall a. Parser a -> Parser a
squares (ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity [SPTerm]
forall a. Parser a -> Parser [a]
commaSep ParsecT [Char] () Identity SPTerm
term) ParsecT [Char] () Identity [SPTerm]
-> Parser [Char] -> ParsecT [Char] () Identity [SPTerm]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser [Char]
comma)
            [SPTerm]
as <- if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
ts then ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity [SPTerm]
forall a. Parser a -> Parser [a]
commaSep ParsecT [Char] () Identity SPTerm
term
                  else (SPTerm -> [SPTerm])
-> ParsecT [Char] () Identity SPTerm
-> ParsecT [Char] () Identity [SPTerm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SPTerm -> [SPTerm] -> [SPTerm]
forall a. a -> [a] -> [a]
: []) ParsecT [Char] () Identity SPTerm
term
            ([SPTerm], [SPTerm]) -> Parser ([SPTerm], [SPTerm])
forall (m :: * -> *) a. Monad m => a -> m a
return ([SPTerm]
ts, [SPTerm]
as)
          if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
ts then if [Char] -> [[Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Char]
iStr [ "forall", "exists", "true", "false"]
              then [Char] -> ParsecT [Char] () Identity SPTerm
forall s (m :: * -> *) t u a.
Stream s m t =>
[Char] -> ParsecT s u m a
unexpected ([Char] -> ParsecT [Char] () Identity SPTerm)
-> [Char] -> ParsecT [Char] () Identity SPTerm
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
iStr else SPTerm -> ParsecT [Char] () Identity SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> ParsecT [Char] () Identity SPTerm)
-> SPTerm -> ParsecT [Char] () Identity SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm
               (SPSymbol -> Maybe SPSymbol -> SPSymbol
forall a. a -> Maybe a -> a
fromMaybe SPSymbol
s ([Char] -> [([Char], SPSymbol)] -> Maybe SPSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
iStr ([([Char], SPSymbol)] -> Maybe SPSymbol)
-> [([Char], SPSymbol)] -> Maybe SPSymbol
forall a b. (a -> b) -> a -> b
$ (SPSymbol -> ([Char], SPSymbol))
-> [SPSymbol] -> [([Char], SPSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ z :: SPSymbol
z -> (SPSymbol -> [Char]
showSPSymbol SPSymbol
z, SPSymbol
z))
                         [ SPSymbol
SPEqual
                         , SPSymbol
SPOr
                         , SPSymbol
SPAnd
                         , SPSymbol
SPNot
                         , SPSymbol
SPImplies
                         , SPSymbol
SPImplied
                         , SPSymbol
SPEquiv])) [SPTerm]
as
            else SPTerm -> ParsecT [Char] () Identity SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return SPQuantTerm :: SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm
              { quantSym :: SPQuantSym
quantSym = SPQuantSym -> Maybe SPQuantSym -> SPQuantSym
forall a. a -> Maybe a -> a
fromMaybe (Token -> SPQuantSym
SPCustomQuantSym Token
i) (Maybe SPQuantSym -> SPQuantSym) -> Maybe SPQuantSym -> SPQuantSym
forall a b. (a -> b) -> a -> b
$ [Char] -> [([Char], SPQuantSym)] -> Maybe SPQuantSym
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
iStr
                            [("forall", SPQuantSym
SPForall), ("exists", SPQuantSym
SPExists)]
              , variableList :: [SPTerm]
variableList = [SPTerm]
ts, qFormula :: SPTerm
qFormula = SPTerm
a }

toClauseBody :: Fail.MonadFail m => SPClauseType -> SPTerm -> m NSPClauseBody
toClauseBody :: SPClauseType -> SPTerm -> m NSPClauseBody
toClauseBody b :: SPClauseType
b t :: SPTerm
t = case SPTerm
t of
    SPComplexTerm n :: SPSymbol
n ts :: [SPTerm]
ts | SPClauseType
b SPClauseType -> SPClauseType -> Bool
forall a. Eq a => a -> a -> Bool
== SPClauseType
SPCNF Bool -> Bool -> Bool
&& SPSymbol
n SPSymbol -> SPSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== SPSymbol
SPOr Bool -> Bool -> Bool
|| SPClauseType
b SPClauseType -> SPClauseType -> Bool
forall a. Eq a => a -> a -> Bool
== SPClauseType
SPDNF Bool -> Bool -> Bool
&& SPSymbol
n SPSymbol -> SPSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== SPSymbol
SPAnd ->
      do [SPLiteral]
ls <- (SPTerm -> m SPLiteral) -> [SPTerm] -> m [SPLiteral]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SPTerm -> m SPLiteral
forall (m :: * -> *). MonadFail m => SPTerm -> m SPLiteral
toLiteral [SPTerm]
ts
         NSPClauseBody -> m NSPClauseBody
forall (m :: * -> *) a. Monad m => a -> m a
return (NSPClauseBody -> m NSPClauseBody)
-> NSPClauseBody -> m NSPClauseBody
forall a b. (a -> b) -> a -> b
$ SPClauseType -> [SPLiteral] -> NSPClauseBody
NSPClauseBody SPClauseType
b [SPLiteral]
ls
    _ -> [Char] -> m NSPClauseBody
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> m NSPClauseBody) -> [Char] -> m NSPClauseBody
forall a b. (a -> b) -> a -> b
$ "expected " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SPClauseType -> [Char]
forall a. Show a => a -> [Char]
show SPClauseType
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "-application"