d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettich

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettich{- HetCATS/Parse_AS_Structured.hs

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder $Id$

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder Author: Till Mossakowski, Christian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder Year: 2002/2003

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettich

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder Parsing the Structured part of hetrogenous specifications.

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder http://www.cofi.info/Documents/CASL/Summary/

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder from 25 March 2001

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder C.2.2 Structured Specifications

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder todo:

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder fixing of details concerning annos

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder logic translations

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder arch specs

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder-}

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maedermodule Parse_AS_Structured where

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maederimport Grothendieck

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederimport Logic

ea608ca1c00ddcee3d3605b96767b9a116c697fdHeng Jiang

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maederimport Logic_CASL -- we need the default logic

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maederimport AS_Structured

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maederimport AS_Library

c9b52747a3b65bdf60f47a842a767eb58d7c2b09Klaus Luettichimport AS_Annotation

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederimport Anno_Parser

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederimport Id(tokPos)

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maederimport Keywords

c9b52747a3b65bdf60f47a842a767eb58d7c2b09Klaus Luettichimport Lexer

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederimport Token

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maederimport Parsec

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maederimport ParsecChar (digit)

ea608ca1c00ddcee3d3605b96767b9a116c697fdHeng Jiangimport Id

ea608ca1c00ddcee3d3605b96767b9a116c697fdHeng Jiangimport List

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettich

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederimport Maybe(maybeToList)

ea608ca1c00ddcee3d3605b96767b9a116c697fdHeng Jiang

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettichimport Print_AS_Structured -- for test purposes

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederimport Print_HetCASL

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder------------------------------------------------------------------------

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder-- annotation adapter

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder------------------------------------------------------------------------

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder

6588ecc93db54073b171dfa13fdb1edabaad326bChristian MaederasKey = pToken . toKey

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder-- skip to leading annotation and read many

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederannos :: GenParser Char st [Annotation]

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maederannos = skip >> many (annotationL << skip)

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian Maeder

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian MaederannoParser parser = bind (\x y -> Annoted y [] x []) annos parser

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian Maeder

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian MaederannoParser2 parser = bind (\x (Annoted y pos l r) -> Annoted y pos (x++l) r) annos parser

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian Maeder

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian MaederemptyAnno :: a -> Annoted a

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian MaederemptyAnno x = Annoted x [] [] []

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian Maeder

c5e74fe76415b43abbed77f869f7d8e24de817e8Christian Maeder------------------------------------------------------------------------

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder-- simpleIds for spec- and view-name

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder------------------------------------------------------------------------

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder

6588ecc93db54073b171dfa13fdb1edabaad326bChristian MaederlogicS = "logic" -- new keyword

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder

6588ecc93db54073b171dfa13fdb1edabaad326bChristian MaedersimpleId = pToken (reserved (logicS:casl_reserved_words) scanAnyWords)

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder------------------------------------------------------------------------

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder-- logic and encoding names

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder------------------------------------------------------------------------

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder-- exclude colon (because encoding must be recognized)

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder-- ecclude dot to recognize optional sublogic name

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettich

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus LuettichotherChars = "_`"

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder

ea608ca1c00ddcee3d3605b96767b9a116c697fdHeng Jiang-- better list what is allowed rather than exclude what is forbidden

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettich-- white spaces und non-printables should be not allowed!

c9b52747a3b65bdf60f47a842a767eb58d7c2b09Klaus LuettichencodingName = pToken(reserved (funS:casl_reserved_words) (many1

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder (oneOf (otherChars ++ (signChars \\ ":."))

5fe1c87d7201d2e97d4ef280c9af0c6eb026e575Christian Maeder <|> scanLPD)))

d6db74366285d5a0ffec71ac252cfa29800c4855Klaus Luettich

6588ecc93db54073b171dfa13fdb1edabaad326bChristian Maeder-- keep these identical in order to

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder-- decide after seeing ".", ":" or "->" what was meant

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian MaederlogicName = do e <- encodingName

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder do string dotS

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder s <- encodingName

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder return (Logic_name e (Just s))

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder <|> return (Logic_name e Nothing)

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder------------------------------------------------------------------------

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder-- parse Logic_code

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder------------------------------------------------------------------------

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian Maeder

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian MaederparseLogic :: GenParser Char AnyLogic Logic_code

f7ef12bb40487f5f910c267aa6c1bf186a8d2752Christian MaederparseLogic =

do l <- asKey logicS

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

case e of

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

Logic_name f Nothing ->

do c <- asKey colonS

parseLogAfterColon (Just f) [l,c]

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

<|> do f <- asKey funS -- parse at least a logic target after "logic"

t <- logicName

return (Logic_code Nothing Nothing (Just t) (map tokPos [l,f]))

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

parseLogAfterColon e l =

do s <- logicName

parseOptLogTarget e (Just s) l

<|> return (Logic_code e (Just s) Nothing (map tokPos l))

<|> parseOptLogTarget e Nothing l

<|> return (Logic_code e Nothing Nothing (map tokPos l))

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

parseOptLogTarget e s l =

do f <- asKey funS

do t <- logicName

return (Logic_code e s (Just t) (map tokPos (l++[f])))

<|> return (Logic_code e s Nothing (map tokPos (l++[f])))

------------------------------------------------------------------------

-- for parsing "," not followed by "logic" within G_mapping

------------------------------------------------------------------------

-- ParsecCombinator.notFollowedBy only allows to check for a single "tok"

-- thus a single Char.

notFollowedWith :: GenParser tok st a -> GenParser tok st b

-> GenParser tok st a

p1 `notFollowedWith` p2 = try ((p1 >> p2 >> pzero) <|> p1)

plainComma = commaT `notFollowedWith` asKey logicS

-- rearrange list to keep current logic as first element

-- does not consume anything! (may only fail)

{-switchLogic :: Logic_code -> LogicGraph -> GenParser Char st LogicGraph

switchLogic n l@(Logic i : _) =

let s = case n of

Logic_code _ _ (Just (Logic_name t _)) _ -> tokStr t

_ -> language_name i

(f, r) = partition (\ (Logic x) -> language_name x == s) l

in if null f then fail ("unknown language " ++ s)

else return (f++r)

-}

------------------------------------------------------------------------

-- parse G_mapping (if you modify this, do so for G_hiding, too!)

------------------------------------------------------------------------

parseItemsMap :: GenParser Char AnyLogic (G_symb_map_items_list, [Token])

parseItemsMap =

do Logic id <- getState

(cs, ps) <- callParser (parse_symb_map_items id) (language_name id) "symbol maps"

`separatedBy` commaT

-- ??? should be plainComma, but does not work for reveal s,t!

return (G_symb_map_items_list id cs, ps)

parseMapping :: LogicGraph -> GenParser Char AnyLogic ([G_mapping], [Token])

parseMapping l =

do n <- parseLogic

do c <- commaT

(gs, ps) <- parseMapping l

return (G_logic_translation n : gs, c:ps)

<|> return ([G_logic_translation n], [])

<|> do (m, ps) <- parseItemsMap

do c <- commaT

(gs, qs) <- parseMapping l

return (G_symb_map m : gs, ps ++ c : qs)

<|> return ([G_symb_map m], ps)

------------------------------------------------------------------------

-- parse G_hiding (copied from above, but code sharing would be better!)

------------------------------------------------------------------------

parseItemsList :: LogicGraph -> GenParser Char AnyLogic (G_symb_items_list, [Token])

parseItemsList l =

do Logic id <- getState

(cs, ps) <- callParser (parse_symb_items id) (language_name id) "symbols"

`separatedBy` plainComma

return (G_symb_items_list id cs, [])

parseHiding :: LogicGraph -> GenParser Char AnyLogic ([G_hiding], [Token])

parseHiding l =

do n <- parseLogic

do c <- commaT

(gs, ps) <- parseHiding l

return (G_logic_projection n : gs, c:ps)

<|> return ([G_logic_projection n], [])

<|> do (m, ps) <- parseItemsList l

do c <- commaT

(gs, qs) <- parseHiding l

return (G_symb_list m : gs, ps ++ c : qs)

<|> return ([G_symb_list m], ps)

parseRevealing :: LogicGraph -> GenParser Char AnyLogic (G_symb_map_items_list, [Token])

parseRevealing l = undefined

------------------------------------------------------------------------

-- specs

------------------------------------------------------------------------

spec :: LogicGraph -> GenParser Char AnyLogic (Annoted SPEC)

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

return (case sps of

[sp] -> sp

otherwise -> emptyAnno (Extension sps (map tokPos ps)))

specA :: LogicGraph -> GenParser Char AnyLogic (Annoted SPEC)

specA l = do (sps,ps) <- annoParser (specB l) `separatedBy` (asKey andS)

return (case sps of

[sp] -> sp

otherwise -> emptyAnno (Union sps (map tokPos ps)))

specB :: LogicGraph -> GenParser Char AnyLogic SPEC

specB l = do p1 <- asKey localS

sp1 <- aSpec l

p2 <- asKey withinS

sp2 <- annoParser (specB l)

return (Local_spec sp1 sp2 (map tokPos [p1,p2]))

<|> do sp <- specC l

return (item sp) -- ??? what to do with anno?

specC :: LogicGraph -> GenParser Char AnyLogic (Annoted SPEC)

specC l = do sp <- annoParser (specD l)

translation_list l sp

translation_list l sp =

do sp' <- translation l sp

translation_list l sp'

<|> return sp

translation l sp =

do p <- asKey withS

(m, ps) <- parseMapping l

return (emptyAnno (Translation sp (Renaming m (map tokPos (p:ps)))))

<|> do p <- asKey hideS

(m, ps) <- parseHiding l

return (emptyAnno (Reduction sp (Hidden m (map tokPos (p:ps)))))

<|> do p <- asKey revealS

(m, ps) <- parseItemsMap

return (emptyAnno (Reduction sp (Revealed m (map tokPos (p:ps)))))

specD :: LogicGraph -> GenParser Char AnyLogic SPEC

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

specD l = do (p,sp) <- try (do p <- asKey freeS

sp <- groupSpec l

return (p,sp))

return (Free_spec (emptyAnno sp) [tokPos p])

<|> do (p,sp) <- try (do p <- asKey cofreeS

sp <- groupSpec l

return (p,sp))

return (Cofree_spec (emptyAnno sp) [tokPos p])

<|> do p <- asKey closedS

sp <- groupSpec l

return (Closed_spec (emptyAnno sp) [tokPos p])

<|> specE l

specE :: LogicGraph -> GenParser Char AnyLogic SPEC

specE l = do lookAhead (try (oBraceT >> cBraceT)) -- avoid overlap with group spec

basicSpec l

<|> groupSpec l

<|> logicSpec l

<|> basicSpec l

callParser p name itemType = do

s <- getInput

pos <- getPosition

(x,rest,line,col) <- case p of

Nothing -> fail ("no "++itemType++" parser for language "

++ name)

Just p -> return (p (sourceName pos)

(sourceLine pos)

(sourceColumn pos) s)

setInput rest

let pos' = setSourceColumn (setSourceLine pos line) col

setPosition pos'

return x

basicSpec :: LogicGraph -> GenParser Char AnyLogic SPEC

basicSpec l = do Logic id <- getState

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

"basic specification"

return (Basic_spec (G_basic_spec id bspec))

logicSpec :: LogicGraph -> GenParser Char AnyLogic SPEC

logicSpec l = do

s1 <- asKey logicS

log <- logicName

let Logic_name t _ = log

s2 <- asKey ":"

setState (lookupLogic log l)

sp <- annoParser (specE l)

return (Qualified_spec log sp (map tokPos [s1,t,s2]))

lookupLogic (Logic_name log sublog) (logics,_) =

case find (\(Logic id) -> language_name id == tokStr log) logics of

Nothing -> error ("logic "++tokStr log++" unknown")

Just (Logic id) ->

case sublog of

Nothing -> Logic id

Just s ->

case find (\sub -> tokStr s `elem` sublogic_names id sub)

(all_sublogics id) of

Nothing -> error ("sublogic "++tokStr s++

" in logic "++tokStr log++" unknown")

Just sub -> Logic id -- ??? can we throw away sublogic?

aSpec l = annoParser2 (spec l)

groupSpec l = do b <- oBraceT

a <- aSpec l

c <- cBraceT

return (Group a (map tokPos [b, c]))

<|>

do n <- simpleId

(f,ps) <- fitArgs l

return (Spec_inst n f)

-- ??? What to do with ps? Spec_inst is not consistent here!

fitArgs :: LogicGraph -> GenParser Char AnyLogic ([Annoted FIT_ARG],[Pos])

fitArgs l = do fas <- many (fitArg l)

let (fas1,ps) = unzip fas

return (fas1,concat ps)

fitArg :: LogicGraph -> GenParser Char AnyLogic (Annoted FIT_ARG,[Pos])

fitArg l = do b <- oBracketT

fa <- annoParser (fittingArg l)

c <- cBracketT

return (fa,[tokPos b,tokPos c])

fittingArg :: LogicGraph -> GenParser Char AnyLogic FIT_ARG

fittingArg l = do (an,s) <- try (do an <- annos

s <- asKey viewS

return (an,s))

vn <- simpleId

(fa,ps) <- fitArgs l

return (Fit_view vn fa (tokPos s:ps) an)

<|>

do sp <- aSpec l

Logic id <- getState

(symbit,ps) <- option (G_symb_map_items_list id [],[])

(do s <- asKey fitS

(m, ps) <- parseItemsMap

return (m,[tokPos s]))

return (Fit_spec sp symbit ps)

optEnd = option Nothing (fmap Just (asKey endS))

generics l = do

(pa,ps1) <- params l

(imp,ps2) <- option ([],[]) (imports l)

return (Genericity (Params pa) (Imported imp) (ps1++ps2))

params :: LogicGraph -> GenParser Char AnyLogic ([Annoted SPEC],[Pos])

params l = do pas <- many (param l)

let (pas1,ps) = unzip pas

return (pas1,concat ps)

param :: LogicGraph -> GenParser Char AnyLogic (Annoted SPEC,[Pos])

param l = do b <- oBracketT

pa <- aSpec l

c <- cBracketT

return (pa,[tokPos b,tokPos c])

imports l = do s <- asKey givenS

(sps,ps) <- annoParser (groupSpec l) `separatedBy` commaT

return (sps,map tokPos (s:ps))

libItem l = -- spec defn

do s <- asKey specS

n <- simpleId

g <- generics l

e <- asKey equalS

a <- aSpec l

q <- optEnd

return (AS_Library.Spec_defn n g a (map tokPos ([s, e] ++ Maybe.maybeToList q)))

<|> -- view defn

do s1 <- asKey viewS

vn <- simpleId

g <- generics l

s2 <- asKey ":"

vt <- viewType l

(symbMap,ps) <- option ([],[])

(do s <- asKey equalS

(m, ps) <- parseMapping l

return (m,[s]))

q <- optEnd

return (AS_Library.View_defn vn g vt symbMap

(map tokPos ([s1,s2] ++ ps ++ Maybe.maybeToList q)))

<|> -- download

do s1 <- asKey fromS

ln <- libName

s2 <- asKey getS

(il,ps) <- itemNameOrMap `separatedBy` commaT

q <- optEnd

return (Download_items ln il

(map tokPos ([s1,s2]++ps++ Maybe.maybeToList q)))

<|> -- logic

do s1 <- asKey logicS

log <- logicName

let Logic_name t _ = log

setState (lookupLogic log l)

return (Logic_decl log (map tokPos [s1,t]))

viewType l = do sp1 <- annoParser (groupSpec l)

s <- asKey toS

sp2 <- annoParser (groupSpec l)

return (View_type sp1 sp2 [tokPos s])

libName = do lid <- libId

v <- option Nothing (fmap Just version)

return (case v of

Nothing -> Lib_id lid

Just v1 -> Lib_version lid v1)

libId = do pos <- getPosition

path <- scanAnyWords `sepBy1` (string "/")

skip

return (Indirect_link (concat (intersperse "/" path)) [pos])

-- ??? URL need to be added

version = do s <- asKey versionS

pos <- getPosition

n <- many1 digit `sepBy1` (string ".")

skip

return (Version_number n ([tokPos s, pos]))

itemNameOrMap = do i1 <- simpleId

i' <- option Nothing (do

s <- asKey "|->"

i <- simpleId

return (Just (i,s)))

return (case i' of

Nothing -> Item_name i1

Just (i2,s) -> Item_name_map i1 i2 [tokPos s])

library l = do skip

s1 <- asKey libraryS

ln <- libName

an <- annos

ls <- many (annoParser (libItem l))

eof

return (Lib_defn ln ls [tokPos s1] an)

-------------------------------------------------------------

-- Testing

-------------------------------------------------------------

mylogicGraph = ([Logic CASL],[])

parseSPEC fname =

do input <- readFile fname

case runParser (do x <- spec mylogicGraph

s1<-getInput

return (x,s1))

(Logic CASL) fname input of

Left err -> error (show err)

Right x -> return x

parseLib fname =

do input <- readFile fname

case runParser (do x <- library mylogicGraph

s1<-getInput

return (x,s1))

(Logic CASL) fname input of

Left err -> error (show err)

Right x -> return x

test fname = do

(x,errs) <- parseLib fname

putStrLn (show (printText0_eGA x))

if errs == "" then return ()

else putStrLn ("\nUnread input:\n"++take 20 errs++" ...")