1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz{- |

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzModule : $Header$

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzDescription : parser for CASL specification librariess

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzCopyright : (c) Maciek Makowski, Uni Bremen 2002-2006

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzLicense : GPLv2 or higher, see LICENSE.txt

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzMaintainer : Christian.Maeder@dfki.de

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndStability : provisional

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndPortability : non-portable(Grothendieck)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndParser for CASL specification librariess

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Follows Sect. II:3.1.5 of the CASL Reference Manual.

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd-}

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndmodule Syntax.Parse_AS_Library (library) where

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

52fff662005b1866a3ff09bb6c902800c5cc6dedjerenkrantzimport Logic.Grothendieck (LogicGraph)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Syntax.AS_Structured

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Syntax.AS_Library

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Syntax.Parse_AS_Structured

4b5981e276e93df97c34e4da05ca5cf8bbd937dand (logicName, groupSpec, aSpec, parseMapping)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Syntax.Parse_AS_Architecture

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport Common.AS_Annotation

0066eddda7203f6345b56f77d146a759298dc635gryzorimport Common.AnnoState

0066eddda7203f6345b56f77d146a759298dc635gryzorimport Common.Id

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport Common.Keywords

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Common.Lexer

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Common.LibName

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Common.Parsec

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Common.Token

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinimport Text.ParserCombinators.Parsec

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Data.List

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Data.Maybe (maybeToList)

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinimport Data.Char

3267af3f6fbf9743e64a9f019c745317f18cd9f7poirierimport Control.Monad

3267af3f6fbf9743e64a9f019c745317f18cd9f7poirier

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinimport Framework.AS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin-- * Parsing functions

cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end

cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end-- | Parse a library of specifications

f8b7daeb0e3f0ac4544fcc665de10c6b69a1ce0dsflibrary :: LogicGraph -> AParser st LIB_DEFN

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantzlibrary lG = do

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz (ps, ln) <- option (nullRange, emptyLibName "") $ do

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz s1 <- asKey libraryS

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz n <- libName

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz return (tokPos s1, n)

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz an <- annos

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz ls <- libItems lG

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return (Lib_defn ln ls ps an)

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin-- | Parse library name

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlibName :: AParser st LibName

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlibName = do

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin libid <- libId

35ff2d06df95b9593ee312dfff883c76f3b97798noodl v <- optionMaybe version

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return $ LibName libid v

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin-- | Parse the library version

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinversion :: AParser st VersionNumber

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinversion = do

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd s <- asKey versionS

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd pos <- getPos

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin n <- sepBy1 (many1 digit) (string dotS)

35ff2d06df95b9593ee312dfff883c76f3b97798noodl skip

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return (VersionNumber n (tokPos s `appRange` Range [pos]))

3267af3f6fbf9743e64a9f019c745317f18cd9f7poirier

3267af3f6fbf9743e64a9f019c745317f18cd9f7poirier-- | Parse library ID

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlibId :: AParser st LibId

f8b7daeb0e3f0ac4544fcc665de10c6b69a1ce0dsflibId = do

f8b7daeb0e3f0ac4544fcc665de10c6b69a1ce0dsf pos <- getPos

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin path <- sepBy1 (many1 $ satisfy $ \ c -> isAlphaNum c || elem c "_-+'")

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (string "/")

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin skip

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz return $ IndirectLink (intercalate "/" path) (Range [pos])

f8b7daeb0e3f0ac4544fcc665de10c6b69a1ce0dsf "" noTime

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz -- ??? URL need to be added

a7a43799fed7fcdeaa70584dbd3ecd130b25deb3noodl

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz-- | Parse the library elements

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlibItems :: LogicGraph -> AParser st [Annoted LIB_ITEM]

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlibItems l =

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (eof >> return [])

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> do

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz r <- libItem l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin la <- lineAnnos

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin an <- annos

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin is <- libItems $ case r of

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin Logic_decl logN _ ->

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin setLogicName logN l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin _ -> l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin case is of

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin [] -> return [Annoted r nullRange [] $ la ++ an]

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin Annoted i p nl ra : rs ->

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return $ Annoted r nullRange [] la : Annoted i p (an ++ nl) ra : rs

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin-- | Parse an element of the library

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlibItem :: LogicGraph -> AParser st LIB_ITEM

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirinlibItem l =

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin -- spec defn

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin do s <- asKey specS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin n <- simpleId

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin g <- generics l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin e <- equalT

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin a <- aSpec l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin q <- optEnd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return (Syntax.AS_Library.Spec_defn n g a

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (catRange ([s, e] ++ maybeToList q)))

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> -- view defn

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin do s1 <- asKey viewS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin vn <- simpleId

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin g <- generics l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin s2 <- asKey ":"

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin vt <- viewType l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (symbMap, ps) <- option ([], []) $ do

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin s <- equalT

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (m, _) <- parseMapping l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return (m, [s])

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin q <- optEnd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return (Syntax.AS_Library.View_defn vn g vt symbMap

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (catRange ([s1, s2] ++ ps ++ maybeToList q)))

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> -- unit spec

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin do kUnit <- asKey unitS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin kSpec <- asKey specS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin name <- simpleId

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin kEqu <- equalT

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin usp <- unitSpec l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin kEnd <- optEnd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return (Syntax.AS_Library.Unit_spec_defn name usp

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz (catRange ([kUnit, kSpec, kEqu] ++ maybeToList kEnd)))

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz <|> -- ref spec

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz do kRef <- asKey refinementS

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz name <- simpleId

a7a43799fed7fcdeaa70584dbd3ecd130b25deb3noodl kEqu <- equalT

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz rsp <- refSpec l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin kEnd <- optEnd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return (Syntax.AS_Library.Ref_spec_defn name rsp

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (catRange ([kRef, kEqu] ++ maybeToList kEnd)))

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> -- arch spec

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz do kArch <- asKey archS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin kASpec <- asKey specS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin name <- simpleId

aa0b2780958e9b1467c9d0153a05738e399811a5nd kEqu <- equalT

9a367ec3d570bcbaf8923dad66cb3b1532963964trawick asp <- annotedArchSpec l

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin kEnd <- optEnd

aa0b2780958e9b1467c9d0153a05738e399811a5nd return (Syntax.AS_Library.Arch_spec_defn name asp

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (catRange ([kArch, kASpec, kEqu] ++ maybeToList kEnd)))

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> -- download

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin do s1 <- asKey fromS

9a367ec3d570bcbaf8923dad66cb3b1532963964trawick iln <- libName

9a367ec3d570bcbaf8923dad66cb3b1532963964trawick s2 <- asKey getS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (il, ps) <- downloadItems

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin q <- optEnd

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin return (Download_items iln il

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin (catRange ([s1, s2] ++ ps ++ maybeToList q)))

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin <|> -- logic

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin do s <- asKey logicS

8951c7d73bfa2ae5a2c8fe5bd27f3e677be02564noirin logN@(Logic_name t _ _) <- logicName

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz return (Logic_decl logN (catRange [s, t]))

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz <|> -- newlogic

1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz do (n, s1) <- newlogicP

1b390add6886fb1c0acdea82be0ef0920f1158casf s2 <- equalT

1b390add6886fb1c0acdea82be0ef0920f1158casf (ml, s3) <- metaP

1b390add6886fb1c0acdea82be0ef0920f1158casf (s, s4) <- syntaxP

1b390add6886fb1c0acdea82be0ef0920f1158casf (m, s5) <- modelsP

1b390add6886fb1c0acdea82be0ef0920f1158casf (f, s6) <- foundationP

1b390add6886fb1c0acdea82be0ef0920f1158casf (p, s7) <- proofsP

1b390add6886fb1c0acdea82be0ef0920f1158casf (pa, s8) <- patternsP

1b390add6886fb1c0acdea82be0ef0920f1158casf q <- optEnd

1b390add6886fb1c0acdea82be0ef0920f1158casf return (Newlogic_defn (LogicDef n ml s m f p pa)

1b390add6886fb1c0acdea82be0ef0920f1158casf (catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))

1b390add6886fb1c0acdea82be0ef0920f1158casf <|> -- newcomorphism

1b390add6886fb1c0acdea82be0ef0920f1158casf do (n, s1) <- newcomorphismP

1b390add6886fb1c0acdea82be0ef0920f1158casf s2 <- equalT

1b390add6886fb1c0acdea82be0ef0920f1158casf (ml, s3) <- metaP

1b390add6886fb1c0acdea82be0ef0920f1158casf (s, s4) <- sourceP

1b390add6886fb1c0acdea82be0ef0920f1158casf (t, s5) <- targetP

1b390add6886fb1c0acdea82be0ef0920f1158casf (sv, s6) <- syntaxP

1b390add6886fb1c0acdea82be0ef0920f1158casf (pv, s8) <- proofsP

1b390add6886fb1c0acdea82be0ef0920f1158casf (mv, s7) <- modelsP

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd q <- optEnd

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return (Newcomorphism_defn (ComorphismDef n ml s t sv pv mv)

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd (catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))

0066eddda7203f6345b56f77d146a759298dc635gryzor <|> -- just a spec (turned into "spec spec = sp")

0066eddda7203f6345b56f77d146a759298dc635gryzor do p1 <- getPos

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd a <- aSpec l

50039065d571fe01fd458a3f031c995a1fd53c22rbowen p2 <- getPos

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd if p1 == p2 then fail "cannot parse spec" else

bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return (Syntax.AS_Library.Spec_defn (mkSimpleId "")

(Genericity (Params []) (Imported []) nullRange) a nullRange)

downloadItems :: AParser st (DownloadItems, [Token])

downloadItems = do

(il, ps) <- separatedBy itemNameOrMap anSemiOrComma

return (ItemMaps il, ps)

<|> do

s <- asKey mapsTo

i <- simpleId

return (UniqueItem i, [s])

-- | Parse view type

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)

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 :: AParser st ItemNameMap

itemNameOrMap = do

i1 <- simpleIdOrDDottedId

i2 <- optionMaybe $ do

_ <- asKey mapsTo

if isInfixOf ".." $ tokStr i1

then simpleIdOrDDottedId else simpleId

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 (Token, Token)

newlogicP = do

s <- asKey newlogicS

n <- simpleId

return (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 (Token, Token)

syntaxP = do

s <- asKey syntaxS

t <- simpleIdOrDDottedId

return (t, s)

modelsP :: AParser st (Token, Token)

modelsP = do

s <- asKey modelsS

m <- simpleIdOrDDottedId

return (m, s)

<|> return (nullTok, nullTok)

foundationP :: AParser st (Token, Token)

foundationP = do

s <- asKey foundationS

f <- simpleId

return (f, s)

<|> return (nullTok, nullTok)

proofsP :: AParser st (Token, Token)

proofsP = do

s <- asKey proofsS

p <- simpleIdOrDDottedId

return (p, s)

<|> return (nullTok, nullTok)

patternsP :: AParser st (Token, Token)

patternsP = do

s <- asKey patternsS

p <- simpleId

return (p, s)

<|> return (nullTok, nullTok)

newcomorphismP :: AParser st (Token, Token)

newcomorphismP = do

-- add newcomorphismS = "newcomorphism" in

s <- asKey newcomorphismS

n <- simpleId

return (n, s)

sourceP :: AParser st (Token, Token)

sourceP = do

s <- asKey sourceS

sl <- simpleIdOrDDottedId

return (sl, s)

targetP :: AParser st (Token, Token)

targetP = do

s <- asKey targetS

tl <- simpleIdOrDDottedId

return (tl, s)