{- |
Module : ./Syntax/Parse_AS_Library.hs
Description : parser for DOL documents and CASL specification librariess
Copyright : (c) Maciek Makowski, Uni Bremen 2002-2016
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable(Grothendieck)
Parser for CASL specification libraries
Follows Sect. II:3.1.5 of the CASL Reference Manual.
Parser for DOL documents
Follows the DOL OMG standard, clause 9.3
-}
module Syntax.Parse_AS_Library (library) where
import Logic.Grothendieck
import Syntax.AS_Structured
import Syntax.AS_Library
import Syntax.Parse_AS_Structured
import Syntax.Parse_AS_Architecture
import Common.AS_Annotation
import Common.AnnoParser
import Common.AnnoState
import Common.Id
import Common.IRI
import Common.Keywords
import Common.Lexer
import Common.LibName
import Common.Parsec
import Common.Token
import Text.ParserCombinators.Parsec
import Data.List
import Data.Maybe (maybeToList)
import qualified Data.Map as Map
import Control.Monad
import Framework.AS
lGAnnos :: LogicGraph -> AParser st (LogicGraph, [Annotation])
lGAnnos lG = do
as <- annos
let (pfx, _) = partPrefixes as
return (lG { prefixes = Map.union pfx $ prefixes lG }, as)
-- * Parsing functions
-- | Parse a library of specifications
library :: LogicGraph -> AParser st LIB_DEFN
library lG = do
(lG1, an1) <- lGAnnos lG
(ps, ln) <- option (nullRange, iriLibName nullIRI) $ do
s1 <- asKey libraryS <|> asKey "distributed-ontology"
n <- libName lG1
return (tokPos s1, n)
(lG2, an2) <- lGAnnos lG1
ls <- libItems lG2
return (Lib_defn ln ls ps (an1 ++ an2))
-- | Parse library name
libName :: LogicGraph -> AParser st LibName
libName lG = liftM2 mkLibName (hetIRI lG)
$ if dolOnly lG then return Nothing else optionMaybe version
-- | Parse the library version
version :: AParser st VersionNumber
version = do
s <- asKey versionS
pos <- getPos
n <- sepBy1 (many1 digit) (string dotS)
skip
return (VersionNumber n (tokPos s `appRange` Range [pos]))
-- | Parse the library elements
libItems :: LogicGraph -> AParser st [Annoted LIB_ITEM]
libItems l =
(eof >> return [])
<|> do
r <- libItem l
la <- lineAnnos
(l', an) <- lGAnnos l
is <- libItems (case r of
Logic_decl logD _ ->
setLogicName logD l'
_ -> l')
case is of
[] -> return [Annoted r nullRange [] $ la ++ an]
Annoted i p nl ra : rs ->
return $ Annoted r nullRange [] la : Annoted i p (an ++ nl) ra : rs
dolImportItem :: LogicGraph -> AParser st LIB_ITEM
dolImportItem l = do
s1 <- asKey "import"
iln <- libName l
return (Download_items iln (ItemMaps []) $ getRange s1)
networkDefn :: LogicGraph -> AParser st LIB_ITEM
networkDefn l = do
kGraph <- asKey "network"
name <- hetIRI l
kEqu <- equalT
n <- parseNetwork l
kEnd <- asKey endS
return . Network_defn name n
. catRange $ [kGraph, kEqu, kEnd]
emptyParams :: GENERICITY
emptyParams = Genericity (Params []) (Imported []) nullRange
-- CASL spec-defn or DOL OMSDefn
specDefn :: LogicGraph -> AParser st LIB_ITEM
specDefn l = do
s <- choice $ map asKey
["specification", specS, ontologyS, "onto", "model", "OMS"]
n <- hetIRI l
g <- generics l
e <- equalT
a <- aSpec l
q <- optEnd
return . Spec_defn n g a
. catRange $ [s, e] ++ maybeToList q
-- CASL view-defn or DOL IntprDefn
viewDefn :: LogicGraph -> AParser st LIB_ITEM
viewDefn l = do
s1 <- choice $ map asKey [viewS, interpretationS, refinementS]
vn <- hetIRI l
do
kEqu <- equalT
rsp <- refSpec l
kEnd <- optEnd
return . Ref_spec_defn vn rsp
. catRange $ [s1, kEqu] ++ maybeToList kEnd
<|> do
g <- generics l
_ <- annotations -- TODO: store annotations
s2 <- colonT
vt <- viewType l
(symbMap, ps) <- option ([], []) $ do
s <- equalT
(m, _) <- parseMapping l
return (m, [s])
q <- optEnd
return . View_defn vn g vt symbMap
. catRange $ [s1, s2] ++ ps ++ maybeToList q
entailDefn :: LogicGraph -> AParser st LIB_ITEM
entailDefn l = do
s <- asKey entailmentS
n <- hetIRI l
e <- equalT
et <- entailType l
q <- optEnd
return . Entail_defn n et . catRange $ [s, e] ++ maybeToList q
queryDefn :: LogicGraph -> AParser st LIB_ITEM
queryDefn l = do
q <- asKey "query"
n <- hetIRI l
e <- equalT
s <- asKey selectS
lg <- lookupCurrentLogic "query-defn" l
(vs, cs) <- parseItemsList lg
w <- asKey whereS
Basic_spec bs _ <- lookupCurrentSyntax "query-defn" l >>= basicSpec l
i <- asKey inS
oms <- aSpec l
mt <- optionMaybe $ asKey "along" >> hetIRI l
o <- optEnd
return . Query_defn n vs bs oms mt . catRange
$ [q, e, s, w] ++ cs ++ [i] ++ maybeToList o
substDefn :: LogicGraph -> AParser st LIB_ITEM
substDefn l = do
q <- asKey "substitution"
n <- hetIRI l
c <- colonT
vt <- viewType l
e <- equalT
lg <- lookupCurrentLogic "subst-defn" l
(m, cs) <- parseItemsMap lg
o <- optEnd
return . Subst_defn n vt m . catRange
$ [q, c, e] ++ cs ++ maybeToList o
resultDefn :: LogicGraph -> AParser st LIB_ITEM
resultDefn l = do
q <- asKey resultS
n <- hetIRI l
(sns, cs) <- separatedBy (hetIRI l) anComma
f <- asKey forS
r <- hetIRI l
a <- annotations
o <- optEnd
return . Result_defn n sns r (any (identAnno "complete") a)
. catRange $ q : cs ++ [f] ++ maybeToList o
-- | Parse an element of the library
libItem :: LogicGraph -> AParser st LIB_ITEM
libItem l = specDefn l
<|> viewDefn l
<|> dolImportItem l
<|> entailDefn l
<|> queryDefn l
<|> substDefn l
<|> resultDefn l
<|> -- equiv defn
do s1 <- asKey equivalenceS
en <- hetIRI l
s2 <- colonT
et <- equivType l
s3 <- equalT
sp <- fmap MkOms $ aSpec l
ep <- optEnd
return . Equiv_defn en et sp
. catRange $ s1 : s2 : s3 : maybeToList ep
<|> -- align defn
do s1 <- asKey alignmentS
an <- hetIRI l
ar <- optionMaybe alignArities
s2 <- colonT
at <- viewType l
(corresps, ps, sem) <- option ([], [], SingleDomain) $ do
s <- equalT
cs <- parseCorrespondences l
aSem <- option SingleDomain $ do
_ <- asKey "assuming"
choice $ map (\ d -> asKey (show d) >> return d)
[minBound .. maxBound]
return (cs, [s], aSem)
q <- optEnd
return . Align_defn an ar at corresps sem
. catRange $ [s1, s2] ++ ps ++ maybeToList q
<|> -- module defn
do s1 <- asKey moduleS
mn <- hetIRI l
_ <- annotations -- TODO: store annotations
s2 <- colonT
mt <- moduleType l
s3 <- asKey forS
rs <- restrictionSignature l
kEnd <- optEnd
return . Module_defn mn mt rs
. catRange $ s1 : s2 : s3 : maybeToList kEnd
<|> -- unit spec
do kUnit <- asKey unitS
kSpec <- asKey specS
name <- hetIRI l
kEqu <- equalT
usp <- unitSpec l
kEnd <- optEnd
return (Unit_spec_defn name usp
(catRange ([kUnit, kSpec, kEqu] ++ maybeToList kEnd)))
<|> networkDefn l
<|> -- arch spec
do kArch <- asKey archS
kASpec <- asKey specS
name <- hetIRI l
kEqu <- equalT
asp <- annotedArchSpec l
kEnd <- optEnd
return (Arch_spec_defn name asp
(catRange ([kArch, kASpec, kEqu] ++ maybeToList kEnd)))
<|> -- download
do s1 <- asKey fromS
iln <- libName l
s2 <- asKey getS
(il, ps) <- downloadItems l
q <- optEnd
return (Download_items iln il
(catRange ([s1, s2] ++ ps ++ maybeToList q)))
<|> -- use (to be removed eventually)
do asKey "use"
fmap (addDownloadAux False) $ hetIRI l
<|> -- logic
do (s, logD) <- qualification l
return $ Logic_decl logD $ tokPos s
<|> -- newlogic
do (n, s1) <- newlogicP
s2 <- equalT
(ml, s3) <- metaP
(s, s4) <- syntaxP
(m, s5) <- modelsP
(f, s6) <- foundationP
(p, s7) <- proofsP
(pa, s8) <- patternsP
q <- optEnd
return (Newlogic_defn (LogicDef n ml s m f p pa)
(catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))
<|> -- newcomorphism
do (n, s1) <- newcomorphismP
s2 <- equalT
(ml, s3) <- metaP
(s, s4) <- sourceP
(t, s5) <- targetP
(sv, s6) <- syntaxP
(pv, s8) <- proofsP
(mv, s7) <- modelsP
q <- optEnd
return (Newcomorphism_defn (ComorphismDef n ml s t sv pv mv)
(catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))
<|> -- just a spec (turned into "spec spec = sp")
do p1 <- getPos
a <- aSpec l
p2 <- getPos
if p1 == p2 then fail "cannot parse spec" else
return (Spec_defn nullIRI
(Genericity (Params []) (Imported []) nullRange) a nullRange)
downloadItems :: LogicGraph -> AParser st (DownloadItems, [Token])
downloadItems l = do
(il, ps) <- separatedBy (itemNameOrMap l) anSemiOrComma
return (ItemMaps il, ps)
<|> do
s <- asKey mapsTo
i <- hetIRI l
return (UniqueItem i, [s])
entailType :: LogicGraph -> AParser st ENTAIL_TYPE
entailType l = do
sp1 <- omsOrNetwork l
do
r <- asKey entailsS
sp2 <- omsOrNetwork l
return $ Entail_type sp1 sp2 $ tokPos r
<|> case sp1 of
MkOms (Annoted (Spec_inst n [] Nothing _) _ _ _) -> do
i <- asKey inS
nw <- parseNetwork l
r <- asKey entailsS
g <- groupSpec l
return . OMSInNetwork n nw g $ catRange [i, r]
_ -> fail "OMSName expected"
omsOrNetwork :: LogicGraph -> AParser st OmsOrNetwork
omsOrNetwork l = fmap (MkOms . emptyAnno) $ groupSpec l
equivType :: LogicGraph -> AParser st EQUIV_TYPE
equivType l = do
sp1 <- omsOrNetwork l
r <- equiT
sp2 <- omsOrNetwork l
return $ Equiv_type sp1 sp2 $ tokPos r
alignArities :: AParser st ALIGN_ARITIES
alignArities = do
asKey alignArityForwardS
f <- alignArity
asKey alignArityBackwardS
b <- alignArity
return $ Align_arities f b
alignArity :: AParser st ALIGN_ARITY
alignArity = choice $ map (\ a -> asKey (showAlignArity a) >> return a)
[minBound .. maxBound]
-- | Parse view type also used in alignments
viewType :: LogicGraph -> AParser st VIEW_TYPE
viewType l = do
sp1 <- annoParser (groupSpec l)
s <- asKey toS
sp2 <- annoParser (groupSpec l)
return $ View_type sp1 sp2 $ tokPos s
moduleType :: LogicGraph -> AParser st MODULE_TYPE
moduleType l = do
sp1 <- aSpec l
s <- asKey ofS
sp2 <- aSpec l
return $ Module_type sp1 sp2 (tokPos s)
restrictionSignature :: LogicGraph -> AParser st G_symb_items_list
restrictionSignature lG = do
l <- lookupCurrentLogic "restrictionSignature" lG
fmap fst $ parseItemsList l
simpleIdOrDDottedId :: GenParser Char st Token
simpleIdOrDDottedId = pToken $ liftM2 (++)
(reserved casl_structured_reserved_words scanAnyWords)
$ optionL $ try $ string ".." <++> scanAnyWords
-- | Parse item name or name map
itemNameOrMap :: LogicGraph -> AParser st ItemNameMap
itemNameOrMap l = do
i1 <- liftM simpleIdToIRI simpleIdOrDDottedId <|> hetIRI l
i2 <- optionMaybe $ do
_ <- asKey mapsTo
if isInfixOf ".." $ iriToStringUnsecure i1
then liftM simpleIdToIRI simpleIdOrDDottedId
else hetIRI l
return $ ItemNameMap i1 i2
optEnd :: AParser st (Maybe Token)
optEnd = try
(addAnnos >> optionMaybe (pToken $ keyWord $ string endS))
<< addLineAnnos
generics :: LogicGraph -> AParser st GENERICITY
generics l = do
(pa, ps1) <- params l
(imp, ps2) <- option ([], nullRange) (imports l)
return $ Genericity (Params pa) (Imported imp) $ appRange ps1 ps2
params :: LogicGraph -> AParser st ([Annoted SPEC], Range)
params l = do
pas <- many (param l)
let (pas1, ps) = unzip pas
return (pas1, concatMapRange id ps)
param :: LogicGraph -> AParser st (Annoted SPEC, Range)
param l = do
b <- oBracketT
pa <- aSpec l
c <- cBracketT
return (pa, toRange b [] c)
imports :: LogicGraph -> AParser st ([Annoted SPEC], Range)
imports l = do
s <- asKey givenS
(sps, ps) <- separatedBy (annoParser $ groupSpec l) anComma
return (sps, catRange (s : ps))
newlogicP :: AParser st (IRI, Token)
newlogicP = do
s <- asKey newlogicS
n <- simpleId
return (simpleIdToIRI n, s)
metaP :: AParser st (FRAM, Token)
metaP = do
s <- asKey metaS
f <- framP
return (f, s)
framP :: AParser st FRAM
framP = do
asKey lfS
return LF
<|> do
asKey isabelleS
return Isabelle
<|> do
asKey maudeS
return Maude
syntaxP :: AParser st (IRI, Token)
syntaxP = do
s <- asKey syntaxS
t <- simpleIdOrDDottedId
return (simpleIdToIRI t, s)
modelsP :: AParser st (IRI, Token)
modelsP = do
s <- asKey modelsS
m <- simpleIdOrDDottedId
return (simpleIdToIRI m, s)
<|> return (nullIRI, nullTok)
foundationP :: AParser st (IRI, Token)
foundationP = do
s <- asKey foundationS
f <- simpleId
return (simpleIdToIRI f, s)
<|> return (nullIRI, nullTok)
proofsP :: AParser st (IRI, Token)
proofsP = do
s <- asKey proofsS
p <- simpleIdOrDDottedId
return (simpleIdToIRI p, s)
<|> return (nullIRI, nullTok)
patternsP :: AParser st (Token, Token)
patternsP = do
s <- asKey patternsS
p <- simpleId
return (p, s)
<|> return (nullTok, nullTok)
newcomorphismP :: AParser st (IRI, Token)
newcomorphismP = do
-- add newcomorphismS = "newcomorphism" in
s <- asKey newcomorphismS
n <- simpleId
return (simpleIdToIRI n, s)
sourceP :: AParser st (IRI, Token)
sourceP = do
s <- asKey sourceS
sl <- simpleIdOrDDottedId
return (simpleIdToIRI sl, s)
targetP :: AParser st (IRI, Token)
targetP = do
s <- asKey targetS
tl <- simpleIdOrDDottedId
return (simpleIdToIRI tl, s)