ParseTHF.hs revision 8fb127028cb7dd361e348a3252e33487f73428bc
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{- |
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 Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Jonathan von Schroeder <j.von_schroeder@dfki.de>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
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 Maeder
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 Maeder-}
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maedermodule THF.ParseTHF (parseTHF) where
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport THF.As
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Text.ParserCombinators.Parsec
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Common.Parsec
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Common.Id (Token(..))
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport Common.Lexer (parseToken)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maederimport Data.Char
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maederimport Data.Maybe
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder--------------------------------------------------------------------------------
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder-- Parser for the THF and THF0 Syntax
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich--------------------------------------------------------------------------------
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]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederparseTHF = do
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
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder
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))
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederheaderSE :: CharParser st Comment
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichheaderSE = do
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich try (char '%' >> notFollowedBy (char '$'))
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder c <- parseToken $ many1 $ char '-' << notFollowedBy printableChar
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder skipSpaces
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder return $ Comment_Line c
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich
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
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maedercomment :: CharParser st TPTP_THF
f13d1e86e58da53680e78043e8df182eed867efbChristian Maedercomment = fmap TPTP_Comment commentLine
cdd280437686b1e2e25e3761d4adf3d4a0a2d11cKlaus Luettich <|> do
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)
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski
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)
47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maeder <|> do
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)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
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)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder <|> do
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder tryString "/*$$"
776a1a086df734581431e6edb4343ed4c8d34d55Christian Maeder c <- parseToken $ many (noneOf "*/")
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder skipMany1 (char '*'); char '/'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ TPTP_System_Comment (System_Comment_Block c)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder
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
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinclude = do
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder key $ tryString "include"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder oParentheses
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder fn <- fileName
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder fs <- formulaSelection
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder cParentheses; char '.'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ TPTP_Include (I_Include fn fs)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederthfAnnotatedFormula :: CharParser st TPTP_THF
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederthfAnnotatedFormula = do
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder key $ tryString "thf"
ad4889ebb40efae8595b0969dd6ba1162d52bac3Christian Maeder oParentheses
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
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- THF & THF0:
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- <annotations> ::= ,<source><optional_info> | <null>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederannotations :: CharParser st Annotations
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederannotations = do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder comma
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder s <- source
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder oi <- optionalInfo
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder return $ Annotations s oi
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder <|> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder notFollowedBy (char ',');
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return Null
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder
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)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- THF
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- <thf_formula> ::= <thf_logic_formula> | <thf_sequent>
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- THF0:
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
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder
89f7631cbfbd1bb99fc152b434bd362a7799d295Christian Maeder-- THF:
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- <thf_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula> |
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- <thf_type_formula> | <thf_subtype>
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder-- THF0:
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
6b6773cf587b74259178641d811746a235faf056Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF:
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>
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- THF0:
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
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder <|> do
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
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder-- THF:
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- <thf_binary_tuple> ::= <thf_or_formula> | <thf_and_formula> |
010c56c4cf12dd7977ca36efe85219b91e265ee3Christian Maeder-- <thf_apply_formula>
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich-- THF0:
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
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- THF:
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-- THF0:
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)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder <|> do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder keyChar '^'
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
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich <|> do
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
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- THF:
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- <thf_quantified_formula> ::= <thf_quantifier> [<thf_variable_list>] :
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- <thf_unitary_formula>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF0:
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
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder <|> do
c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maeder q <- thfQuantifier
38352346eb1a67ba0f4eab8ad6f718528cf0cde0Christian Maeder uf <- parentheses thfUnitaryFormula
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder return $ T0QF_THF_Quantified_Novar q uf --added this for thf0
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder <|> do
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder q <- thfQuantifier
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder vl <- brackets thfVariableList; colon
11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maeder uf <- thfUnitaryFormula
11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maeder return $ TQF_THF_Quantified_Formula q vl uf
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder
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
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
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- THF0:
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)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder <|> do
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke c <- try (constant << colon)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder tlt <- thfTopLevelType
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke return $ T0TC_Typed_Const c tlt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
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
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder-- THF:
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
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder <|> do
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder c <- try (constant << colon)
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder tlt <- thfTopLevelType
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder return $ TTF_THF_Typed_Const c tlt
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder
0c355dd0b739631ee472f9a656e266be27fa4e64Christian Maeder-- THF:
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)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- THF:
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
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich
5c69cef4668bbd959d721668313a779126014d1eKlaus Luettich-- THF:
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich-- <thf_top_level_type> ::= <thf_logic_formula>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF0:
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
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich-- THF:
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich-- <thf_unitary_type> ::= <thf_unitary_formula>
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich-- THF0:
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
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF:
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-- THF0:
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)
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder-- THF:
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>
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- THF0:
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
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder-- THF:
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)
9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder-- THF:
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)
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder <|> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder tf <- try (thfTuple << gentzenArrow)
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder tb <- thfTuple
94d3aa05411444596b44ede4531f05dd7ac20fdfChristian Maeder return $ TS_THF_Sequent tf tb
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder--THF:
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder-- <thf_conn_term> ::= <thf_pair_connective> | <assoc_connective> |
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder-- <thf_unary_connective>
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder-- THF0:
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
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- THF:
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- <thf_quantifier> ::= <fol_quantifier> | ^ | !> | ?* | @+ | @-
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- <fol_quantifier> ::= ! | ?
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- THF0:
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"
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich-- THF0:
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- <quantifier> ::= ! | ?
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederquantifier :: CharParser st Quantifier
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersquantifier = (keyChar '!' >> return T0Q_ForAll)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder <|> (keyChar '?' >> return T0Q_Exists)
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder <?> "quantifier"
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder--THF:
1c9a63e4f7c6879f51fe0f32154a9116f2c126dbChristian Maeder-- <thf_pair_connective> ::= <infix_equality> | <infix_inequality> |
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder-- <binary_connective>
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <infix_equality> ::= =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <infix_inequality> ::= !=
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- THF0:
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"
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- THF:
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- <thf_unary_connective> ::= <unary_connective> | !! | ??
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner-- THF0:
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)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder-- THF & THF0:
8555737bcc9bf1d0afb6624e4d8668f070bcaba1Christian Maeder-- <assoc_connective> ::= <vline> | &
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersassocConnective :: CharParser st AssocConnective
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederassocConnective = (keyChar '|' >> return OR)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> (keyChar '&' >> return AND)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- THF:
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich-- <defined_type> :== $oType | $o | $iType | $i | $tType |
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- $real | $rat | $int
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich-- THF0:
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)
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich-- THF & THF0:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- <system_type> ::= <atomic_system_word>
c5e3fc166373b0d90f6e36e8aa234396a1dcd879Christian MaedersystemType :: CharParser st Token
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian MaedersystemType = atomicSystemWord
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF:
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
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> do
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder dp <- definedPred
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder a <- parentheses arguments
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ DPF_Defined_Formula dp a
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
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)
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski-- THF:
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
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF:
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
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- THF:
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
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- THF:
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
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- THF & THF0:
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- <constant> ::= <functor>
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maederconstant :: CharParser st Constant
fdef3358918491badb0e29e42b5d3b5a01950716Christian Maederconstant = tptpFunctor
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder-- THF & THF0:
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder-- <functor> ::= <atomic_word>
88318aafc287e92931dceffbb943d58a9310001dChristian MaedertptpFunctor :: CharParser st AtomicWord
fdef3358918491badb0e29e42b5d3b5a01950716Christian MaedertptpFunctor = atomicWord
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- THF:
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
bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski-- THF:
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
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich-- THF:
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
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- THF:
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)
438f9bd974c8e668203e636b0f2bc80c589af043Klaus Luettich
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- THF:
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- <system_term> ::= <system_constant> | <system_functor>(<arguments>)
-- <system_constant> ::= <system_functor>
systemTerm :: CharParser st SystemTerm
systemTerm = try (do
sf <- systemFunctor
a <- parentheses arguments
return $ ST_System_Term sf a)
<|> fmap ST_System_Constant systemFunctor
-- THF:
-- <system_functor> ::= <atomic_system_word>
systemFunctor :: CharParser st Token
systemFunctor = atomicSystemWord
-- THF & THF0:
-- <variable> ::= <upper_word>
variable :: CharParser st Token
variable = parseToken
(do
u <- upper
an <- many alphaNum
skipAll
return (u : an)
<?> "Variable")
-- THF:
-- <arguments> ::= <term> | <term>,<arguments>
-- at least one term is neaded
arguments :: CharParser st Arguments
arguments = sepBy1 term comma
-- THF & THF0:
-- <principal_symbol> :== <functor> | <variable>
principalSymbol :: CharParser st PrincipalSymbol
principalSymbol = fmap PS_Functor tptpFunctor
<|> fmap PS_Variable 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 = (key (tryString "unknown") >> return S_Unknown)
<|> fmap S_Dag_Source dagSource
<|> fmap S_External_Source externalSource
<|> fmap S_Sources (sepBy1 source comma)
<|> do -- internal_source
key $ tryString "introduced"; oParentheses
it <- introType
oi <- optionalInfo; cParentheses
return $ S_Internal_Source it 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 = do
key (tryString "inference"); oParentheses
ir <- atomicWord; comma
ui <- usefulInfo; comma
pl <- brackets (sepBy1 parentInfo comma)
cParentheses
return (DS_Inference_Record ir ui pl)
<|> fmap DS_Name name
-- THF & THF0:
-- <parent_info> :== <source><parent_details>
-- <parent_details> :== :<general_list> | <null>
parentInfo :: CharParser st ParentInfo
parentInfo = do
s <- source
pd <- parentDetails
return $ PI_Parent_Info s pd
parentDetails :: CharParser st (Maybe GeneralList)
parentDetails = fmap Just (colon >> generalList)
<|> (notFollowedBy (char ':') >> return Nothing)
-- THF & THF0:
-- <intro_type> :== definition | axiom_of_choice | tautology | assumption
introType :: CharParser st IntroType
introType = (key (tryString "definition") >> return IT_definition)
<|> (key (tryString "axiom_of_choice") >> return IT_axiom_of_choice)
<|> (key (tryString "tautology") >> return IT_tautology)
<|> (key (tryString "assumption") >> return 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 = fmap ES_File_Source fileSource
<|> do
key $ tryString "theory"; oParentheses
tn <- theoryName
oi <- optionalInfo; cParentheses
return $ ES_Theory tn oi
<|> do
key $ tryString "creator"; oParentheses
cn <- atomicWord
oi <- optionalInfo; cParentheses
return $ ES_Creator_Source cn oi
-- THF & THF0:
-- <file_source> :== file(<file_name><file_info>)
-- <file_info> :== ,<name> | <null>
fileSource :: CharParser st FileSource
fileSource = do
key $ tryString "file"; oParentheses
fn <- fileName
fi <- fileInfo; cParentheses
return $ FS_File fn fi
fileInfo :: CharParser st (Maybe Name)
fileInfo = fmap Just (comma >> name)
<|> (notFollowedBy (char ',') >> return Nothing)
-- THF & THF0:
-- <theory_name> :== equality | ac
theoryName :: CharParser st TheoryName
theoryName = (key (tryString "equality") >> return Equality)
<|> (key (tryString "ac") >> return Ac)
-- THF & THF0:
-- <optional_info> ::= ,<useful_info> | <null>
optionalInfo :: CharParser st OptionalInfo
optionalInfo = fmap Just (comma >> usefulInfo)
<|> (notFollowedBy (char ',') >> return Nothing)
-- THF & THF0:
-- <useful_info> ::= <general_list>
-- <useful_info> :== [] | [<info_items>]
-- <info_items> :== <info_item> | <info_item>,<info_items>
usefulInfo :: CharParser st UsefulInfo
usefulInfo = (oBracket >> cBracket >> return [])
<|> brackets (sepBy1 infoItem comma)
-- THF & THF0:
-- <info_item> :== <formula_item> | <inference_item> |
-- <general_function>
infoItem :: CharParser st InfoItem
infoItem = fmap II_Formula_Item formulaItem
<|> fmap II_Inference_Item inferenceItem
<|> fmap II_General_Function generalFunction
-- THF & THF0:
-- <formula_item> :== <description_item> | <iquote_item>
-- <description_item> :== description(<atomic_word>)
-- <iquote_item> :== iquote(<atomic_word>)
formulaItem :: CharParser st FormulaItem
formulaItem = do
key $ tryString "description"
fmap FI_Description_Item (parentheses atomicWord)
<|> do
key $ tryString "iquote"
fmap FI_Iquote_Item (parentheses 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 = fmap II_Inference_Status inferenceStatus
<|> do
key $ tryString "assumptions"
fmap II_Assumptions_Record (parentheses (brackets nameList))
<|> do
key $ tryString "new_symbols"; oParentheses
aw <- atomicWord; comma
nsl <- brackets (sepBy1 principalSymbol comma); cParentheses
return $ II_New_Symbol_Record aw nsl
<|> do
key $ tryString "refutation"
fmap II_Refutation (parentheses 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 = do
key $ tryString "status"
fmap IS_Status (parentheses statusValue)
<|> do
ir <- try (atomicWord << oParentheses)
aw <- atomicWord; comma
gl <- generalList; cParentheses
return $ IS_Inference_Info ir aw 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 = choice $ map (\ r -> key (tryString $ showStatusValue r)
>> return r) allStatusValues
allStatusValues :: [StatusValue]
allStatusValues =
[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]
showStatusValue :: StatusValue -> String
showStatusValue = map toLower . show
formulaSelection :: CharParser st (Maybe NameList)
formulaSelection = fmap Just (comma >> brackets nameList)
<|> (notFollowedBy (char ',') >> return Nothing)
-- THF & THF0:
-- <name_list> ::= <name> | <name>,<name_list>
-- the list must mot be empty
nameList :: CharParser st NameList
nameList = sepBy1 name comma
-- THF & THF0:
-- <general_term> ::= <general_data> | <general_data>:<general_term> |
-- <general_list>
generalTerm :: CharParser st GeneralTerm
generalTerm = do
gd <- try (generalData << notFollowedBy (char ':'))
return $ GT_General_Data gd
<|> do
gd <- try (generalData << colon)
gt <- generalTerm
return $ GT_General_Data_Term gd gt
<|> fmap GT_General_List 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 = fmap GD_Variable variable
<|> fmap GD_Number number
<|> fmap GD_Distinct_Object distinctObject
<|> do
key $ tryString "bind"; oParentheses
v <- variable; comma
fd <- formulaData; cParentheses
return (GD_Bind v fd)
<|> fmap GD_General_Function generalFunction
<|> fmap GD_Atomic_Word atomicWord
<|> fmap GD_Formula_Data formulaData
-- THF & THF0:
-- <general_function> ::= <atomic_word>(<general_terms>)
-- general_terms must not be empty
generalFunction :: CharParser st GeneralFunction
generalFunction = do
aw <- atomicWord
gts <- parentheses generalTerms
return $ GF_General_Function aw 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 = fmap THF_Formula thfFormula
-- THF & THF0:
-- <general_list> ::= [] | [<general_terms>]
generalList :: CharParser st GeneralList
generalList = (try (oBracket >> cBracket) >> return [])
<|> brackets generalTerms
-- THF & THF0:
-- <general_terms> ::= <general_term> | <general_term>,<general_terms>
generalTerms :: CharParser st [GeneralTerm]
generalTerms = sepBy1 generalTerm comma
-- THF:
-- <name> ::= <atomic_word> | <integer>
--THF0:
-- <name> ::= <atomic_word> | <unsigned_integer>
name :: CharParser st Name
name = fmap T0N_Unsigned_Integer (parseToken (unsignedInteger << skipAll))
--added for thf0
<|> fmap N_Integer (integer << skipAll)
<|> fmap N_Atomic_Word atomicWord
-- THF & THF0:
-- <atomic_word> ::= <lower_word> | <single_quoted>
atomicWord :: CharParser st AtomicWord
atomicWord = fmap A_Lower_Word lowerWord
<|> fmap A_Single_Quoted singleQuoted
<?> "lowerWord or singleQuoted"
-- THF & THF0:
-- <atomic_defined_word> ::= <dollar_word>
atomicDefinedWord :: CharParser st Token
atomicDefinedWord = char '$' >> lowerWord
-- THF & THF0:
-- <atomic_system_word> ::= <dollar_dollar_word>
-- <dollar_dollar_word> ::- <dollar><dollar><lower_word>
-- <dollar> ::: [$]
atomicSystemWord :: CharParser st Token
atomicSystemWord = tryString "$$" >> 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 = fmap Num_Real (real << skipAll)
<|> fmap Num_Rational (rational << skipAll)
<|> fmap Num_Integer (integer << skipAll)
-- THF & THF0:
-- <file_name> ::= <single_quoted>
fileName :: CharParser st Token
fileName = 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 = parseToken $ do
char '\''
s <- fmap concat $ many1 (tryString "\\\\" <|> tryString "\\'"
<|> tryString "\\\'"
<|> single ( satisfy (\ c -> printable c && notElem c ['\'', '\\'])))
keyChar '\''
return 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 = parseToken $ do
char '\"'
s <- fmap concat $ many1 (tryString "\\\\" <|> tryString "\\\""
<|> single ( satisfy (\ c -> printable c && notElem c ['\'', '\\'])))
keyChar '\"'
return 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 = parseToken (do
l <- lower
an <- many (alphaNum <|> char '_'); skipAll
return (l : an)
<?> "alphanumeric word with leading lowercase letter")
printableChar :: CharParser st Char
printableChar = satisfy printable
printable :: Char -> Bool
printable c = ord c >= 32 && ord c <= 126
-- Numbers
real :: CharParser st Token
real = parseToken (try (do
s <- oneOf "-+"
ur <- unsignedReal
return (s : ur))
<|> unsignedReal
<?> "(signed) real")
unsignedReal :: CharParser st String
unsignedReal = do
de <- try (do
d <- decimalFractional <|> decimal
e <- oneOf "Ee"
return (d ++ [e]))
ex <- decimal
return (de ++ ex)
<|> decimalFractional
<?> "unsigned real"
rational :: CharParser st Token
rational = parseToken (try (do
s <- oneOf "-+"
ur <- unsignedRational
return (s : ur))
<|> unsignedRational
<?> "(signed) rational")
unsignedRational :: CharParser st String
unsignedRational = do
d1 <- try (decimal << char '/')
d2 <- positiveDecimal
return (d1 ++ "/" ++ d2)
integer :: CharParser st Token
integer = parseToken (try (do
s <- oneOf "-+"
ui <- unsignedInteger
return (s : ui))
<|> unsignedInteger
<?> "(signed) integer")
unsignedInteger :: CharParser st String
unsignedInteger = try (decimal << notFollowedBy (oneOf "eE/."))
decimal :: CharParser st String
decimal = do
char '0'
notFollowedBy digit
return "0"
<|> positiveDecimal
<?> "single zero or digits"
positiveDecimal :: CharParser st String
positiveDecimal = do
nz <- satisfy (\ c -> isDigit c && c /= '0')
d <- many digit
return (nz : d)
<?> "positiv decimal"
decimalFractional :: CharParser st String
decimalFractional = do
dec <- try (decimal << char '.')
n <- many1 digit
return (dec ++ "." ++ n)
<?> "decimal fractional"
--------------------------------------------------------------------------------
-- Some helper functions
--------------------------------------------------------------------------------
skipAll :: CharParser st ()
skipAll = skipMany (skipMany1 space <|>
((comment <|> definedComment <|>
systemComment) >> return ()))
skipSpaces :: CharParser st ()
skipSpaces = skipMany space
key :: CharParser st a -> CharParser st ()
key = (>> skipAll)
keyChar :: Char -> CharParser st ()
keyChar = key . char
myManyTill :: CharParser st a -> CharParser st a -> CharParser st [a]
myManyTill p end = do
e <- end ; return [e]
<|> do
x <- p; xs <- myManyTill p end; return (x : xs)
--------------------------------------------------------------------------------
-- Different simple symbols
--------------------------------------------------------------------------------
vLine :: CharParser st ()
vLine = keyChar '|'
star :: CharParser st ()
star = keyChar '*'
plus :: CharParser st ()
plus = keyChar '+'
arrow :: CharParser st ()
arrow = keyChar '>'
comma :: CharParser st ()
comma = keyChar ','
colon :: CharParser st ()
colon = keyChar ':'
oParentheses :: CharParser st ()
oParentheses = keyChar '('
cParentheses :: CharParser st ()
cParentheses = keyChar ')'
parentheses :: CharParser st a -> CharParser st a
parentheses p = do
r <- try (oParentheses >> p)
cParentheses
return r
oBracket :: CharParser st ()
oBracket = keyChar '['
cBracket :: CharParser st ()
cBracket = keyChar ']'
brackets :: CharParser st a -> CharParser st a
brackets p = do
r <- try (oBracket >> p)
cBracket
return r
ampersand :: CharParser st ()
ampersand = keyChar '&'
at :: CharParser st ()
at = keyChar '@'
gentzenArrow :: CharParser st ()
gentzenArrow = key $ string "-->"