Parse_AS_Library.hs revision dd9ab23d84f402532a6b651f6463e0c3bdb60cfd
2509N/A{- |
0N/AModule : $Header$
0N/ADescription : parser for CASL specification librariess
0N/ACopyright : (c) Maciek Makowski, Uni Bremen 2002-2006
0N/ALicense : GPLv2 or higher, see LICENSE.txt
0N/AMaintainer : Christian.Maeder@dfki.de
0N/AStability : provisional
0N/APortability : non-portable(Grothendieck)
0N/A
0N/AParser for CASL specification librariess
0N/A Follows Sect. II:3.1.5 of the CASL Reference Manual.
0N/A-}
0N/A
0N/Amodule Syntax.Parse_AS_Library (library, useItem, useItems) where
0N/A
0N/Aimport Logic.Grothendieck (LogicGraph, prefixes)
0N/Aimport Syntax.AS_Structured
2362N/Aimport Syntax.AS_Library
2362N/Aimport Syntax.Parse_AS_Structured
2362N/Aimport Syntax.Parse_AS_Architecture
1178N/A
2509N/Aimport Common.AS_Annotation
0N/Aimport Common.AnnoState
0N/Aimport Common.Id
1178N/Aimport Common.IRI
0N/A
0N/Aimport Common.Keywords
0N/Aimport Common.Lexer
0N/Aimport Common.LibName
0N/Aimport Common.Parsec
0N/Aimport Common.Token
0N/A
0N/Aimport Text.ParserCombinators.Parsec
0N/Aimport Data.List
0N/Aimport Data.Maybe (maybeToList)
0N/Aimport qualified Data.Map as Map
0N/Aimport Control.Monad
0N/A
0N/Aimport Framework.AS
0N/A
1178N/AlGAnnos :: LogicGraph -> AParser st (LogicGraph, [Annotation])
0N/AlGAnnos lG = do
0N/A as <- annos
0N/A let (pfx, _) = partPrefixes as
0N/A return (lG { prefixes = Map.union pfx $ prefixes lG }, as)
0N/A
0N/A-- * Parsing functions
0N/A
0N/A-- | Parse a library of specifications
0N/Alibrary :: LogicGraph -> AParser st LIB_DEFN
1178N/Alibrary lG = do
1178N/A (lG1, an1) <- lGAnnos lG
0N/A (ps, ln) <- option (nullRange, iriLibName nullIRI) $ do
0N/A s1 <- asKey libraryS <|> asKey distributedOntologyS
0N/A n <- libName lG1
0N/A return (tokPos s1, n)
0N/A (lG2, an2) <- lGAnnos lG1
0N/A ls <- libItems lG2
0N/A return (Lib_defn ln ls ps (an1 ++ an2))
0N/A
0N/A-- | Parse library name
0N/AlibName :: LogicGraph -> AParser st LibName
0N/AlibName lG = do
0N/A p <- getPos
0N/A i <- hetIRI lG
0N/A v <- optionMaybe version
0N/A return $ LibName i (Range [p]) Nothing v
1178N/A
0N/A-- | Parse the library version
0N/Aversion :: AParser st VersionNumber
0N/Aversion = do
0N/A s <- asKey versionS
0N/A pos <- getPos
1178N/A n <- sepBy1 (many1 digit) (string dotS)
0N/A skip
0N/A return (VersionNumber n (tokPos s `appRange` Range [pos]))
0N/A
0N/A-- | Parse the library elements
0N/AlibItems :: LogicGraph -> AParser st [Annoted LIB_ITEM]
0N/AlibItems l =
0N/A (eof >> return [])
0N/A <|> do
0N/A r <- libItem l
0N/A la <- lineAnnos
0N/A (l', an) <- lGAnnos l
0N/A is <- libItems (case r of
0N/A Logic_decl logD _ ->
0N/A setLogicName logD l'
0N/A _ -> l')
0N/A case is of
0N/A [] -> return [Annoted r nullRange [] $ la ++ an]
0N/A Annoted i p nl ra : rs ->
0N/A return $ Annoted r nullRange [] la : Annoted i p (an ++ nl) ra : rs
0N/A
0N/A-- | Parse an element of the library
0N/AlibItem :: LogicGraph -> AParser st LIB_ITEM
0N/AlibItem l =
0N/A -- spec defn
0N/A do s <- asKey specS <|> asKey ontologyS
0N/A n <- hetIRI l
0N/A g <- generics l
0N/A e <- equalT
0N/A a <- aSpec l
0N/A q <- optEnd
0N/A return (Syntax.AS_Library.Spec_defn n g a
0N/A (catRange ([s, e] ++ maybeToList q)))
0N/A <|> -- view defn
0N/A do s1 <- asKey viewS <|> asKey interpretationS
0N/A vn <- liftM simpleIdToIRI simpleId
0N/A g <- generics l
0N/A s2 <- asKey ":"
0N/A vt <- viewType l
0N/A (symbMap, ps) <- option ([], []) $ do
0N/A s <- equalT
0N/A optional $ try $ asKey "translation"
0N/A (m, _) <- parseMapping l
0N/A return (m, [s])
0N/A q <- optEnd
0N/A return (Syntax.AS_Library.View_defn vn g vt symbMap
0N/A (catRange ([s1, s2] ++ ps ++ maybeToList q)))
0N/A
0N/A <|> -- equiv defn
0N/A do s1 <- asKey equivalenceS
0N/A en <- hetIRI l
0N/A s2 <- colonT
0N/A et <- equivType l
0N/A s3 <- equalT
0N/A sp <- aSpec l
0N/A ep <- optEnd
0N/A return (Syntax.AS_Library.Equiv_defn en et sp
0N/A (catRange (s1 : s2 : s3 : maybeToList ep)))
0N/A
0N/A <|> -- align defn
0N/A do s1 <- asKey alignmentS
0N/A an <- hetIRI l
0N/A ar <- optionMaybe alignArities
0N/A s2 <- asKey ":"
0N/A at <- alignType l
0N/A (corresps, ps) <- option ([], []) $ do
0N/A s <- equalT
0N/A cs <- parseCorrespondences l
0N/A return (cs, [s])
0N/A q <- optEnd
0N/A return (Syntax.AS_Library.Align_defn an ar at corresps
0N/A (catRange ([s1, s2] ++ ps ++ maybeToList q)))
0N/A <|> -- module defn
0N/A do s1 <- asKey moduleS
0N/A mn <- hetIRI l
0N/A -- TODO: parse annotations
0N/A s2 <- asKey ":"
0N/A mt <- moduleType l
0N/A s3 <- asKey forS
0N/A rs <- restrictionSignature l
0N/A return (Syntax.AS_Library.Module_defn mn mt rs (catRange [s1, s2, s3]))
0N/A <|> -- unit spec
0N/A do kUnit <- asKey unitS
0N/A kSpec <- asKey specS
0N/A name <- liftM simpleIdToIRI simpleId
0N/A kEqu <- equalT
0N/A usp <- unitSpec l
0N/A kEnd <- optEnd
0N/A return (Syntax.AS_Library.Unit_spec_defn name usp
0N/A (catRange ([kUnit, kSpec, kEqu] ++ maybeToList kEnd)))
0N/A <|> -- ref spec
0N/A do kRef <- asKey refinementS
0N/A name' <- simpleId
0N/A let name = simpleIdToIRI name'
0N/A kEqu <- equalT
0N/A rsp <- refSpec l
0N/A kEnd <- optEnd
0N/A return (Syntax.AS_Library.Ref_spec_defn name rsp
0N/A (catRange ([kRef, kEqu] ++ maybeToList kEnd)))
0N/A <|> -- arch spec
0N/A do kArch <- asKey archS
0N/A kASpec <- asKey specS
0N/A name <- hetIRI l
0N/A kEqu <- equalT
0N/A asp <- annotedArchSpec l
0N/A kEnd <- optEnd
0N/A return (Syntax.AS_Library.Arch_spec_defn name asp
0N/A (catRange ([kArch, kASpec, kEqu] ++ maybeToList kEnd)))
1178N/A <|> -- download
0N/A do s1 <- asKey fromS
0N/A iln <- libName l
0N/A s2 <- asKey getS
0N/A (il, ps) <- downloadItems
0N/A q <- optEnd
1178N/A return (Download_items iln il
1178N/A (catRange ([s1, s2] ++ ps ++ maybeToList q)))
0N/A <|> -- use (to be removed eventually)
1178N/A do asKey "use"
0N/A i <- hetIRI l
0N/A useItem i
0N/A <|> -- logic
1178N/A do s <- asKey logicS
1178N/A logD <- logicDescr l
0N/A return $ Logic_decl logD $ tokPos s
0N/A <|> -- newlogic
0N/A do (n, s1) <- newlogicP
0N/A s2 <- equalT
0N/A (ml, s3) <- metaP
0N/A (s, s4) <- syntaxP
0N/A (m, s5) <- modelsP
0N/A (f, s6) <- foundationP
0N/A (p, s7) <- proofsP
0N/A (pa, s8) <- patternsP
0N/A q <- optEnd
1178N/A return (Newlogic_defn (LogicDef n ml s m f p pa)
0N/A (catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))
0N/A <|> -- newcomorphism
0N/A do (n, s1) <- newcomorphismP
0N/A s2 <- equalT
0N/A (ml, s3) <- metaP
0N/A (s, s4) <- sourceP
1178N/A (t, s5) <- targetP
1178N/A (sv, s6) <- syntaxP
0N/A (pv, s8) <- proofsP
0N/A (mv, s7) <- modelsP
0N/A q <- optEnd
0N/A return (Newcomorphism_defn (ComorphismDef n ml s t sv pv mv)
0N/A (catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))
0N/A <|> -- just a spec (turned into "spec spec = sp")
0N/A do p1 <- getPos
0N/A a <- aSpec l
0N/A p2 <- getPos
0N/A if p1 == p2 then fail "cannot parse spec" else
0N/A return (Syntax.AS_Library.Spec_defn nullIRI
0N/A (Genericity (Params []) (Imported []) nullRange) a nullRange)
0N/A
0N/AuseItem :: Monad m => IRI -> m LIB_ITEM
0N/AuseItem i = do
0N/A let libPath = deleteQuery i
0N/A query = iriQuery i -- this used to be the fragment
0N/A libNameIri <- if null query || null (tail query)
0N/A then return libPath else case parseIRIManchester $ tail query of
0N/A Just i' -> return i'
0N/A Nothing -> fail $ "could not read " ++ query ++ " into IRI"
1178N/A return $ Download_items
0N/A (LibName libPath nullRange (Just libPath) Nothing)
0N/A (ItemMaps [ItemNameMap libNameIri (Just i)]) nullRange
0N/A
0N/AuseItems :: Monad m => [IRI] -> m [LIB_ITEM]
0N/AuseItems = mapM useItem
0N/A
0N/AdownloadItems :: AParser st (DownloadItems, [Token])
0N/AdownloadItems = do
0N/A (il, ps) <- separatedBy itemNameOrMap anSemiOrComma
1178N/A return (ItemMaps il, ps)
1178N/A <|> do
0N/A s <- asKey mapsTo
0N/A i <- liftM simpleIdToIRI simpleId
0N/A return (UniqueItem i, [s])
0N/A
0N/A
1178N/A-- | Parse view type
0N/AviewType :: LogicGraph -> AParser st VIEW_TYPE
1178N/AviewType l = do
0N/A (sp1, sp2, r) <- viewOrAlignType l
1178N/A return (View_type sp1 sp2 r)
0N/A
0N/AequivType :: LogicGraph -> AParser st EQUIV_TYPE
0N/AequivType l = do
0N/A sp1 <- groupSpec l
0N/A r <- equiT
0N/A sp2 <- groupSpec l
0N/A return $ Equiv_type sp1 sp2 $ tokPos r
1178N/A
0N/A-- | Parse align type
0N/AalignType :: LogicGraph -> AParser st ALIGN_TYPE
0N/AalignType l = do
0N/A (sp1, sp2, r) <- viewOrAlignType l
0N/A return (Align_type sp1 sp2 r)
0N/A
0N/AalignArities :: AParser st ALIGN_ARITIES
0N/AalignArities = do
0N/A asKey alignArityForwardS
0N/A f <- alignArity
0N/A asKey alignArityBackwardS
1178N/A b <- alignArity
1178N/A return $ Align_arities f b
0N/A
0N/AalignArity :: AParser st ALIGN_ARITY
0N/AalignArity = choice $ map (\ a -> asKey (showAlignArity a) >> return a)
0N/A [minBound .. maxBound]
0N/A
0N/AviewOrAlignType :: LogicGraph -> AParser st (Annoted SPEC, Annoted SPEC, Range)
0N/AviewOrAlignType l = do
0N/A sp1 <- annoParser (groupSpec l)
0N/A s <- asKey toS
0N/A sp2 <- annoParser (groupSpec l)
0N/A return (sp1, sp2, tokPos s)
0N/A
0N/AmoduleType :: LogicGraph -> AParser st MODULE_TYPE
0N/AmoduleType l = do
0N/A sp1 <- aSpec l
0N/A s <- asKey ofS
0N/A sp2 <- aSpec l
0N/A return $ Module_type sp1 sp2 (tokPos s)
0N/A
0N/ArestrictionSignature :: LogicGraph -> AParser st RESTRICTION_SIGNATURE
0N/ArestrictionSignature lG = many1 $ hetIRI lG
0N/A
0N/AsimpleIdOrDDottedId :: GenParser Char st Token
0N/AsimpleIdOrDDottedId = pToken $ liftM2 (++)
0N/A (reserved casl_structured_reserved_words scanAnyWords)
0N/A $ optionL $ try $ string ".." <++> scanAnyWords
0N/A
0N/A-- | Parse item name or name map
0N/AitemNameOrMap :: AParser st ItemNameMap
0N/AitemNameOrMap = do
0N/A i1 <- liftM simpleIdToIRI simpleIdOrDDottedId
0N/A i2 <- optionMaybe $ liftM simpleIdToIRI $ do
0N/A _ <- asKey mapsTo
0N/A if isInfixOf ".." $ iriToStringUnsecure i1
0N/A then simpleIdOrDDottedId
0N/A else simpleId
0N/A return $ ItemNameMap i1 i2
0N/A
0N/AoptEnd :: AParser st (Maybe Token)
0N/AoptEnd = try
0N/A (addAnnos >> optionMaybe (pToken $ keyWord $ string endS))
0N/A << addLineAnnos
0N/A
0N/Agenerics :: LogicGraph -> AParser st GENERICITY
0N/Agenerics l = do
0N/A (pa, ps1) <- params l
0N/A (imp, ps2) <- option ([], nullRange) (imports l)
0N/A return $ Genericity (Params pa) (Imported imp) $ appRange ps1 ps2
0N/A
0N/Aparams :: LogicGraph -> AParser st ([Annoted SPEC], Range)
0N/Aparams l = do
0N/A pas <- many (param l)
0N/A let (pas1, ps) = unzip pas
0N/A return (pas1, concatMapRange id ps)
0N/A
0N/Aparam :: LogicGraph -> AParser st (Annoted SPEC, Range)
0N/Aparam l = do
0N/A b <- oBracketT
0N/A pa <- aSpec l
0N/A c <- cBracketT
0N/A return (pa, toRange b [] c)
0N/A
0N/Aimports :: LogicGraph -> AParser st ([Annoted SPEC], Range)
0N/Aimports l = do
0N/A s <- asKey givenS
0N/A (sps, ps) <- separatedBy (annoParser $ groupSpec l) anComma
0N/A return (sps, catRange (s : ps))
0N/A
0N/AnewlogicP :: AParser st (IRI, Token)
0N/AnewlogicP = do
0N/A s <- asKey newlogicS
0N/A n <- simpleId
0N/A return (simpleIdToIRI n, s)
0N/A
0N/AmetaP :: AParser st (FRAM, Token)
0N/AmetaP = do
0N/A s <- asKey metaS
0N/A f <- framP
0N/A return (f, s)
0N/A
0N/AframP :: AParser st FRAM
0N/AframP = do
0N/A asKey lfS
0N/A return LF
0N/A <|> do
0N/A asKey isabelleS
0N/A return Isabelle
0N/A <|> do
0N/A asKey maudeS
0N/A return Maude
0N/A
0N/AsyntaxP :: AParser st (IRI, Token)
0N/AsyntaxP = do
0N/A s <- asKey syntaxS
0N/A t <- simpleIdOrDDottedId
0N/A return (simpleIdToIRI t, s)
0N/A
0N/AmodelsP :: AParser st (IRI, Token)
0N/AmodelsP = do
0N/A s <- asKey modelsS
0N/A m <- simpleIdOrDDottedId
0N/A return (simpleIdToIRI m, s)
0N/A <|> return (nullIRI, nullTok)
0N/A
0N/AfoundationP :: AParser st (IRI, Token)
0N/AfoundationP = do
0N/A s <- asKey foundationS
1178N/A f <- simpleId
1178N/A return (simpleIdToIRI f, s)
0N/A <|> return (nullIRI, nullTok)
1178N/A
1178N/AproofsP :: AParser st (IRI, Token)
1178N/AproofsP = do
1178N/A s <- asKey proofsS
1178N/A p <- simpleIdOrDDottedId
0N/A return (simpleIdToIRI p, s)
1178N/A <|> return (nullIRI, nullTok)
0N/A
0N/ApatternsP :: AParser st (Token, Token)
0N/ApatternsP = do
0N/A s <- asKey patternsS
0N/A p <- simpleId
1178N/A return (p, s)
1178N/A <|> return (nullTok, nullTok)
0N/A
1178N/AnewcomorphismP :: AParser st (IRI, Token)
1178N/AnewcomorphismP = do
1178N/A -- add newcomorphismS = "newcomorphism" in
1178N/A s <- asKey newcomorphismS
1178N/A n <- simpleId
0N/A return (simpleIdToIRI n, s)
0N/A
0N/AsourceP :: AParser st (IRI, Token)
0N/AsourceP = do
0N/A s <- asKey sourceS
0N/A sl <- simpleIdOrDDottedId
0N/A return (simpleIdToIRI sl, s)
0N/A
0N/AtargetP :: AParser st (IRI, Token)
0N/AtargetP = do
0N/A s <- asKey targetS
1178N/A tl <- simpleIdOrDDottedId
1178N/A return (simpleIdToIRI tl, s)
0N/A