{- |

Module : ./CommonLogic/Lexer_CLIF.hs

Description : Parser of common logic interchange format

Copyright : (c) Karl Luc, DFKI Bremen 2010

License : GPLv2 or higher

Maintainer : kluc@informatik.uni-bremen.de

Stability : provisional

Portability : portable

Parser of common logic interchange format

-}

-- Ref. Common Logic ISO/IEC IS 24707:2007(E)

module CommonLogic.Lexer_CLIF where

import CommonLogic.AS_CommonLogic

import Common.Id as Id

import qualified Common.Lexer as Lexer

import Common.Parsec

import Common.Keywords

import Text.ParserCombinators.Parsec as Parsec

import Data.Char (ord)

pToken :: CharParser st String -> CharParser st Token

pToken p = Lexer.pToken p << many white

oParenT :: CharParser st Token

oParenT = Lexer.oParenT << many white

cParenT :: CharParser st Token

cParenT = Lexer.cParenT << many white

quotedstring :: CharParser st String

quotedstring = do

c1 <- char '\''

s <- many (satisfy clLetters2 <|> oneOf (whitec ++ "()\""))

<?> "quotedstring: word"

c2 <- char '\''

many white

return $ c1 : s ++ [c2]

enclosedname :: CharParser st String

enclosedname = do

c1 <- char '\"'

s <- many (satisfy clLetters2 <|> oneOf (whitec ++ "@()'"))

<?> "word"

c2 <- char '\"' <?> "\""

many white

return $ c1 : s ++ [c2]

-- | parser for parens

-- Note that these use different oParenT and cParenT from the ones in

-- Common.Lexer to skip whitespaces and comments.

parens :: CharParser st a -> CharParser st a

parens p = oParenT >> p << cParenT

-- Parser Keywords

andKey :: CharParser st Id.Token

andKey = pToken (string andS) <?> "conjunction"

notKey :: CharParser st Id.Token

notKey = pToken (string notS) <?> "negation"

orKey :: CharParser st Id.Token

orKey = pToken (string orS) <?> "disjunction"

ifKey :: CharParser st Id.Token

ifKey = pToken (string ifS) <?> "implication"

iffKey :: CharParser st Id.Token

iffKey = pToken (string iffS) <?> "equivalence"

forallKey :: CharParser st Id.Token

forallKey = pToken (string forallS) <?> "universal quantification"

existsKey :: CharParser st Id.Token

existsKey = pToken (string existsS) <?> "existential quantification"

thatKey :: CharParser st Id.Token

thatKey = pToken (string "that") <?> "\"that\" term"

-- cl keys

clTextKey :: CharParser st Id.Token

clTextKey = pToken (try (string "cl-text") <|> string "cl:text") <?> "text"

clModuleKey :: CharParser st Id.Token

clModuleKey = pToken (try (string "cl-module") <|> string "cl:module")

<?> "module"

clImportsKey :: CharParser st Id.Token

clImportsKey = pToken (try (string "cl-imports") <|> string "cl:imports")

<?> "importation"

clExcludesKey :: CharParser st Id.Token

clExcludesKey = pToken (try (string "cl-excludes") <|> string "cl:excludes")

<?> "exclusion list"

clEqualsKey :: CharParser st Id.Token

clEqualsKey = pToken (string "=") <?> "equation"

clCommentKey :: CharParser st Id.Token

clCommentKey = pToken (try (string "cl-comment") <|> string "cl:comment")

<?> "comment"

clRolesetKey :: CharParser st Id.Token

clRolesetKey = pToken (string "cl-roleset" <|> string "roleset:") <?> "roleset"

clPrefixKey :: CharParser st Id.Token

clPrefixKey = pToken (string "cl-prefix") <?> "prefix"

seqmark :: CharParser st Id.Token

seqmark = pToken (reserved reservedelement2 scanSeqMark) <?> "sequence marker"

identifier :: CharParser st Id.Token

identifier = pToken (reserved reservedelement scanClWord) <?> "name"

scanSeqMark :: CharParser st String

scanSeqMark = do

sq <- string "..."

w <- many clLetter <?> "sequence marker"

return $ sq ++ w

scanClWord :: CharParser st String

scanClWord = quotedstring <|> enclosedname <|> (many1 clLetter <?> "words")

clLetters :: Char -> Bool

clLetters ch = let c = ord ch in

c >= 33 && c <= 126 && (c <= 38 && c /= 34

|| c >= 42 && c /= 64 && c /= 92)

clLetters2 :: Char -> Bool

clLetters2 ch = let c = ord ch in

(c >= 32 && c <= 126 && (c <= 38 && c /= 34

|| c >= 42 && c /= 64)) || c >= 128

-- a..z, A..z, 0..9, ~!#$%^&*_+{}|:<>?`-=[];,.

clLetter :: CharParser st Char

clLetter = satisfy clLetters <?> "cl letter"

reservedelement :: [String]

reservedelement = ["=", "and", "or", "iff", "if", "forall", "exists", "not"

, "that", "...", "cl:text", "cl:imports", "cl:excludes"

, "cl:module", "cl:comment", "roleset:"] ++ reservedcl

reservedcl :: [String]

reservedcl = ["cl-text", "cl-imports", "cl-excludes", "cl-module"

, "cl-comment", "cl-roleset"]

-- reserved elements for sequence marker

reservedelement2 :: [String]

reservedelement2 = ["=", "and", "or", "iff", "if", "forall", "exists", "not"

, "that", "cl:text", "cl:imports", "cl:excludes", "cl:module"

, "cl:comment", "roleset:"]

commentBlockOpen :: String

commentBlockOpen = "/*"

commentBlockClose :: String

commentBlockClose = "*/"

commentLineStart :: String

commentLineStart = "//"

newLinec :: String

newLinec = "\n\r"

whitec :: String

whitec = newLinec ++ "\t\v\f "

whiteSpace :: CharParser st String

whiteSpace = many1 $ oneOf whitec

commentBlock :: CharParser st String

commentBlock =

string commentBlockOpen >> manyTill anyChar (try $ string commentBlockClose)

<?> ""

commentLine :: CharParser st String

commentLine =

string commentLineStart >> many (noneOf newLinec) <?> ""

white :: CharParser st String

white =

whiteSpace

<|>

try commentLine

<|>

commentBlock