ParseTHF.hs revision 8fb127028cb7dd361e348a3252e33487f73428bc
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : A Parser for the TPTP-THF Syntax
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (c) A. Tsogias, DFKI Bremen 2011
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Jonathan von Schroeder <j.von_schroeder@dfki.de>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : portable
d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian MaederA Parser for the TPTP-THF Input Syntax v5.4.0.0 taken from
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html> and THF0
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederSyntax taken from <http://www.ags.uni-sb.de/~chris/papers/C25.pdf> P. 15-16
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederNote: The parser prefers a THF0 parse tree over a THF parse tree
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus LuettichNote: We pretend as if tuples were still part of the syntax
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maedermodule THF.ParseTHF (parseTHF) where
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Common.Id (Token(..))
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport Common.Lexer (parseToken)
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder--------------------------------------------------------------------------------
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder-- Parser for the THF and THF0 Syntax
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich--------------------------------------------------------------------------------
8c7a54ad8bf776a530ecf907a373d42415cf4faeChristian Maeder-- THF & THF0:
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski-- <TPTP_input> ::= <annotated_formula> | <include>
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <thf_annotated> ::= thf(<name>,<formula_role>,<thf_formula><annotations>).
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- Data Type: TPTP_THF
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederparseTHF :: CharParser st [TPTP_THF]
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder h <- optionMaybe header
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder thf <- many ((systemComment <|> definedComment <|> comment <|>
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder include <|> thfAnnotatedFormula) << skipSpaces)
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder return $ if isJust h then fromJust h : thf else thf
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederheader :: CharParser st TPTP_THF
8410667510a76409aca9bb24ff0eda0420088274Christian Maederheader = try (do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder s <- headerSE
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder c <- myManyTill (try (commentLine << skipSpaces)) (try headerSE)
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder return $ TPTP_Header (s : c))
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederheaderSE :: CharParser st Comment
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich try (char '%' >> notFollowedBy (char '$'))
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder c <- parseToken $ many1 $ char '-' << notFollowedBy printableChar
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder return $ Comment_Line c
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- THF & THF0:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <comment> ::- <comment_line>|<comment_block>
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder-- <comment_line> ::- [%]<printable_char>*
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <comment_block> ::: [/][*]<not_star_slash>[*][*]*[/]
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- <not_star_slash> ::: ([^*]*[*][*]*[^/*])*[^*]*
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercommentLine :: CharParser st Comment
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercommentLine = do
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder try (char '%' >> notFollowedBy (char '$'))
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder c <- parseToken $ many printableChar
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder return $ Comment_Line c
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maedercomment :: CharParser st TPTP_THF
f13d1e86e58da53680e78043e8df182eed867efbChristian Maedercomment = fmap TPTP_Comment commentLine
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder try (string "/*" >> notFollowedBy (char '$'))
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder c <- parseToken $ many (noneOf "*/")
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder skipMany1 (char '*'); char '/'
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maeder return $ TPTP_Comment (Comment_Block c)
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich-- THF & THF0:
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich-- <defined_comment> ::- <def_comment_line>|<def_comment_block>
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich-- <def_comment_line> ::: [%]<dollar><printable_char>*
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- <def_comment_block> ::: [/][*]<dollar><not_star_slash>[*][*]*[/]
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- Data Type: DefinedComment
8cacad2a09782249243b80985f28e9387019fe40Christian MaederdefinedComment :: CharParser st TPTP_THF
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederdefinedComment = do
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder try (string "%$" >> notFollowedBy (char '$'))
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder c <- parseToken $ many printableChar
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder return $ TPTP_Defined_Comment (Defined_Comment_Line c)
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder try (string "/*$" >> notFollowedBy (char '$'))
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder c <- parseToken $ many (noneOf "*/")
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder skipMany1 (char '*'); char '/'
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return $ TPTP_Defined_Comment (Defined_Comment_Block c)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF & THF0:
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- <system_comment> ::- <sys_comment_line>|<sys_comment_block>
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- <sys_comment_line> ::: [%]<dollar><dollar><printable_char>*
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- <sys_comment_block> ::: [/][*]<dollar><dollar><not_star_slash>[*][*]*[/]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- Data Type: SystemComment
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedersystemComment :: CharParser st TPTP_THF
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedersystemComment = do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder tryString "%$$"
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder c <- parseToken $ many printableChar
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return $ TPTP_System_Comment (System_Comment_Line c)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder tryString "/*$$"
776a1a086df734581431e6edb4343ed4c8d34d55Christian Maeder c <- parseToken $ many (noneOf "*/")
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder skipMany1 (char '*'); char '/'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ TPTP_System_Comment (System_Comment_Block c)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder-- THF & THF0:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <include> ::= include(<file_name><formula_selection>).
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <formula_selection> ::= ,[<name_list>] | <null>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- Data Type: Include
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinclude :: CharParser st TPTP_THF
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder key $ tryString "include"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder fn <- fileName
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder fs <- formulaSelection
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder cParentheses; char '.'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ TPTP_Include (I_Include fn fs)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederthfAnnotatedFormula :: CharParser st TPTP_THF
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederthfAnnotatedFormula = do
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder key $ tryString "thf"
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder n <- name; comma
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder fr <- formulaRole; comma
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder tf <- thfFormula
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder a <- annotations
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder cParentheses; char '.'
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return $ TPTP_THF_Annotated_Formula n fr tf a
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- THF & THF0:
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- <annotations> ::= ,<source><optional_info> | <null>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederannotations :: CharParser st Annotations
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederannotations = do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder oi <- optionalInfo
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder return $ Annotations s oi
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder notFollowedBy (char ',');
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- THF & THF0:
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- <formula_role> ::= <lower_word>
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- <formula_role> :== axiom | hypothesis | definition | assumption |
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- lemma | theorem | conjecture | negated_conjecture |
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- plain | fi_domain | fi_functors | fi_predicates |
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- type | unknown
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederformulaRole :: CharParser st FormulaRole
4017ebc0f692820736d796af3110c3b3018c108aChristian MaederformulaRole = do
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder r <- lowerWord
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich case show r of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder "axiom" -> return Axiom
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "hypothesis" -> return Hypothesis
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "definition" -> return Definition
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "assumption" -> return Assumption
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder "lemma" -> return Lemma
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder "theorem" -> return Theorem
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder "conjecture" -> return Conjecture
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder "negated_conjecture" -> return Negated_Conjecture
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder "plain" -> return Plain
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder "fi_domain" -> return Fi_Domain
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "fi_functors" -> return Fi_Functors
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder "fi_predicates" -> return Fi_Predicates
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "type" -> return Type
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "unknown" -> return Unknown
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder s -> fail ("No such Role: " ++ s)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <thf_formula> ::= <thf_logic_formula> | <thf_sequent>
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- <thf_formula> ::= <thf_logic_formula> | <thf_typed_const>
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederthfFormula :: CharParser st THFFormula
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederthfFormula = fmap T0F_THF_Typed_Const thfTypedConst
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder <|> fmap TF_THF_Logic_Formula thfLogicFormula
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder <|> fmap TF_THF_Sequent thfSequent
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- <thf_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula> |
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- <thf_type_formula> | <thf_subtype>
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- <thf_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula>
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederthfLogicFormula :: CharParser st THFLogicFormula
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichthfLogicFormula = fmap TLF_THF_Binary_Formula thfBinaryFormula
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap TLF_THF_Unitary_Formula thfUnitaryFormula
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- different position for unitary formula to prefer thf0 parse
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich <|> fmap TLF_THF_Type_Formula thfTypeFormula
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder <|> fmap TLF_THF_Sub_Type thfSubType
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder-- <thf_binary_formula> ::= <thf_binary_pair> | <thf_binary_tuple> |
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich-- <thf_binary_type>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <thf_binary_pair> ::= <thf_unitary_formula> <thf_pair_connective>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <thf_unitary_formula>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <thf_binary_formula> ::= <thf_pair_binary> | <thf_tuple_binary>
d272062059eea4d7479e1c6e8517469f02f61287Christian Maeder-- <thf_pair_binary> ::= <thf_unitary_formula> <thf_pair_connective>
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder-- <thf_unitary_formula>
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder-- Note: For THF0
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder-- <thf_binary_pair> is used like <thf_pair_binary> and
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder-- <thf_binary_tuple> are used like <thf_tuple_binary>
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian MaederthfBinaryFormula :: CharParser st THFBinaryFormula
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian MaederthfBinaryFormula = fmap TBF_THF_Binary_Tuple thfBinaryTuple
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder (uff, pc) <- try $ do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder uff1 <- thfUnitaryFormula
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder pc1 <- thfPairConnective
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return (uff1, pc1)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ufb <- thfUnitaryFormula
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return $ TBF_THF_Binary_Pair uff pc ufb
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder <|> fmap TBF_THF_Binary_Type thfBinaryType
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- different position for binary type to prefer thf0 parse
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- <thf_binary_tuple> ::= <thf_or_formula> | <thf_and_formula> |
010c56c4cf12dd7977ca36efe85219b91e265ee3Christian Maeder-- <thf_apply_formula>
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski-- <thf_tuple_binary> ::= <thf_or_formula> | <thf_and_formula> |
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder-- <thf_apply_formula>
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- THF & THF0:
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder-- <thf_or_formula> ::= <thf_unitary_formula> <vline> <thf_unitary_formula> |
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <thf_or_formula> <vline> <thf_unitary_formula>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <thf_and_formula> ::= <thf_unitary_formula> & <thf_unitary_formula> |
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder-- thf_and_formula> & <thf_unitary_formula>
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- <thf_apply_formula> ::= <thf_unitary_formula> @ <thf_unitary_formula> |
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- <thf_apply_formula> @ <thf_unitary_formula>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <vline> :== |
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederthfBinaryTuple :: CharParser st THFBinaryTuple
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederthfBinaryTuple = do -- or
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder uff <- try (thfUnitaryFormula << vLine)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder ufb <- sepBy1 thfUnitaryFormula vLine
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder return $ TBT_THF_Or_Formula (uff : ufb)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder <|> do -- and
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder uff <- try (thfUnitaryFormula << ampersand)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ufb <- sepBy1 thfUnitaryFormula ampersand
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return $ TBT_THF_And_Formula (uff : ufb)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> do -- apply
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder uff <- try (thfUnitaryFormula << at)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder ufb <- sepBy1 thfUnitaryFormula at
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder return $ TBT_THF_Apply_Formula (uff : ufb)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_unitary_formula> ::= <thf_quantified_formula> | <thf_unary_formula> |
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_atom> | <thf_tuple> | <thf_let> |
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_conditional> | (<thf_logic_formula>)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- note: thf let is currently not well defined and thus ommited
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_conditional> ::= $itef(<thf_logic_formula>,<thf_logic_formula>,
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_logic_formula>)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_unitary_formula> ::= <thf_quantified_formula> | <thf_abstraction> |
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_unary_formula> | <thf_atom> |
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- (<thf_logic_formula>)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_abstraction> ::= <thf_lambda> [<thf_variable_list>] :
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_unitary_formula>
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_lambda> ::= ^
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- THF & THF0:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <thf_unary_formula> ::= <thf_unary_connective> (<thf_logic_formula>)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederthfUnitaryFormula :: CharParser st THFUnitaryFormula
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederthfUnitaryFormula = fmap TUF_THF_Logic_Formula_Par (parentheses thfLogicFormula)
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder <|> fmap TUF_THF_Quantified_Formula (try thfQuantifiedFormula)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder vl <- brackets thfVariableList; colon
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski uf <- thfUnitaryFormula
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder return $ T0UF_THF_Abstraction vl uf --added this for thf0
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder --changed positions of parses below to prefer th0
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder <|> try thfUnaryFormula
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder <|> fmap TUF_THF_Atom thfAtom
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich <|> fmap TUF_THF_Tuple thfTuple
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner key $ tryString "$itef"; oParentheses
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner lf1 <- thfLogicFormula; comma
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich lf2 <- thfLogicFormula; comma
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich lf3 <- thfLogicFormula; cParentheses
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder return $ TUF_THF_Conditional lf1 lf2 lf3
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- <thf_quantified_formula> ::= <thf_quantifier> [<thf_variable_list>] :
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- <thf_unitary_formula>
b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder-- <thf_quantified_formula> ::= <thf_quantified_var> | <thf_quantified_novar>
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder-- <thf_quantified_var> ::= <quantifier> [<thf_variable_list>] :
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich-- <thf_unitary_formula>
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- <thf_quantified_novar> ::= <thf_quantifier> (<thf_unitary_formula>)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederthfQuantifiedFormula :: CharParser st THFQuantifiedFormula
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskithfQuantifiedFormula = do
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder q <- quantifier
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder vl <- brackets thfVariableList; colon
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski uf <- thfUnitaryFormula
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder return $ T0QF_THF_Quantified_Var q vl uf --added this for thf0
c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maeder q <- thfQuantifier
38352346eb1a67ba0f4eab8ad6f718528cf0cde0Christian Maeder uf <- parentheses thfUnitaryFormula
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder return $ T0QF_THF_Quantified_Novar q uf --added this for thf0
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder q <- thfQuantifier
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder vl <- brackets thfVariableList; colon
11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maeder uf <- thfUnitaryFormula
11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maeder return $ TQF_THF_Quantified_Formula q vl uf
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- THF & THF0:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <thf_variable_list> ::= <thf_variable> |
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_variable>,<thf_variable_list>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederthfVariableList :: CharParser st THFVariableList
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederthfVariableList = sepBy1 thfVariable comma
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- THF & THF0:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <thf_variable> ::= <thf_typed_variable> | <variable>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <thf_typed_variable> ::= <variable> : <thf_top_level_type>
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian MaederthfVariable :: CharParser st THFVariable
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederthfVariable = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder v <- try (variable << colon)
ffd3a0c7339cc3637f022c38e66a7aa9f0cf10d3Rainer Grabbe tlt <- thfTopLevelType
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder return $ TV_THF_Typed_Variable v tlt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap TV_Variable variable
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- <thf_typed_const> ::= <constant> : <thf_top_level_type> |
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder-- (<thf_typed_const>)
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian MaederthfTypedConst :: CharParser st THFTypedConst --added this for thf0
53818ced114da21321063fff307aa41c1ab31dd3Achim MahnkethfTypedConst = fmap T0TC_THF_TypedConst_Par (parentheses thfTypedConst)
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke c <- try (constant << colon)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder tlt <- thfTopLevelType
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke return $ T0TC_Typed_Const c tlt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederthfUnaryFormula :: CharParser st THFUnitaryFormula
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederthfUnaryFormula = do
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich uc <- thfUnaryConnective
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich lf <- parentheses thfLogicFormula
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder return $ TUF_THF_Unary_Formula uc lf
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder-- <thf_type_formula> ::= <thf_typeable_formula> : <thf_top_level_type>
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski-- <thf_type_formula> :== <constant> : <thf_top_level_type>
7c99e334446bb97120e30e967baeeddfdd1278deKlaus LuettichthfTypeFormula :: CharParser st THFTypeFormula
4017ebc0f692820736d796af3110c3b3018c108aChristian MaederthfTypeFormula = do
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder tp <- try (thfTypeableFormula << colon)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder tlt <- thfTopLevelType
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder return $ TTF_THF_Type_Formula tp tlt
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder c <- try (constant << colon)
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder tlt <- thfTopLevelType
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder return $ TTF_THF_Typed_Const c tlt
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <thf_typeable_formula> ::= <thf_atom> | <thf_tuple> | (<thf_logic_formula>)
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian MaederthfTypeableFormula :: CharParser st THFTypeableFormula
b49276c9f50038e0bd499ad49f7bd6444566a834Christian MaederthfTypeableFormula = fmap TTyF_THF_Atom thfAtom
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap TTyF_THF_Tuple thfTuple
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder <|> fmap TTyF_THF_Logic_Formula (parentheses thfLogicFormula)
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich-- <thf_subtype> ::= <constant> <subtype_sign> <constant>
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich-- <subtype_sign> == <<
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus LuettichthfSubType :: CharParser st THFSubType
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus LuettichthfSubType = do
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich cf <- try (constant << key (string "<<"))
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich cb <- constant
5ea9168eddbfbfe2282ed46dfe107a8962d6727bChristian Maeder return $ TST_THF_Sub_Type cf cb
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich-- <thf_top_level_type> ::= <thf_logic_formula>
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <thf_top_level_type> ::= <constant> | <variable> | <defined_type> |
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <system_type> | <thf_binary_type>
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederthfTopLevelType :: CharParser st THFTopLevelType
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederthfTopLevelType = fmap T0TLT_THF_Binary_Type thfBinaryType
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap T0TLT_Constant constant
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder <|> fmap T0TLT_Variable variable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap T0TLT_Defined_Type definedType
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder <|> fmap T0TLT_System_Type systemType
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap TTLT_THF_Logic_Formula thfLogicFormula
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich --added all except for this for thf0
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich-- <thf_unitary_type> ::= <thf_unitary_formula>
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich-- <thf_unitary_type> ::= <constant> | <variable> | <defined_type> |
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich-- <system_type> | (<thf_binary_type>)
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus LuettichthfUnitaryType :: CharParser st THFUnitaryType
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus LuettichthfUnitaryType = fmap T0UT_Constant constant
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich <|> fmap T0UT_Variable variable
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich <|> fmap T0UT_Defined_Type definedType
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap T0UT_System_Type systemType
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich <|> fmap T0UT_THF_Binary_Type_Par (parentheses thfBinaryType)
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich <|> fmap TUT_THF_Unitary_Formula thfUnitaryFormula
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich --added all except for this for th0
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder-- <thf_binary_type> ::= <thf_mapping_type> | <thf_xprod_type> |
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <thf_union_type>
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder-- <thf_xprod_type> ::= <thf_unitary_type> <star> <thf_unitary_type> |
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- <thf_xprod_type> <star> <thf_unitary_type>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <star> ::- *
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- <thf_union_type> ::= <thf_unitary_type> <plus> <thf_unitary_type> |
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- <thf_union_type> <plus> <thf_unitary_type>
68aab98a58d1460c77a1573a86c32a891756a420Christian Maeder-- <plus> ::- +
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- <thf_binary_type> ::= <thf_mapping_type> | (<thf_binary_type>)
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder-- THF & THF0:
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder-- <thf_mapping_type> ::= <thf_unitary_type> <arrow> <thf_unitary_type> |
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- <thf_unitary_type> <arrow> <thf_mapping_type>
3a7788e09dd23b364a46c9488cbd1522369113dbChristian Maeder-- <arrow> ::- >
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederthfBinaryType :: CharParser st THFBinaryType
ef67402074be14deb95e4ff564737d5593144130Klaus LuettichthfBinaryType = do
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder utf <- try (thfUnitaryType << arrow)
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich utb <- sepBy1 thfUnitaryType arrow
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder return $ TBT_THF_Mapping_Type (utf : utb)
c9e197862d9d8ef2585270dd08f5194b3aed4a9dKlaus Luettich <|> fmap T0BT_THF_Binary_Type_Par (parentheses thfBinaryType)
e7e1ab2ac3f1fded8611bb92ae00e8f3b8c693fbKlaus Luettich -- added this for thf0
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich <|> do -- xprodType
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich utf <- try (thfUnitaryType << star)
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich utb <- sepBy1 thfUnitaryType star
d784803f9c752667b4fcf7393d698002bedf3f89Klaus Luettich return $ TBT_THF_Xprod_Type (utf : utb)
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich <|> do -- unionType
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich utf <- try (thfUnitaryType << plus)
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder utb <- sepBy1 thfUnitaryType plus
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder return $ TBT_THF_Union_Type (utf : utb)
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder-- <thf_atom> ::= <term> | <thf_conn_term>
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- %----<thf_atom> can also be <defined_type> | <defined_plain_formula> |
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- %----<system_type> | <system_atomic_formula>, but they are syntactically
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- %----captured by <term>.
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- <system_atomic_formula> ::= <system_term>
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- <thf_atom> ::= <constant> | <defined_constant> |
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- <system_constant> | <variable> | <thf_conn_term>
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- <defined_constant> ::= <atomic_defined_word>
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- <system_constant> ::= <atomic_system_word>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederthfAtom :: CharParser st THFAtom
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederthfAtom = fmap T0A_Constant constant
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich <|> fmap T0A_Defined_Constant atomicDefinedWord
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder <|> fmap T0A_System_Constant atomicSystemWord
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder <|> fmap T0A_Variable variable
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- added all above for thf0
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder <|> fmap TA_THF_Conn_Term thfConnTerm
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder -- changed position to prefer thf0
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder <|> fmap TA_Defined_Type definedType
43bb71dfe7ec405f563864d57c1cacdaa8ce9a80Christian Maeder <|> fmap TA_Defined_Plain_Formula definedPlainFormula
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder <|> fmap TA_System_Type systemType
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder <|> fmap TA_System_Atomic_Formula systemTerm
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski <|> fmap TA_Term term
37951dbd8e5f2418a07f072d9bf551d0c3a1eafcChristian Maeder-- <thf_tuple> ::= [] | [<thf_tuple_list>]
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <thf_tuple_list> ::= <thf_logic_formula> |
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- <thf_logic_formula>,<thf_tuple_list>
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- THFTupleList must not be empty
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian MaederthfTuple :: CharParser st THFTuple
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederthfTuple = try ((oBracket >> cBracket) >> return [])
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder <|> brackets (sepBy1 thfLogicFormula comma)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <thf_sequent> ::= <thf_tuple> <gentzen_arrow> <thf_tuple> |
68b77966b2cf7bf2e340bf0fb6b9efc3e6a00467Christian Maeder-- (<thf_sequent>)
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder-- <gentzen_arrow> ::= -->
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaederthfSequent :: CharParser st THFSequent
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaederthfSequent = fmap TS_THF_Sequent_Par (parentheses thfSequent)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder tf <- try (thfTuple << gentzenArrow)
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder tb <- thfTuple
94d3aa05411444596b44ede4531f05dd7ac20fdfChristian Maeder return $ TS_THF_Sequent tf tb
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder-- <thf_conn_term> ::= <thf_pair_connective> | <assoc_connective> |
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder-- <thf_unary_connective>
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder-- <thf_conn_term> ::= <thf_quantifier> | <thf_pair_connective> |
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder-- <assoc_connective> | <thf_unary_connective>
8410667510a76409aca9bb24ff0eda0420088274Christian MaederthfConnTerm :: CharParser st THFConnTerm
8410667510a76409aca9bb24ff0eda0420088274Christian MaederthfConnTerm = fmap TCT_THF_Pair_Connective thfPairConnective
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder <|> fmap TCT_Assoc_Connective assocConnective
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder <|> fmap TCT_THF_Unary_Connective thfUnaryConnective
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich <|> fmap T0CT_THF_Quantifier thfQuantifier
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich -- added for thf0
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- <thf_quantifier> ::= <fol_quantifier> | ^ | !> | ?* | @+ | @-
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- <fol_quantifier> ::= ! | ?
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- <thf_quantifier> ::= !! | ??
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichthfQuantifier :: CharParser st THFQuantifier
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichthfQuantifier = (key (tryString "!!") >> return T0Q_PiForAll)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <|> (key (tryString "??") >> return T0Q_SigmaExists)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich --added all above for thf0
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <|> (keyChar '!' >> return TQ_ForAll)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <|> (keyChar '?' >> return TQ_Exists)
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich <|> (keyChar '^' >> return TQ_Lambda_Binder)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <|> (key (tryString "!>") >> return TQ_Dependent_Product)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <|> (key (tryString "?*") >> return TQ_Dependent_Sum)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <|> (key (tryString "@+") >> return TQ_Indefinite_Description)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <|> (key (tryString "@-") >> return TQ_Definite_Description)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich <?> "thfQuantifier"
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- <quantifier> ::= ! | ?
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederquantifier :: CharParser st Quantifier
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersquantifier = (keyChar '!' >> return T0Q_ForAll)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> (keyChar '?' >> return T0Q_Exists)
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder <?> "quantifier"
1c9a63e4f7c6879f51fe0f32154a9116f2c126dbChristian Maeder-- <thf_pair_connective> ::= <infix_equality> | <infix_inequality> |
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder-- <binary_connective>
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <infix_equality> ::= =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <infix_inequality> ::= !=
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_pair_connective> ::= <defined_infix_pred> | <binary_connective>
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <defined_infix_pred> ::= = | !=
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich-- THF & THF0:
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski-- <binary_connective> ::= <=> | => | <= | <~> | ~<vline> | ~&
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till MossakowskithfPairConnective :: CharParser st THFPairConnective
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till MossakowskithfPairConnective = (key (tryString "!=") >> return Infix_Inequality)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> (key (tryString "<=>") >> return Equivalent)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> (key (tryString "=>") >> return Implication)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder <|> (key (tryString "<=") >> return IF)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> (key (tryString "<~>") >> return XOR)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> (key (tryString "~|") >> return NOR)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder <|> (key (tryString "~&") >> return NAND)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> (keyChar '=' >> return Infix_Equality)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <?> "pairConnective"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_unary_connective> ::= <unary_connective> | !! | ??
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_unary_connective> ::= <unary_connective>
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- THF & THF0:
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich-- <unary_connective> ::= ~
abf2487c3aece95c371ea89ac64319370dcb6483Klaus LuettichthfUnaryConnective :: CharParser st THFUnaryConnective
abf2487c3aece95c371ea89ac64319370dcb6483Klaus LuettichthfUnaryConnective = (keyChar '~' >> return Negation)
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich <|> (key (tryString "!!") >> return PiForAll)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers <|> (key (tryString "??") >> return SigmaExists)
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder-- THF & THF0:
8555737bcc9bf1d0afb6624e4d8668f070bcaba1Christian Maeder-- <assoc_connective> ::= <vline> | &
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersassocConnective :: CharParser st AssocConnective
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederassocConnective = (keyChar '|' >> return OR)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> (keyChar '&' >> return AND)
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich-- <defined_type> :== $oType | $o | $iType | $i | $tType |
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- $real | $rat | $int
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- <defined_type> :== $oType | $o | $iType | $i | $tType
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder-- THF & THF0:
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <defined_type> ::= <atomic_defined_word>
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederdefinedType :: CharParser st DefinedType
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederdefinedType = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder adw <- atomicDefinedWord
d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maeder case show adw of
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder "oType" -> return DT_oType
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "o" -> return DT_o
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder "iType" -> return DT_iType
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich "i" -> return DT_i
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich "tType" -> return DT_tType
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich "real" -> return DT_real
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder "rat" -> return DT_rat
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich "int" -> return DT_int
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder s -> fail ("No such definedType: " ++ s)
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich-- THF & THF0:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <system_type> ::= <atomic_system_word>
c5e3fc166373b0d90f6e36e8aa234396a1dcd879Christian MaedersystemType :: CharParser st Token
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian MaedersystemType = atomicSystemWord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <defined_plain_formula> ::= <defined_plain_term>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <defined_plain_formula> :== <defined_prop> | <defined_pred>(<arguments>)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederdefinedPlainFormula :: CharParser st DefinedPlainFormula
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederdefinedPlainFormula = fmap DPF_Defined_Prop definedProp
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder dp <- definedPred
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder a <- parentheses arguments
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ DPF_Defined_Formula dp a
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder-- THF & THF0:
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder-- <defined_prop> :== <atomic_defined_word>
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder-- <defined_prop> :== $true | $false
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederdefinedProp :: CharParser st DefinedProp
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederdefinedProp = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder adw <- atomicDefinedWord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case show adw of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "true" -> return DP_True
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "false" -> return DP_False
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski s -> fail ("No such definedProp: " ++ s)
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini-- <defined_pred> :== <atomic_defined_word>
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder-- <defined_pred> :== $distinct |
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini-- $less | $lesseq | $greater | $greatereq |
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder-- $is_int | $is_rat
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian MaederdefinedPred :: CharParser st DefinedPred
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian MaederdefinedPred = do
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini adw <- atomicDefinedWord
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder case show adw of
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder "distinct" -> return Disrinct
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder "less" -> return Less
e50e41135ece589f7202bd4ef8d6b97531c2a56eKlaus Luettich "lesseq" -> return Lesseq
47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maeder "greater" -> return Greater
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "greatereq" -> return Greatereq
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "is_int" -> return Is_int
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder "is_rat" -> return Is_rat
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder s -> fail ("No such definedPred: " ++ s)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <term> ::= <function_term> | <variable> | <conditional_term>
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- %----Conditional terms should only be used by TFF and not by THF.
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- Thus tey are not implemented.
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederterm :: CharParser st Term
88318aafc287e92931dceffbb943d58a9310001dChristian Maederterm = fmap T_Function_Term functionTerm
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap T_Variable variable
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- <function_term> ::= <plain_term> | <defined_term> | <system_term>
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichfunctionTerm :: CharParser st FunctionTerm
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian MaederfunctionTerm = fmap FT_System_Term systemTerm
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder <|> fmap FT_Defined_Term definedTerm
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich <|> fmap FT_Plain_Term plainTerm
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- <plain_term> ::= <constant> | <functor>(<arguments>)
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichplainTerm :: CharParser st PlainTerm
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichplainTerm = try (do
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich f <- tptpFunctor
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder a <- parentheses arguments
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ PT_Plain_Term f a)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder <|> fmap PT_Constant constant
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- THF & THF0:
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- <constant> ::= <functor>
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maederconstant :: CharParser st Constant
fdef3358918491badb0e29e42b5d3b5a01950716Christian Maederconstant = tptpFunctor
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder-- THF & THF0:
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder-- <functor> ::= <atomic_word>
88318aafc287e92931dceffbb943d58a9310001dChristian MaedertptpFunctor :: CharParser st AtomicWord
fdef3358918491badb0e29e42b5d3b5a01950716Christian MaedertptpFunctor = atomicWord
7767474aba4fa2dc51a6c68017d3bcef3b773001Christian Maeder-- <defined_term> ::= <defined_atom> | <defined_atomic_term>
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- <defined_atomic_term> ::= <defined_plain_term>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederdefinedTerm :: CharParser st DefinedTerm
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskidefinedTerm = fmap DT_Defined_Atomic_Term definedPlainTerm
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder <|> fmap DT_Defined_Atom definedAtom
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- <defined_atom> ::= <number> | <distinct_object>
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskidefinedAtom :: CharParser st DefinedAtom
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederdefinedAtom = fmap DA_Number number
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich <|> fmap DA_Distinct_Object distinctObject
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <defined_plain_term> ::= <defined_constant> | <defined_functor>(<arguments>)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <defined_constant> ::= <defined_functor>
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichdefinedPlainTerm :: CharParser st DefinedPlainTerm
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederdefinedPlainTerm = try (do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder df <- definedFunctor
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich a <- parentheses arguments
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ DPT_Defined_Function df a)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> fmap DPT_Defined_Constant definedFunctor
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <defined_functor> ::= <atomic_defined_word>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- <defined_functor> :== $uminus | $sum | $difference | $product |
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- $quotient | $quotient_e | $quotient_t | $quotient_f |
1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder-- $remainder_e | $remainder_t | $remainder_f |
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich-- $floor | $ceiling | $truncate | $round |
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich-- $to_int | $to_rat | $to_real
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichdefinedFunctor :: CharParser st DefinedFunctor
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichdefinedFunctor = do
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich adw <- atomicDefinedWord
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich case show adw of
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "uminus" -> return UMinus
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "sum" -> return Sum
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "difference" -> return Difference
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "product" -> return Product
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "quotient" -> return Quotient
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "quotient_e" -> return Quotient_e
2e62113845a35e07cb46db05714627c95450f267Klaus Luettich "quotient_t" -> return Quotient_t
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "quotient_f" -> return Quotient_f
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "floor" -> return Floor
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "ceiling" -> return Ceiling
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich "truncate" -> return Truncate
438f9bd974c8e668203e636b0f2bc80c589af043Klaus Luettich "round" -> return Round
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder "to_int" -> return To_int
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder "to_rat" -> return To_rat
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "to_real" -> return To_real
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder s -> fail ("No such definedFunctor: " ++ s)
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- <system_term> ::= <system_constant> | <system_functor>(<arguments>)