Lexer_CLIF.hs revision f421deecab114bd770fbe1397140fea91189525b
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Parser of common logic interchange format
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederCopyright : (c) Karl Luc, DFKI Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : kluc@informatik.uni-bremen.de
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederStability : provisional
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiParser of common logic interchange format
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- Ref. Common Logic ISO/IEC IS 24707:2007(E)
75eb4b8bca5dc18a680471287ebe996d908ae5ccChristian Maederimport qualified Common.Lexer as Lexer
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Text.ParserCombinators.Parsec as Parsec
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederpToken :: CharParser st String -> CharParser st Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederpToken p = Lexer.pToken p << many white
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederoParenT :: CharParser st Token
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian MaederoParenT = Lexer.oParenT << many white
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedercParenT :: CharParser st Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedercParenT = Lexer.cParenT << many white
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederquotedstring :: CharParser st String
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederquotedstring = do
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder c1 <- char '\''
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder s <- many (satisfy clLetters2 <|> oneOf (whitec ++ "()\""))
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder <?> "quotedstring: word"
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder c2 <- char '\''
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder return $ c1 : s ++ [c2]
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederenclosedname :: CharParser st String
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederenclosedname = do
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder c1 <- char '\"'
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder s <- many (satisfy clLetters2 <|> oneOf (whitec ++ "@()'"))
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder c2 <- char '\"' <?> "\""
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder return $ c1 : s ++ [c2]
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder-- | parser for parens
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederparens :: CharParser st a -> CharParser st a
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederparens p = oParenT >> p << cParenT
a008ea3d3b5667969f058f75e9919f9b9c26260fChristian Maeder-- Parser Keywords
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederandKey :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederandKey = pToken (string andS) <?> "conjunction"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedernotKey :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedernotKey = pToken (string notS) <?> "negation"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederorKey :: CharParser st Id.Token
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederorKey = pToken (string orS) <?> "disjunction"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederifKey :: CharParser st Id.Token
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederifKey = pToken (string ifS) <?> "implication"
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederiffKey :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederiffKey = pToken (string iffS) <?> "equivalence"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederforallKey :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederforallKey = pToken (string forallS) <?> "universal quantification"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederexistsKey :: CharParser st Id.Token
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederexistsKey = pToken (string existsS) <?> "existential quantification"
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederthatKey :: CharParser st Id.Token
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederthatKey = pToken (string "that") <?> "\"that\" term"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederclTextKey :: CharParser st Id.Token
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclTextKey = pToken (try (string "cl-text") <|> string "cl:text") <?> "text"
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclModuleKey :: CharParser st Id.Token
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederclModuleKey = pToken (try (string "cl-module") <|> string "cl:module")
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclImportsKey :: CharParser st Id.Token
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederclImportsKey = pToken (try (string "cl-imports") <|> string "cl:imports")
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder <?> "importation"
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclExcludesKey :: CharParser st Id.Token
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederclExcludesKey = pToken (try (string "cl-excludes") <|> string "cl:excludes")
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder <?> "exclusion list"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederclEqualsKey :: CharParser st Id.Token
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclEqualsKey = pToken (string "=") <?> "equation"
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian MaederclCommentKey :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederclCommentKey = pToken (try (string "cl-comment") <|> string "cl:comment")
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder <?> "comment"
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclRolesetKey :: CharParser st Id.Token
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclRolesetKey = pToken (string "cl-roleset" <|> string "roleset:") <?> "roleset"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederclPrefixKey :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederclPrefixKey = pToken (string "cl-prefix") <?> "prefix"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederseqmark :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederseqmark = pToken (reserved reservedelement2 scanSeqMark) <?> "sequence marker"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederidentifier :: CharParser st Id.Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederidentifier = pToken (reserved reservedelement scanClWord) <?> "name"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederscanSeqMark :: CharParser st String
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederscanSeqMark = do
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder sq <- string "..."
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder w <- many clLetter <?> "sequence marker"
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder return $ sq ++ w
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederscanClWord :: CharParser st String
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederscanClWord = quotedstring <|> enclosedname <|> (many1 clLetter <?> "words")
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclLetters :: Char -> Bool
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederclLetters ch = let c = ord ch in
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder c >= 33 && c <= 126 && (c <= 38 && c /= 34
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder || c >= 42 && c /= 64 && c /= 92)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederclLetters2 :: Char -> Bool
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederclLetters2 ch = let c = ord ch in
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder (c >= 32 && c <= 126 && (c <= 38 && c /= 34
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder || c >= 42 && c /= 64 && c /= 92)) || c >= 128
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder-- a..z, A..z, 0..9, ~!#$%^&*_+{}|:<>?`-=[];,.
eed6203a39f88e398d86431a66d367036a3d17baChristian MaederclLetter :: CharParser st Char
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederclLetter = satisfy clLetters <?> "cl letter"
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederreservedelement :: [String]
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maederreservedelement = ["=", "and", "or", "iff", "if", "forall", "exists", "not"
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder , "that", "...", "cl:text", "cl:imports", "cl:excludes"
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder , "cl:module", "cl:comment", "roleset:"] ++ reservedcl
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederreservedcl :: [String]
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederreservedcl = ["cl-text", "cl-imports", "cl-excludes", "cl-module"
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , "cl-comment", "cl-roleset"]
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian Maeder-- reserved elements for sequence marker
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maederreservedelement2 :: [String]
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maederreservedelement2 = ["=", "and", "or", "iff", "if", "forall", "exists", "not"
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian Maeder , "that", "cl:text", "cl:imports", "cl:excludes", "cl:module"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder , "cl:comment", "roleset:"]
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedercommentBlockOpen :: String
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedercommentBlockOpen = "/*"
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaedercommentBlockClose :: String
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaedercommentBlockClose = "*/"
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaedercommentLineStart :: String
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaedercommentLineStart = "//"
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaedernewLinec :: String
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaedernewLinec = "\n\r"
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maederwhitec :: String
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maederwhitec = newLinec ++ "\t\v\f "
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaederwhiteSpace :: CharParser st String
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaederwhiteSpace = many1 $ oneOf whitec
35c791e6c59ef269ec639360dc94943e264d3ad1Christian MaedercommentBlock :: CharParser st String
a3000204685374be86c84d76323d95d86e4735acChristian MaedercommentBlock =
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder string commentBlockOpen >> manyTill anyChar (try $ string commentBlockClose)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedercommentLine :: CharParser st String
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder string commentLineStart >> many (noneOf newLinec) <?> ""
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maederwhite :: CharParser st String
a3000204685374be86c84d76323d95d86e4735acChristian Maeder try commentLine