1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz{- |

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzModule : $Header$

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzDescription : parser for CASL (heterogeneous) structured specifications

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzCopyright : (c) Till Mossakowski, Christian Maeder, Uni Bremen 2002-2005

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzLicense : GPLv2 or higher, see LICENSE.txt

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzMaintainer : Christian.Maeder@dfki.de

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndStability : provisional

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndPortability : non-portable(Grothendieck)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndParser for CASL (heterogeneous) structured specifications

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen Concerning the homogeneous syntax, this follows Sect II:3.1.3

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen of the CASL Reference Manual.

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen-}

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndmodule Syntax.Parse_AS_Structured

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd ( annoParser2

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , groupSpec

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , aSpec

3f08db06526d6901aa08c110b5bc7dde6bc39905nd , logicDescr

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , parseMapping

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , parseCorrespondences

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , translationList

3f08db06526d6901aa08c110b5bc7dde6bc39905nd , hetIRI

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd ) where

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport Logic.Logic (AnyLogic (..), language_name, data_logic, Syntax (..))

0066eddda7203f6345b56f77d146a759298dc635gryzorimport Logic.Comorphism (targetLogic, AnyComorphism (..))

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungimport Logic.Grothendieck

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd ( LogicGraph

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , setCurLogic

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , G_basic_spec (..)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , G_symb_map_items_list (..)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , G_symb_items_list (..)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , lookupCurrentLogic

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin , lookupComorphism)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Syntax.AS_Structured

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinimport Common.AS_Annotation

3267af3f6fbf9743e64a9f019c745317f18cd9f7poirierimport Common.AnnoState

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfimport Common.Id

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinimport Common.IRI

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfimport Common.Keywords

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinimport Common.Lexer

cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0endimport Common.Parsec

cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0endimport Common.Token

f8b7daeb0e3f0ac4544fcc665de10c6b69a1ce0dsf

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzimport Text.ParserCombinators.Parsec

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzimport Data.Char

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzimport Data.Maybe

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzimport Control.Monad

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzhetIRI :: GenParser Char st IRI

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndhetIRI = try $ do

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd i <- iriManchester

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin skipSmart

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin if iriToStringUnsecure i `elem` casl_reserved_words then

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin unexpected $ show i

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin else return i

35ff2d06df95b9593ee312dfff883c76f3b97798noodl

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin-- | parse annotations and then still call an annotation parser

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndannoParser2 :: AParser st (Annoted a) -> AParser st (Annoted a)

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinannoParser2 =

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin liftM2 (\ x (Annoted y pos l r) -> Annoted y pos (x ++ l) r) annos

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd-- * logic and encoding names

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin-- within sublogics we allow some further symbol characters

35ff2d06df95b9593ee312dfff883c76f3b97798noodlsublogicName :: AParser st String

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinsublogicName = many $ satisfy $ \ c -> notElem c ":./\\" && isSignChar c

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf || elem c "_'" || isAlphaNum c

3267af3f6fbf9743e64a9f019c745317f18cd9f7poirier

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf{- keep these identical in order to

f8b7daeb0e3f0ac4544fcc665de10c6b69a1ce0dsfdecide after seeing ".", ":" or "->" what was meant -}

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsflogicName :: AParser st Logic_name

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlogicName = do

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin i <- iriManchester

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin let (ft, rt) = break (== '.') $ abbrevPath i

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

f8b7daeb0e3f0ac4544fcc665de10c6b69a1ce0dsf else do

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz s <- sublogicName -- try more sublogic characters

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

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz skipSmart

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin mt <- optionMaybe $ oParenT >> iriCurie << cParenT

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf return $ Logic_name e ms mt

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlogicDescr :: AParser st LogicDescr

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzlogicDescr = do

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin n <- logicName

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf option (nameToLogicDescr n) $ do

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic r <- asKey serializationS

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic s <- hetIRI

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic return $ LogicDescr n (Just s) $ tokPos r

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic-- * parse Logic_code

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseLogic :: LogicGraph -> AParser st (Logic_code, LogicGraph)

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfparseLogic lG = do

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin lc <- parseLogicAux

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf case lc of

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic Logic_code _ _ (Just l) _ ->

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic return (lc, setLogicName (nameToLogicDescr l) lG)

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic Logic_code (Just c) _ _ _ -> do

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic nLg <- lookupAndSetComorphismName c lG

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic return (lc, nLg)

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin _ -> return (lc, lG)

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfparseLogicAux :: AParser st Logic_code

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseLogicAux =

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf do l <- asKey logicS

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic do e <- logicName -- try to parse encoding or logic source after "logic"

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin case e of

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic Logic_name f Nothing Nothing ->

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic do c <- colonT

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin parseLogAfterColon (Just f) [l, c]

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> parseOptLogTarget Nothing (Just e) [l]

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf <|> return (Logic_code (Just f) Nothing Nothing

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin $ tokPos l)

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf _ -> parseOptLogTarget Nothing (Just e) [l]

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic <|> do

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin f <- asKey funS -- parse at least a logic target after "logic"

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic t <- logicName

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic return $ Logic_code Nothing Nothing (Just t)

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin $ tokPos l `appRange` tokPos f

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

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

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseLogAfterColon :: Maybe IRI -> [Token] -> AParser st Logic_code

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseLogAfterColon e l =

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf do s <- logicName

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin parseOptLogTarget e (Just s) l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> return (Logic_code e (Just s) Nothing $ catRange l)

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf <|> parseOptLogTarget e Nothing l

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic-- parse an optional logic target (given encoding e or source s)

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalicparseOptLogTarget :: Maybe IRI -> Maybe Logic_name -> [Token]

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic -> AParser st Logic_code

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalicparseOptLogTarget e s l =

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz do f <- asKey funS

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz let p = catRange $ l ++ [f]

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz do t <- logicName

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz return (Logic_code e s (Just t) p)

a7a43799fed7fcdeaa70584dbd3ecd130b25deb3noodl <|> return (Logic_code e s Nothing p)

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinplainComma :: AParser st Token

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfplainComma = anComma `notFollowedWith` asKey logicS

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin-- * parse G_mapping

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirincallSymParser :: Maybe (AParser st a) -> String -> String ->

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf AParser st ([a], [Token])

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igaliccallSymParser p name itemType = case p of

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic Nothing ->

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic fail $ "no symbol" ++ itemType ++ " parser for language " ++ name

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic Just pa -> separatedBy pa plainComma

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfparseItemsMap :: AnyLogic -> AParser st (G_symb_map_items_list, [Token])

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseItemsMap (Logic lid) = do

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (cs, ps) <- callSymParser (parse_symb_map_items lid)

9a367ec3d570bcbaf8923dad66cb3b1532963964trawick (language_name lid) " maps"

9a367ec3d570bcbaf8923dad66cb3b1532963964trawick return (G_symb_map_items_list lid cs, ps)

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseMapping :: LogicGraph -> AParser st ([G_mapping], [Token])

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseMapping = parseMapOrHide G_logic_translation G_symb_map parseItemsMap

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinparseMapOrHide :: (Logic_code -> a) -> (t -> a)

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin -> (AnyLogic -> AParser st (t, [Token])) -> LogicGraph

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz -> AParser st ([a], [Token])

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzparseMapOrHide constrLogic constrMap pa lG =

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz do (n, nLg) <- parseLogic lG

1b390add6886fb1c0acdea82be0ef0920f1158casf do c <- anComma

1b390add6886fb1c0acdea82be0ef0920f1158casf (gs, ps) <- parseMapOrHide constrLogic constrMap pa nLg

1b390add6886fb1c0acdea82be0ef0920f1158casf return (constrLogic n : gs, c : ps)

1b390add6886fb1c0acdea82be0ef0920f1158casf <|> return ([constrLogic n], [])

1b390add6886fb1c0acdea82be0ef0920f1158casf <|> do

1b390add6886fb1c0acdea82be0ef0920f1158casf l <- lookupCurrentLogic "parseMapOrHide" lG

1b390add6886fb1c0acdea82be0ef0920f1158casf (m, ps) <- pa l

1b390add6886fb1c0acdea82be0ef0920f1158casf do c <- anComma

1b390add6886fb1c0acdea82be0ef0920f1158casf (gs, qs) <- parseMapOrHide constrLogic constrMap pa lG

1b390add6886fb1c0acdea82be0ef0920f1158casf return (constrMap m : gs, ps ++ c : qs)

1b390add6886fb1c0acdea82be0ef0920f1158casf <|> return ([constrMap m], ps)

1b390add6886fb1c0acdea82be0ef0920f1158casf

1b390add6886fb1c0acdea82be0ef0920f1158casf-- * parse G_hiding

1b390add6886fb1c0acdea82be0ef0920f1158casf

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

1b390add6886fb1c0acdea82be0ef0920f1158casfparseItemsList (Logic lid) = do

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic (cs, ps) <- callSymParser (parse_symb_items lid)

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic (language_name lid) ""

1b390add6886fb1c0acdea82be0ef0920f1158casf return (G_symb_items_list lid cs, ps)

1b390add6886fb1c0acdea82be0ef0920f1158casf

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndparseHiding :: LogicGraph -> AParser st ([G_hiding], [Token])

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndparseHiding = parseMapOrHide G_logic_projection G_symb_list parseItemsList

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd

0066eddda7203f6345b56f77d146a759298dc635gryzor-- * specs

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd-- "then" is associative, therefore flatten extensions

5effc8b39fae5cd169d17f342bfc265705840014rbowen

7fec19672a491661b2fe4b29f685bc7f4efa64d4ndflatExts :: [Annoted SPEC] -> [Annoted SPEC]

7fec19672a491661b2fe4b29f685bc7f4efa64d4ndflatExts = concatMap $ \ as -> case item as of

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd Extension sps _ -> sps

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd Group sp _ -> case flatExts [sp] of

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd [_] -> [as]

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd sps -> sps

_ -> [as]

spec :: LogicGraph -> AParser st (Annoted SPEC)

spec l = do

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

return $ case sps of

[sp] -> sp

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

specA :: LogicGraph -> AParser st (Annoted SPEC)

specA l = do

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

return $ case sps of

[sp] -> sp

_ -> emptyAnno (Union sps $ catRange ps)

specB :: LogicGraph -> AParser st (Annoted SPEC)

specB l = do

p1 <- asKey localS

sp1 <- aSpec l

p2 <- asKey withinS

sp2 <- annoParser2 $ specB l

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

<|> specC l

specC :: LogicGraph -> AParser st (Annoted SPEC)

specC lG = do

let spD = annoParser $ specD lG

rest = spD >>= translationList lG Translation Reduction

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

{- if the current logic has an associated data_logic,

parse "data SPEC1 SPEC2", where SPEC1 is in the data_logic

SPEC1 needs to be a basic spec or a grouped spec

SPEC2 is in the currrent logic -}

case data_logic lid of

Nothing -> rest

Just lD@(Logic dl) -> do

p1 <- asKey dataS -- not a keyword

sp1 <- annoParser $ basicSpec lD

<|> groupSpec (setCurLogic (language_name dl) lG)

sp2 <- spD

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

<|> rest

translationList :: LogicGraph -> (Annoted b -> RENAMING -> b)

-> (Annoted b -> RESTRICTION -> b) -> Annoted b -> AParser st (Annoted b)

translationList l ftrans frestr sp =

do sp' <- translation l sp ftrans frestr

translationList l ftrans frestr (emptyAnno sp')

<|> return sp

{- | Parse renaming

@

RENAMING ::= with SYMB-MAP-ITEMS-LIST

@

SYMB-MAP-ITEMS-LIST is parsed using parseMapping -}

renaming :: LogicGraph -> AParser st RENAMING

renaming l =

do kWith <- asKey withS

(mappings, commas) <- parseMapping l

return (Renaming mappings $ catRange $ kWith : commas)

{- | Parse restriction

@

RESTRICTION ::= hide SYMB-ITEMS-LIST

| reveal SYMB-MAP-ITEMS-LIST

@

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

parsed using parseItemsMap -}

restriction :: LogicGraph -> AParser st RESTRICTION

restriction lg =

-- hide

do kHide <- asKey hideS

(symbs, commas) <- parseHiding lg

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

<|> -- reveal

do kReveal <- asKey revealS

nl <- lookupCurrentLogic "reveal" lg

(mappings, commas) <- parseItemsMap nl

return (Revealed mappings (catRange (kReveal : commas)))

translation :: LogicGraph -> a -> (a -> RENAMING -> b)

-> (a -> RESTRICTION -> b) -> AParser st b

translation l sp ftrans frestr =

do r <- renaming l

return (ftrans sp r)

<|>

do r <- restriction l

return (frestr sp r)

groupSpecLookhead :: AParser st IRI

groupSpecLookhead =

let tok2IRI = liftM simpleIdToIRI in

tok2IRI oBraceT <|> followedWith (hetIRI << annos)

(choice (map (tok2IRI . asKey) criticalKeywords)

<|> tok2IRI cBraceT <|> tok2IRI oBracketT <|> tok2IRI cBracketT

<|> (eof >> return nullIRI))

specD :: LogicGraph -> AParser st SPEC

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

specD l = do

p <- asKey freeS `followedWith` groupSpecLookhead

sp <- annoParser $ groupSpec l

return (Free_spec sp $ tokPos p)

<|> do

p <- asKey cofreeS `followedWith` groupSpecLookhead

sp <- annoParser $ groupSpec l

return (Cofree_spec sp $ tokPos p)

<|> do

p <- asKey closedS `followedWith` groupSpecLookhead

sp <- annoParser $ groupSpec l

return (Closed_spec sp $ tokPos p)

<|> specE l

specE :: LogicGraph -> AParser st SPEC

specE l = logicSpec l

<|> combineSpec

<|> (lookAhead groupSpecLookhead >> groupSpec l)

<|> (lookupCurrentLogic "basic spec" l >>= basicSpec)

-- | call a logic specific parser if it exists

callParser :: Maybe (AParser st a) -> String -> String -> AParser st a

callParser p name itemType =

fromMaybe (fail $ "no " ++ itemType ++ " parser for language " ++ name) p

basicSpec :: AnyLogic -> AParser st SPEC

basicSpec (Logic lid) = do

p <- getPos

bspec <- callParser (parse_basic_spec lid) (language_name lid)

"basic specification"

q <- getPos

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

logicSpec :: LogicGraph -> AParser st SPEC

logicSpec lG = do

s1 <- asKey logicS

ln <- logicDescr

s2 <- colonT

sp <- annoParser $ specD $ setLogicName ln lG

return $ Qualified_spec ln sp $ toRange s1 [] s2

combineSpec :: AParser st SPEC

combineSpec = do

s1 <- asKey combineS

(oir, ps1) <- separatedBy hetIRI commaT

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

s2 <- asKey excludingS

(e, ps2) <- separatedBy hetIRI commaT

return (e, s2 : ps2)

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

lookupAndSetComorphismName :: IRI -> LogicGraph -> AParser st LogicGraph

lookupAndSetComorphismName cIRI lg = do

Comorphism cid <- lookupComorphism (iriToStringUnsecure cIRI) lg

return $ setCurLogic (language_name $ targetLogic cid) lg

aSpec :: LogicGraph -> AParser st (Annoted SPEC)

aSpec = annoParser2 . spec

groupSpec :: LogicGraph -> AParser st SPEC

groupSpec l = do

b <- oBraceT

do

c <- cBraceT

return $ EmptySpec $ catRange [b, c]

<|> do

a <- aSpec l

c <- cBraceT

return $ Group a $ catRange [b, c]

<|> do

n <- hetIRI

(f, ps) <- fitArgs l

return (Spec_inst n f ps)

fitArgs :: LogicGraph -> AParser st ([Annoted FIT_ARG], Range)

fitArgs l = do

fas <- many (fitArg l)

let (fas1, ps) = unzip fas

return (fas1, concatMapRange id ps)

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

fitArg l = do

b <- oBracketT

fa <- annoParser (fittingArg l)

c <- cBracketT

return (fa, toRange b [] c)

fittingArg :: LogicGraph -> AParser st FIT_ARG

fittingArg l = do

s <- asKey viewS

vn <- hetIRI

(fa, ps) <- fitArgs l

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

<|> do

sp <- aSpec l

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

s <- asKey fitS

(m, qs) <- parseMapping l

return (m, catRange $ s : qs)

return (Fit_spec sp symbit ps)

parseCorrespondences :: LogicGraph -> AParser st [CORRESPONDENCE]

parseCorrespondences l = commaSep1 $ correspondence l << addAnnos

correspondence :: LogicGraph -> AParser st CORRESPONDENCE

correspondence l = do

asKey "*"

return Default_correspondence

<|> do

asKey relationS

rref <- optionMaybe relationRef

conf <- optionMaybe confidence

oBraceT

cs <- parseCorrespondences l

cBraceT

return $ Correspondence_block rref conf cs

<|> do

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

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

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

only commented out for future debugging purposes -}

return $ Single_correspondence mcid eRef toer mrRef mconf

corr1 :: LogicGraph

-> AParser st ( Maybe CORRESPONDENCE_ID, ENTITY_REF

, Maybe RELATION_REF, Maybe CONFIDENCE, TERM_OR_ENTITY_REF)

corr1 l = do

cid <- try $ correspondenceIdWithLookahead l

eRef <- hetIRI

(mrRef, mconf, toer) <- corr2 l

return (Just cid, eRef, mrRef, mconf, toer)

<|> do

eRef <- hetIRI

(mrRef, mconf, toer) <- corr2 l

return (Nothing, eRef, mrRef, mconf, toer)

corr2 :: LogicGraph

-> AParser st (Maybe RELATION_REF, Maybe CONFIDENCE, TERM_OR_ENTITY_REF)

corr2 l = do

rRef <- try relationRefWithLookAhead

(mconf, toer) <- corr3 l

return (Just rRef, mconf, toer)

<|> do

(mconf, toer) <- corr3 l

return (Nothing, mconf, toer)

corr3 :: LogicGraph -> AParser st (Maybe CONFIDENCE, TERM_OR_ENTITY_REF)

corr3 l = do

conf <- try confidence

toer <- termOrEntityRef l

return (Just conf, toer)

<|> do

toer <- termOrEntityRef l

return (Nothing, toer)

correspondenceIdWithLookahead :: LogicGraph -> AParser st CORRESPONDENCE_ID

correspondenceIdWithLookahead l = do

cid <- hetIRI

asKey equalS

lookAhead (try $ hetIRI >> corr2 l)

return cid

relationRefWithLookAhead :: AParser st RELATION_REF

relationRefWithLookAhead = do

r <- relationRef

lookAhead (confidenceBegin >> return nullIRI)

<|> lookAhead (try hetIRI)

return r

relationRef :: AParser st RELATION_REF

relationRef = ((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

return $ Iri i

confidenceBegin :: AParser st Char

confidenceBegin = char '('

termOrEntityRef :: LogicGraph -> AParser st TERM_OR_ENTITY_REF

termOrEntityRef l = do

i <- hetIRI

return $ Entity_ref i

<|> (lookupCurrentLogic "term" l >>= term)

-- TODO: implement

term :: AnyLogic -> AParser st TERM_OR_ENTITY_REF

term (Logic lid) = do

_symbs <- callParser (parse_symb_items lid) (language_name lid) "term"

-- return $ Term (G_symb_items_list lid [symbs]) $ Range [p, q]

fail "term not implemented yet"

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