{- |
Module      :  ./SoftFOL/ParseTPTP.hs
Description :  A parser for the TPTP Input Syntax
Copyright   :  (c) C.Maeder, DFKI Lab Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

A parser for the TPTP Input Syntax v3.4.0.1 taken from
<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
-}

module SoftFOL.ParseTPTP
  ( tptp
  , singleQuoted
  , form
  , genList
  , genTerm
  , GenTerm (..)
  , GenData (..)
  , AWord (..)
  , prTPTPs
  , tptpModel
  , ppGenTerm
 ) where

import Text.ParserCombinators.Parsec
import SoftFOL.Sign
import SoftFOL.PrintTPTP

import qualified Common.Doc as Doc
import Common.Id
import Common.Lexer (getPos)
import Common.Parsec

import Control.Monad
import Data.Char (ord, toLower, isAlphaNum)
import Data.Maybe

showRole :: Role -> String
showRole :: Role -> String
showRole = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> (Role -> String) -> Role -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Role -> String
forall a. Show a => a -> String
show

allRoles :: [Role]
allRoles :: [Role]
allRoles =
  [ Role
Axiom
  , Role
Hypothesis
  , Role
Definition
  , Role
Assumption
  , Role
Lemma
  , Role
Theorem
  , Role
Conjecture
  , Role
Negated_conjecture
  , Role
Plain
  , Role
Fi_domain
  , Role
Fi_functors
  , Role
Fi_predicates
  , Role
Type
  , Role
Unknown ]

tptp :: Parser [TPTP]
tptp :: Parser [TPTP]
tptp = Parser ()
skip Parser () -> Parser [TPTP] -> Parser [TPTP]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity TPTP -> Parser [TPTP]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String () Identity TPTP
headerLine ParsecT String () Identity TPTP
-> ParsecT String () Identity TPTP
-> ParsecT String () Identity TPTP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity TPTP
include ParsecT String () Identity TPTP
-> ParsecT String () Identity TPTP
-> ParsecT String () Identity TPTP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity TPTP
formAnno
   ParsecT String () Identity TPTP
-> ParsecT String () Identity TPTP
-> ParsecT String () Identity TPTP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
newline ParsecT String () Identity Char -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skip Parser ()
-> ParsecT String () Identity TPTP
-> ParsecT String () Identity TPTP
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TPTP -> ParsecT String () Identity TPTP
forall (m :: * -> *) a. Monad m => a -> m a
return TPTP
EmptyLine)) Parser [TPTP] -> Parser () -> Parser [TPTP]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof

blank :: Parser p -> Parser ()
blank :: Parser p -> Parser ()
blank = (Parser p -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 Parser ()
whiteSpace)

szsOutput :: Parser ()
szsOutput :: Parser ()
szsOutput = Parser String -> Parser ()
forall p. Parser p -> Parser ()
blank (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "SZS") Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser ()
forall p. Parser p -> Parser ()
blank (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "output")

iproverSzsEnd :: Parser ()
iproverSzsEnd :: Parser ()
iproverSzsEnd = Parser () -> Parser ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '%' ParsecT String () Identity Char -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser () -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany Parser ()
whiteSpace Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
szsOutput

otherCommentLine :: Parser ()
otherCommentLine :: Parser ()
otherCommentLine = (Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead Parser ()
iproverSzsEnd Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity Char -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '%'))
  Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget Parser String
commentLine

skipAllButEnd :: Parser ()
skipAllButEnd :: Parser ()
skipAllButEnd = 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 ()
whiteSpace Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ()
commentBlock Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ()
otherCommentLine
  Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity Char -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
newline

tptpModel :: Parser [(String, SPTerm)]
tptpModel :: Parser [(String, SPTerm)]
tptpModel = do
  String
_ <- ParsecT String () Identity Char -> Parser () -> Parser String
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 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar
    (Parser () -> Parser ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Parser ()
szsOutput Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser ()
forall p. Parser p -> Parser ()
blank (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "start"))
     Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser () -> Parser ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Parser String -> Parser ()
forall p. Parser p -> Parser ()
blank (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "START OF MODEL"))
  String
_ <- ParsecT String () Identity Char
-> ParsecT String () Identity Char -> Parser String
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 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
newline
  Parser ()
skipAllButEnd
  [TPTP]
ts <- ParsecT String () Identity TPTP -> Parser [TPTP]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT String () Identity TPTP
formAnno ParsecT String () Identity TPTP
-> Parser () -> ParsecT String () Identity TPTP
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
skipAllButEnd)
  (Parser ()
szsOutput Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser ()
forall p. Parser p -> Parser ()
blank (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "end"))
    Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "END OF MODEL")
  [(String, SPTerm)] -> Parser [(String, SPTerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, SPTerm)] -> Parser [(String, SPTerm)])
-> [(String, SPTerm)] -> Parser [(String, SPTerm)]
forall a b. (a -> b) -> a -> b
$ (TPTP -> [(String, SPTerm)] -> [(String, SPTerm)])
-> [(String, SPTerm)] -> [TPTP] -> [(String, SPTerm)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ t :: TPTP
t l :: [(String, SPTerm)]
l -> case TPTP
t of
    FormAnno _ (Name n :: String
n) _ e :: SPTerm
e _ -> (String
n, SPTerm
e) (String, SPTerm) -> [(String, SPTerm)] -> [(String, SPTerm)]
forall a. a -> [a] -> [a]
: [(String, SPTerm)]
l
    _ -> [(String, SPTerm)]
l) [] [TPTP]
ts

printable :: Char -> Bool
printable :: Char -> Bool
printable c :: Char
c = let i :: Int
i = Char -> Int
ord Char
c in Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 32 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 126

commentLine :: Parser String
commentLine :: Parser String
commentLine = (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '%' ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '#') ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity Char
-> ParsecT String () Identity Char -> Parser String
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 ((Char -> Bool) -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy Char -> Bool
printable) ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
newline

headerLine :: Parser TPTP
headerLine :: ParsecT String () Identity TPTP
headerLine = (String -> TPTP)
-> Parser String -> ParsecT String () Identity TPTP
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> TPTP
CommentLine (Parser String -> ParsecT String () Identity TPTP)
-> Parser String -> ParsecT String () Identity TPTP
forall a b. (a -> b) -> a -> b
$ Parser String
commentLine Parser String -> Parser () -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
skip

commentBlock :: Parser ()
commentBlock :: Parser ()
commentBlock = Parser String -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> String -> Parser String
forall st. String -> String -> CharParser st String
plainBlock "/*" "*/"

whiteSpace :: Parser ()
whiteSpace :: Parser ()
whiteSpace = ParsecT String () Identity Char -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (ParsecT String () Identity Char -> Parser ())
-> ParsecT String () Identity Char -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "\r\t\v\f "

skip :: Parser ()
skip :: Parser ()
skip = 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 ()
whiteSpace Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ()
commentBlock

skipAll :: Parser ()
skipAll :: Parser ()
skipAll = 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 ()
whiteSpace Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ()
commentBlock Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget Parser String
commentLine
  Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity Char -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
newline

lexeme :: Parser a -> Parser a
lexeme :: Parser a -> Parser a
lexeme = (Parser a -> Parser () -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
skipAll)

key :: Parser a -> Parser ()
key :: Parser a -> Parser ()
key = (Parser a -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipAll)

keyChar :: Char -> Parser ()
keyChar :: Char -> Parser ()
keyChar = ParsecT String () Identity Char -> Parser ()
forall p. Parser p -> Parser ()
key (ParsecT String () Identity Char -> Parser ())
-> (Char -> ParsecT String () Identity Char) -> Char -> Parser ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char

comma :: Parser ()
comma :: Parser ()
comma = Char -> Parser ()
keyChar ','

oParen :: Parser ()
oParen :: Parser ()
oParen = Char -> Parser ()
keyChar '('

cDotParen :: Parser ()
cDotParen :: Parser ()
cDotParen = String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string ")." Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skip Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Parser () -> Parser ()
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option () (ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
newline ParsecT String () Identity Char -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skip)

include :: Parser TPTP
include :: ParsecT String () Identity TPTP
include = do
  Parser String -> Parser ()
forall p. Parser p -> Parser ()
key (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall st. String -> CharParser st String
tryString "include"
  Parser ()
oParen
  String
a <- Parser String
atomicWord
  [Name]
m <- GenParser Char () [Name] -> GenParser Char () [Name]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (GenParser Char () [Name] -> GenParser Char () [Name])
-> GenParser Char () [Name] -> GenParser Char () [Name]
forall a b. (a -> b) -> a -> b
$ do
    Parser ()
comma
    ParsecT String () Identity Name
-> Parser () -> GenParser Char () [Name]
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 ParsecT String () Identity Name
aname Parser ()
comma
  Parser ()
cDotParen
  TPTP -> ParsecT String () Identity TPTP
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP -> ParsecT String () Identity TPTP)
-> TPTP -> ParsecT String () Identity TPTP
forall a b. (a -> b) -> a -> b
$ FileName -> [Name] -> TPTP
Include (String -> FileName
FileName String
a) [Name]
m

-- | does not allow leading zeros
natural :: Parser String
natural :: Parser String
natural = String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "0" Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity Char -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit

aname :: Parser Name
aname :: ParsecT String () Identity Name
aname = (String -> Name)
-> Parser String -> ParsecT String () Identity Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Name
Name (Parser String
atomicWord Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme Parser String
natural)

atomicWord :: Parser String
atomicWord :: Parser String
atomicWord = Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ Parser String
lowerWord Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
singleQuoted

isUAlphaNum :: Char -> Bool
isUAlphaNum :: Char -> Bool
isUAlphaNum c :: Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "_$"

luWord :: Parser Char -> Parser String
luWord :: ParsecT String () Identity Char -> Parser String
luWord p :: ParsecT String () Identity Char
p = do
  Char
c <- ParsecT String () Identity Char
p
  String
r <- ParsecT String () Identity Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String () Identity Char -> Parser String)
-> ParsecT String () Identity Char -> Parser String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy Char -> Bool
isUAlphaNum
  String -> Parser String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Parser String) -> String -> Parser String
forall a b. (a -> b) -> a -> b
$ Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
r

lowerWord :: Parser String
lowerWord :: Parser String
lowerWord = ParsecT String () Identity Char -> Parser String
luWord ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
lower

upperWord :: Parser String
upperWord :: Parser String
upperWord = ParsecT String () Identity Char -> Parser String
luWord ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
upper

singleQuoted :: Parser String
singleQuoted :: Parser String
singleQuoted =
  let quote :: Char
quote = '\'' in ([String] -> String)
-> ParsecT String () Identity [String] -> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (ParsecT String () Identity [String] -> Parser String)
-> ParsecT String () Identity [String] -> Parser String
forall a b. (a -> b) -> a -> b
$
  Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
quote
  ParsecT String () Identity Char
-> ParsecT String () Identity [String]
-> ParsecT String () Identity [String]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> ParsecT String () Identity [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (String -> Parser String
forall st. String -> CharParser st String
tryString "\\'" Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single
       ((Char -> Bool) -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy ((Char -> Bool) -> ParsecT String () Identity Char)
-> (Char -> Bool) -> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ \ c :: Char
c -> Char -> Bool
printable Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
quote))
  ParsecT String () Identity [String]
-> ParsecT String () Identity Char
-> ParsecT String () Identity [String]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
quote

formKind :: Parser FormKind
formKind :: Parser FormKind
formKind = [Parser FormKind] -> Parser FormKind
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([Parser FormKind] -> Parser FormKind)
-> [Parser FormKind] -> Parser FormKind
forall a b. (a -> b) -> a -> b
$ (FormKind -> Parser FormKind) -> [FormKind] -> [Parser FormKind]
forall a b. (a -> b) -> [a] -> [b]
map (\ k :: FormKind
k -> Parser String -> Parser ()
forall p. Parser p -> Parser ()
key (String -> Parser String
forall st. String -> CharParser st String
tryString (String -> Parser String) -> String -> Parser String
forall a b. (a -> b) -> a -> b
$ FormKind -> String
forall a. Show a => a -> String
show FormKind
k) Parser () -> Parser FormKind -> Parser FormKind
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FormKind -> Parser FormKind
forall (m :: * -> *) a. Monad m => a -> m a
return FormKind
k)
    [FormKind
FofKind, FormKind
CnfKind, FormKind
FotKind]

role :: Parser Role
role :: Parser Role
role = [Parser Role] -> Parser Role
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([Parser Role] -> Parser Role) -> [Parser Role] -> Parser Role
forall a b. (a -> b) -> a -> b
$ (Role -> Parser Role) -> [Role] -> [Parser Role]
forall a b. (a -> b) -> [a] -> [b]
map (\ r :: Role
r -> Parser String -> Parser ()
forall p. Parser p -> Parser ()
key (String -> Parser String
forall st. String -> CharParser st String
tryString (String -> Parser String) -> String -> Parser String
forall a b. (a -> b) -> a -> b
$ Role -> String
showRole Role
r)
                     Parser () -> Parser Role -> Parser Role
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Role -> Parser Role
forall (m :: * -> *) a. Monad m => a -> m a
return Role
r) [Role]
allRoles

formAnno :: Parser TPTP
formAnno :: ParsecT String () Identity TPTP
formAnno = do
  FormKind
k <- Parser FormKind
formKind
  Parser ()
oParen
  Name
n <- ParsecT String () Identity Name
aname
  Parser ()
comma
  Role
r <- Parser Role
role
  Parser ()
comma
  SPTerm
f <- Parser SPTerm
form
  Maybe Annos
m <- ParsecT String () Identity Annos
-> ParsecT String () Identity (Maybe Annos)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String () Identity Annos
 -> ParsecT String () Identity (Maybe Annos))
-> ParsecT String () Identity Annos
-> ParsecT String () Identity (Maybe Annos)
forall a b. (a -> b) -> a -> b
$ do
    Parser ()
comma
    Source
gt <- (GenTerm -> Source)
-> ParsecT String () Identity GenTerm
-> ParsecT String () Identity Source
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GenTerm -> Source
Source ParsecT String () Identity GenTerm
genTerm
    Maybe Info
i <- ParsecT String () Identity Info
-> ParsecT String () Identity (Maybe Info)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String () Identity Info
 -> ParsecT String () Identity (Maybe Info))
-> ParsecT String () Identity Info
-> ParsecT String () Identity (Maybe Info)
forall a b. (a -> b) -> a -> b
$ do
      Parser ()
comma
      ([GenTerm] -> Info)
-> ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [GenTerm] -> Info
Info ParsecT String () Identity [GenTerm]
genList
    Annos -> ParsecT String () Identity Annos
forall (m :: * -> *) a. Monad m => a -> m a
return (Annos -> ParsecT String () Identity Annos)
-> Annos -> ParsecT String () Identity Annos
forall a b. (a -> b) -> a -> b
$ Source -> Maybe Info -> Annos
Annos Source
gt Maybe Info
i
  Parser ()
cDotParen
  TPTP -> ParsecT String () Identity TPTP
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP -> ParsecT String () Identity TPTP)
-> TPTP -> ParsecT String () Identity TPTP
forall a b. (a -> b) -> a -> b
$ FormKind -> Name -> Role -> SPTerm -> Maybe Annos -> TPTP
FormAnno FormKind
k Name
n Role
r SPTerm
f Maybe Annos
m

colon :: Parser ()
colon :: Parser ()
colon = Char -> Parser ()
keyChar ':'

genTerm :: Parser GenTerm
genTerm :: ParsecT String () Identity GenTerm
genTerm = ([GenTerm] -> GenTerm)
-> ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity GenTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [GenTerm] -> GenTerm
GenTermList ParsecT String () Identity [GenTerm]
genList ParsecT String () Identity GenTerm
-> ParsecT String () Identity GenTerm
-> ParsecT String () Identity GenTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
  GenData
gd <- Parser GenData
genData
  Maybe GenTerm
m <- ParsecT String () Identity GenTerm
-> ParsecT String () Identity (Maybe GenTerm)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String () Identity GenTerm
 -> ParsecT String () Identity (Maybe GenTerm))
-> ParsecT String () Identity GenTerm
-> ParsecT String () Identity (Maybe GenTerm)
forall a b. (a -> b) -> a -> b
$ do
    Char -> Parser ()
keyChar ':'
    ParsecT String () Identity GenTerm
genTerm
  GenTerm -> ParsecT String () Identity GenTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (GenTerm -> ParsecT String () Identity GenTerm)
-> GenTerm -> ParsecT String () Identity GenTerm
forall a b. (a -> b) -> a -> b
$ GenData -> Maybe GenTerm -> GenTerm
GenTerm GenData
gd Maybe GenTerm
m

genData :: Parser GenData
genData :: Parser GenData
genData = Parser GenData
formData Parser GenData -> Parser GenData -> Parser GenData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser GenData
otherData Parser GenData -> Parser GenData -> Parser GenData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
  AWord
a <- (String -> AWord)
-> Parser String -> ParsecT String () Identity AWord
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> AWord
AWord Parser String
atomicWord
  [GenTerm]
l <- ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity [GenTerm]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (ParsecT String () Identity [GenTerm]
 -> ParsecT String () Identity [GenTerm])
-> ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity [GenTerm]
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity [GenTerm]
forall a. Parser a -> Parser a
parens (ParsecT String () Identity [GenTerm]
 -> ParsecT String () Identity [GenTerm])
-> ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity [GenTerm]
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity GenTerm
-> Parser () -> ParsecT String () Identity [GenTerm]
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 ParsecT String () Identity GenTerm
genTerm Parser ()
comma
  GenData -> Parser GenData
forall (m :: * -> *) a. Monad m => a -> m a
return (GenData -> Parser GenData) -> GenData -> Parser GenData
forall a b. (a -> b) -> a -> b
$ AWord -> [GenTerm] -> GenData
GenData AWord
a [GenTerm]
l

otherData :: Parser GenData
otherData :: Parser GenData
otherData = (String -> GenData) -> Parser String -> Parser GenData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> GenData
OtherGenData (Parser String -> Parser GenData)
-> Parser String -> Parser GenData
forall a b. (a -> b) -> a -> b
$ (Parser String
upperWord Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
real Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
distinct) Parser String -> Parser () -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
skipAll

distinct :: Parser String
distinct :: Parser String
distinct =
  let dquot :: Char
dquot = '"' in
  Parser String -> ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m a -> m [a]
enclosedBy (ParsecT String () Identity [String] -> Parser String
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (ParsecT String () Identity [String] -> Parser String)
-> ParsecT String () Identity [String] -> Parser String
forall a b. (a -> b) -> a -> b
$ Parser String -> ParsecT String () Identity [String]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser String -> ParsecT String () Identity [String])
-> Parser String -> ParsecT String () Identity [String]
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall st. String -> CharParser st String
tryString "\\\"" Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single ((Char -> Bool) -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
dquot)))
  (ParsecT String () Identity Char -> Parser String)
-> ParsecT String () Identity Char -> Parser String
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
dquot

decimal :: Parser String
decimal :: Parser String
decimal = Parser String -> Parser String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single (ParsecT String () Identity Char -> Parser String)
-> ParsecT String () Identity Char -> Parser String
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "-+") Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> Parser String
natural

real :: Parser String
real :: Parser String
real = do
  String
d <- Parser String
decimal
  String
f <- Parser String -> Parser String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.' ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> ParsecT String () Identity Char -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
  String
e <- Parser String -> Parser String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "eE" ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> Parser String
decimal
  String -> Parser String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Parser String) -> String -> Parser String
forall a b. (a -> b) -> a -> b
$ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e

formData :: Parser GenData
formData :: Parser GenData
formData =
  (FormData -> GenData)
-> ParsecT String () Identity FormData -> Parser GenData
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FormData -> GenData
GenFormData (ParsecT String () Identity FormData -> Parser GenData)
-> ParsecT String () Identity FormData -> Parser GenData
forall a b. (a -> b) -> a -> b
$ (FormKind -> SPTerm -> FormData)
-> Parser FormKind
-> Parser SPTerm
-> ParsecT String () Identity FormData
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 FormKind -> SPTerm -> FormData
FormData (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '$' ParsecT String () Identity Char
-> Parser FormKind -> Parser FormKind
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser FormKind
formKind) (Parser SPTerm -> ParsecT String () Identity FormData)
-> Parser SPTerm -> ParsecT String () Identity FormData
forall a b. (a -> b) -> a -> b
$ Parser SPTerm -> Parser SPTerm
forall a. Parser a -> Parser a
parens Parser SPTerm
form

orOp :: Parser ()
orOp :: Parser ()
orOp = Char -> Parser ()
keyChar '|'

andOp :: Parser ()
andOp :: Parser ()
andOp = Char -> Parser ()
keyChar '&'

pToken :: Parser String -> Parser Token
pToken :: Parser String -> Parser Token
pToken = (Pos -> String -> Token)
-> ParsecT String () Identity Pos -> Parser String -> Parser Token
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\ p :: Pos
p s :: String
s -> String -> Range -> Token
Token String
s ([Pos] -> Range
Range [Pos
p])) ParsecT String () Identity Pos
forall tok st. GenParser tok st Pos
getPos (Parser String -> Parser Token)
-> (Parser String -> Parser String)
-> Parser String
-> Parser Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Parser String -> Parser () -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
skipAll)

form :: Parser SPTerm
form :: Parser SPTerm
form = do
  SPTerm
u <- Parser SPTerm
unitary
  do Parser ()
orOp
     [SPTerm]
us <- Parser SPTerm -> Parser () -> ParsecT String () Identity [SPTerm]
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 SPTerm
unitary Parser ()
orOp
     SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> Parser SPTerm) -> SPTerm -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPOr ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPTerm
u SPTerm -> [SPTerm] -> [SPTerm]
forall a. a -> [a] -> [a]
: [SPTerm]
us
    Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Parser ()
andOp
      [SPTerm]
us <- Parser SPTerm -> Parser () -> ParsecT String () Identity [SPTerm]
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 SPTerm
unitary Parser ()
andOp
      SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> Parser SPTerm) -> SPTerm -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPAnd ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPTerm
u SPTerm -> [SPTerm] -> [SPTerm]
forall a. a -> [a] -> [a]
: [SPTerm]
us
    Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Token
o <- [Parser Token] -> Parser Token
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([Parser Token] -> Parser Token) -> [Parser Token] -> Parser Token
forall a b. (a -> b) -> a -> b
$ (String -> Parser Token) -> [String] -> [Parser Token]
forall a b. (a -> b) -> [a] -> [b]
map (Parser String -> Parser Token
pToken (Parser String -> Parser Token)
-> (String -> Parser String) -> String -> Parser Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Parser String
forall st. String -> CharParser st String
tryString)
           ["<=>", "=>", "<=", "<~>", "~|", "~&"]
      SPTerm
u2 <- Parser SPTerm
unitary
      let s :: String
s = Token -> String
tokStr Token
o
          a :: [SPTerm]
a = [SPTerm
u, SPTerm
u2]
      SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> Parser SPTerm) -> SPTerm -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ case String -> [(String, SPSymbol)] -> Maybe SPSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s ([(String, SPSymbol)] -> Maybe SPSymbol)
-> [(String, SPSymbol)] -> Maybe SPSymbol
forall a b. (a -> b) -> a -> b
$ [String] -> [SPSymbol] -> [(String, SPSymbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ["<=>", "=>", "<="]
         [SPSymbol
SPEquiv, SPSymbol
SPImplies, SPSymbol
SPImplied] of
           Just ks :: SPSymbol
ks -> SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
ks [SPTerm]
a
           Nothing -> case String -> [(String, SPSymbol)] -> Maybe SPSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s ([(String, SPSymbol)] -> Maybe SPSymbol)
-> [(String, SPSymbol)] -> Maybe SPSymbol
forall a b. (a -> b) -> a -> b
$ [String] -> [SPSymbol] -> [(String, SPSymbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ["<~>", "~|", "~&"]
             [SPSymbol
SPEquiv, SPSymbol
SPOr, SPSymbol
SPAnd] of
               Just ks :: SPSymbol
ks -> SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPNot [SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
ks [SPTerm]
a]
               Nothing -> SPSymbol -> [SPTerm] -> SPTerm
compTerm (Token -> SPSymbol
SPCustomSymbol Token
o) [SPTerm]
a
    Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return SPTerm
u

unitary :: Parser SPTerm
unitary :: Parser SPTerm
unitary = Parser SPTerm -> Parser SPTerm
forall a. Parser a -> Parser a
parens Parser SPTerm
form Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser SPTerm
quantForm Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser SPTerm
unaryForm Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser SPTerm
atomicForm

quantForm :: Parser SPTerm
quantForm :: Parser SPTerm
quantForm = do
  SPQuantSym
q <- Parser SPQuantSym -> Parser SPQuantSym
forall a. Parser a -> Parser a
lexeme (Parser SPQuantSym -> Parser SPQuantSym)
-> Parser SPQuantSym -> Parser SPQuantSym
forall a b. (a -> b) -> a -> b
$ (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '!' ParsecT String () Identity Char
-> Parser SPQuantSym -> Parser SPQuantSym
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SPQuantSym -> Parser SPQuantSym
forall (m :: * -> *) a. Monad m => a -> m a
return SPQuantSym
SPForall)
            Parser SPQuantSym -> Parser SPQuantSym -> Parser SPQuantSym
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '?' ParsecT String () Identity Char
-> Parser SPQuantSym -> Parser SPQuantSym
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SPQuantSym -> Parser SPQuantSym
forall (m :: * -> *) a. Monad m => a -> m a
return SPQuantSym
SPExists)
  [SPTerm]
vs <- ParsecT String () Identity [SPTerm]
-> ParsecT String () Identity [SPTerm]
forall a. Parser a -> Parser a
brackets (ParsecT String () Identity [SPTerm]
 -> ParsecT String () Identity [SPTerm])
-> ParsecT String () Identity [SPTerm]
-> ParsecT String () Identity [SPTerm]
forall a b. (a -> b) -> a -> b
$ Parser SPTerm -> Parser () -> ParsecT String () Identity [SPTerm]
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 SPTerm
variable Parser ()
comma
  Parser ()
colon
  SPTerm
u <- Parser SPTerm
unitary
  SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return SPQuantTerm :: SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm
    { quantSym :: SPQuantSym
quantSym = SPQuantSym
q
    , variableList :: [SPTerm]
variableList = [SPTerm]
vs
    , qFormula :: SPTerm
qFormula = SPTerm
u }

unaryForm :: Parser SPTerm
unaryForm :: Parser SPTerm
unaryForm = do
  Char -> Parser ()
keyChar '~'
  SPTerm
u <- Parser SPTerm
unitary
  SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> Parser SPTerm) -> SPTerm -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPNot [SPTerm
u]

atomicForm :: Parser SPTerm
atomicForm :: Parser SPTerm
atomicForm = do
  SPTerm
t <- Parser SPTerm
term
  do ParsecT String () Identity Char -> Parser ()
forall p. Parser p -> Parser ()
key (ParsecT String () Identity Char -> Parser ())
-> ParsecT String () Identity Char -> Parser ()
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity Char -> ParsecT String () Identity Char
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String () Identity Char
 -> ParsecT String () Identity Char)
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '=' ParsecT String () Identity Char
-> Parser () -> ParsecT String () Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String () Identity Char -> Parser ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '>' )
     SPTerm
t2 <- Parser SPTerm
term
     SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> Parser SPTerm) -> SPTerm -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ SPTerm -> SPTerm -> SPTerm
mkEq SPTerm
t SPTerm
t2
    Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Parser String -> Parser ()
forall p. Parser p -> Parser ()
key (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall st. String -> CharParser st String
tryString "!="
      SPTerm
t2 <- Parser SPTerm
term
      SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> Parser SPTerm) -> SPTerm -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPNot [SPTerm -> SPTerm -> SPTerm
mkEq SPTerm
t SPTerm
t2]
    Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return SPTerm
t

variable :: Parser SPTerm
variable :: Parser SPTerm
variable = (Token -> SPTerm) -> Parser Token -> Parser SPTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> (Token -> SPSymbol) -> Token -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> SPSymbol
SPCustomSymbol) (Parser Token -> Parser SPTerm) -> Parser Token -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser Token
pToken Parser String
upperWord

definedAtom :: Parser SPTerm
definedAtom :: Parser SPTerm
definedAtom = (Token -> SPTerm) -> Parser Token -> Parser SPTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> (Token -> SPSymbol) -> Token -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> SPSymbol
SPCustomSymbol) (Parser Token -> Parser SPTerm) -> Parser Token -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser Token
pToken (Parser String -> Parser Token) -> Parser String -> Parser Token
forall a b. (a -> b) -> a -> b
$ Parser String
real Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
distinct

functor :: Parser SPSymbol
functor :: Parser SPSymbol
functor = (Token -> SPSymbol) -> Parser Token -> Parser SPSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ t :: Token
t -> SPSymbol -> Maybe SPSymbol -> SPSymbol
forall a. a -> Maybe a -> a
fromMaybe (Token -> SPSymbol
SPCustomSymbol Token
t)
    (Maybe SPSymbol -> SPSymbol) -> Maybe SPSymbol -> SPSymbol
forall a b. (a -> b) -> a -> b
$ String -> [(String, SPSymbol)] -> Maybe SPSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Token -> String
tokStr Token
t)
    ([(String, SPSymbol)] -> Maybe SPSymbol)
-> [(String, SPSymbol)] -> Maybe SPSymbol
forall a b. (a -> b) -> a -> b
$ [String] -> [SPSymbol] -> [(String, SPSymbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ["$true", "$false", "$equal"] [SPSymbol
SPTrue, SPSymbol
SPFalse, SPSymbol
SPEqual])
  (Parser Token -> Parser SPSymbol)
-> Parser Token -> Parser SPSymbol
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser Token
pToken
  (Parser String -> Parser Token) -> Parser String -> Parser Token
forall a b. (a -> b) -> a -> b
$ Parser String
lowerWord Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
singleQuoted Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
dollarWord

-- system and defined words
dollarWord :: Parser String
dollarWord :: Parser String
dollarWord = do
  String
d <- String -> Parser String
forall st. String -> CharParser st String
tryString "$$" Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "$"
  String
w <- Parser String
lowerWord
  String -> Parser String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Parser String) -> String -> Parser String
forall a b. (a -> b) -> a -> b
$ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w

-- mixed plain, defined and system terms
term :: Parser SPTerm
term :: Parser SPTerm
term = Parser SPTerm
variable Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser SPTerm
definedAtom Parser SPTerm -> Parser SPTerm -> Parser SPTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
  SPSymbol
f <- Parser SPSymbol
functor
  [SPTerm]
as <- ParsecT String () Identity [SPTerm]
-> ParsecT String () Identity [SPTerm]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (ParsecT String () Identity [SPTerm]
 -> ParsecT String () Identity [SPTerm])
-> ParsecT String () Identity [SPTerm]
-> ParsecT String () Identity [SPTerm]
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity [SPTerm]
-> ParsecT String () Identity [SPTerm]
forall a. Parser a -> Parser a
parens (ParsecT String () Identity [SPTerm]
 -> ParsecT String () Identity [SPTerm])
-> ParsecT String () Identity [SPTerm]
-> ParsecT String () Identity [SPTerm]
forall a b. (a -> b) -> a -> b
$ Parser SPTerm -> Parser () -> ParsecT String () Identity [SPTerm]
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 SPTerm
term Parser ()
comma
  SPTerm -> Parser SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SPTerm -> Parser SPTerm) -> SPTerm -> Parser SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
f [SPTerm]
as

brackets :: Parser a -> Parser a
brackets :: Parser a -> Parser a
brackets p :: Parser a
p = do
  Char -> Parser ()
keyChar '['
  a
a <- Parser a
p
  Char -> Parser ()
keyChar ']'
  a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

parens :: Parser a -> Parser a
parens :: Parser a -> Parser a
parens p :: Parser a
p = do
  Parser ()
oParen
  a
a <- Parser a
p
  Char -> Parser ()
keyChar ')'
  a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

genList :: Parser [GenTerm]
genList :: ParsecT String () Identity [GenTerm]
genList = ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity [GenTerm]
forall a. Parser a -> Parser a
brackets (ParsecT String () Identity [GenTerm]
 -> ParsecT String () Identity [GenTerm])
-> ParsecT String () Identity [GenTerm]
-> ParsecT String () Identity [GenTerm]
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity GenTerm
-> Parser () -> ParsecT String () Identity [GenTerm]
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 ParsecT String () Identity GenTerm
genTerm Parser ()
comma

prTPTPs :: [TPTP] -> Doc.Doc
prTPTPs :: [TPTP] -> Doc
prTPTPs = [Doc] -> Doc
Doc.vcat ([Doc] -> Doc) -> ([TPTP] -> [Doc]) -> [TPTP] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TPTP -> Doc) -> [TPTP] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TPTP -> Doc
prTPTP

prTPTP :: TPTP -> Doc.Doc
prTPTP :: TPTP -> Doc
prTPTP p :: TPTP
p = case TPTP
p of
  FormAnno k :: FormKind
k (Name n :: String
n) r :: Role
r t :: SPTerm
t m :: Maybe Annos
m ->
      String -> Doc
Doc.text (FormKind -> String
forall a. Show a => a -> String
show FormKind
k)
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
Doc.parens
      ([Doc] -> Doc
Doc.sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
       [ String -> Doc
Doc.text String
n
       , String -> Doc
Doc.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Role -> String
showRole Role
r
       , SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPTerm
t]
       [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc] -> (Annos -> [Doc]) -> Maybe Annos -> [Doc]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Annos -> [Doc]
ppAnnos Maybe Annos
m)
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
Doc.dot
  Include (FileName f :: String
f) ns :: [Name]
ns ->
      String -> Doc
Doc.text "include"
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
Doc.parens
      ([Doc] -> Doc
Doc.sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
       String -> Doc
ppName String
f Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: if [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
ns then [] else
          [Doc -> Doc
Doc.brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
Doc.sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
ppAName [Name]
ns])
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
Doc.dot
  CommentLine l :: String
l -> String -> Doc
Doc.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ '%' Char -> String -> String
forall a. a -> [a] -> [a]
: String
l
  EmptyLine -> String -> Doc
Doc.text ""

ppName :: String -> Doc.Doc
ppName :: String -> Doc
ppName s :: String
s = (if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isUAlphaNum String
s then Doc -> Doc
forall a. a -> a
id else Doc -> Doc
Doc.quotes) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
Doc.text String
s

ppAName :: Name -> Doc.Doc
ppAName :: Name -> Doc
ppAName (Name n :: String
n) = String -> Doc
ppName String
n

ppAnnos :: Annos -> [Doc.Doc]
ppAnnos :: Annos -> [Doc]
ppAnnos (Annos (Source gt :: GenTerm
gt) m :: Maybe Info
m) = GenTerm -> Doc
ppGenTerm GenTerm
gt Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc] -> (Info -> [Doc]) -> Maybe Info -> [Doc]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Info -> [Doc]
ppInfo Maybe Info
m

ppInfo :: Info -> [Doc.Doc]
ppInfo :: Info -> [Doc]
ppInfo (Info l :: [GenTerm]
l) = [[GenTerm] -> Doc
ppGenList [GenTerm]
l]

ppList :: [GenTerm] -> Doc.Doc
ppList :: [GenTerm] -> Doc
ppList = [Doc] -> Doc
Doc.sepByCommas ([Doc] -> Doc) -> ([GenTerm] -> [Doc]) -> [GenTerm] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenTerm -> Doc) -> [GenTerm] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map GenTerm -> Doc
ppGenTerm

ppGenList :: [GenTerm] -> Doc.Doc
ppGenList :: [GenTerm] -> Doc
ppGenList = Doc -> Doc
Doc.brackets (Doc -> Doc) -> ([GenTerm] -> Doc) -> [GenTerm] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenTerm] -> Doc
ppList

ppGenTerm :: GenTerm -> Doc.Doc
ppGenTerm :: GenTerm -> Doc
ppGenTerm gt :: GenTerm
gt = case GenTerm
gt of
  GenTerm gd :: GenData
gd m :: Maybe GenTerm
m -> let d :: Doc
d = GenData -> Doc
ppGenData GenData
gd in case Maybe GenTerm
m of
    Just t :: GenTerm
t -> [Doc] -> Doc
Doc.fsep [Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
Doc.colon, GenTerm -> Doc
ppGenTerm GenTerm
t]
    Nothing -> Doc
d
  GenTermList l :: [GenTerm]
l -> [GenTerm] -> Doc
ppGenList [GenTerm]
l

ppGenData :: GenData -> Doc.Doc
ppGenData :: GenData -> Doc
ppGenData gd :: GenData
gd = case GenData
gd of
  GenData (AWord aw :: String
aw) l :: [GenTerm]
l -> String -> Doc
ppName String
aw Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
    if [GenTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GenTerm]
l then Doc
Doc.empty else Doc -> Doc
Doc.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [GenTerm] -> Doc
ppList [GenTerm]
l
  OtherGenData s :: String
s -> String -> Doc
Doc.text String
s
  GenFormData (FormData k :: FormKind
k t :: SPTerm
t) ->
     String -> Doc
Doc.text ('$' Char -> String -> String
forall a. a -> [a] -> [a]
: FormKind -> String
forall a. Show a => a -> String
show FormKind
k)
     Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
Doc.parens (SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPTerm
t)