{- |
Module      :  ./THF/ParseTHF.hs
Description :  A Parser for the TPTP-THF Syntax
Copyright   :  (c) Jonathan von Schroeder, DFKI Bremen 2012
               (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  portable

A Parser for the TPTP-THF Input Syntax v5.4.0.0 taken from
<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html> and THF0
Syntax taken from <http://www.ags.uni-sb.de/~chris/papers/C25.pdf> P. 15-16

Note: The parser prefers a THF0 parse tree over a THF parse tree
Note: We pretend as if tuples were still part of the syntax
-}

module THF.ParseTHF (parseTHF) where

import THF.As

import Text.ParserCombinators.Parsec

import Common.Parsec
import Common.Id (Token (..))
import Common.Lexer (parseToken)
import qualified Control.Monad.Fail as Fail

import Data.Char
import Data.Maybe

{- -----------------------------------------------------------------------------
Parser for the THF  and THF0 Syntax
----------------------------------------------------------------------------- -}

{- THF & THF0:
<TPTP_input>       ::= <annotated_formula> | <include>
<thf_annotated>    ::= thf(<name>,<formula_role>,<thf_formula><annotations>).
Data Type: TPTP_THF -}
parseTHF :: CharParser st [TPTP_THF]
parseTHF :: CharParser st [TPTP_THF]
parseTHF = do
    Maybe TPTP_THF
h <- ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity (Maybe TPTP_THF)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
header
    [TPTP_THF]
thf <- ParsecT [Char] st Identity TPTP_THF -> CharParser st [TPTP_THF]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ((ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
systemComment ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
definedComment ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
comment ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                 ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
include ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
thfAnnotatedFormula) ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity TPTP_THF
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
skipSpaces)
    [TPTP_THF] -> CharParser st [TPTP_THF]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TPTP_THF] -> CharParser st [TPTP_THF])
-> [TPTP_THF] -> CharParser st [TPTP_THF]
forall a b. (a -> b) -> a -> b
$ if Maybe TPTP_THF -> Bool
forall a. Maybe a -> Bool
isJust Maybe TPTP_THF
h then Maybe TPTP_THF -> TPTP_THF
forall a. HasCallStack => Maybe a -> a
fromJust Maybe TPTP_THF
h TPTP_THF -> [TPTP_THF] -> [TPTP_THF]
forall a. a -> [a] -> [a]
: [TPTP_THF]
thf else [TPTP_THF]
thf


header :: CharParser st TPTP_THF
header :: CharParser st TPTP_THF
header = CharParser st TPTP_THF -> CharParser st TPTP_THF
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    Comment
s <- CharParser st Comment
forall st. CharParser st Comment
headerSE
    [Comment]
c <- CharParser st Comment
-> CharParser st Comment -> CharParser st [Comment]
forall st a.
CharParser st a -> CharParser st a -> CharParser st [a]
myManyTill (CharParser st Comment -> CharParser st Comment
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st Comment
forall st. CharParser st Comment
commentLine CharParser st Comment
-> ParsecT [Char] st Identity () -> CharParser st Comment
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
skipSpaces)) (CharParser st Comment -> CharParser st Comment
forall tok st a. GenParser tok st a -> GenParser tok st a
try CharParser st Comment
forall st. CharParser st Comment
headerSE)
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ [Comment] -> TPTP_THF
TPTP_Header (Comment
s Comment -> [Comment] -> [Comment]
forall a. a -> [a] -> [a]
: [Comment]
c))

headerSE :: CharParser st Comment
headerSE :: CharParser st Comment
headerSE = do
    GenParser Char st () -> GenParser Char st ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '%' ParsecT [Char] st Identity Char
-> GenParser Char st () -> GenParser Char st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity Char -> GenParser Char st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '$'))
    Token
c <- CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st Token)
-> CharParser st [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT [Char] st Identity Char -> CharParser st [Char])
-> ParsecT [Char] st Identity Char -> CharParser st [Char]
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '-' ParsecT [Char] st Identity Char
-> GenParser Char st () -> ParsecT [Char] st Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity Char -> GenParser Char st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy ParsecT [Char] st Identity Char
forall st. CharParser st Char
printableChar
    GenParser Char st ()
forall st. CharParser st ()
skipSpaces
    Comment -> CharParser st Comment
forall (m :: * -> *) a. Monad m => a -> m a
return (Comment -> CharParser st Comment)
-> Comment -> CharParser st Comment
forall a b. (a -> b) -> a -> b
$ Token -> Comment
Comment_Line Token
c

{- THF & THF0:
<comment>            ::- <comment_line>|<comment_block>
<comment_line>       ::- [%]<printable_char>*
<comment_block>      ::: [/][*]<not_star_slash>[*][*]*[/]
<not_star_slash>     ::: ([^*]*[*][*]*[^/*])*[^*]* -}
commentLine :: CharParser st Comment
commentLine :: CharParser st Comment
commentLine = do
    GenParser Char st () -> GenParser Char st ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '%' ParsecT [Char] st Identity Char
-> GenParser Char st () -> GenParser Char st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity Char -> GenParser Char st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '$'))
    Token
c <- CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st Token)
-> CharParser st [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity Char
forall st. CharParser st Char
printableChar
    Comment -> CharParser st Comment
forall (m :: * -> *) a. Monad m => a -> m a
return (Comment -> CharParser st Comment)
-> Comment -> CharParser st Comment
forall a b. (a -> b) -> a -> b
$ Token -> Comment
Comment_Line Token
c

comment_ :: String -> CharParser st Token
comment_ :: [Char] -> CharParser st Token
comment_ start :: [Char]
start = do
    GenParser Char st () -> GenParser Char st ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try ([Char] -> ParsecT [Char] st Identity [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string [Char]
start ParsecT [Char] st Identity [Char]
-> GenParser Char st () -> GenParser Char st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity Char -> GenParser Char st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '$'))
    Token
c <- ParsecT [Char] st Identity [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (ParsecT [Char] st Identity [Char] -> CharParser st Token)
-> ParsecT [Char] st Identity [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] st Identity Char
-> ParsecT [Char] st Identity [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ([Char] -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
noneOf "*/")
    ParsecT [Char] st Identity Char -> GenParser Char st ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '*')
    Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '/'
    Token -> CharParser st Token
forall (m :: * -> *) a. Monad m => a -> m a
return Token
c

comment :: CharParser st TPTP_THF
comment :: CharParser st TPTP_THF
comment = (Comment -> TPTP_THF)
-> ParsecT [Char] st Identity Comment -> CharParser st TPTP_THF
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Comment -> TPTP_THF
TPTP_Comment ParsecT [Char] st Identity Comment
forall st. CharParser st Comment
commentLine
  CharParser st TPTP_THF
-> CharParser st TPTP_THF -> CharParser st TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- [Char] -> CharParser st Token
forall st. [Char] -> CharParser st Token
comment_ "/*"
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ Comment -> TPTP_THF
TPTP_Comment (Token -> Comment
Comment_Block Token
c)

{- THF & THF0:
<defined_comment>    ::- <def_comment_line>|<def_comment_block>
<def_comment_line>   ::: [%]<dollar><printable_char>*
<def_comment_block>  ::: [/][*]<dollar><not_star_slash>[*][*]*[/]
Data Type: DefinedComment -}
definedComment :: CharParser st TPTP_THF
definedComment :: CharParser st TPTP_THF
definedComment = do
    GenParser Char st () -> GenParser Char st ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try ([Char] -> ParsecT [Char] st Identity [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string "%$" ParsecT [Char] st Identity [Char]
-> GenParser Char st () -> GenParser Char st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity Char -> GenParser Char st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '$'))
    Token
c <- ParsecT [Char] st Identity [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (ParsecT [Char] st Identity [Char] -> CharParser st Token)
-> ParsecT [Char] st Identity [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] st Identity Char
-> ParsecT [Char] st Identity [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity Char
forall st. CharParser st Char
printableChar
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ DefinedComment -> TPTP_THF
TPTP_Defined_Comment (Token -> DefinedComment
Defined_Comment_Line Token
c)
  CharParser st TPTP_THF
-> CharParser st TPTP_THF -> CharParser st TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- [Char] -> CharParser st Token
forall st. [Char] -> CharParser st Token
comment_ "/*$"
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ DefinedComment -> TPTP_THF
TPTP_Defined_Comment (Token -> DefinedComment
Defined_Comment_Block Token
c)

{- THF & THF0:
<system_comment>     ::- <sys_comment_line>|<sys_comment_block>
<sys_comment_line>   ::: [%]<dollar><dollar><printable_char>*
<sys_comment_block>  ::: [/][*]<dollar><dollar><not_star_slash>[*][*]*[/]
Data Type: SystemComment -}
systemComment :: CharParser st TPTP_THF
systemComment :: CharParser st TPTP_THF
systemComment = do
    [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "%$$"
    Token
c <- CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st Token)
-> CharParser st [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity Char
forall st. CharParser st Char
printableChar
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ SystemComment -> TPTP_THF
TPTP_System_Comment (Token -> SystemComment
System_Comment_Line Token
c)
  CharParser st TPTP_THF
-> CharParser st TPTP_THF -> CharParser st TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- [Char] -> CharParser st Token
forall st. [Char] -> CharParser st Token
comment_ "/*$$"
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ SystemComment -> TPTP_THF
TPTP_System_Comment (Token -> SystemComment
System_Comment_Block Token
c)

{- THF & THF0:
<include>            ::= include(<file_name><formula_selection>).
<formula_selection>  ::= ,[<name_list>] | <null>
Data Type: Include -}
include :: CharParser st TPTP_THF
include :: CharParser st TPTP_THF
include = do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "include"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    Token
fn <- CharParser st Token
forall st. CharParser st Token
fileName
    Maybe NameList
fs <- CharParser st (Maybe NameList)
forall st. CharParser st (Maybe NameList)
formulaSelection
    CharParser st ()
forall st. CharParser st ()
cParentheses
    Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.'
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ Include -> TPTP_THF
TPTP_Include (Token -> Maybe NameList -> Include
I_Include Token
fn Maybe NameList
fs)

thfAnnotatedFormula :: CharParser st TPTP_THF
thfAnnotatedFormula :: CharParser st TPTP_THF
thfAnnotatedFormula = do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "thf"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    Name
n <- CharParser st Name
forall st. CharParser st Name
name
    CharParser st ()
forall st. CharParser st ()
comma
    FormulaRole
fr <- CharParser st FormulaRole
forall st. CharParser st FormulaRole
formulaRole
    CharParser st ()
forall st. CharParser st ()
comma
    THFFormula
tf <- CharParser st THFFormula
forall st. CharParser st THFFormula
thfFormula
    Annotations
a <- CharParser st Annotations
forall st. CharParser st Annotations
annotations
    CharParser st ()
forall st. CharParser st ()
cParentheses
    Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.'
    TPTP_THF -> CharParser st TPTP_THF
forall (m :: * -> *) a. Monad m => a -> m a
return (TPTP_THF -> CharParser st TPTP_THF)
-> TPTP_THF -> CharParser st TPTP_THF
forall a b. (a -> b) -> a -> b
$ Name -> FormulaRole -> THFFormula -> Annotations -> TPTP_THF
TPTP_THF_Annotated_Formula Name
n FormulaRole
fr THFFormula
tf Annotations
a

{- THF & THF0:
<annotations>        ::= ,<source><optional_info> | <null> -}
annotations :: CharParser st Annotations
annotations :: CharParser st Annotations
annotations = do
    CharParser st ()
forall st. CharParser st ()
comma
    Source
s <- CharParser st Source
forall st. CharParser st Source
source
    OptionalInfo
oi <- CharParser st OptionalInfo
forall st. CharParser st OptionalInfo
optionalInfo
    Annotations -> CharParser st Annotations
forall (m :: * -> *) a. Monad m => a -> m a
return (Annotations -> CharParser st Annotations)
-> Annotations -> CharParser st Annotations
forall a b. (a -> b) -> a -> b
$ Source -> OptionalInfo -> Annotations
Annotations Source
s OptionalInfo
oi
  CharParser st Annotations
-> CharParser st Annotations -> CharParser st Annotations
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    ParsecT [Char] st Identity Char -> CharParser st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ',')
    Annotations -> CharParser st Annotations
forall (m :: * -> *) a. Monad m => a -> m a
return Annotations
Null

{- THF & THF0:
<formula_role>       ::= <lower_word>
<formula_role>       :== axiom | hypothesis | definition | assumption |
lemma | theorem | conjecture | negated_conjecture |
plain | fi_domain | fi_functors | fi_predicates |
type | unknown -}
formulaRole :: CharParser st FormulaRole
formulaRole :: CharParser st FormulaRole
formulaRole = do
    Token
r <- CharParser st Token
forall st. CharParser st Token
lowerWord
    case Token -> [Char]
forall a. Show a => a -> [Char]
show Token
r of
        "axiom" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Axiom
        "hypothesis" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Hypothesis
        "definition" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Definition
        "assumption" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Assumption
        "lemma" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Lemma
        "theorem" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Theorem
        "conjecture" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Conjecture
        "negated_conjecture" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Negated_Conjecture
        "plain" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Plain
        "fi_domain" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Fi_Domain
        "fi_functors" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Fi_Functors
        "fi_predicates" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Fi_Predicates
        "type" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Type
        "unknown" -> FormulaRole -> CharParser st FormulaRole
forall (m :: * -> *) a. Monad m => a -> m a
return FormulaRole
Unknown
        s :: [Char]
s -> [Char] -> CharParser st FormulaRole
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ("No such Role: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s)

{- THF
<thf_formula>        ::= <thf_logic_formula> | <thf_sequent>
THF0:
<thf_formula>        ::= <thf_logic_formula> | <thf_typed_const> -}
thfFormula :: CharParser st THFFormula
thfFormula :: CharParser st THFFormula
thfFormula = (THFTypedConst -> THFFormula)
-> ParsecT [Char] st Identity THFTypedConst
-> CharParser st THFFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFTypedConst -> THFFormula
T0F_THF_Typed_Const ParsecT [Char] st Identity THFTypedConst
forall st. CharParser st THFTypedConst
thfTypedConst
  CharParser st THFFormula
-> CharParser st THFFormula -> CharParser st THFFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFLogicFormula -> THFFormula)
-> ParsecT [Char] st Identity THFLogicFormula
-> CharParser st THFFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFLogicFormula -> THFFormula
TF_THF_Logic_Formula ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula
  CharParser st THFFormula
-> CharParser st THFFormula -> CharParser st THFFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFSequent -> THFFormula)
-> ParsecT [Char] st Identity THFSequent
-> CharParser st THFFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFSequent -> THFFormula
TF_THF_Sequent ParsecT [Char] st Identity THFSequent
forall st. CharParser st THFSequent
thfSequent

{- THF:
<thf_logic_formula>  ::= <thf_binary_formula> | <thf_unitary_formula> |
<thf_type_formula> | <thf_subtype>
THF0:
<thf_logic_formula>   ::= <thf_binary_formula> | <thf_unitary_formula> -}
thfLogicFormula :: CharParser st THFLogicFormula
thfLogicFormula :: CharParser st THFLogicFormula
thfLogicFormula = (THFBinaryFormula -> THFLogicFormula)
-> ParsecT [Char] st Identity THFBinaryFormula
-> CharParser st THFLogicFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula ParsecT [Char] st Identity THFBinaryFormula
forall st. CharParser st THFBinaryFormula
thfBinaryFormula
  CharParser st THFLogicFormula
-> CharParser st THFLogicFormula -> CharParser st THFLogicFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFUnitaryFormula -> THFLogicFormula)
-> ParsecT [Char] st Identity THFUnitaryFormula
-> CharParser st THFLogicFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula ParsecT [Char] st Identity THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula
  -- different position for unitary formula to prefer thf0 parse
  CharParser st THFLogicFormula
-> CharParser st THFLogicFormula -> CharParser st THFLogicFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFTypeFormula -> THFLogicFormula)
-> ParsecT [Char] st Identity THFTypeFormula
-> CharParser st THFLogicFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFTypeFormula -> THFLogicFormula
TLF_THF_Type_Formula ParsecT [Char] st Identity THFTypeFormula
forall st. CharParser st THFTypeFormula
thfTypeFormula
  CharParser st THFLogicFormula
-> CharParser st THFLogicFormula -> CharParser st THFLogicFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFSubType -> THFLogicFormula)
-> ParsecT [Char] st Identity THFSubType
-> CharParser st THFLogicFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFSubType -> THFLogicFormula
TLF_THF_Sub_Type ParsecT [Char] st Identity THFSubType
forall st. CharParser st THFSubType
thfSubType

{- THF:
<thf_binary_formula> ::= <thf_binary_pair> | <thf_binary_tuple> |
<thf_binary_type>
<thf_binary_pair>    ::= <thf_unitary_formula> <thf_pair_connective>
<thf_unitary_formula>
THF0:
<thf_binary_formula> ::= <thf_pair_binary> | <thf_tuple_binary>
<thf_pair_binary>    ::= <thf_unitary_formula> <thf_pair_connective>
<thf_unitary_formula>
Note: For THF0
<thf_binary_pair> is used like <thf_pair_binary> and
<thf_binary_tuple> are used like <thf_tuple_binary> -}
thfBinaryFormula :: CharParser st THFBinaryFormula
thfBinaryFormula :: CharParser st THFBinaryFormula
thfBinaryFormula = (THFBinaryTuple -> THFBinaryFormula)
-> ParsecT [Char] st Identity THFBinaryTuple
-> CharParser st THFBinaryFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple ParsecT [Char] st Identity THFBinaryTuple
forall st. CharParser st THFBinaryTuple
thfBinaryTuple
  CharParser st THFBinaryFormula
-> CharParser st THFBinaryFormula -> CharParser st THFBinaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (uff :: THFUnitaryFormula
uff, pc :: THFPairConnective
pc) <- GenParser Char st (THFUnitaryFormula, THFPairConnective)
-> GenParser Char st (THFUnitaryFormula, THFPairConnective)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st (THFUnitaryFormula, THFPairConnective)
 -> GenParser Char st (THFUnitaryFormula, THFPairConnective))
-> GenParser Char st (THFUnitaryFormula, THFPairConnective)
-> GenParser Char st (THFUnitaryFormula, THFPairConnective)
forall a b. (a -> b) -> a -> b
$ do
        THFUnitaryFormula
uff1 <- CharParser st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula
        THFPairConnective
pc1 <- CharParser st THFPairConnective
forall st. CharParser st THFPairConnective
thfPairConnective
        (THFUnitaryFormula, THFPairConnective)
-> GenParser Char st (THFUnitaryFormula, THFPairConnective)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula
uff1, THFPairConnective
pc1)
    THFUnitaryFormula
ufb <- CharParser st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula
    THFBinaryFormula -> CharParser st THFBinaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryFormula -> CharParser st THFBinaryFormula)
-> THFBinaryFormula -> CharParser st THFBinaryFormula
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula
-> THFPairConnective -> THFUnitaryFormula -> THFBinaryFormula
TBF_THF_Binary_Pair THFUnitaryFormula
uff THFPairConnective
pc THFUnitaryFormula
ufb
   CharParser st THFBinaryFormula
-> CharParser st THFBinaryFormula -> CharParser st THFBinaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFBinaryType -> THFBinaryFormula)
-> ParsecT [Char] st Identity THFBinaryType
-> CharParser st THFBinaryFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFBinaryType -> THFBinaryFormula
TBF_THF_Binary_Type ParsecT [Char] st Identity THFBinaryType
forall st. CharParser st THFBinaryType
thfBinaryType
   -- different position for binary type to prefer thf0 parse

{- THF:
<thf_binary_tuple>  ::= <thf_or_formula> | <thf_and_formula> |
<thf_apply_formula>
THF0:
<thf_tuple_binary>  ::= <thf_or_formula> | <thf_and_formula> |
<thf_apply_formula>
THF & THF0:
<thf_or_formula>    ::= <thf_unitary_formula> <vline> <thf_unitary_formula> |
<thf_or_formula> <vline> <thf_unitary_formula>
<thf_and_formula>   ::= <thf_unitary_formula> & <thf_unitary_formula> |
thf_and_formula> & <thf_unitary_formula>
<thf_apply_formula> ::= <thf_unitary_formula> @ <thf_unitary_formula> |
<thf_apply_formula> @ <thf_unitary_formula>
<vline>             :== | -}
thfBinaryTuple :: CharParser st THFBinaryTuple
thfBinaryTuple :: CharParser st THFBinaryTuple
thfBinaryTuple = do -- or
    THFUnitaryFormula
uff <- GenParser Char st THFUnitaryFormula
-> GenParser Char st THFUnitaryFormula
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula GenParser Char st THFUnitaryFormula
-> ParsecT [Char] st Identity ()
-> GenParser Char st THFUnitaryFormula
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
vLine)
    [THFUnitaryFormula]
ufb <- GenParser Char st THFUnitaryFormula
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity [THFUnitaryFormula]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 GenParser Char st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula ParsecT [Char] st Identity ()
forall st. CharParser st ()
vLine
    THFBinaryTuple -> CharParser st THFBinaryTuple
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryTuple -> CharParser st THFBinaryTuple)
-> THFBinaryTuple -> CharParser st THFBinaryTuple
forall a b. (a -> b) -> a -> b
$ [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Or_Formula (THFUnitaryFormula
uff THFUnitaryFormula -> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. a -> [a] -> [a]
: [THFUnitaryFormula]
ufb)
  CharParser st THFBinaryTuple
-> CharParser st THFBinaryTuple -> CharParser st THFBinaryTuple
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do -- and
    THFUnitaryFormula
uff <- GenParser Char st THFUnitaryFormula
-> GenParser Char st THFUnitaryFormula
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula GenParser Char st THFUnitaryFormula
-> ParsecT [Char] st Identity ()
-> GenParser Char st THFUnitaryFormula
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
ampersand)
    [THFUnitaryFormula]
ufb <- GenParser Char st THFUnitaryFormula
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity [THFUnitaryFormula]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 GenParser Char st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula ParsecT [Char] st Identity ()
forall st. CharParser st ()
ampersand
    THFBinaryTuple -> CharParser st THFBinaryTuple
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryTuple -> CharParser st THFBinaryTuple)
-> THFBinaryTuple -> CharParser st THFBinaryTuple
forall a b. (a -> b) -> a -> b
$ [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_And_Formula (THFUnitaryFormula
uff THFUnitaryFormula -> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. a -> [a] -> [a]
: [THFUnitaryFormula]
ufb)
  CharParser st THFBinaryTuple
-> CharParser st THFBinaryTuple -> CharParser st THFBinaryTuple
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do -- apply
    THFUnitaryFormula
uff <- GenParser Char st THFUnitaryFormula
-> GenParser Char st THFUnitaryFormula
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula GenParser Char st THFUnitaryFormula
-> ParsecT [Char] st Identity ()
-> GenParser Char st THFUnitaryFormula
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
at)
    [THFUnitaryFormula]
ufb <- GenParser Char st THFUnitaryFormula
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity [THFUnitaryFormula]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 GenParser Char st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula ParsecT [Char] st Identity ()
forall st. CharParser st ()
at
    THFBinaryTuple -> CharParser st THFBinaryTuple
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryTuple -> CharParser st THFBinaryTuple)
-> THFBinaryTuple -> CharParser st THFBinaryTuple
forall a b. (a -> b) -> a -> b
$ [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Apply_Formula (THFUnitaryFormula
uff THFUnitaryFormula -> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. a -> [a] -> [a]
: [THFUnitaryFormula]
ufb)

formulaWithVariables :: CharParser st (THFVariableList, THFUnitaryFormula)
formulaWithVariables :: CharParser st (THFVariableList, THFUnitaryFormula)
formulaWithVariables = do
    THFVariableList
vl <- CharParser st THFVariableList -> CharParser st THFVariableList
forall st a. CharParser st a -> CharParser st a
brackets CharParser st THFVariableList
forall st. CharParser st THFVariableList
thfVariableList
    CharParser st ()
forall st. CharParser st ()
colon
    THFUnitaryFormula
uf <- CharParser st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula
    (THFVariableList, THFUnitaryFormula)
-> CharParser st (THFVariableList, THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFVariableList
vl, THFUnitaryFormula
uf)

{- THF:
<thf_unitary_formula>    ::= <thf_quantified_formula> | <thf_unary_formula> |
<thf_atom> | <thf_tuple> | <thf_let> |
<thf_conditional> | (<thf_logic_formula>)
note: thf let is currently not well defined and thus ommited
<thf_conditional>        ::= $itef(<thf_logic_formula>,<thf_logic_formula>,
<thf_logic_formula>)
THF0:
<thf_unitary_formula>    ::= <thf_quantified_formula> | <thf_abstraction> |
<thf_unary_formula> | <thf_atom> |
(<thf_logic_formula>)
<thf_abstraction>        ::= <thf_lambda> [<thf_variable_list>] :
<thf_unitary_formula>
<thf_lambda>             ::= ^
THF & THF0:
<thf_unary_formula>      ::= <thf_unary_connective> (<thf_logic_formula>) -}
thfUnitaryFormula :: CharParser st THFUnitaryFormula
thfUnitaryFormula :: CharParser st THFUnitaryFormula
thfUnitaryFormula = (THFLogicFormula -> THFUnitaryFormula)
-> ParsecT [Char] st Identity THFLogicFormula
-> CharParser st THFUnitaryFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par (ParsecT [Char] st Identity THFLogicFormula
-> ParsecT [Char] st Identity THFLogicFormula
forall st a. CharParser st a -> CharParser st a
parentheses ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula)
  CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFQuantifiedFormula -> THFUnitaryFormula)
-> ParsecT [Char] st Identity THFQuantifiedFormula
-> CharParser st THFUnitaryFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFQuantifiedFormula -> THFUnitaryFormula
TUF_THF_Quantified_Formula (ParsecT [Char] st Identity THFQuantifiedFormula
-> ParsecT [Char] st Identity THFQuantifiedFormula
forall tok st a. GenParser tok st a -> GenParser tok st a
try ParsecT [Char] st Identity THFQuantifiedFormula
forall st. CharParser st THFQuantifiedFormula
thfQuantifiedFormula)
  CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '^'
    (vl :: THFVariableList
vl, uf :: THFUnitaryFormula
uf) <- CharParser st (THFVariableList, THFUnitaryFormula)
forall st. CharParser st (THFVariableList, THFUnitaryFormula)
formulaWithVariables
    THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> CharParser st THFUnitaryFormula)
-> THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFVariableList -> THFUnitaryFormula -> THFUnitaryFormula
T0UF_THF_Abstraction THFVariableList
vl THFUnitaryFormula
uf {- added this for thf0
  changed positions of parses below to prefer th0 -}
  CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall tok st a. GenParser tok st a -> GenParser tok st a
try CharParser st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnaryFormula
  CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFAtom -> THFUnitaryFormula)
-> ParsecT [Char] st Identity THFAtom
-> CharParser st THFUnitaryFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFAtom -> THFUnitaryFormula
TUF_THF_Atom ParsecT [Char] st Identity THFAtom
forall st. CharParser st THFAtom
thfAtom
  CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFTuple -> THFUnitaryFormula)
-> ParsecT [Char] st Identity THFTuple
-> CharParser st THFUnitaryFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFTuple -> THFUnitaryFormula
TUF_THF_Tuple ParsecT [Char] st Identity THFTuple
forall st. CharParser st THFTuple
thfTuple
  CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
-> CharParser st THFUnitaryFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "$itef"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    THFLogicFormula
lf1 <- ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula
    CharParser st ()
forall st. CharParser st ()
comma
    THFLogicFormula
lf2 <- ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula
    CharParser st ()
forall st. CharParser st ()
comma
    THFLogicFormula
lf3 <- ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula
    CharParser st ()
forall st. CharParser st ()
cParentheses
    THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> CharParser st THFUnitaryFormula)
-> THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFLogicFormula
-> THFLogicFormula -> THFLogicFormula -> THFUnitaryFormula
TUF_THF_Conditional THFLogicFormula
lf1 THFLogicFormula
lf2 THFLogicFormula
lf3

{- THF:
<thf_quantified_formula> ::= <thf_quantifier> [<thf_variable_list>] :
<thf_unitary_formula>
THF0:
<thf_quantified_formula> ::= <thf_quantified_var> | <thf_quantified_novar>
<thf_quantified_var>     ::= <quantifier> [<thf_variable_list>] :
<thf_unitary_formula>
<thf_quantified_novar>   ::= <thf_quantifier> (<thf_unitary_formula>) -}
thfQuantifiedFormula :: CharParser st THFQuantifiedFormula
thfQuantifiedFormula :: CharParser st THFQuantifiedFormula
thfQuantifiedFormula = do
    Quantifier
q <- CharParser st Quantifier
forall st. CharParser st Quantifier
quantifier
    (vl :: THFVariableList
vl, uf :: THFUnitaryFormula
uf) <- CharParser st (THFVariableList, THFUnitaryFormula)
forall st. CharParser st (THFVariableList, THFUnitaryFormula)
formulaWithVariables
    THFQuantifiedFormula -> CharParser st THFQuantifiedFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFQuantifiedFormula -> CharParser st THFQuantifiedFormula)
-> THFQuantifiedFormula -> CharParser st THFQuantifiedFormula
forall a b. (a -> b) -> a -> b
$ Quantifier
-> THFVariableList -> THFUnitaryFormula -> THFQuantifiedFormula
T0QF_THF_Quantified_Var Quantifier
q THFVariableList
vl THFUnitaryFormula
uf -- added this for thf0
  CharParser st THFQuantifiedFormula
-> CharParser st THFQuantifiedFormula
-> CharParser st THFQuantifiedFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    THFQuantifier
q <- CharParser st THFQuantifier
forall st. CharParser st THFQuantifier
thfQuantifier
    THFUnitaryFormula
uf <- CharParser st THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula
    THFQuantifiedFormula -> CharParser st THFQuantifiedFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFQuantifiedFormula -> CharParser st THFQuantifiedFormula)
-> THFQuantifiedFormula -> CharParser st THFQuantifiedFormula
forall a b. (a -> b) -> a -> b
$ THFQuantifier -> THFUnitaryFormula -> THFQuantifiedFormula
T0QF_THF_Quantified_Novar THFQuantifier
q THFUnitaryFormula
uf -- added this for thf0
  CharParser st THFQuantifiedFormula
-> CharParser st THFQuantifiedFormula
-> CharParser st THFQuantifiedFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    THFQuantifier
q <- CharParser st THFQuantifier
forall st. CharParser st THFQuantifier
thfQuantifier
    (vl :: THFVariableList
vl, uf :: THFUnitaryFormula
uf) <- CharParser st (THFVariableList, THFUnitaryFormula)
forall st. CharParser st (THFVariableList, THFUnitaryFormula)
formulaWithVariables
    THFQuantifiedFormula -> CharParser st THFQuantifiedFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFQuantifiedFormula -> CharParser st THFQuantifiedFormula)
-> THFQuantifiedFormula -> CharParser st THFQuantifiedFormula
forall a b. (a -> b) -> a -> b
$ THFQuantifier
-> THFVariableList -> THFUnitaryFormula -> THFQuantifiedFormula
TQF_THF_Quantified_Formula THFQuantifier
q THFVariableList
vl THFUnitaryFormula
uf

{- THF & THF0:
<thf_variable_list>      ::= <thf_variable> |
<thf_variable>,<thf_variable_list> -}
thfVariableList :: CharParser st THFVariableList
thfVariableList :: CharParser st THFVariableList
thfVariableList = ParsecT [Char] st Identity THFVariable
-> ParsecT [Char] st Identity () -> CharParser st THFVariableList
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity THFVariable
forall st. CharParser st THFVariable
thfVariable ParsecT [Char] st Identity ()
forall st. CharParser st ()
comma

{- THF & THF0:
<thf_variable>           ::= <thf_typed_variable> | <variable>
<thf_typed_variable>     ::= <variable> : <thf_top_level_type> -}
thfVariable :: CharParser st THFVariable
thfVariable :: CharParser st THFVariable
thfVariable = do
    Token
v <- GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Token
forall st. CharParser st Token
variable GenParser Char st Token
-> ParsecT [Char] st Identity () -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
colon)
    THFTopLevelType
tlt <- CharParser st THFTopLevelType
forall st. CharParser st THFTopLevelType
thfTopLevelType
    THFVariable -> CharParser st THFVariable
forall (m :: * -> *) a. Monad m => a -> m a
return (THFVariable -> CharParser st THFVariable)
-> THFVariable -> CharParser st THFVariable
forall a b. (a -> b) -> a -> b
$ Token -> THFTopLevelType -> THFVariable
TV_THF_Typed_Variable Token
v THFTopLevelType
tlt
  CharParser st THFVariable
-> CharParser st THFVariable -> CharParser st THFVariable
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFVariable)
-> GenParser Char st Token -> CharParser st THFVariable
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFVariable
TV_Variable GenParser Char st Token
forall st. CharParser st Token
variable

{- THF0:
<thf_typed_const>        ::= <constant> : <thf_top_level_type> |
(<thf_typed_const>) -}
thfTypedConst :: CharParser st THFTypedConst -- added this for thf0
thfTypedConst :: CharParser st THFTypedConst
thfTypedConst = (THFTypedConst -> THFTypedConst)
-> CharParser st THFTypedConst -> CharParser st THFTypedConst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFTypedConst -> THFTypedConst
T0TC_THF_TypedConst_Par (CharParser st THFTypedConst -> CharParser st THFTypedConst
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st THFTypedConst
forall st. CharParser st THFTypedConst
thfTypedConst)
  CharParser st THFTypedConst
-> CharParser st THFTypedConst -> CharParser st THFTypedConst
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Constant
c <- GenParser Char st Constant -> GenParser Char st Constant
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Constant
forall st. CharParser st Constant
constant GenParser Char st Constant
-> ParsecT [Char] st Identity () -> GenParser Char st Constant
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
colon)
    THFTopLevelType
tlt <- CharParser st THFTopLevelType
forall st. CharParser st THFTopLevelType
thfTopLevelType
    THFTypedConst -> CharParser st THFTypedConst
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTypedConst -> CharParser st THFTypedConst)
-> THFTypedConst -> CharParser st THFTypedConst
forall a b. (a -> b) -> a -> b
$ Constant -> THFTopLevelType -> THFTypedConst
T0TC_Typed_Const Constant
c THFTopLevelType
tlt

thfUnaryFormula :: CharParser st THFUnitaryFormula
thfUnaryFormula :: CharParser st THFUnitaryFormula
thfUnaryFormula = do
    THFUnaryConnective
uc <- CharParser st THFUnaryConnective
forall st. CharParser st THFUnaryConnective
thfUnaryConnective
    THFLogicFormula
lf <- CharParser st THFLogicFormula -> CharParser st THFLogicFormula
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula
    THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> CharParser st THFUnitaryFormula)
-> THFUnitaryFormula -> CharParser st THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFUnaryConnective -> THFLogicFormula -> THFUnitaryFormula
TUF_THF_Unary_Formula THFUnaryConnective
uc THFLogicFormula
lf

{- THF:
<thf_type_formula>       ::= <thf_typeable_formula> : <thf_top_level_type>
<thf_type_formula>       :== <constant> : <thf_top_level_type> -}
thfTypeFormula :: CharParser st THFTypeFormula
thfTypeFormula :: CharParser st THFTypeFormula
thfTypeFormula = do
    THFTypeableFormula
tp <- GenParser Char st THFTypeableFormula
-> GenParser Char st THFTypeableFormula
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFTypeableFormula
forall st. CharParser st THFTypeableFormula
thfTypeableFormula GenParser Char st THFTypeableFormula
-> ParsecT [Char] st Identity ()
-> GenParser Char st THFTypeableFormula
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
colon)
    THFTopLevelType
tlt <- CharParser st THFTopLevelType
forall st. CharParser st THFTopLevelType
thfTopLevelType
    THFTypeFormula -> CharParser st THFTypeFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTypeFormula -> CharParser st THFTypeFormula)
-> THFTypeFormula -> CharParser st THFTypeFormula
forall a b. (a -> b) -> a -> b
$ THFTypeableFormula -> THFTopLevelType -> THFTypeFormula
TTF_THF_Type_Formula THFTypeableFormula
tp THFTopLevelType
tlt
  CharParser st THFTypeFormula
-> CharParser st THFTypeFormula -> CharParser st THFTypeFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Constant
c <- GenParser Char st Constant -> GenParser Char st Constant
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Constant
forall st. CharParser st Constant
constant GenParser Char st Constant
-> ParsecT [Char] st Identity () -> GenParser Char st Constant
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
colon)
    THFTopLevelType
tlt <- CharParser st THFTopLevelType
forall st. CharParser st THFTopLevelType
thfTopLevelType
    THFTypeFormula -> CharParser st THFTypeFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTypeFormula -> CharParser st THFTypeFormula)
-> THFTypeFormula -> CharParser st THFTypeFormula
forall a b. (a -> b) -> a -> b
$ Constant -> THFTopLevelType -> THFTypeFormula
TTF_THF_Typed_Const Constant
c THFTopLevelType
tlt

{- THF:
<thf_typeable_formula> ::= <thf_atom> | <thf_tuple> | (<thf_logic_formula>) -}
thfTypeableFormula :: CharParser st THFTypeableFormula
thfTypeableFormula :: CharParser st THFTypeableFormula
thfTypeableFormula = (THFAtom -> THFTypeableFormula)
-> ParsecT [Char] st Identity THFAtom
-> CharParser st THFTypeableFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFAtom -> THFTypeableFormula
TTyF_THF_Atom ParsecT [Char] st Identity THFAtom
forall st. CharParser st THFAtom
thfAtom
  CharParser st THFTypeableFormula
-> CharParser st THFTypeableFormula
-> CharParser st THFTypeableFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFTuple -> THFTypeableFormula)
-> ParsecT [Char] st Identity THFTuple
-> CharParser st THFTypeableFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFTuple -> THFTypeableFormula
TTyF_THF_Tuple ParsecT [Char] st Identity THFTuple
forall st. CharParser st THFTuple
thfTuple
  CharParser st THFTypeableFormula
-> CharParser st THFTypeableFormula
-> CharParser st THFTypeableFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFLogicFormula -> THFTypeableFormula)
-> ParsecT [Char] st Identity THFLogicFormula
-> CharParser st THFTypeableFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFLogicFormula -> THFTypeableFormula
TTyF_THF_Logic_Formula (ParsecT [Char] st Identity THFLogicFormula
-> ParsecT [Char] st Identity THFLogicFormula
forall st a. CharParser st a -> CharParser st a
parentheses ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula)

{- THF:
<thf_subtype> ::= <constant> <subtype_sign> <constant>
<subtype_sign> == << -}
thfSubType :: CharParser st THFSubType
thfSubType :: CharParser st THFSubType
thfSubType = do
    Constant
cf <- GenParser Char st Constant -> GenParser Char st Constant
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Constant
forall st. CharParser st Constant
constant GenParser Char st Constant
-> ParsecT [Char] st Identity () -> GenParser Char st Constant
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser st [Char] -> ParsecT [Char] st Identity ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string "<<"))
    Constant
cb <- GenParser Char st Constant
forall st. CharParser st Constant
constant
    THFSubType -> CharParser st THFSubType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFSubType -> CharParser st THFSubType)
-> THFSubType -> CharParser st THFSubType
forall a b. (a -> b) -> a -> b
$ Constant -> Constant -> THFSubType
TST_THF_Sub_Type Constant
cf Constant
cb

{- THF:
<thf_top_level_type> ::= <thf_logic_formula>
THF0:
<thf_top_level_type> ::= <constant> | <variable> | <defined_type> |
<system_type> | <thf_binary_type> -}
thfTopLevelType :: CharParser st THFTopLevelType
thfTopLevelType :: CharParser st THFTopLevelType
thfTopLevelType = (THFBinaryType -> THFTopLevelType)
-> ParsecT [Char] st Identity THFBinaryType
-> CharParser st THFTopLevelType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFBinaryType -> THFTopLevelType
T0TLT_THF_Binary_Type ParsecT [Char] st Identity THFBinaryType
forall st. CharParser st THFBinaryType
thfBinaryType
  CharParser st THFTopLevelType
-> CharParser st THFTopLevelType -> CharParser st THFTopLevelType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Constant -> THFTopLevelType)
-> ParsecT [Char] st Identity Constant
-> CharParser st THFTopLevelType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> THFTopLevelType
T0TLT_Constant ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
constant
  CharParser st THFTopLevelType
-> CharParser st THFTopLevelType -> CharParser st THFTopLevelType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFTopLevelType)
-> ParsecT [Char] st Identity Token
-> CharParser st THFTopLevelType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFTopLevelType
T0TLT_Variable ParsecT [Char] st Identity Token
forall st. CharParser st Token
variable
  CharParser st THFTopLevelType
-> CharParser st THFTopLevelType -> CharParser st THFTopLevelType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DefinedType -> THFTopLevelType)
-> ParsecT [Char] st Identity DefinedType
-> CharParser st THFTopLevelType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedType -> THFTopLevelType
T0TLT_Defined_Type ParsecT [Char] st Identity DefinedType
forall st. CharParser st DefinedType
definedType
  CharParser st THFTopLevelType
-> CharParser st THFTopLevelType -> CharParser st THFTopLevelType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFTopLevelType)
-> ParsecT [Char] st Identity Token
-> CharParser st THFTopLevelType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFTopLevelType
T0TLT_System_Type ParsecT [Char] st Identity Token
forall st. CharParser st Token
systemType
  CharParser st THFTopLevelType
-> CharParser st THFTopLevelType -> CharParser st THFTopLevelType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFLogicFormula -> THFTopLevelType)
-> ParsecT [Char] st Identity THFLogicFormula
-> CharParser st THFTopLevelType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFLogicFormula -> THFTopLevelType
TTLT_THF_Logic_Formula ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula
  -- added all except for this for thf0

{- THF:
<thf_unitary_type>   ::= <thf_unitary_formula>
THF0:
<thf_unitary_type>   ::= <constant> | <variable> | <defined_type> |
<system_type> | (<thf_binary_type>) -}
thfUnitaryType :: CharParser st THFUnitaryType
thfUnitaryType :: CharParser st THFUnitaryType
thfUnitaryType = (Constant -> THFUnitaryType)
-> ParsecT [Char] st Identity Constant
-> CharParser st THFUnitaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> THFUnitaryType
T0UT_Constant ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
constant
  CharParser st THFUnitaryType
-> CharParser st THFUnitaryType -> CharParser st THFUnitaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFUnitaryType)
-> ParsecT [Char] st Identity Token -> CharParser st THFUnitaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFUnitaryType
T0UT_Variable ParsecT [Char] st Identity Token
forall st. CharParser st Token
variable
  CharParser st THFUnitaryType
-> CharParser st THFUnitaryType -> CharParser st THFUnitaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DefinedType -> THFUnitaryType)
-> ParsecT [Char] st Identity DefinedType
-> CharParser st THFUnitaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedType -> THFUnitaryType
T0UT_Defined_Type ParsecT [Char] st Identity DefinedType
forall st. CharParser st DefinedType
definedType
  CharParser st THFUnitaryType
-> CharParser st THFUnitaryType -> CharParser st THFUnitaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFUnitaryType)
-> ParsecT [Char] st Identity Token -> CharParser st THFUnitaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFUnitaryType
T0UT_System_Type ParsecT [Char] st Identity Token
forall st. CharParser st Token
systemType
  CharParser st THFUnitaryType
-> CharParser st THFUnitaryType -> CharParser st THFUnitaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFBinaryType -> THFUnitaryType)
-> ParsecT [Char] st Identity THFBinaryType
-> CharParser st THFUnitaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFBinaryType -> THFUnitaryType
T0UT_THF_Binary_Type_Par (ParsecT [Char] st Identity THFBinaryType
-> ParsecT [Char] st Identity THFBinaryType
forall st a. CharParser st a -> CharParser st a
parentheses ParsecT [Char] st Identity THFBinaryType
forall st. CharParser st THFBinaryType
thfBinaryType)
  CharParser st THFUnitaryType
-> CharParser st THFUnitaryType -> CharParser st THFUnitaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFUnitaryFormula -> THFUnitaryType)
-> ParsecT [Char] st Identity THFUnitaryFormula
-> CharParser st THFUnitaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFUnitaryFormula -> THFUnitaryType
TUT_THF_Unitary_Formula ParsecT [Char] st Identity THFUnitaryFormula
forall st. CharParser st THFUnitaryFormula
thfUnitaryFormula
  -- added all except for this for th0

{- THF:
<thf_binary_type>    ::= <thf_mapping_type> | <thf_xprod_type> |
<thf_union_type>
<thf_xprod_type>     ::= <thf_unitary_type> <star> <thf_unitary_type> |
<thf_xprod_type> <star> <thf_unitary_type>
<star> ::- *
<thf_union_type>     ::= <thf_unitary_type> <plus> <thf_unitary_type> |
<thf_union_type> <plus> <thf_unitary_type>
<plus> ::- +
THF0:
<thf_binary_type>    ::= <thf_mapping_type> | (<thf_binary_type>)
THF & THF0:
<thf_mapping_type>   ::= <thf_unitary_type> <arrow> <thf_unitary_type> |
<thf_unitary_type> <arrow> <thf_mapping_type>
<arrow> ::- > -}
thfBinaryType :: CharParser st THFBinaryType
thfBinaryType :: CharParser st THFBinaryType
thfBinaryType = do
    THFUnitaryType
utf <- GenParser Char st THFUnitaryType
-> GenParser Char st THFUnitaryType
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFUnitaryType
forall st. CharParser st THFUnitaryType
thfUnitaryType GenParser Char st THFUnitaryType
-> ParsecT [Char] st Identity ()
-> GenParser Char st THFUnitaryType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
arrow)
    [THFUnitaryType]
utb <- GenParser Char st THFUnitaryType
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity [THFUnitaryType]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 GenParser Char st THFUnitaryType
forall st. CharParser st THFUnitaryType
thfUnitaryType ParsecT [Char] st Identity ()
forall st. CharParser st ()
arrow
    THFBinaryType -> CharParser st THFBinaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryType -> CharParser st THFBinaryType)
-> THFBinaryType -> CharParser st THFBinaryType
forall a b. (a -> b) -> a -> b
$ [THFUnitaryType] -> THFBinaryType
TBT_THF_Mapping_Type (THFUnitaryType
utf THFUnitaryType -> [THFUnitaryType] -> [THFUnitaryType]
forall a. a -> [a] -> [a]
: [THFUnitaryType]
utb)
  CharParser st THFBinaryType
-> CharParser st THFBinaryType -> CharParser st THFBinaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFBinaryType -> THFBinaryType)
-> CharParser st THFBinaryType -> CharParser st THFBinaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFBinaryType -> THFBinaryType
T0BT_THF_Binary_Type_Par (CharParser st THFBinaryType -> CharParser st THFBinaryType
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st THFBinaryType
forall st. CharParser st THFBinaryType
thfBinaryType)
  -- added this for thf0
  CharParser st THFBinaryType
-> CharParser st THFBinaryType -> CharParser st THFBinaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do -- xprodType
    THFUnitaryType
utf <- GenParser Char st THFUnitaryType
-> GenParser Char st THFUnitaryType
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFUnitaryType
forall st. CharParser st THFUnitaryType
thfUnitaryType GenParser Char st THFUnitaryType
-> ParsecT [Char] st Identity ()
-> GenParser Char st THFUnitaryType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
star)
    [THFUnitaryType]
utb <- GenParser Char st THFUnitaryType
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity [THFUnitaryType]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 GenParser Char st THFUnitaryType
forall st. CharParser st THFUnitaryType
thfUnitaryType ParsecT [Char] st Identity ()
forall st. CharParser st ()
star
    THFBinaryType -> CharParser st THFBinaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryType -> CharParser st THFBinaryType)
-> THFBinaryType -> CharParser st THFBinaryType
forall a b. (a -> b) -> a -> b
$ [THFUnitaryType] -> THFBinaryType
TBT_THF_Xprod_Type (THFUnitaryType
utf THFUnitaryType -> [THFUnitaryType] -> [THFUnitaryType]
forall a. a -> [a] -> [a]
: [THFUnitaryType]
utb)
  CharParser st THFBinaryType
-> CharParser st THFBinaryType -> CharParser st THFBinaryType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do -- unionType
    THFUnitaryType
utf <- GenParser Char st THFUnitaryType
-> GenParser Char st THFUnitaryType
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFUnitaryType
forall st. CharParser st THFUnitaryType
thfUnitaryType GenParser Char st THFUnitaryType
-> ParsecT [Char] st Identity ()
-> GenParser Char st THFUnitaryType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
plus)
    [THFUnitaryType]
utb <- GenParser Char st THFUnitaryType
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity [THFUnitaryType]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 GenParser Char st THFUnitaryType
forall st. CharParser st THFUnitaryType
thfUnitaryType ParsecT [Char] st Identity ()
forall st. CharParser st ()
plus
    THFBinaryType -> CharParser st THFBinaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryType -> CharParser st THFBinaryType)
-> THFBinaryType -> CharParser st THFBinaryType
forall a b. (a -> b) -> a -> b
$ [THFUnitaryType] -> THFBinaryType
TBT_THF_Union_Type (THFUnitaryType
utf THFUnitaryType -> [THFUnitaryType] -> [THFUnitaryType]
forall a. a -> [a] -> [a]
: [THFUnitaryType]
utb)

{- THF:
<thf_atom>               ::= <term> | <thf_conn_term>
%----<thf_atom> can also be <defined_type> | <defined_plain_formula> |
%----<system_type> | <system_atomic_formula>, but they are syntactically
%----captured by <term>.
<system_atomic_formula>  ::= <system_term>
THF0:
<thf_atom>               ::= <constant> | <defined_constant> |
<system_constant> | <variable> | <thf_conn_term>
<defined_constant>       ::= <atomic_defined_word>
<system_constant>        ::= <atomic_system_word> -}
thfAtom :: CharParser st THFAtom
thfAtom :: CharParser st THFAtom
thfAtom = (Constant -> THFAtom)
-> ParsecT [Char] st Identity Constant -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> THFAtom
T0A_Constant ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
constant
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFAtom)
-> ParsecT [Char] st Identity Token -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFAtom
T0A_Defined_Constant ParsecT [Char] st Identity Token
forall st. CharParser st Token
atomicDefinedWord
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFAtom)
-> ParsecT [Char] st Identity Token -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFAtom
T0A_System_Constant ParsecT [Char] st Identity Token
forall st. CharParser st Token
atomicSystemWord
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFAtom)
-> ParsecT [Char] st Identity Token -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFAtom
T0A_Variable ParsecT [Char] st Identity Token
forall st. CharParser st Token
variable
  -- added all above for thf0
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFConnTerm -> THFAtom)
-> ParsecT [Char] st Identity THFConnTerm -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFConnTerm -> THFAtom
TA_THF_Conn_Term ParsecT [Char] st Identity THFConnTerm
forall st. CharParser st THFConnTerm
thfConnTerm
  -- changed position to prefer thf0
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DefinedType -> THFAtom)
-> ParsecT [Char] st Identity DefinedType -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedType -> THFAtom
TA_Defined_Type ParsecT [Char] st Identity DefinedType
forall st. CharParser st DefinedType
definedType
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DefinedPlainFormula -> THFAtom)
-> ParsecT [Char] st Identity DefinedPlainFormula
-> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedPlainFormula -> THFAtom
TA_Defined_Plain_Formula ParsecT [Char] st Identity DefinedPlainFormula
forall st. CharParser st DefinedPlainFormula
definedPlainFormula
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> THFAtom)
-> ParsecT [Char] st Identity Token -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> THFAtom
TA_System_Type ParsecT [Char] st Identity Token
forall st. CharParser st Token
systemType
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (SystemTerm -> THFAtom)
-> ParsecT [Char] st Identity SystemTerm -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SystemTerm -> THFAtom
TA_System_Atomic_Formula ParsecT [Char] st Identity SystemTerm
forall st. CharParser st SystemTerm
systemTerm
  CharParser st THFAtom
-> CharParser st THFAtom -> CharParser st THFAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Term -> THFAtom)
-> ParsecT [Char] st Identity Term -> CharParser st THFAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> THFAtom
TA_Term ParsecT [Char] st Identity Term
forall st. CharParser st Term
term

{- THF:
<thf_tuple> ::= [] | [<thf_tuple_list>]
<thf_tuple_list> ::= <thf_logic_formula> |
<thf_logic_formula>,<thf_tuple_list>
THFTupleList must not be empty -}
thfTuple :: CharParser st THFTuple
thfTuple :: CharParser st THFTuple
thfTuple = CharParser st THFTuple -> CharParser st THFTuple
forall tok st a. GenParser tok st a -> GenParser tok st a
try ((CharParser st ()
forall st. CharParser st ()
oBracket CharParser st () -> CharParser st () -> CharParser st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser st ()
forall st. CharParser st ()
cBracket) CharParser st ()
-> CharParser st THFTuple -> CharParser st THFTuple
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFTuple -> CharParser st THFTuple
forall (m :: * -> *) a. Monad m => a -> m a
return [])
  CharParser st THFTuple
-> CharParser st THFTuple -> CharParser st THFTuple
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st THFTuple -> CharParser st THFTuple
forall st a. CharParser st a -> CharParser st a
brackets (ParsecT [Char] st Identity THFLogicFormula
-> CharParser st () -> CharParser st THFTuple
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity THFLogicFormula
forall st. CharParser st THFLogicFormula
thfLogicFormula CharParser st ()
forall st. CharParser st ()
comma)

{- THF:
<thf_sequent> ::= <thf_tuple> <gentzen_arrow> <thf_tuple> |
(<thf_sequent>)
<gentzen_arrow> ::= --> -}
thfSequent :: CharParser st THFSequent
thfSequent :: CharParser st THFSequent
thfSequent = (THFSequent -> THFSequent)
-> CharParser st THFSequent -> CharParser st THFSequent
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFSequent -> THFSequent
TS_THF_Sequent_Par (CharParser st THFSequent -> CharParser st THFSequent
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st THFSequent
forall st. CharParser st THFSequent
thfSequent)
  CharParser st THFSequent
-> CharParser st THFSequent -> CharParser st THFSequent
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    THFTuple
tf <- GenParser Char st THFTuple -> GenParser Char st THFTuple
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st THFTuple
forall st. CharParser st THFTuple
thfTuple GenParser Char st THFTuple
-> ParsecT [Char] st Identity () -> GenParser Char st THFTuple
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
gentzenArrow)
    THFTuple
tb <- GenParser Char st THFTuple
forall st. CharParser st THFTuple
thfTuple
    THFSequent -> CharParser st THFSequent
forall (m :: * -> *) a. Monad m => a -> m a
return (THFSequent -> CharParser st THFSequent)
-> THFSequent -> CharParser st THFSequent
forall a b. (a -> b) -> a -> b
$ THFTuple -> THFTuple -> THFSequent
TS_THF_Sequent THFTuple
tf THFTuple
tb

{- THF:
<thf_conn_term>  ::= <thf_pair_connective> | <assoc_connective> |
<thf_unary_connective>
THF0:
<thf_conn_term>  ::= <thf_quantifier> | <thf_pair_connective> |
<assoc_connective> | <thf_unary_connective> -}
thfConnTerm :: CharParser st THFConnTerm
thfConnTerm :: CharParser st THFConnTerm
thfConnTerm = (THFPairConnective -> THFConnTerm)
-> ParsecT [Char] st Identity THFPairConnective
-> CharParser st THFConnTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFPairConnective -> THFConnTerm
TCT_THF_Pair_Connective ParsecT [Char] st Identity THFPairConnective
forall st. CharParser st THFPairConnective
thfPairConnective
  CharParser st THFConnTerm
-> CharParser st THFConnTerm -> CharParser st THFConnTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (AssocConnective -> THFConnTerm)
-> ParsecT [Char] st Identity AssocConnective
-> CharParser st THFConnTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AssocConnective -> THFConnTerm
TCT_Assoc_Connective ParsecT [Char] st Identity AssocConnective
forall st. CharParser st AssocConnective
assocConnective
  CharParser st THFConnTerm
-> CharParser st THFConnTerm -> CharParser st THFConnTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFUnaryConnective -> THFConnTerm)
-> ParsecT [Char] st Identity THFUnaryConnective
-> CharParser st THFConnTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFUnaryConnective -> THFConnTerm
TCT_THF_Unary_Connective ParsecT [Char] st Identity THFUnaryConnective
forall st. CharParser st THFUnaryConnective
thfUnaryConnective
  CharParser st THFConnTerm
-> CharParser st THFConnTerm -> CharParser st THFConnTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (THFQuantifier -> THFConnTerm)
-> ParsecT [Char] st Identity THFQuantifier
-> CharParser st THFConnTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFQuantifier -> THFConnTerm
T0CT_THF_Quantifier ParsecT [Char] st Identity THFQuantifier
forall st. CharParser st THFQuantifier
thfQuantifier
  -- added for thf0

{- THF:
<thf_quantifier>     ::= <fol_quantifier> | ^ | !> | ?* | @+ | @-
<fol_quantifier>     ::= ! | ?
THF0:
<thf_quantifier>     ::= !! | ?? -}
thfQuantifier :: CharParser st THFQuantifier
thfQuantifier :: CharParser st THFQuantifier
thfQuantifier = (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "!!") CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
T0Q_PiForAll)
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "??") CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
T0Q_SigmaExists)
  -- added all above for thf0
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '!' CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
TQ_ForAll)
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '?' CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
TQ_Exists)
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '^' CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
TQ_Lambda_Binder)
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "!>") CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
TQ_Dependent_Product)
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "?*") CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
TQ_Dependent_Sum)
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "@+") CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
TQ_Indefinite_Description)
  CharParser st THFQuantifier
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "@-") CharParser st ()
-> CharParser st THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFQuantifier -> CharParser st THFQuantifier
forall (m :: * -> *) a. Monad m => a -> m a
return THFQuantifier
TQ_Definite_Description)
  CharParser st THFQuantifier
-> [Char] -> CharParser st THFQuantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "thfQuantifier"

{- THF0:
<quantifier>         ::= ! | ? -}
quantifier :: CharParser st Quantifier
quantifier :: CharParser st Quantifier
quantifier = (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '!' CharParser st ()
-> CharParser st Quantifier -> CharParser st Quantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Quantifier -> CharParser st Quantifier
forall (m :: * -> *) a. Monad m => a -> m a
return Quantifier
T0Q_ForAll)
  CharParser st Quantifier
-> CharParser st Quantifier -> CharParser st Quantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '?' CharParser st ()
-> CharParser st Quantifier -> CharParser st Quantifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Quantifier -> CharParser st Quantifier
forall (m :: * -> *) a. Monad m => a -> m a
return Quantifier
T0Q_Exists)
  CharParser st Quantifier -> [Char] -> CharParser st Quantifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "quantifier"

{- THF:
<thf_pair_connective> ::= <infix_equality> | <infix_inequality> |
<binary_connective>
<infix_equality>     ::= =
<infix_inequality>   ::= !=
THF0:
<thf_pair_connective> ::= <defined_infix_pred> | <binary_connective>
<defined_infix_pred> ::= = | !=
THF & THF0:
<binary_connective>  ::= <=> | => | <= | <~> | ~<vline> | ~& -}
thfPairConnective :: CharParser st THFPairConnective
thfPairConnective :: CharParser st THFPairConnective
thfPairConnective = (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "!=") CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
Infix_Inequality)
  CharParser st THFPairConnective
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "<=>") CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
Equivalent)
  CharParser st THFPairConnective
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "=>") CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
Implication)
  CharParser st THFPairConnective
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "<=") CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
IF)
  CharParser st THFPairConnective
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "<~>") CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
XOR)
  CharParser st THFPairConnective
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "~|") CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
NOR)
  CharParser st THFPairConnective
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "~&") CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
NAND)
  CharParser st THFPairConnective
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '=' CharParser st ()
-> CharParser st THFPairConnective
-> CharParser st THFPairConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFPairConnective -> CharParser st THFPairConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFPairConnective
Infix_Equality)
  CharParser st THFPairConnective
-> [Char] -> CharParser st THFPairConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "pairConnective"

{- THF:
<thf_unary_connective> ::= <unary_connective> | !! | ??
THF0:
<thf_unary_connective> ::= <unary_connective>
THF & THF0:
<unary_connective>   ::= ~ -}
thfUnaryConnective :: CharParser st THFUnaryConnective
thfUnaryConnective :: CharParser st THFUnaryConnective
thfUnaryConnective = (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '~' CharParser st ()
-> CharParser st THFUnaryConnective
-> CharParser st THFUnaryConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFUnaryConnective -> CharParser st THFUnaryConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFUnaryConnective
Negation)
  CharParser st THFUnaryConnective
-> CharParser st THFUnaryConnective
-> CharParser st THFUnaryConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "!!") CharParser st ()
-> CharParser st THFUnaryConnective
-> CharParser st THFUnaryConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFUnaryConnective -> CharParser st THFUnaryConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFUnaryConnective
PiForAll)
  CharParser st THFUnaryConnective
-> CharParser st THFUnaryConnective
-> CharParser st THFUnaryConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "??") CharParser st ()
-> CharParser st THFUnaryConnective
-> CharParser st THFUnaryConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> THFUnaryConnective -> CharParser st THFUnaryConnective
forall (m :: * -> *) a. Monad m => a -> m a
return THFUnaryConnective
SigmaExists)

{- THF & THF0:
<assoc_connective>   ::= <vline> | & -}
assocConnective :: CharParser st AssocConnective
assocConnective :: CharParser st AssocConnective
assocConnective = (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '|' CharParser st ()
-> CharParser st AssocConnective -> CharParser st AssocConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AssocConnective -> CharParser st AssocConnective
forall (m :: * -> *) a. Monad m => a -> m a
return AssocConnective
OR)
  CharParser st AssocConnective
-> CharParser st AssocConnective -> CharParser st AssocConnective
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '&' CharParser st ()
-> CharParser st AssocConnective -> CharParser st AssocConnective
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AssocConnective -> CharParser st AssocConnective
forall (m :: * -> *) a. Monad m => a -> m a
return AssocConnective
AND)

{- THF:
<defined_type>       :== $oType | $o | $iType | $i | $tType |
real | $rat | $int
THF0:
<defined_type>       :== $oType | $o | $iType | $i | $tType
THF & THF0:
<defined_type>       ::= <atomic_defined_word> -}
definedType :: CharParser st DefinedType
definedType :: CharParser st DefinedType
definedType = do
    Token
adw <- CharParser st Token
forall st. CharParser st Token
atomicDefinedWord
    case Token -> [Char]
forall a. Show a => a -> [Char]
show Token
adw of
        "oType" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_oType
        "o" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_o
        "iType" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_iType
        "i" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_i
        "tType" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_tType
        "real" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_real
        "rat" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_rat
        "int" -> DefinedType -> CharParser st DefinedType
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedType
DT_int
        s :: [Char]
s -> [Char] -> CharParser st DefinedType
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ("No such definedType: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s)

{- THF & THF0:
<system_type>        ::= <atomic_system_word> -}
systemType :: CharParser st Token
systemType :: CharParser st Token
systemType = CharParser st Token
forall st. CharParser st Token
atomicSystemWord

{- THF:
<defined_plain_formula> ::= <defined_plain_term>
<defined_plain_formula> :== <defined_prop> | <defined_pred>(<arguments>) -}
definedPlainFormula :: CharParser st DefinedPlainFormula
definedPlainFormula :: CharParser st DefinedPlainFormula
definedPlainFormula = (DefinedProp -> DefinedPlainFormula)
-> ParsecT [Char] st Identity DefinedProp
-> CharParser st DefinedPlainFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedProp -> DefinedPlainFormula
DPF_Defined_Prop ParsecT [Char] st Identity DefinedProp
forall st. CharParser st DefinedProp
definedProp
  CharParser st DefinedPlainFormula
-> CharParser st DefinedPlainFormula
-> CharParser st DefinedPlainFormula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    DefinedPred
dp <- CharParser st DefinedPred
forall st. CharParser st DefinedPred
definedPred
    Arguments
a <- CharParser st Arguments -> CharParser st Arguments
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st Arguments
forall st. CharParser st Arguments
arguments
    DefinedPlainFormula -> CharParser st DefinedPlainFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (DefinedPlainFormula -> CharParser st DefinedPlainFormula)
-> DefinedPlainFormula -> CharParser st DefinedPlainFormula
forall a b. (a -> b) -> a -> b
$ DefinedPred -> Arguments -> DefinedPlainFormula
DPF_Defined_Formula DefinedPred
dp Arguments
a

{- THF & THF0:
<defined_prop>       :== <atomic_defined_word>
<defined_prop>       :== $true | $false -}
definedProp :: CharParser st DefinedProp
definedProp :: CharParser st DefinedProp
definedProp = do
    Token
adw <- CharParser st Token
forall st. CharParser st Token
atomicDefinedWord
    case Token -> [Char]
forall a. Show a => a -> [Char]
show Token
adw of
        "true" -> DefinedProp -> CharParser st DefinedProp
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedProp
DP_True
        "false" -> DefinedProp -> CharParser st DefinedProp
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedProp
DP_False
        s :: [Char]
s -> [Char] -> CharParser st DefinedProp
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ("No such definedProp: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s)

{- THF:
<defined_pred>       :== <atomic_defined_word>
<defined_pred>       :== $distinct |
less | $lesseq | $greater | $greatereq |
is_int | $is_rat -}
definedPred :: CharParser st DefinedPred
definedPred :: CharParser st DefinedPred
definedPred = do
    Token
adw <- CharParser st Token
forall st. CharParser st Token
atomicDefinedWord
    case Token -> [Char]
forall a. Show a => a -> [Char]
show Token
adw of
        "distinct" -> DefinedPred -> CharParser st DefinedPred
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedPred
Disrinct
        "less" -> DefinedPred -> CharParser st DefinedPred
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedPred
Less
        "lesseq" -> DefinedPred -> CharParser st DefinedPred
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedPred
Lesseq
        "greater" -> DefinedPred -> CharParser st DefinedPred
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedPred
Greater
        "greatereq" -> DefinedPred -> CharParser st DefinedPred
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedPred
Greatereq
        "is_int" -> DefinedPred -> CharParser st DefinedPred
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedPred
Is_int
        "is_rat" -> DefinedPred -> CharParser st DefinedPred
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedPred
Is_rat
        s :: [Char]
s -> [Char] -> CharParser st DefinedPred
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ("No such definedPred: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s)

{- THF:
<term> ::= <function_term> | <variable> | <conditional_term>
%----Conditional terms should only be used by TFF and not by THF.
Thus tey are not implemented. -}
term :: CharParser st Term
term :: CharParser st Term
term = (FunctionTerm -> Term)
-> ParsecT [Char] st Identity FunctionTerm -> CharParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FunctionTerm -> Term
T_Function_Term ParsecT [Char] st Identity FunctionTerm
forall st. CharParser st FunctionTerm
functionTerm
  CharParser st Term -> CharParser st Term -> CharParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> Term)
-> ParsecT [Char] st Identity Token -> CharParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Term
T_Variable ParsecT [Char] st Identity Token
forall st. CharParser st Token
variable

{- THF:
<function_term> ::= <plain_term> | <defined_term> | <system_term> -}
functionTerm :: CharParser st FunctionTerm
functionTerm :: CharParser st FunctionTerm
functionTerm = (SystemTerm -> FunctionTerm)
-> ParsecT [Char] st Identity SystemTerm
-> CharParser st FunctionTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SystemTerm -> FunctionTerm
FT_System_Term ParsecT [Char] st Identity SystemTerm
forall st. CharParser st SystemTerm
systemTerm
  CharParser st FunctionTerm
-> CharParser st FunctionTerm -> CharParser st FunctionTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DefinedTerm -> FunctionTerm)
-> ParsecT [Char] st Identity DefinedTerm
-> CharParser st FunctionTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedTerm -> FunctionTerm
FT_Defined_Term ParsecT [Char] st Identity DefinedTerm
forall st. CharParser st DefinedTerm
definedTerm
  CharParser st FunctionTerm
-> CharParser st FunctionTerm -> CharParser st FunctionTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (PlainTerm -> FunctionTerm)
-> ParsecT [Char] st Identity PlainTerm
-> CharParser st FunctionTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainTerm -> FunctionTerm
FT_Plain_Term ParsecT [Char] st Identity PlainTerm
forall st. CharParser st PlainTerm
plainTerm

{- THF:
<plain_term> ::= <constant> | <functor>(<arguments>) -}
plainTerm :: CharParser st PlainTerm
plainTerm :: CharParser st PlainTerm
plainTerm = CharParser st PlainTerm -> CharParser st PlainTerm
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    Constant
f <- CharParser st Constant
forall st. CharParser st Constant
tptpFunctor
    Arguments
a <- CharParser st Arguments -> CharParser st Arguments
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st Arguments
forall st. CharParser st Arguments
arguments
    PlainTerm -> CharParser st PlainTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PlainTerm -> CharParser st PlainTerm)
-> PlainTerm -> CharParser st PlainTerm
forall a b. (a -> b) -> a -> b
$ Constant -> Arguments -> PlainTerm
PT_Plain_Term Constant
f Arguments
a)
  CharParser st PlainTerm
-> CharParser st PlainTerm -> CharParser st PlainTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Constant -> PlainTerm)
-> CharParser st Constant -> CharParser st PlainTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> PlainTerm
PT_Constant CharParser st Constant
forall st. CharParser st Constant
constant

{- THF & THF0:
<constant> ::= <functor> -}
constant :: CharParser st Constant
constant :: CharParser st Constant
constant = CharParser st Constant
forall st. CharParser st Constant
tptpFunctor

{- THF & THF0:
<functor>  ::= <atomic_word> -}
tptpFunctor :: CharParser st AtomicWord
tptpFunctor :: CharParser st Constant
tptpFunctor = CharParser st Constant
forall st. CharParser st Constant
atomicWord

{- THF:
<defined_term> ::= <defined_atom> | <defined_atomic_term>
<defined_atomic_term> ::= <defined_plain_term> -}
definedTerm :: CharParser st DefinedTerm
definedTerm :: CharParser st DefinedTerm
definedTerm = (DefinedPlainTerm -> DefinedTerm)
-> ParsecT [Char] st Identity DefinedPlainTerm
-> CharParser st DefinedTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedPlainTerm -> DefinedTerm
DT_Defined_Atomic_Term ParsecT [Char] st Identity DefinedPlainTerm
forall st. CharParser st DefinedPlainTerm
definedPlainTerm
  CharParser st DefinedTerm
-> CharParser st DefinedTerm -> CharParser st DefinedTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DefinedAtom -> DefinedTerm)
-> ParsecT [Char] st Identity DefinedAtom
-> CharParser st DefinedTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedAtom -> DefinedTerm
DT_Defined_Atom ParsecT [Char] st Identity DefinedAtom
forall st. CharParser st DefinedAtom
definedAtom

{- THF:
<defined_atom> ::= <number> | <distinct_object> -}
definedAtom :: CharParser st DefinedAtom
definedAtom :: CharParser st DefinedAtom
definedAtom = (Number -> DefinedAtom)
-> ParsecT [Char] st Identity Number -> CharParser st DefinedAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Number -> DefinedAtom
DA_Number ParsecT [Char] st Identity Number
forall st. CharParser st Number
number
  CharParser st DefinedAtom
-> CharParser st DefinedAtom -> CharParser st DefinedAtom
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> DefinedAtom)
-> ParsecT [Char] st Identity Token -> CharParser st DefinedAtom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> DefinedAtom
DA_Distinct_Object ParsecT [Char] st Identity Token
forall st. CharParser st Token
distinctObject

{- THF:
<defined_plain_term> ::= <defined_constant> | <defined_functor>(<arguments>)
<defined_constant> ::= <defined_functor> -}
definedPlainTerm :: CharParser st DefinedPlainTerm
definedPlainTerm :: CharParser st DefinedPlainTerm
definedPlainTerm = CharParser st DefinedPlainTerm -> CharParser st DefinedPlainTerm
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    DefinedFunctor
df <- CharParser st DefinedFunctor
forall st. CharParser st DefinedFunctor
definedFunctor
    Arguments
a <- CharParser st Arguments -> CharParser st Arguments
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st Arguments
forall st. CharParser st Arguments
arguments
    DefinedPlainTerm -> CharParser st DefinedPlainTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DefinedPlainTerm -> CharParser st DefinedPlainTerm)
-> DefinedPlainTerm -> CharParser st DefinedPlainTerm
forall a b. (a -> b) -> a -> b
$ DefinedFunctor -> Arguments -> DefinedPlainTerm
DPT_Defined_Function DefinedFunctor
df Arguments
a)
  CharParser st DefinedPlainTerm
-> CharParser st DefinedPlainTerm -> CharParser st DefinedPlainTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DefinedFunctor -> DefinedPlainTerm)
-> CharParser st DefinedFunctor -> CharParser st DefinedPlainTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinedFunctor -> DefinedPlainTerm
DPT_Defined_Constant CharParser st DefinedFunctor
forall st. CharParser st DefinedFunctor
definedFunctor

{- THF:
<defined_functor> ::= <atomic_defined_word>
<defined_functor> :== $uminus | $sum | $difference | $product |
quotient | $quotient_e | $quotient_t | $quotient_f |
remainder_e | $remainder_t | $remainder_f |
floor | $ceiling | $truncate | $round |
to_int | $to_rat | $to_real -}
definedFunctor :: CharParser st DefinedFunctor
definedFunctor :: CharParser st DefinedFunctor
definedFunctor = do
    Token
adw <- CharParser st Token
forall st. CharParser st Token
atomicDefinedWord
    case Token -> [Char]
forall a. Show a => a -> [Char]
show Token
adw of
        "uminus" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
UMinus
        "sum" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Sum
        "difference" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Difference
        "product" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Product
        "quotient" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Quotient
        "quotient_e" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Quotient_e
        "quotient_t" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Quotient_t
        "quotient_f" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Quotient_f
        "floor" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Floor
        "ceiling" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Ceiling
        "truncate" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Truncate
        "round" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
Round
        "to_int" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
To_int
        "to_rat" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
To_rat
        "to_real" -> DefinedFunctor -> CharParser st DefinedFunctor
forall (m :: * -> *) a. Monad m => a -> m a
return DefinedFunctor
To_real
        s :: [Char]
s -> [Char] -> CharParser st DefinedFunctor
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ("No such definedFunctor: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s)

{- THF:
<system_term>        ::= <system_constant> | <system_functor>(<arguments>)
<system_constant>    ::= <system_functor> -}
systemTerm :: CharParser st SystemTerm
systemTerm :: CharParser st SystemTerm
systemTerm = CharParser st SystemTerm -> CharParser st SystemTerm
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    Token
sf <- CharParser st Token
forall st. CharParser st Token
systemFunctor
    Arguments
a <- CharParser st Arguments -> CharParser st Arguments
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st Arguments
forall st. CharParser st Arguments
arguments
    SystemTerm -> CharParser st SystemTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SystemTerm -> CharParser st SystemTerm)
-> SystemTerm -> CharParser st SystemTerm
forall a b. (a -> b) -> a -> b
$ Token -> Arguments -> SystemTerm
ST_System_Term Token
sf Arguments
a)
  CharParser st SystemTerm
-> CharParser st SystemTerm -> CharParser st SystemTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> SystemTerm)
-> CharParser st Token -> CharParser st SystemTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> SystemTerm
ST_System_Constant CharParser st Token
forall st. CharParser st Token
systemFunctor

{- THF:
<system_functor>     ::= <atomic_system_word> -}
systemFunctor :: CharParser st Token
systemFunctor :: CharParser st Token
systemFunctor = CharParser st Token
forall st. CharParser st Token
atomicSystemWord

{- THF & THF0:
<variable>           ::= <upper_word> -}
variable :: CharParser st Token
variable :: CharParser st Token
variable = CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken
  (do
    Char
u <- ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
upper
    [Char]
an <- ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT [Char] st Identity Char
-> ParsecT [Char] st Identity Char
-> ParsecT [Char] st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '_')
    CharParser st ()
forall st. CharParser st ()
skipAll
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
u Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
an)
   CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "Variable")

{- THF:
<arguments> ::= <term> | <term>,<arguments>
at least one term is neaded -}
arguments :: CharParser st Arguments
arguments :: CharParser st Arguments
arguments = ParsecT [Char] st Identity Term
-> ParsecT [Char] st Identity () -> CharParser st Arguments
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity Term
forall st. CharParser st Term
term ParsecT [Char] st Identity ()
forall st. CharParser st ()
comma

{- THF & THF0:
<principal_symbol>   :== <functor> | <variable> -}
principalSymbol :: CharParser st PrincipalSymbol
principalSymbol :: CharParser st PrincipalSymbol
principalSymbol = (Constant -> PrincipalSymbol)
-> ParsecT [Char] st Identity Constant
-> CharParser st PrincipalSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> PrincipalSymbol
PS_Functor ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
tptpFunctor
  CharParser st PrincipalSymbol
-> CharParser st PrincipalSymbol -> CharParser st PrincipalSymbol
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> PrincipalSymbol)
-> ParsecT [Char] st Identity Token
-> CharParser st PrincipalSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> PrincipalSymbol
PS_Variable ParsecT [Char] st Identity Token
forall st. CharParser st Token
variable

{- THF & THF0:
<source>           ::= <general_term>
<source>           :== <dag_source> | <internal_source> | <external_source> |
unknown | [<sources>]
<internal_source>  :== introduced(<intro_type><optional_info>)
<sources>          :== <source> | <source>,<sources> -}
source :: CharParser st Source
source :: CharParser st Source
source = (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "unknown") CharParser st () -> CharParser st Source -> CharParser st Source
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Source -> CharParser st Source
forall (m :: * -> *) a. Monad m => a -> m a
return Source
S_Unknown)
  CharParser st Source
-> CharParser st Source -> CharParser st Source
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (DagSource -> Source)
-> ParsecT [Char] st Identity DagSource -> CharParser st Source
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DagSource -> Source
S_Dag_Source ParsecT [Char] st Identity DagSource
forall st. CharParser st DagSource
dagSource
  CharParser st Source
-> CharParser st Source -> CharParser st Source
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ExternalSource -> Source)
-> ParsecT [Char] st Identity ExternalSource
-> CharParser st Source
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExternalSource -> Source
S_External_Source ParsecT [Char] st Identity ExternalSource
forall st. CharParser st ExternalSource
externalSource
  CharParser st Source
-> CharParser st Source -> CharParser st Source
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Source] -> Source)
-> ParsecT [Char] st Identity [Source] -> CharParser st Source
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Source] -> Source
S_Sources (CharParser st Source
-> CharParser st () -> ParsecT [Char] st Identity [Source]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 CharParser st Source
forall st. CharParser st Source
source CharParser st ()
forall st. CharParser st ()
comma)
  CharParser st Source
-> CharParser st Source -> CharParser st Source
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do -- internal_source
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "introduced"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    IntroType
it <- CharParser st IntroType
forall st. CharParser st IntroType
introType
    OptionalInfo
oi <- CharParser st OptionalInfo
forall st. CharParser st OptionalInfo
optionalInfo
    CharParser st ()
forall st. CharParser st ()
cParentheses
    Source -> CharParser st Source
forall (m :: * -> *) a. Monad m => a -> m a
return (Source -> CharParser st Source) -> Source -> CharParser st Source
forall a b. (a -> b) -> a -> b
$ IntroType -> OptionalInfo -> Source
S_Internal_Source IntroType
it OptionalInfo
oi

{- THF & THF0:
<dag_source>         :== <name> | <inference_record>
<inference_record>   :== inference(<inference_rule>,<useful_info>,
[<parent_list>])
<inference_rule>     :== <atomic_word>
<parent_list>        :== <parent_info> | <parent_info>,<parent_list> -}
dagSource :: CharParser st DagSource
dagSource :: CharParser st DagSource
dagSource = do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "inference")
    CharParser st ()
forall st. CharParser st ()
oParentheses
    Constant
ir <- CharParser st Constant
forall st. CharParser st Constant
atomicWord
    CharParser st ()
forall st. CharParser st ()
comma
    UsefulInfo
ui <- CharParser st UsefulInfo
forall st. CharParser st UsefulInfo
usefulInfo
    CharParser st ()
forall st. CharParser st ()
comma
    [ParentInfo]
pl <- CharParser st [ParentInfo] -> CharParser st [ParentInfo]
forall st a. CharParser st a -> CharParser st a
brackets (ParsecT [Char] st Identity ParentInfo
-> CharParser st () -> CharParser st [ParentInfo]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity ParentInfo
forall st. CharParser st ParentInfo
parentInfo CharParser st ()
forall st. CharParser st ()
comma)
    CharParser st ()
forall st. CharParser st ()
cParentheses
    DagSource -> CharParser st DagSource
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> UsefulInfo -> [ParentInfo] -> DagSource
DS_Inference_Record Constant
ir UsefulInfo
ui [ParentInfo]
pl)
  CharParser st DagSource
-> CharParser st DagSource -> CharParser st DagSource
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Name -> DagSource)
-> ParsecT [Char] st Identity Name -> CharParser st DagSource
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> DagSource
DS_Name ParsecT [Char] st Identity Name
forall st. CharParser st Name
name

{- THF & THF0:
<parent_info>        :== <source><parent_details>
<parent_details>     :== :<general_list> | <null> -}
parentInfo :: CharParser st ParentInfo
parentInfo :: CharParser st ParentInfo
parentInfo = do
    Source
s <- CharParser st Source
forall st. CharParser st Source
source
    Maybe GeneralList
pd <- CharParser st (Maybe GeneralList)
forall st. CharParser st (Maybe GeneralList)
parentDetails
    ParentInfo -> CharParser st ParentInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ParentInfo -> CharParser st ParentInfo)
-> ParentInfo -> CharParser st ParentInfo
forall a b. (a -> b) -> a -> b
$ Source -> Maybe GeneralList -> ParentInfo
PI_Parent_Info Source
s Maybe GeneralList
pd


parentDetails :: CharParser st (Maybe GeneralList)
parentDetails :: CharParser st (Maybe GeneralList)
parentDetails = (GeneralList -> Maybe GeneralList)
-> ParsecT [Char] st Identity GeneralList
-> CharParser st (Maybe GeneralList)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GeneralList -> Maybe GeneralList
forall a. a -> Maybe a
Just (CharParser st ()
forall st. CharParser st ()
colon CharParser st ()
-> ParsecT [Char] st Identity GeneralList
-> ParsecT [Char] st Identity GeneralList
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity GeneralList
forall st. CharParser st GeneralList
generalList)
  CharParser st (Maybe GeneralList)
-> CharParser st (Maybe GeneralList)
-> CharParser st (Maybe GeneralList)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT [Char] st Identity Char -> CharParser st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ':') CharParser st ()
-> CharParser st (Maybe GeneralList)
-> CharParser st (Maybe GeneralList)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe GeneralList -> CharParser st (Maybe GeneralList)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe GeneralList
forall a. Maybe a
Nothing)

{- THF & THF0:
<intro_type>     :== definition | axiom_of_choice | tautology | assumption -}
introType :: CharParser st IntroType
introType :: CharParser st IntroType
introType = (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "definition") CharParser st ()
-> CharParser st IntroType -> CharParser st IntroType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IntroType -> CharParser st IntroType
forall (m :: * -> *) a. Monad m => a -> m a
return IntroType
IT_definition)
  CharParser st IntroType
-> CharParser st IntroType -> CharParser st IntroType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "axiom_of_choice") CharParser st ()
-> CharParser st IntroType -> CharParser st IntroType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IntroType -> CharParser st IntroType
forall (m :: * -> *) a. Monad m => a -> m a
return IntroType
IT_axiom_of_choice)
  CharParser st IntroType
-> CharParser st IntroType -> CharParser st IntroType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "tautology") CharParser st ()
-> CharParser st IntroType -> CharParser st IntroType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IntroType -> CharParser st IntroType
forall (m :: * -> *) a. Monad m => a -> m a
return IntroType
IT_tautology)
  CharParser st IntroType
-> CharParser st IntroType -> CharParser st IntroType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "assumption") CharParser st ()
-> CharParser st IntroType -> CharParser st IntroType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IntroType -> CharParser st IntroType
forall (m :: * -> *) a. Monad m => a -> m a
return IntroType
IT_assumption)

{- THF & THF0:
<external_source>    :== <file_source> | <theory> | <creator_source>
<theory>             :== theory(<theory_name><optional_info>)
<creator_source>     :== creator(<creator_name><optional_info>)
<creator_name>       :== <atomic_word> -}
externalSource :: CharParser st ExternalSource
externalSource :: CharParser st ExternalSource
externalSource = (FileSource -> ExternalSource)
-> ParsecT [Char] st Identity FileSource
-> CharParser st ExternalSource
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FileSource -> ExternalSource
ES_File_Source ParsecT [Char] st Identity FileSource
forall st. CharParser st FileSource
fileSource
  CharParser st ExternalSource
-> CharParser st ExternalSource -> CharParser st ExternalSource
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "theory"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    TheoryName
tn <- CharParser st TheoryName
forall st. CharParser st TheoryName
theoryName
    OptionalInfo
oi <- CharParser st OptionalInfo
forall st. CharParser st OptionalInfo
optionalInfo
    CharParser st ()
forall st. CharParser st ()
cParentheses
    ExternalSource -> CharParser st ExternalSource
forall (m :: * -> *) a. Monad m => a -> m a
return (ExternalSource -> CharParser st ExternalSource)
-> ExternalSource -> CharParser st ExternalSource
forall a b. (a -> b) -> a -> b
$ TheoryName -> OptionalInfo -> ExternalSource
ES_Theory TheoryName
tn OptionalInfo
oi
  CharParser st ExternalSource
-> CharParser st ExternalSource -> CharParser st ExternalSource
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "creator"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    Constant
cn <- CharParser st Constant
forall st. CharParser st Constant
atomicWord
    OptionalInfo
oi <- CharParser st OptionalInfo
forall st. CharParser st OptionalInfo
optionalInfo
    CharParser st ()
forall st. CharParser st ()
cParentheses
    ExternalSource -> CharParser st ExternalSource
forall (m :: * -> *) a. Monad m => a -> m a
return (ExternalSource -> CharParser st ExternalSource)
-> ExternalSource -> CharParser st ExternalSource
forall a b. (a -> b) -> a -> b
$ Constant -> OptionalInfo -> ExternalSource
ES_Creator_Source Constant
cn OptionalInfo
oi

{- THF & THF0:
<file_source>        :== file(<file_name><file_info>)
<file_info>          :== ,<name> | <null> -}
fileSource :: CharParser st FileSource
fileSource :: CharParser st FileSource
fileSource = do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "file"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    Token
fn <- CharParser st Token
forall st. CharParser st Token
fileName
    Maybe Name
fi <- CharParser st (Maybe Name)
forall st. CharParser st (Maybe Name)
fileInfo
    CharParser st ()
forall st. CharParser st ()
cParentheses
    FileSource -> CharParser st FileSource
forall (m :: * -> *) a. Monad m => a -> m a
return (FileSource -> CharParser st FileSource)
-> FileSource -> CharParser st FileSource
forall a b. (a -> b) -> a -> b
$ Token -> Maybe Name -> FileSource
FS_File Token
fn Maybe Name
fi


fileInfo :: CharParser st (Maybe Name)
fileInfo :: CharParser st (Maybe Name)
fileInfo = (Name -> Maybe Name)
-> ParsecT [Char] st Identity Name -> CharParser st (Maybe Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Maybe Name
forall a. a -> Maybe a
Just (CharParser st ()
forall st. CharParser st ()
comma CharParser st ()
-> ParsecT [Char] st Identity Name
-> ParsecT [Char] st Identity Name
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity Name
forall st. CharParser st Name
name)
  CharParser st (Maybe Name)
-> CharParser st (Maybe Name) -> CharParser st (Maybe Name)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT [Char] st Identity Char -> CharParser st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ',') CharParser st ()
-> CharParser st (Maybe Name) -> CharParser st (Maybe Name)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Name -> CharParser st (Maybe Name)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
forall a. Maybe a
Nothing)

{- THF & THF0:
<theory_name>        :== equality | ac -}
theoryName :: CharParser st TheoryName
theoryName :: CharParser st TheoryName
theoryName = (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "equality") CharParser st ()
-> CharParser st TheoryName -> CharParser st TheoryName
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TheoryName -> CharParser st TheoryName
forall (m :: * -> *) a. Monad m => a -> m a
return TheoryName
Equality)
  CharParser st TheoryName
-> CharParser st TheoryName -> CharParser st TheoryName
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "ac") CharParser st ()
-> CharParser st TheoryName -> CharParser st TheoryName
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TheoryName -> CharParser st TheoryName
forall (m :: * -> *) a. Monad m => a -> m a
return TheoryName
Ac)

{- THF & THF0:
<optional_info>      ::= ,<useful_info> | <null> -}
optionalInfo :: CharParser st OptionalInfo
optionalInfo :: CharParser st OptionalInfo
optionalInfo = (UsefulInfo -> OptionalInfo)
-> ParsecT [Char] st Identity UsefulInfo
-> CharParser st OptionalInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UsefulInfo -> OptionalInfo
forall a. a -> Maybe a
Just (CharParser st ()
forall st. CharParser st ()
comma CharParser st ()
-> ParsecT [Char] st Identity UsefulInfo
-> ParsecT [Char] st Identity UsefulInfo
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity UsefulInfo
forall st. CharParser st UsefulInfo
usefulInfo)
  CharParser st OptionalInfo
-> CharParser st OptionalInfo -> CharParser st OptionalInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT [Char] st Identity Char -> CharParser st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ',') CharParser st ()
-> CharParser st OptionalInfo -> CharParser st OptionalInfo
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OptionalInfo -> CharParser st OptionalInfo
forall (m :: * -> *) a. Monad m => a -> m a
return OptionalInfo
forall a. Maybe a
Nothing)

{- THF & THF0:
<useful_info>        ::= <general_list>
<useful_info>        :== [] | [<info_items>]
<info_items>         :== <info_item> | <info_item>,<info_items> -}
usefulInfo :: CharParser st UsefulInfo
usefulInfo :: CharParser st UsefulInfo
usefulInfo = (CharParser st ()
forall st. CharParser st ()
oBracket CharParser st () -> CharParser st () -> CharParser st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser st ()
forall st. CharParser st ()
cBracket CharParser st ()
-> CharParser st UsefulInfo -> CharParser st UsefulInfo
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> UsefulInfo -> CharParser st UsefulInfo
forall (m :: * -> *) a. Monad m => a -> m a
return [])
  CharParser st UsefulInfo
-> CharParser st UsefulInfo -> CharParser st UsefulInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st UsefulInfo -> CharParser st UsefulInfo
forall st a. CharParser st a -> CharParser st a
brackets (ParsecT [Char] st Identity InfoItem
-> CharParser st () -> CharParser st UsefulInfo
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity InfoItem
forall st. CharParser st InfoItem
infoItem CharParser st ()
forall st. CharParser st ()
comma)

{- THF & THF0:
<info_item>          :== <formula_item> | <inference_item> |
<general_function> -}
infoItem :: CharParser st InfoItem
infoItem :: CharParser st InfoItem
infoItem = (FormulaItem -> InfoItem)
-> ParsecT [Char] st Identity FormulaItem -> CharParser st InfoItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FormulaItem -> InfoItem
II_Formula_Item ParsecT [Char] st Identity FormulaItem
forall st. CharParser st FormulaItem
formulaItem
  CharParser st InfoItem
-> CharParser st InfoItem -> CharParser st InfoItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (InferenceItem -> InfoItem)
-> ParsecT [Char] st Identity InferenceItem
-> CharParser st InfoItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap InferenceItem -> InfoItem
II_Inference_Item ParsecT [Char] st Identity InferenceItem
forall st. CharParser st InferenceItem
inferenceItem
  CharParser st InfoItem
-> CharParser st InfoItem -> CharParser st InfoItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (GeneralFunction -> InfoItem)
-> ParsecT [Char] st Identity GeneralFunction
-> CharParser st InfoItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GeneralFunction -> InfoItem
II_General_Function ParsecT [Char] st Identity GeneralFunction
forall st. CharParser st GeneralFunction
generalFunction

{- THF & THF0:
<formula_item>       :== <description_item> | <iquote_item>
<description_item>   :== description(<atomic_word>)
<iquote_item>        :== iquote(<atomic_word>) -}
formulaItem :: CharParser st FormulaItem
formulaItem :: CharParser st FormulaItem
formulaItem = do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "description"
    (Constant -> FormulaItem)
-> ParsecT [Char] st Identity Constant -> CharParser st FormulaItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> FormulaItem
FI_Description_Item (ParsecT [Char] st Identity Constant
-> ParsecT [Char] st Identity Constant
forall st a. CharParser st a -> CharParser st a
parentheses ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
atomicWord)
  CharParser st FormulaItem
-> CharParser st FormulaItem -> CharParser st FormulaItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "iquote"
    (Constant -> FormulaItem)
-> ParsecT [Char] st Identity Constant -> CharParser st FormulaItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> FormulaItem
FI_Iquote_Item (ParsecT [Char] st Identity Constant
-> ParsecT [Char] st Identity Constant
forall st a. CharParser st a -> CharParser st a
parentheses ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
atomicWord)

{- THF & THF0:
<inference_item>     :== <inference_status> | <assumptions_record> |
<new_symbol_record> | <refutation>
<assumptions_record> :== assumptions([<name_list>])
<refutation>         :== refutation(<file_source>)
<new_symbol_record>  :== new_symbols(<atomic_word>,[<new_symbol_list>])
<new_symbol_list>    :== <principal_symbol> |
<principal_symbol>,<new_symbol_list> -}
inferenceItem :: CharParser st InferenceItem
inferenceItem :: CharParser st InferenceItem
inferenceItem = (InferenceStatus -> InferenceItem)
-> ParsecT [Char] st Identity InferenceStatus
-> CharParser st InferenceItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap InferenceStatus -> InferenceItem
II_Inference_Status ParsecT [Char] st Identity InferenceStatus
forall st. CharParser st InferenceStatus
inferenceStatus
  CharParser st InferenceItem
-> CharParser st InferenceItem -> CharParser st InferenceItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "assumptions"
    (NameList -> InferenceItem)
-> ParsecT [Char] st Identity NameList
-> CharParser st InferenceItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameList -> InferenceItem
II_Assumptions_Record (ParsecT [Char] st Identity NameList
-> ParsecT [Char] st Identity NameList
forall st a. CharParser st a -> CharParser st a
parentheses (ParsecT [Char] st Identity NameList
-> ParsecT [Char] st Identity NameList
forall st a. CharParser st a -> CharParser st a
brackets ParsecT [Char] st Identity NameList
forall st. CharParser st NameList
nameList))
  CharParser st InferenceItem
-> CharParser st InferenceItem -> CharParser st InferenceItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "new_symbols"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    Constant
aw <- CharParser st Constant
forall st. CharParser st Constant
atomicWord
    CharParser st ()
forall st. CharParser st ()
comma
    [PrincipalSymbol]
nsl <- CharParser st [PrincipalSymbol] -> CharParser st [PrincipalSymbol]
forall st a. CharParser st a -> CharParser st a
brackets (ParsecT [Char] st Identity PrincipalSymbol
-> CharParser st () -> CharParser st [PrincipalSymbol]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity PrincipalSymbol
forall st. CharParser st PrincipalSymbol
principalSymbol CharParser st ()
forall st. CharParser st ()
comma)
    CharParser st ()
forall st. CharParser st ()
cParentheses
    InferenceItem -> CharParser st InferenceItem
forall (m :: * -> *) a. Monad m => a -> m a
return (InferenceItem -> CharParser st InferenceItem)
-> InferenceItem -> CharParser st InferenceItem
forall a b. (a -> b) -> a -> b
$ Constant -> [PrincipalSymbol] -> InferenceItem
II_New_Symbol_Record Constant
aw [PrincipalSymbol]
nsl
  CharParser st InferenceItem
-> CharParser st InferenceItem -> CharParser st InferenceItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "refutation"
    (FileSource -> InferenceItem)
-> ParsecT [Char] st Identity FileSource
-> CharParser st InferenceItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FileSource -> InferenceItem
II_Refutation (ParsecT [Char] st Identity FileSource
-> ParsecT [Char] st Identity FileSource
forall st a. CharParser st a -> CharParser st a
parentheses ParsecT [Char] st Identity FileSource
forall st. CharParser st FileSource
fileSource)

{- THF & THF0:
<inference_status>   :== status(<status_value>) | <inference_info>
<inference_info>     :== <inference_rule>(<atomic_word>,<general_list>)
<inference_rule>     :== <atomic_word> -}
inferenceStatus :: CharParser st InferenceStatus
inferenceStatus :: CharParser st InferenceStatus
inferenceStatus = do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "status"
    (StatusValue -> InferenceStatus)
-> ParsecT [Char] st Identity StatusValue
-> CharParser st InferenceStatus
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap StatusValue -> InferenceStatus
IS_Status (ParsecT [Char] st Identity StatusValue
-> ParsecT [Char] st Identity StatusValue
forall st a. CharParser st a -> CharParser st a
parentheses ParsecT [Char] st Identity StatusValue
forall st. CharParser st StatusValue
statusValue)
  CharParser st InferenceStatus
-> CharParser st InferenceStatus -> CharParser st InferenceStatus
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Constant
ir <- GenParser Char st Constant -> GenParser Char st Constant
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Constant
forall st. CharParser st Constant
atomicWord GenParser Char st Constant
-> CharParser st () -> GenParser Char st Constant
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser st ()
forall st. CharParser st ()
oParentheses)
    Constant
aw <- GenParser Char st Constant
forall st. CharParser st Constant
atomicWord
    CharParser st ()
forall st. CharParser st ()
comma
    GeneralList
gl <- CharParser st GeneralList
forall st. CharParser st GeneralList
generalList
    CharParser st ()
forall st. CharParser st ()
cParentheses
    InferenceStatus -> CharParser st InferenceStatus
forall (m :: * -> *) a. Monad m => a -> m a
return (InferenceStatus -> CharParser st InferenceStatus)
-> InferenceStatus -> CharParser st InferenceStatus
forall a b. (a -> b) -> a -> b
$ Constant -> Constant -> GeneralList -> InferenceStatus
IS_Inference_Info Constant
ir Constant
aw GeneralList
gl

{- THF & THF0:
<status_value>   :== suc | unp | sap | esa | sat | fsa | thm | eqv | tac |
wec | eth | tau | wtc | wth | cax | sca | tca | wca |
cup | csp | ecs | csa | cth | ceq | unc | wcc | ect |
fun | uns | wuc | wct | scc | uca | noc -}
statusValue :: CharParser st StatusValue
statusValue :: CharParser st StatusValue
statusValue = [CharParser st StatusValue] -> CharParser st StatusValue
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([CharParser st StatusValue] -> CharParser st StatusValue)
-> [CharParser st StatusValue] -> CharParser st StatusValue
forall a b. (a -> b) -> a -> b
$ (StatusValue -> CharParser st StatusValue)
-> [StatusValue] -> [CharParser st StatusValue]
forall a b. (a -> b) -> [a] -> [b]
map (\ r :: StatusValue
r -> CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString ([Char] -> CharParser st [Char]) -> [Char] -> CharParser st [Char]
forall a b. (a -> b) -> a -> b
$ StatusValue -> [Char]
showStatusValue StatusValue
r)
                            CharParser st ()
-> CharParser st StatusValue -> CharParser st StatusValue
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StatusValue -> CharParser st StatusValue
forall (m :: * -> *) a. Monad m => a -> m a
return StatusValue
r) [StatusValue]
allStatusValues

allStatusValues :: [StatusValue]
allStatusValues :: [StatusValue]
allStatusValues =
  [StatusValue
Suc, StatusValue
Unp, StatusValue
Sap, StatusValue
Esa, StatusValue
Sat, StatusValue
Fsa, StatusValue
Thm, StatusValue
Eqv, StatusValue
Tac,
   StatusValue
Wec, StatusValue
Eth, StatusValue
Tau, StatusValue
Wtc, StatusValue
Wth, StatusValue
Cax, StatusValue
Sca, StatusValue
Tca, StatusValue
Wca,
   StatusValue
Cup, StatusValue
Csp, StatusValue
Ecs, StatusValue
Csa, StatusValue
Cth, StatusValue
Ceq, StatusValue
Unc, StatusValue
Wcc, StatusValue
Ect,
   StatusValue
Fun, StatusValue
Uns, StatusValue
Wuc, StatusValue
Wct, StatusValue
Scc, StatusValue
Uca, StatusValue
Noc]

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

formulaSelection :: CharParser st (Maybe NameList)
formulaSelection :: CharParser st (Maybe NameList)
formulaSelection = (NameList -> Maybe NameList)
-> ParsecT [Char] st Identity NameList
-> CharParser st (Maybe NameList)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameList -> Maybe NameList
forall a. a -> Maybe a
Just (CharParser st ()
forall st. CharParser st ()
comma CharParser st ()
-> ParsecT [Char] st Identity NameList
-> ParsecT [Char] st Identity NameList
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] st Identity NameList
-> ParsecT [Char] st Identity NameList
forall st a. CharParser st a -> CharParser st a
brackets ParsecT [Char] st Identity NameList
forall st. CharParser st NameList
nameList)
  CharParser st (Maybe NameList)
-> CharParser st (Maybe NameList) -> CharParser st (Maybe NameList)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT [Char] st Identity Char -> CharParser st ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ',') CharParser st ()
-> CharParser st (Maybe NameList) -> CharParser st (Maybe NameList)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe NameList -> CharParser st (Maybe NameList)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe NameList
forall a. Maybe a
Nothing)

{- THF & THF0:
<name_list>          ::= <name> | <name>,<name_list>
the list must mot be empty -}
nameList :: CharParser st NameList
nameList :: CharParser st NameList
nameList = ParsecT [Char] st Identity Name
-> ParsecT [Char] st Identity () -> CharParser st NameList
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity Name
forall st. CharParser st Name
name ParsecT [Char] st Identity ()
forall st. CharParser st ()
comma

{- THF & THF0:
<general_term>       ::= <general_data> | <general_data>:<general_term> |
<general_list> -}
generalTerm :: CharParser st GeneralTerm
generalTerm :: CharParser st GeneralTerm
generalTerm = do
    GeneralData
gd <- GenParser Char st GeneralData -> GenParser Char st GeneralData
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st GeneralData
forall st. CharParser st GeneralData
generalData GenParser Char st GeneralData
-> ParsecT [Char] st Identity () -> GenParser Char st GeneralData
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity Char -> ParsecT [Char] st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ':'))
    GeneralTerm -> CharParser st GeneralTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (GeneralTerm -> CharParser st GeneralTerm)
-> GeneralTerm -> CharParser st GeneralTerm
forall a b. (a -> b) -> a -> b
$ GeneralData -> GeneralTerm
GT_General_Data GeneralData
gd
  CharParser st GeneralTerm
-> CharParser st GeneralTerm -> CharParser st GeneralTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    GeneralData
gd <- GenParser Char st GeneralData -> GenParser Char st GeneralData
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st GeneralData
forall st. CharParser st GeneralData
generalData GenParser Char st GeneralData
-> ParsecT [Char] st Identity () -> GenParser Char st GeneralData
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
colon)
    GeneralTerm
gt <- CharParser st GeneralTerm
forall st. CharParser st GeneralTerm
generalTerm
    GeneralTerm -> CharParser st GeneralTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (GeneralTerm -> CharParser st GeneralTerm)
-> GeneralTerm -> CharParser st GeneralTerm
forall a b. (a -> b) -> a -> b
$ GeneralData -> GeneralTerm -> GeneralTerm
GT_General_Data_Term GeneralData
gd GeneralTerm
gt
  CharParser st GeneralTerm
-> CharParser st GeneralTerm -> CharParser st GeneralTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (GeneralList -> GeneralTerm)
-> ParsecT [Char] st Identity GeneralList
-> CharParser st GeneralTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GeneralList -> GeneralTerm
GT_General_List ParsecT [Char] st Identity GeneralList
forall st. CharParser st GeneralList
generalList

{- THF & THF0:
<general_data>       ::= <atomic_word> | <general_function> |
<variable> | <number> | <distinct_object> |
<formula_data>
<general_data>       :== bind(<variable>,<formula_data>) -}
generalData :: CharParser st GeneralData
generalData :: CharParser st GeneralData
generalData = (Token -> GeneralData)
-> ParsecT [Char] st Identity Token -> CharParser st GeneralData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> GeneralData
GD_Variable ParsecT [Char] st Identity Token
forall st. CharParser st Token
variable
  CharParser st GeneralData
-> CharParser st GeneralData -> CharParser st GeneralData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Number -> GeneralData)
-> ParsecT [Char] st Identity Number -> CharParser st GeneralData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Number -> GeneralData
GD_Number ParsecT [Char] st Identity Number
forall st. CharParser st Number
number
  CharParser st GeneralData
-> CharParser st GeneralData -> CharParser st GeneralData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> GeneralData)
-> ParsecT [Char] st Identity Token -> CharParser st GeneralData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> GeneralData
GD_Distinct_Object ParsecT [Char] st Identity Token
forall st. CharParser st Token
distinctObject
  CharParser st GeneralData
-> CharParser st GeneralData -> CharParser st GeneralData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "bind"
    CharParser st ()
forall st. CharParser st ()
oParentheses
    Token
v <- ParsecT [Char] st Identity Token
forall st. CharParser st Token
variable
    CharParser st ()
forall st. CharParser st ()
comma
    FormulaData
fd <- CharParser st FormulaData
forall st. CharParser st FormulaData
formulaData
    CharParser st ()
forall st. CharParser st ()
cParentheses
    GeneralData -> CharParser st GeneralData
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> FormulaData -> GeneralData
GD_Bind Token
v FormulaData
fd)
  CharParser st GeneralData
-> CharParser st GeneralData -> CharParser st GeneralData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (GeneralFunction -> GeneralData)
-> ParsecT [Char] st Identity GeneralFunction
-> CharParser st GeneralData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GeneralFunction -> GeneralData
GD_General_Function ParsecT [Char] st Identity GeneralFunction
forall st. CharParser st GeneralFunction
generalFunction
  CharParser st GeneralData
-> CharParser st GeneralData -> CharParser st GeneralData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Constant -> GeneralData)
-> ParsecT [Char] st Identity Constant -> CharParser st GeneralData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> GeneralData
GD_Atomic_Word ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
atomicWord
  CharParser st GeneralData
-> CharParser st GeneralData -> CharParser st GeneralData
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (FormulaData -> GeneralData)
-> CharParser st FormulaData -> CharParser st GeneralData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FormulaData -> GeneralData
GD_Formula_Data CharParser st FormulaData
forall st. CharParser st FormulaData
formulaData

{- THF & THF0:
<general_function>   ::= <atomic_word>(<general_terms>)
general_terms must not be empty -}
generalFunction :: CharParser st GeneralFunction
generalFunction :: CharParser st GeneralFunction
generalFunction = do
    Constant
aw <- CharParser st Constant
forall st. CharParser st Constant
atomicWord
    GeneralList
gts <- CharParser st GeneralList -> CharParser st GeneralList
forall st a. CharParser st a -> CharParser st a
parentheses CharParser st GeneralList
forall st. CharParser st GeneralList
generalTerms
    GeneralFunction -> CharParser st GeneralFunction
forall (m :: * -> *) a. Monad m => a -> m a
return (GeneralFunction -> CharParser st GeneralFunction)
-> GeneralFunction -> CharParser st GeneralFunction
forall a b. (a -> b) -> a -> b
$ Constant -> GeneralList -> GeneralFunction
GF_General_Function Constant
aw GeneralList
gts

{- THF & THF0:
<formula_data>       ::= $thf(<thf_formula>) | $tff(<tff_formula>) |
fof(<fof_formula>) | $cnf(<cnf_formula>) |
fot(<term>)
only thf is used here -}
formulaData :: CharParser st FormulaData
formulaData :: CharParser st FormulaData
formulaData = (THFFormula -> FormulaData)
-> ParsecT [Char] st Identity THFFormula
-> CharParser st FormulaData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap THFFormula -> FormulaData
THF_Formula ParsecT [Char] st Identity THFFormula
forall st. CharParser st THFFormula
thfFormula

{- THF & THF0:
<general_list>       ::= [] | [<general_terms>] -}
generalList :: CharParser st GeneralList
generalList :: CharParser st GeneralList
generalList = (GenParser Char st () -> GenParser Char st ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st ()
forall st. CharParser st ()
oBracket GenParser Char st ()
-> GenParser Char st () -> GenParser Char st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char st ()
forall st. CharParser st ()
cBracket) GenParser Char st ()
-> CharParser st GeneralList -> CharParser st GeneralList
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GeneralList -> CharParser st GeneralList
forall (m :: * -> *) a. Monad m => a -> m a
return [])
  CharParser st GeneralList
-> CharParser st GeneralList -> CharParser st GeneralList
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st GeneralList -> CharParser st GeneralList
forall st a. CharParser st a -> CharParser st a
brackets CharParser st GeneralList
forall st. CharParser st GeneralList
generalTerms

{- THF & THF0:
<general_terms>      ::= <general_term> | <general_term>,<general_terms> -}
generalTerms :: CharParser st [GeneralTerm]
generalTerms :: CharParser st GeneralList
generalTerms = ParsecT [Char] st Identity GeneralTerm
-> ParsecT [Char] st Identity () -> CharParser st GeneralList
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT [Char] st Identity GeneralTerm
forall st. CharParser st GeneralTerm
generalTerm ParsecT [Char] st Identity ()
forall st. CharParser st ()
comma

{- THF:
<name>               ::= <atomic_word> | <integer>
THF0:
<name>               ::= <atomic_word> | <unsigned_integer> -}
name :: CharParser st Name
name :: CharParser st Name
name = (Token -> Name)
-> ParsecT [Char] st Identity Token -> CharParser st Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Name
T0N_Unsigned_Integer (CharParser st [Char] -> ParsecT [Char] st Identity Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char]
forall st. CharParser st [Char]
unsignedInteger CharParser st [Char]
-> ParsecT [Char] st Identity () -> CharParser st [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
skipAll))
  -- added for thf0
  CharParser st Name -> CharParser st Name -> CharParser st Name
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> Name)
-> ParsecT [Char] st Identity Token -> CharParser st Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Name
N_Integer (ParsecT [Char] st Identity Token
forall st. CharParser st Token
integer ParsecT [Char] st Identity Token
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
skipAll)
  CharParser st Name -> CharParser st Name -> CharParser st Name
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Constant -> Name)
-> ParsecT [Char] st Identity Constant -> CharParser st Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constant -> Name
N_Atomic_Word ParsecT [Char] st Identity Constant
forall st. CharParser st Constant
atomicWord

{- THF & THF0:
<atomic_word>        ::= <lower_word> | <single_quoted> -}
atomicWord :: CharParser st AtomicWord
atomicWord :: CharParser st Constant
atomicWord = (Token -> Constant)
-> ParsecT [Char] st Identity Token -> CharParser st Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Constant
A_Lower_Word ParsecT [Char] st Identity Token
forall st. CharParser st Token
lowerWord
  CharParser st Constant
-> CharParser st Constant -> CharParser st Constant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> Constant)
-> ParsecT [Char] st Identity Token -> CharParser st Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Constant
A_Single_Quoted ParsecT [Char] st Identity Token
forall st. CharParser st Token
singleQuoted
  CharParser st Constant -> [Char] -> CharParser st Constant
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "lowerWord or singleQuoted"

{- THF & THF0:
<atomic_defined_word> ::= <dollar_word> -}
atomicDefinedWord :: CharParser st Token
atomicDefinedWord :: CharParser st Token
atomicDefinedWord = Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '$' ParsecT [Char] st Identity Char
-> CharParser st Token -> CharParser st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser st Token
forall st. CharParser st Token
lowerWord

{- THF & THF0:
<atomic_system_word> ::= <dollar_dollar_word>
<dollar_dollar_word> ::- <dollar><dollar><lower_word>
<dollar>             ::: [$] -}
atomicSystemWord :: CharParser st Token
atomicSystemWord :: CharParser st Token
atomicSystemWord = [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "$$" CharParser st [Char] -> CharParser st Token -> CharParser st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser st Token
forall st. CharParser st Token
lowerWord

{- THF & THF0:
<number> ::= <integer> | <rational> | <real>
<real>               ::- (<signed_real>|<unsigned_real>)
<signed_real>        ::- <sign><unsigned_real>
<unsigned_real>      ::- (<decimal_fraction>|<decimal_exponent>)
<rational>           ::- (<signed_rational>|<unsigned_rational>)
<signed_rational>    ::- <sign><unsigned_rational>
<unsigned_rational>  ::- <decimal><slash><positive_decimal>
<integer>            ::- (<signed_integer>|<unsigned_integer>)
<signed_integer>     ::- <sign><unsigned_integer>
<unsigned_integer>   ::- <decimal>
<decimal>            ::- (<zero_numeric>|<positive_decimal>)
<positive_decimal>   ::- <non_zero_numeric><numeric>*
<decimal_exponent>   ::- (<decimal>|<decimal_fraction>)<exponent><decimal>
<decimal_fraction>   ::- <decimal><dot_decimal>
<dot_decimal>        ::- <dot><numeric><numeric>*
<sign>               ::: [+-]
<dot>                ::: [.]
<exponent>           ::: [Ee]
<slash>              ::: [/]
<zero_numeric>       ::: [0]
<non_zero_numeric>   ::: [1-9]
<numeric>            ::: [0-9] -}
number :: CharParser st Number
number :: CharParser st Number
number = (Token -> Number)
-> ParsecT [Char] st Identity Token -> CharParser st Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Number
Num_Real (ParsecT [Char] st Identity Token
forall st. CharParser st Token
real ParsecT [Char] st Identity Token
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
skipAll)
  CharParser st Number
-> CharParser st Number -> CharParser st Number
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> Number)
-> ParsecT [Char] st Identity Token -> CharParser st Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Number
Num_Rational (ParsecT [Char] st Identity Token
forall st. CharParser st Token
rational ParsecT [Char] st Identity Token
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
skipAll)
  CharParser st Number
-> CharParser st Number -> CharParser st Number
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> Number)
-> ParsecT [Char] st Identity Token -> CharParser st Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Number
Num_Integer (ParsecT [Char] st Identity Token
forall st. CharParser st Token
integer ParsecT [Char] st Identity Token
-> ParsecT [Char] st Identity ()
-> ParsecT [Char] st Identity Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity ()
forall st. CharParser st ()
skipAll)

{- THF & THF0:
<file_name>          ::= <single_quoted> -}
fileName :: CharParser st Token
fileName :: CharParser st Token
fileName = CharParser st Token
forall st. CharParser st Token
singleQuoted

{- THF & THF0:
<single_quoted>      ::- <single_quote><sq_char><sq_char>*<single_quote>
<single_quote>       ::: [']
<sq_char>            ::: ([\40-\46\50-\133\135-\176]|[\\]['\\]) -}
singleQuoted :: CharParser st Token
singleQuoted :: CharParser st Token
singleQuoted = CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st Token)
-> CharParser st [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ do
    Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '\''
    [Char]
s <- ([[Char]] -> [Char])
-> ParsecT [Char] st Identity [[Char]] -> CharParser st [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (ParsecT [Char] st Identity [[Char]] -> CharParser st [Char])
-> ParsecT [Char] st Identity [[Char]] -> CharParser st [Char]
forall a b. (a -> b) -> a -> b
$ CharParser st [Char] -> ParsecT [Char] st Identity [[Char]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "\\\\" CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "\\'"
        CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "\\\'"
        CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity Char -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => m a -> m [a]
single ( (Char -> Bool) -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (\ c :: Char
c -> Char -> Bool
printable Char
c Bool -> Bool -> Bool
&& Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Char
c "'\\")))
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '\''
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
s

{- THF & THF0:
<distinct_object> ::- <double_quote><do_char>*<double_quote>
<do_char> ::: ([\40-\41\43-\133\135-\176]|[\\]["\\])
<double_quote> ::: ["] -}
distinctObject :: CharParser st Token
distinctObject :: CharParser st Token
distinctObject = CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st Token)
-> CharParser st [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ do
    Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '\"'
    [Char]
s <- ([[Char]] -> [Char])
-> ParsecT [Char] st Identity [[Char]] -> CharParser st [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (ParsecT [Char] st Identity [[Char]] -> CharParser st [Char])
-> ParsecT [Char] st Identity [[Char]] -> CharParser st [Char]
forall a b. (a -> b) -> a -> b
$ CharParser st [Char] -> ParsecT [Char] st Identity [[Char]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ([Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "\\\\" CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
tryString "\\\""
        CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity Char -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => m a -> m [a]
single ( (Char -> Bool) -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (\ c :: Char
c -> Char -> Bool
printable Char
c Bool -> Bool -> Bool
&& Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Char
c "\"\\")))
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '\"'
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
s

{- THF & THF0:
<lower_word>         ::- <lower_alpha><alpha_numeric>*
<alpha_numeric>      ::: (<lower_alpha>|<upper_alpha>|<numeric>|[_])
<lower_alpha>        ::: [a-z]
<upper_alpha>        ::: [A-Z]
<numeric>            ::: [0-9] -}
lowerWord :: CharParser st Token
lowerWord :: CharParser st Token
lowerWord = CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (do
    Char
l <- ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
lower
    [Char]
an <- ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT [Char] st Identity Char
-> ParsecT [Char] st Identity Char
-> ParsecT [Char] st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '_')
    CharParser st ()
forall st. CharParser st ()
skipAll
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
l Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
an)
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "alphanumeric word with leading lowercase letter")

printableChar :: CharParser st Char
printableChar :: CharParser st Char
printableChar = (Char -> Bool) -> CharParser st Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy Char -> Bool
printable

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

-- Numbers
real :: CharParser st Token
real :: CharParser st Token
real = CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    Char
s <- [Char] -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf "-+"
    [Char]
ur <- CharParser st [Char]
forall st. CharParser st [Char]
unsignedReal
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
s Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
ur))
  CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
unsignedReal
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "(signed) real")

unsignedReal :: CharParser st String
unsignedReal :: CharParser st [Char]
unsignedReal = do
    [Char]
de <- CharParser st [Char] -> CharParser st [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
        [Char]
d <- CharParser st [Char]
forall st. CharParser st [Char]
decimalFractional CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
decimal
        Char
e <- [Char] -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf "Ee"
        [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
d [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char
e]))
    Token
ex <- CharParser st Token
forall st. CharParser st Token
integer
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
de [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Token -> [Char]
forall a. Show a => a -> [Char]
show Token
ex))
  CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
decimalFractional
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "unsigned real"

rational :: CharParser st Token
rational :: CharParser st Token
rational = CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    Char
s <- [Char] -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf "-+"
    [Char]
ur <- CharParser st [Char]
forall st. CharParser st [Char]
unsignedRational
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
s Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
ur))
  CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
unsignedRational
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "(signed) rational")

unsignedRational :: CharParser st String
unsignedRational :: CharParser st [Char]
unsignedRational = do
    [Char]
d1 <- CharParser st [Char] -> CharParser st [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st [Char]
forall st. CharParser st [Char]
decimal CharParser st [Char]
-> ParsecT [Char] st Identity Char -> CharParser st [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '/')
    [Char]
d2 <- CharParser st [Char]
forall st. CharParser st [Char]
positiveDecimal
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
d1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "/" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
d2)

integer :: CharParser st Token
integer :: CharParser st Token
integer = CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
parseToken (CharParser st [Char] -> CharParser st [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    Char
s <- [Char] -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf "-+"
    [Char]
ui <- CharParser st [Char]
forall st. CharParser st [Char]
unsignedInteger
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
s Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
ui))
  CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
unsignedInteger
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "(signed) integer")

unsignedInteger :: CharParser st String
unsignedInteger :: CharParser st [Char]
unsignedInteger = CharParser st [Char] -> CharParser st [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st [Char]
forall st. CharParser st [Char]
decimal CharParser st [Char]
-> ParsecT [Char] st Identity () -> CharParser st [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] st Identity Char -> ParsecT [Char] st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy ([Char] -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf "eE/."))

decimal :: CharParser st String
decimal :: CharParser st [Char]
decimal = do
    Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0'
    ParsecT [Char] st Identity Char -> ParsecT [Char] st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return "0"
  CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
positiveDecimal
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "single zero or digits"

positiveDecimal :: CharParser st String
positiveDecimal :: CharParser st [Char]
positiveDecimal = do
    Char
nz <- (Char -> Bool) -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (\ c :: Char
c -> Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '0')
    [Char]
d <- ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
nz Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
d)
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "positiv decimal"

decimalFractional :: CharParser st String
decimalFractional :: CharParser st [Char]
decimalFractional = do
    [Char]
dec <- CharParser st [Char] -> CharParser st [Char]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st [Char]
forall st. CharParser st [Char]
decimal CharParser st [Char]
-> ParsecT [Char] st Identity Char -> CharParser st [Char]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Char -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.')
    [Char]
n <- ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
    [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
dec [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n)
  CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "decimal fractional"


{- -----------------------------------------------------------------------------
Some helper functions
----------------------------------------------------------------------------- -}

skipAll :: CharParser st ()
skipAll :: CharParser st ()
skipAll = CharParser st () -> CharParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany (ParsecT [Char] st Identity Char -> CharParser st ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space CharParser st () -> CharParser st () -> CharParser st ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                    ParsecT [Char] st Identity TPTP_THF -> CharParser st ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
comment ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
definedComment ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
-> ParsecT [Char] st Identity TPTP_THF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity TPTP_THF
forall st. CharParser st TPTP_THF
systemComment))

skipSpaces :: CharParser st ()
skipSpaces :: CharParser st ()
skipSpaces = ParsecT [Char] st Identity Char -> CharParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany ParsecT [Char] st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space

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

keyChar :: Char -> CharParser st ()
keyChar :: Char -> CharParser st ()
keyChar = CharParser st Char -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st Char -> CharParser st ())
-> (Char -> CharParser st Char) -> Char -> CharParser st ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> CharParser st Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char

myManyTill :: CharParser st a -> CharParser st a -> CharParser st [a]
myManyTill :: CharParser st a -> CharParser st a -> CharParser st [a]
myManyTill p :: CharParser st a
p end :: CharParser st a
end = do
    a
e <- CharParser st a
end
    [a] -> CharParser st [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
e]
  CharParser st [a] -> CharParser st [a] -> CharParser st [a]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    a
x <- CharParser st a
p
    [a]
xs <- CharParser st a -> CharParser st a -> CharParser st [a]
forall st a.
CharParser st a -> CharParser st a -> CharParser st [a]
myManyTill CharParser st a
p CharParser st a
end
    [a] -> CharParser st [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)


{- -----------------------------------------------------------------------------
Different simple symbols
----------------------------------------------------------------------------- -}

vLine :: CharParser st ()
vLine :: CharParser st ()
vLine = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '|'

star :: CharParser st ()
star :: CharParser st ()
star = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '*'

plus :: CharParser st ()
plus :: CharParser st ()
plus = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '+'

arrow :: CharParser st ()
arrow :: CharParser st ()
arrow = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '>'

comma :: CharParser st ()
comma :: CharParser st ()
comma = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar ','

colon :: CharParser st ()
colon :: CharParser st ()
colon = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar ':'

oParentheses :: CharParser st ()
oParentheses :: CharParser st ()
oParentheses = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '('

cParentheses :: CharParser st ()
cParentheses :: CharParser st ()
cParentheses = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar ')'

parentheses :: CharParser st a -> CharParser st a
parentheses :: CharParser st a -> CharParser st a
parentheses p :: CharParser st a
p = do
    a
r <- CharParser st a -> CharParser st a
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st ()
forall st. CharParser st ()
oParentheses CharParser st () -> CharParser st a -> CharParser st a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser st a
p)
    CharParser st ()
forall st. CharParser st ()
cParentheses
    a -> CharParser st a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

oBracket :: CharParser st ()
oBracket :: CharParser st ()
oBracket = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '['

cBracket :: CharParser st ()
cBracket :: CharParser st ()
cBracket = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar ']'

brackets :: CharParser st a -> CharParser st a
brackets :: CharParser st a -> CharParser st a
brackets p :: CharParser st a
p = do
    a
r <- CharParser st a -> CharParser st a
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st ()
forall st. CharParser st ()
oBracket CharParser st () -> CharParser st a -> CharParser st a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser st a
p)
    CharParser st ()
forall st. CharParser st ()
cBracket
    a -> CharParser st a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

ampersand :: CharParser st ()
ampersand :: CharParser st ()
ampersand = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '&'

at :: CharParser st ()
at :: CharParser st ()
at = Char -> CharParser st ()
forall st. Char -> CharParser st ()
keyChar '@'

gentzenArrow :: CharParser st ()
gentzenArrow :: CharParser st ()
gentzenArrow = CharParser st [Char] -> CharParser st ()
forall st a. CharParser st a -> CharParser st ()
key (CharParser st [Char] -> CharParser st ())
-> CharParser st [Char] -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string "-->"