7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder{- |

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : parser for CASL (heterogeneous) structured specifications

7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederCopyright : (c) Till Mossakowski, Christian Maeder, Uni Bremen 2002-2005

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : Christian.Maeder@dfki.de

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable(Grothendieck)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiParser for CASL (heterogeneous) structured specifications

679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski Concerning the homogeneous syntax, this follows Sect II:3.1.3

679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski of the CASL Reference Manual.

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-}

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maedermodule Syntax.Parse_AS_Structured

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder ( annoParser2

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder , caslGroupSpec

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , groupSpec

fa1efeb55163f27f261d22a9062fbc25ab4d8d52Michael Chan , aSpec

fa1efeb55163f27f261d22a9062fbc25ab4d8d52Michael Chan , qualification

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder , parseMapping

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder , parseCorrespondences

f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowski , translationList

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian Maeder , renaming

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder , restriction

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder , hetIRI

d420c2a27c4dfa0a9c8031449db2e1a89ad2cc3aChristian Maeder ) where

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Logic.Logic

cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maederimport Logic.Comorphism

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederimport Logic.Grothendieck

c208973c890b8f993297720fd0247bc7481d4304Christian Maederimport Logic.KnownIris

ec25781c1180ea07f66b48c34f93cf5634e9277cChristian Maeder

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maederimport Syntax.AS_Structured

e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maederimport Common.AS_Annotation

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Common.AnnoState

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettichimport Common.AnnoParser

78efc385d85998e49a363929b2d1016e37835b6dChristian Maederimport Common.Id

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maederimport Common.IRI

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Common.Keywords

56cd0da55d058b262b1626ddcd78db6bd9a90551Christian Maederimport Common.Lexer

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maederimport Common.Parsec

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maederimport Common.Token

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maederimport Text.ParserCombinators.Parsec

d5a8d891500a642ce629854857fc00b7c21aec47Christian Maeder

1b9ecb3b9c41106d0c90dcdb731b360eb5240c33Christian Maederimport Data.Char

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Data.Maybe

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederimport Control.Monad

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian MaederexpandCurieM :: LogicGraph -> IRI -> GenParser Char st IRI

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederexpandCurieM lG i =

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder case expandCurie (prefixes lG) i of

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder Just ei -> return ei

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Nothing -> if isSimple i

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder then return i

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder else fail $ "could not expand IRI " ++ show i

b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederexpandCurieMConservative :: LogicGraph -> IRI -> GenParser Char st IRI

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederexpandCurieMConservative lG i = if isSimple i then return i

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder else expandCurieM lG i

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederhetIRI :: LogicGraph -> GenParser Char st IRI

99d38db8cb1b6528b5ee07e06507d7a7b3ef2fdeChristian MaederhetIRI lG = try $ do

c4040537e6f2153af475dd8b07260a1ee9a56ac0Christian Maeder i <- iriCurie

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder skipSmart

b0294d73dcefc502ddaa13e18b46103a5916971fTill Mossakowski if iriToStringUnsecure i `elem`

53a877c93b93d82cffe0f1977b5bf757ed84f9a5Mihai Codescu (casl_reserved_words ++ casl_reserved_fops ++ map (: []) ")(,|;")

8a4ad94c497663adf4d1ee03f8352534faa23323Kristina Sojakova then unexpected $ show i

f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova else expandCurieM lG i

f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder-- | parse annotations and then still call an annotation parser

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederannoParser2 :: AParser st (Annoted a) -> AParser st (Annoted a)

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian MaederannoParser2 =

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder liftM2 (\ x (Annoted y pos l r) -> Annoted y pos (x ++ l) r) annos

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder-- * logic and encoding names

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder-- within sublogics we allow some further symbol characters

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaedersublogicChars :: AParser st String

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaedersublogicChars = many $ satisfy $ \ c -> notElem c ":./\\" && isSignChar c

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder || elem c "_'" || isAlphaNum c

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder

acc358348c23ba8b7a0c58aff12c49c947b01825Christian MaederlookupLogicM :: IRI -> AParser st String

acc358348c23ba8b7a0c58aff12c49c947b01825Christian MaederlookupLogicM i = if isSimple i

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder then return l

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder else case lookupLogicName l of

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder Just s -> return s

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder Nothing -> fail $ "logic " ++ show i ++ " not found"

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder where l = iriToStringUnsecure i

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder

f39c70229e74147a02d15bd45c05a0b1b325532dChristian Maeder{- keep these identical in order to

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowskidecide after seeing ".", ":" or "->" what was meant -}

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian MaederlogicName :: LogicGraph -> AParser st Logic_name

f39c70229e74147a02d15bd45c05a0b1b325532dChristian MaederlogicName l = do

b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder i <- iriCurie >>= expandCurieMConservative l

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder let (ft, rt) = if isSimple i

c74fa53dd2c397e85d995f71380e2bab60b619ccChristian Maeder then break (== '.') $ abbrevPath i -- HetCASL

dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maeder else (abbrevPath i, [])

1b9ecb3b9c41106d0c90dcdb731b360eb5240c33Christian Maeder (e, ms) <- if null rt then return (i, Nothing)

1b9ecb3b9c41106d0c90dcdb731b360eb5240c33Christian Maeder else do

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder s <- sublogicChars -- try more sublogic characters

94c729aeac99df6d844da014f46d584c035a91a6Christian Maeder return (i { abbrevPath = ft}, Just . mkSimpleId $ tail rt ++ s)

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder skipSmart

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder -- an optional spec name for a sublogic based on a theory #171

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder mt <- optionMaybe

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder $ oParenT >> (iriCurie >>= expandCurieMConservative l) << cParenT

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder lo <- lookupLogicM e

99d38db8cb1b6528b5ee07e06507d7a7b3ef2fdeChristian Maeder return $ Logic_name lo ms mt

53a877c93b93d82cffe0f1977b5bf757ed84f9a5Mihai Codescu

53a877c93b93d82cffe0f1977b5bf757ed84f9a5Mihai Codescuqualification :: LogicGraph -> AParser st (Token, LogicDescr)

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maederqualification l =

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder pair (asKey logicS) (logicDescr l)

1b14aa136f3eb64b421dc610e46072aefcbd7c9fKristina Sojakova <|> do

1b14aa136f3eb64b421dc610e46072aefcbd7c9fKristina Sojakova s <- asKey serializationS <|> asKey "language"

1b14aa136f3eb64b421dc610e46072aefcbd7c9fKristina Sojakova i <- iriCurie

54d25074b7ddc5534322f0627e54a51e66568c14Christian Maeder skipSmart

d5a8d891500a642ce629854857fc00b7c21aec47Christian Maeder return (s,

f0e85ee7e4accfc01f46aa0363acc59fcd248e8aTill Mossakowski (if tokStr s == serializationS then SyntaxQual else LanguageQual) i)

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian MaederlogicDescr :: LogicGraph -> AParser st LogicDescr

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederlogicDescr l = do

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder n@(Logic_name ln _ _) <- logicName l

429df04296fa571432f62cbfad6855e1420e0fd6Christian Maeder option (nameToLogicDescr n) $ do

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder r <- asKey serializationS

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder sp <- sneakAhead iriCurie

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder case sp of

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder Left _ -> iriCurie >> error "logicDescr" -- reproduce the error

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder Right s -> do

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder s' <- if isSimple s then return s else expandCurieMConservative l s

d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder let ld = LogicDescr n (Just s') $ tokPos r

acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder (Logic lid, sm) <- lookupCurrentSyntax "logicDescr" $ setLogicName ld l

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz case basicSpecParser sm lid of

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz Just _ -> iriCurie >> skipSmart >> return ld -- consume and return

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz Nothing -> unexpected ("serialization \"" ++ show s

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz ++ "\" for logic " ++ show ln)

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz <|> choice (map (\ pn -> pzero <?> '"' : pn ++ "\"")

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz (filter (not . null)

4d886fa3abade88e5e1c0a5b20980b1ede3d05b1Christian Maeder (basicSpecSyntaxes lid)))

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz-- * parse Logic_code

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst SchulzparseLogic :: String -> LogicGraph -> AParser st (Logic_code, LogicGraph)

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst SchulzparseLogic altKw lG = do

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz lc <- parseLogicAux altKw lG

4d886fa3abade88e5e1c0a5b20980b1ede3d05b1Christian Maeder case lc of

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz Logic_code _ _ (Just l) _ ->

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder return (lc, setLogicName (nameToLogicDescr l) lG)

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder Logic_code (Just c) _ _ _ -> do

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder nLg <- lookupAndSetComorphismName c lG

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder return (lc, nLg)

4cbba4634ba267c438f75fa7a5009f6249d3dda1Christian Maeder _ -> return (lc, lG)

4d886fa3abade88e5e1c0a5b20980b1ede3d05b1Christian Maeder

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederparseLogicAux :: String -> LogicGraph -> AParser st Logic_code

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederparseLogicAux altKw lG =

429df04296fa571432f62cbfad6855e1420e0fd6Christian Maeder do l <- asKey logicS <|> asKey altKw

55e1458efb5b53c71df7d3263f5d7fae04503619Christian Maeder do

55e1458efb5b53c71df7d3263f5d7fae04503619Christian Maeder f <- asKey funS -- parse at least a logic target after "logic"

55e1458efb5b53c71df7d3263f5d7fae04503619Christian Maeder t <- logicName lG

55e1458efb5b53c71df7d3263f5d7fae04503619Christian Maeder return $ Logic_code Nothing Nothing (Just t)

99d38db8cb1b6528b5ee07e06507d7a7b3ef2fdeChristian Maeder $ tokPos l `appRange` tokPos f

99d38db8cb1b6528b5ee07e06507d7a7b3ef2fdeChristian Maeder <|> do

df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder e <- logicName lG

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder -- try to parse encoding or logic source after "logic"

e97bcfa4f74907e1a5ccfc3bc1509d1849cda603Christian Maeder case e of

2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder Logic_name f Nothing Nothing ->

df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder do c <- colonT

0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder parseLogAfterColon lG (Just f) [l, c]

2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder <|> parseOptLogTarget lG Nothing (Just e) [l]

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder <|> return (Logic_code (Just f) Nothing Nothing

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski $ tokPos l)

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder _ -> parseOptLogTarget lG Nothing (Just e) [l]

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder-- parse optional logic source and target after a colon (given an encoding e)

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian MaederparseLogAfterColon :: LogicGraph -> Maybe String -> [Token]

89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder -> AParser st Logic_code

b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederparseLogAfterColon lG e l = parseOptLogTarget lG e Nothing l

89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder <|>

42972ddff400840d46eb54422b60083228b2996cChristian Maeder do s <- logicName lG

b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder parseOptLogTarget lG e (Just s) l

bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder <|> return (Logic_code e (Just s) Nothing $ catRange l)

bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder

44afe69b6b3cc7314ef270e125196127777c6c87Christian Maeder-- parse an optional logic target (given encoding e or source s)

44afe69b6b3cc7314ef270e125196127777c6c87Christian MaederparseOptLogTarget :: LogicGraph -> Maybe String -> Maybe Logic_name -> [Token]

44afe69b6b3cc7314ef270e125196127777c6c87Christian Maeder -> AParser st Logic_code

f39c70229e74147a02d15bd45c05a0b1b325532dChristian MaederparseOptLogTarget lG e s l =

bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder do f <- asKey funS

bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder let p = catRange $ l ++ [f]

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder do t <- logicName lG

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder return (Logic_code e s (Just t) p)

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder <|> return (Logic_code e s Nothing p)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederplainComma :: AParser st Token

be8b8876edf3d7138ddd39a4ec07d857dde5bbb5Christian MaederplainComma = anComma `notFollowedWith` asKey logicS

be8b8876edf3d7138ddd39a4ec07d857dde5bbb5Christian Maeder

be8b8876edf3d7138ddd39a4ec07d857dde5bbb5Christian Maeder-- * parse G_mapping

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaedercallSymParser :: Bool -> Maybe (AParser st a) -> String -> String ->

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder AParser st ([a], [Token])

7f7460e7095628f3437b116ee78d3043d11f8febChristian MaedercallSymParser oneOnly p name itemType = case p of

be8b8876edf3d7138ddd39a4ec07d857dde5bbb5Christian Maeder Nothing ->

a55b09f4ef6e58ad617b59899d93c63bb4d6f287Christian Maeder fail $ "no symbol" ++ itemType ++ " parser for language " ++ name

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder Just pa -> if oneOnly then do

b83ff3749d99d03b641adee264b781039a551addChristian Maeder s <- pa

4cbba4634ba267c438f75fa7a5009f6249d3dda1Christian Maeder return ([s], [])

7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder else separatedBy pa plainComma

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder

17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian MaederparseItemsMap :: AnyLogic -> AParser st (G_symb_map_items_list, [Token])

17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian MaederparseItemsMap (Logic lid) = do

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder (cs, ps) <- callSymParser False (parse_symb_map_items lid)

f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder (language_name lid) " maps"

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder return (G_symb_map_items_list lid cs, ps)

f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder

4b0e0613129ebfc53e3e87985c20a537da91d18dChristian Maeder

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederparseMapping :: LogicGraph -> AParser st ([G_mapping], [Token])

17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian MaederparseMapping =

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder parseMapOrHide "translation" G_logic_translation G_symb_map parseItemsMap

2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederparseMapOrHide :: String -> (Logic_code -> a) -> (t -> a)

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder -> (AnyLogic -> AParser st (t, [Token])) -> LogicGraph

2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder -> AParser st ([a], [Token])

2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederparseMapOrHide altKw constrLogic constrMap pa lG =

26ed2a19326560786ff94dfc462309d6d5d862a8Heng Jiang do (n, nLg) <- parseLogic altKw lG

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder do optional anComma

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder (gs, ps) <- parseMapOrHide altKw constrLogic constrMap pa nLg

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder return (constrLogic n : gs, ps)

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder <|> return ([constrLogic n], [])

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder <|> do

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder l <- lookupCurrentLogic "parseMapOrHide" lG

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder (m, ps) <- pa l

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder do optional anComma

df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder (gs, qs) <- parseMapOrHide altKw constrLogic constrMap pa lG

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder return (constrMap m : gs, ps ++ qs)

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder <|> return ([constrMap m], ps)

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder

74b841a4b332085d5fd79975a13313c2681ae595Christian Maeder-- * parse G_hiding

a765ab85cf4bffb8216ebe9a9ed4ffaf7ee61a18Mihai Codescu

a765ab85cf4bffb8216ebe9a9ed4ffaf7ee61a18Mihai CodescuparseItemsList :: AnyLogic -> AParser st (G_symb_items_list, [Token])

df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian MaederparseItemsList (Logic lid) = do

df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder (cs, ps) <- callSymParser False (parse_symb_items lid)

df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder (language_name lid) ""

eb7c2e900fad04edc597cc832ffc46c4494ea142Christian Maeder return (G_symb_items_list lid cs, ps)

0155c8d32b79581866f07cc593aa8a4c722ceef2Christian Maeder

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederparseSingleSymb :: AnyLogic -> AParser st (G_symb_items_list, [Token])

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederparseSingleSymb (Logic lid) = do

0155c8d32b79581866f07cc593aa8a4c722ceef2Christian Maeder (cs, ps) <- callSymParser True (parseSingleSymbItem lid)

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (language_name lid) ""

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder return (G_symb_items_list lid cs, ps)

78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder

78efc385d85998e49a363929b2d1016e37835b6dChristian MaederparseHiding :: LogicGraph -> AParser st ([G_hiding], [Token])

78efc385d85998e49a363929b2d1016e37835b6dChristian MaederparseHiding =

78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder parseMapOrHide "along" G_logic_projection G_symb_list parseItemsList

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder-- * specs

4b0e0613129ebfc53e3e87985c20a537da91d18dChristian Maeder

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder-- "then" is associative, therefore flatten extensions

4b0e0613129ebfc53e3e87985c20a537da91d18dChristian Maeder

aeb4e74b8b3328d8ea15512ec4e1e1b8d0919f01Christian MaederflatExts :: [Annoted SPEC] -> [Annoted SPEC]

78efc385d85998e49a363929b2d1016e37835b6dChristian MaederflatExts = concatMap $ \ as -> case item as of

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder Extension sps _ -> sps

7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder Group sp _ -> case flatExts [sp] of

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder [_] -> [as]

78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder sps -> sps

78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder _ -> [as]

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder

948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maederspec :: LogicGraph -> AParser st (Annoted SPEC)

948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maederspec l = do

1e3950d5c1f0e041dd7677856e43f07796567d5bChristian Maeder sp1 <- annoParser2 (specThen l)

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder option sp1 $ do

948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder k <- asKey "bridge"

89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder rs <- many (renaming l)

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder sp2 <- annoParser2 (specThen l)

89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder return . emptyAnno . Bridge sp1 rs sp2 $ tokPos k

1e3950d5c1f0e041dd7677856e43f07796567d5bChristian Maeder

89ab08979dc23d72e9e09c8990a8c44847041d6fChristian MaederspecThen :: LogicGraph -> AParser st (Annoted SPEC)

89ab08979dc23d72e9e09c8990a8c44847041d6fChristian MaederspecThen l = do

f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder (sps, ps) <- annoParser2 (specA l) `separatedBy` asKey thenS

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder return $ case sps of

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder [sp] -> sp

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder _ -> emptyAnno (Extension (flatExts sps) $ catRange ps)

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian MaederspecA :: LogicGraph -> AParser st (Annoted SPEC)

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian MaederspecA l = do

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder (sps, ps) <- annoParser2 (specB l) `separatedBy` asKey andS

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder return $ case sps of

1f315f2e146d15c0aec01f7ae076708bbac29796Christian Maeder [sp] -> sp

ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder _ -> emptyAnno (Union sps $ catRange ps)

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian MaederspecB :: LogicGraph -> AParser st (Annoted SPEC)

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian MaederspecB l = do

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder p1 <- asKey localS

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder sp1 <- aSpec l

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder p2 <- asKey withinS

3bcf8bbafdda23d3c6be2deec9e68f98223b78c1Christian Maeder sp2 <- annoParser2 $ specB l

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder return (emptyAnno $ Local_spec sp1 sp2 $ tokPos p1 `appRange` tokPos p2)

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder <|> specC l

3bcf8bbafdda23d3c6be2deec9e68f98223b78c1Christian Maeder

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian MaederspecC :: LogicGraph -> AParser st (Annoted SPEC)

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian MaederspecC lG = do

f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder let spD = annoParser $ specD lG

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder rest = spD >>= translationList

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder [ (`fmap` extraction lG) . Extraction

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder , (`fmap` renaming lG) . Translation

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder , (`fmap` restriction lG) . Reduction

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder , (`fmap` approximation lG) . Approximation

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder , (`fmap` minimization lG) . Minimization]

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder l@(Logic lid) <- lookupCurrentLogic "specC" lG

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder {- if the current logic has an associated data_logic,

54d25074b7ddc5534322f0627e54a51e66568c14Christian Maeder parse "data SPEC1 SPEC2", where SPEC1 is in the data_logic

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder SPEC1 needs to be a basic spec or a grouped spec

4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder SPEC2 is in the currrent logic -}

4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder case data_logic lid of

4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder Nothing -> rest

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder Just lD@(Logic dl) -> do

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder p1 <- asKey dataS -- not a keyword

5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder sp1 <- annoParser $ basicSpec lG (lD, Nothing)

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder <|> caslGroupSpec (setCurLogic (language_name dl) lG)

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder sp2 <- spD

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder return (emptyAnno $ Data lD l sp1 sp2 $ tokPos p1)

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder <|> rest

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder

54d25074b7ddc5534322f0627e54a51e66568c14Christian MaedertranslationList :: [Annoted b -> AParser st b] -> Annoted b

54d25074b7ddc5534322f0627e54a51e66568c14Christian Maeder -> AParser st (Annoted b)

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai CodescutranslationList cs sp =

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu do sp' <- choice $ map ($ sp) cs

32647be84c5f21615df50b202bb0ea689e65500cMihai Codescu translationList cs (emptyAnno sp')

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu <|> return sp

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder{- | Parse renaming

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder@

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian MaederRENAMING ::= with SYMB-MAP-ITEMS-LIST

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder@

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian MaederSYMB-MAP-ITEMS-LIST is parsed using parseMapping -}

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maederrenaming :: LogicGraph -> AParser st RENAMING

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maederrenaming l =

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder do kWith <- asKey withS

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder (mappings, commas) <- parseMapping l

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder return (Renaming mappings $ catRange $ kWith : commas)

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder{- | Parse restriction

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder@

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai CodescuRESTRICTION ::= hide SYMB-ITEMS-LIST

32647be84c5f21615df50b202bb0ea689e65500cMihai Codescu | reveal SYMB-MAP-ITEMS-LIST

32647be84c5f21615df50b202bb0ea689e65500cMihai Codescu@

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian MaederSYMB-ITEMS-LIST is parsed using parseHiding; SYMB-MAP-ITEMS-LIST is

3b6782384a88e4b6aa95eca12355278fa22cbb58Mihai Codescuparsed using parseItemsMap -}

23a0c19ea8d6075fc765c64a20c70b119434823aMihai Codescurestriction :: LogicGraph -> AParser st RESTRICTION

54d25074b7ddc5534322f0627e54a51e66568c14Christian Maederrestriction lg =

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu -- hide

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder do kHide <- asKey hideS

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder (symbs, commas) <- parseHiding lg

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder return (Hidden symbs (catRange (kHide : commas)))

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder <|> -- reveal

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder do kReveal <- asKey revealS

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu nl <- lookupCurrentLogic "reveal" lg

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (mappings, commas) <- parseItemsMap nl

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu return (Revealed mappings (catRange (kReveal : commas)))

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder-- | Parse approximation

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maederapproximation :: LogicGraph -> AParser st APPROXIMATION

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maederapproximation lg =

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder do p1 <- asKey "forget" <|> asKey "keep"

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder (hs, _) <- parseHiding lg

b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder li <- optionMaybe $ asKey withS >> hetIRI lg

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder return $ ForgetOrKeep (tokStr p1 /= "keep") hs li $ tokPos p1

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maederminimization :: LogicGraph -> AParser st MINIMIZATION

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maederminimization lg = do

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder p <- minimizeKey <|> asKey freeS <|> asKey cofreeS

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (cm) <- many1 (hetIRI lg)

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu (cv, p2) <- option ([], []) $ do

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu p3 <- asKey varsS

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu ct <- many1 (hetIRI lg)

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder return (ct, [p3])

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder return . Mini p cm cv . catRange $ p : p2

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maederextraction :: LogicGraph -> AParser st EXTRACTION

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maederextraction lg = do

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder p <- asKey "extract" <|> asKey "remove"

78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder is <- many1 (hetIRI lg)

78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder return . ExtractOrRemove (tokStr p == "extract") is $ tokPos p

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian MaedergroupSpecLookhead :: LogicGraph -> AParser st IRI

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian MaedergroupSpecLookhead lG =

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder let tok2IRI = liftM simpleIdToIRI in

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder tok2IRI oBraceT <|> followedWith (hetIRI lG << annos)

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (choice (map (tok2IRI . asKey) criticalKeywords)

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder <|> tok2IRI cBraceT <|> tok2IRI oBracketT <|> tok2IRI cBracketT

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder <|> (eof >> return nullIRI))

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian MaederminimizeKey :: AParser st Token

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian MaederminimizeKey = choice $ map asKey [minimizeS, closedworldS, "maximize"]

1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian MaederspecD :: LogicGraph -> AParser st SPEC

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder -- do some lookahead for free spec, to avoid clash with free type

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian MaederspecD l = do

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder p <- asKey freeS `followedWith` groupSpecLookhead l

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder sp <- annoParser $ groupSpec l

1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder return (Free_spec sp $ tokPos p)

1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder <|> do

1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder p <- asKey cofreeS `followedWith` groupSpecLookhead l

1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder sp <- annoParser $ groupSpec l

1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder return (Cofree_spec sp $ tokPos p)

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder <|> do

1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder p <- minimizeKey `followedWith` groupSpecLookhead l

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder sp <- annoParser $ groupSpec l

a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder return (Minimize_spec sp $ tokPos p)

8fcb35320a5bacb7a8649bd0a26d3ac1a14e2008Ewaryst Schulz <|> do

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder p <- asKey closedS `followedWith` groupSpecLookhead l

c35969f341eb137848e9c0874503bed8c419cbd2Kristina Sojakova sp <- annoParser $ groupSpec l

c35969f341eb137848e9c0874503bed8c419cbd2Kristina Sojakova return (Closed_spec sp $ tokPos p)

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder <|> specE l

429b8f515a133b86a5771f8d8f6a71a15a70a315Iulia Ignatov

429b8f515a133b86a5771f8d8f6a71a15a70a315Iulia IgnatovspecE :: LogicGraph -> AParser st SPEC

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian MaederspecE l = logicSpec l

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder <|> combineSpec l

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder <|> applySpec l

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder <|> (lookAhead (groupSpecLookhead l) >> groupSpec l)

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder <|> (lookupCurrentSyntax "basic spec" l >>= basicSpec l)

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian MaederapplySpec :: LogicGraph -> AParser st SPEC

16023c23c9d17743033afd994ad11c386d17b376Christian MaederapplySpec l = do

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder k <- asKey "apply"

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder n <- hetIRI l

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder Basic_spec bs _ <- lookupCurrentSyntax "apply spec" l >>= basicSpec l

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder return $ Apply n bs $ tokPos k

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian Maeder-- | call a logic specific parser if it exists

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaedercallParser :: Maybe (AParser st a) -> String -> String -> AParser st a

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaedercallParser p name itemType =

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder fromMaybe (unexpected $ "no " ++ itemType ++ " parser for " ++ name) p

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

3d4e57e86d8aee818b589cd1029838e0accade55Christian MaederbasicSpec :: LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC

ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian MaederbasicSpec lG (Logic lid, sm) = do

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder p <- getPos

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian Maeder bspec <- callParser

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian Maeder (liftM (\ ps -> ps (prefixes lG)) (basicSpecParser sm lid))

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (showSyntax lid sm) "basic specification"

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian Maeder q <- getPos

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder return $ Basic_spec (G_basic_spec lid bspec) $ Range [p, q]

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian MaederlogicSpec :: LogicGraph -> AParser st SPEC

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian MaederlogicSpec lG = do

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder (s1, ln) <- qualification lG

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder many $ qualification lG -- ignore multiple qualifications for now

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder s2 <- colonT

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder sp <- annoParser $ specD $ setLogicName ln lG

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder return $ Qualified_spec ln sp $ toRange s1 [] s2

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian MaedercombineSpec :: LogicGraph -> AParser st SPEC

953127f27b7854580057a92e8269fd7a8716a800Christian MaedercombineSpec lG = do

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder s1 <- asKey combineS

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder (oir, ps1) <- separatedBy (parseLabeled lG) commaT

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder (exl, ps) <- option ([], []) $ do

953127f27b7854580057a92e8269fd7a8716a800Christian Maeder s2 <- asKey excludingS

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (e, ps2) <- separatedBy (hetIRI lG) commaT

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian Maeder return (e, s2 : ps2)

ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder return $ Combination oir exl $ catRange $ s1 : ps1 ++ ps

5fe604bfecb45b5cf2a5c1db003d39d670423476Christian Maeder

d6ee14efd13f136be5a2b03b7f27dc77aa52c754Christian MaederparseLabeled :: LogicGraph -> AParser st LABELED_ONTO_OR_INTPR_REF

d6ee14efd13f136be5a2b03b7f27dc77aa52c754Christian MaederparseLabeled lG = do

d6ee14efd13f136be5a2b03b7f27dc77aa52c754Christian Maeder x <- option Nothing $ do

fb7c3ffc41767729db506ad0ac1262ecfb5febf8Christian Maeder str <- try (simpleId `followedWith` colonT)

d6ee14efd13f136be5a2b03b7f27dc77aa52c754Christian Maeder colonT

38e6a7281140deb96436868d396e1a0a3c934c2cChristian Maeder return $ Just str

8528053a6a766c3614276df0f59fb2a2e8ab6d18Christian Maeder y <- hetIRI lG

2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder return $ Labeled x y

c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederlookupAndSetComorphismName :: String -> LogicGraph -> AParser st LogicGraph

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian MaederlookupAndSetComorphismName c lg = do

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder Comorphism cid <- lookupComorphism c lg

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder return $ setCurLogic (language_name $ targetLogic cid) lg

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian MaederaSpec :: LogicGraph -> AParser st (Annoted SPEC)

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederaSpec = annoParser2 . spec

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder-- | grouped spec or spec-inst without optional DOL import

1f315f2e146d15c0aec01f7ae076708bbac29796Christian MaedercaslGroupSpec :: LogicGraph -> AParser st SPEC

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaedercaslGroupSpec = groupSpecAux False

3bcf8bbafdda23d3c6be2deec9e68f98223b78c1Christian Maeder

4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder-- | grouped spec or spec-inst with optional import

3bcf8bbafdda23d3c6be2deec9e68f98223b78c1Christian MaedergroupSpec :: LogicGraph -> AParser st SPEC

3ea571db6dd6e0c42d02de4e56648c7cd86a3734Christian MaedergroupSpec = groupSpecAux True

3ea571db6dd6e0c42d02de4e56648c7cd86a3734Christian Maeder

3ea571db6dd6e0c42d02de4e56648c7cd86a3734Christian MaedergroupSpecAux :: Bool -> LogicGraph -> AParser st SPEC

3ea571db6dd6e0c42d02de4e56648c7cd86a3734Christian MaedergroupSpecAux withImport l = do

3ea571db6dd6e0c42d02de4e56648c7cd86a3734Christian Maeder b <- oBraceT

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder do

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder c <- cBraceT

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder return $ EmptySpec $ catRange [b, c]

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder <|> do

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder a <- aSpec l

ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder c <- cBraceT

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return $ Group a $ catRange [b, c]

e5fae0f42a23c12fce5389f405659d4e5dce73a4Christian Maeder <|> do

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder n <- hetIRI l

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder (f, ps) <- fitArgs l

e5fae0f42a23c12fce5389f405659d4e5dce73a4Christian Maeder mi <- if withImport then optionMaybe (hetIRI l) else return Nothing

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder return (Spec_inst n f mi ps)

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder

16023c23c9d17743033afd994ad11c386d17b376Christian MaederfitArgs :: LogicGraph -> AParser st ([Annoted FIT_ARG], Range)

3d4e57e86d8aee818b589cd1029838e0accade55Christian MaederfitArgs l = do

5c13d1acd6298569a5574c07c833cd3fdac4ae4cChristian Maeder fas <- many (fitArg l)

89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder let (fas1, ps) = unzip fas

eb462c821104069a719090787f0f44793ba9a081Christian Maeder return (fas1, concatMapRange id ps)

eb462c821104069a719090787f0f44793ba9a081Christian Maeder

eb462c821104069a719090787f0f44793ba9a081Christian MaederfitArg :: LogicGraph -> AParser st (Annoted FIT_ARG, Range)

eb462c821104069a719090787f0f44793ba9a081Christian MaederfitArg l = do

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder b <- oBracketT

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder fa <- annoParser (fittingArg l)

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder c <- cBracketT

c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder return (fa, toRange b [] c)

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder

c35969f341eb137848e9c0874503bed8c419cbd2Kristina SojakovafittingArg :: LogicGraph -> AParser st FIT_ARG

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian MaederfittingArg l = do

c35969f341eb137848e9c0874503bed8c419cbd2Kristina Sojakova s <- asKey viewS

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder vn <- hetIRI l

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder (fa, ps) <- fitArgs l

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder return (Fit_view vn fa (tokPos s `appRange` ps))

d21dd452cd68abade683103a5c0cfe6d02c5f17bTill Mossakowski <|> do

e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder sp <- aSpec l

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder (symbit, ps) <- option ([], nullRange) $ do

16023c23c9d17743033afd994ad11c386d17b376Christian Maeder s <- asKey fitS

28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu (m, qs) <- parseMapping l

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (m, catRange $ s : qs)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder return (Fit_spec sp symbit ps)

b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder

cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maeder

c2cd56b00fe132c78b9f4f86dbc2ab757dbc59ddChristian MaederparseCorrespondences :: LogicGraph -> AParser st [CORRESPONDENCE]

84a30e66aef85cc54d3dd6f8e408729007fe8809Christian MaederparseCorrespondences l = commaSep1 $ correspondence l

cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maeder

cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maedercorrespondence :: LogicGraph -> AParser st CORRESPONDENCE

cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maedercorrespondence l = do

edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian asKey "*"

84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder return Default_correspondence

2c08058468dab64c89a8eae51b56f9afb8b6cb71Cui Jian <|> do

84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder asKey relationS

cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maeder rref <- optionMaybe $ relationRef l

84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder conf <- optionMaybe confidence

cd34f330714d6b3ef21a314ea98842c4b8c2fcedCui Jian oBraceT

37e30366abd83c00a5d5447b45694627fd783de8Cui Jian cs <- parseCorrespondences l

37e30366abd83c00a5d5447b45694627fd783de8Cui Jian cBraceT

37e30366abd83c00a5d5447b45694627fd783de8Cui Jian return $ Correspondence_block rref conf cs

37e30366abd83c00a5d5447b45694627fd783de8Cui Jian <|> do

c2cd56b00fe132c78b9f4f86dbc2ab757dbc59ddChristian Maeder (mcid, eRef, mrRef, mconf, toer) <- corr1 l

cd34f330714d6b3ef21a314ea98842c4b8c2fcedCui Jian {- trace (concat ["\t", show mcid, " \t", show eRef, "\t", show mrRef,

5efed683fd173e9d53bd5f1929ba5b0c8a228710Christian Maeder " \t", show mconf, " \t", show toer]) $ return ()

876bd2c70a93981cc80f8376284616bce4a0fefcChristian Maeder only commented out for future debugging purposes -}

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder return $ Single_correspondence mcid eRef toer mrRef mconf

fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder

5efed683fd173e9d53bd5f1929ba5b0c8a228710Christian Maedercorr1 :: LogicGraph

c2cd56b00fe132c78b9f4f86dbc2ab757dbc59ddChristian Maeder -> AParser st ( Maybe CORRESPONDENCE_ID, G_symb_items_list

2c08058468dab64c89a8eae51b56f9afb8b6cb71Cui Jian , Maybe RELATION_REF, Maybe CONFIDENCE, G_symb_items_list)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maedercorr1 l = do

2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder al <- lookupCurrentLogic "correspondence" l

54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder (eRef, _) <- parseSingleSymb al

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (mrRef, mconf, toer) <- corr2 l

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder cids <- annotations

2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder if not (null cids || null (tail cids))

ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder then fail "more than one correspondence id"

22250d2b3c9f86fe19cba665d71c301de03db142Christian Maeder else return (listToMaybe cids, eRef, mrRef, mconf, toer)

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maedercorr2 :: LogicGraph

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder -> AParser st (Maybe RELATION_REF, Maybe CONFIDENCE, G_symb_items_list)

22250d2b3c9f86fe19cba665d71c301de03db142Christian Maedercorr2 l = do

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder rRef <- optionMaybe . try $ relationRefWithLookAhead l

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder (mconf, toer) <- corr3 l

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder return (rRef, mconf, toer)

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maedercorr3 :: LogicGraph -> AParser st (Maybe CONFIDENCE, G_symb_items_list)

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maedercorr3 l = do

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder al <- lookupCurrentLogic "corr3" l

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder conf <- optionMaybe $ try confidence

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder (sym, _) <- parseSingleSymb al

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder return (conf, sym)

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder

3d4e57e86d8aee818b589cd1029838e0accade55Christian MaederrelationRefWithLookAhead :: LogicGraph -> AParser st RELATION_REF

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederrelationRefWithLookAhead lG = do

7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder r <- relationRef lG

3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder lookAhead (confidenceBegin >> return nullIRI)

22250d2b3c9f86fe19cba665d71c301de03db142Christian Maeder <|> lookAhead (try $ hetIRI lG)

22250d2b3c9f86fe19cba665d71c301de03db142Christian Maeder return r

7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder

relationRef :: LogicGraph -> AParser st RELATION_REF

relationRef lG = ((do

asKey ">"

return Subsumes

<|> do

asKey "<"

return IsSubsumed

<|> do

asKey "="

return Equivalent

<|> do

asKey "%"

return Incompatible

<|> do

try $ asKey "$\\ni$"

return HasInstance

<|> do

try $ asKey "$\\in$"

return InstanceOf

<|> do

asKey "$\\mapsto$"

return DefaultRelation

) << skipSmart)

<|> do

i <- hetIRI lG

return $ Iri i

confidenceBegin :: AParser st Char

confidenceBegin = char '('

confidence :: AParser st Double

confidence = char '(' >> confidenceNumber << char ')' << skipSmart

confidenceNumber :: AParser st Double

confidenceNumber = do

d1 <- char '0'

option 0 $ do

d2 <- char '.'

ds <- many digit

return $ read $ d1 : d2 : ds

<|> do

char '1'

option 1 $ do

char '.'

many $ char '0'

return 1