5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu{- HetCATS/Parse_AS_Structured.hs

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu $Id$

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Author: Till Mossakowski, Christian Maeder

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu Year: 2002/2003

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu Parsing the Structured part of hetrogenous specifications.

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu http://www.cofi.info/Documents/CASL/Summary/

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu from 25 March 2001

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu C.2.2 Structured Specifications

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu todo:

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance fixing of details concerning annos

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu logic translations

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance arch specs

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-}

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mancemodule Parse_AS_Structured where

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport Grothendieck

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport Logic

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport Logic_CASL -- we need the default logic

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport AS_Structured

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport AS_Library

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport AS_Annotation

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport Anno_Parser

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport Id(tokPos)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport Keywords

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceimport Lexer

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport Token

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport Parsec

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport ParsecChar (digit)

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport Id

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport List

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport Maybe(maybeToList)

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport Print_AS_Structured -- for test purposes

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuimport Print_HetCASL

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu------------------------------------------------------------------------

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu-- annotation adapter

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu------------------------------------------------------------------------

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu-- skip to leading annotation and read many

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuannos :: GenParser Char st [Annotation]

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiuannos = skip >> many (annotationL << skip)

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

67fc6fe7ffa26acdf15b246a26161a5872aff8bcFelix Gabriel ManceannoParser parser = bind (\x y -> Annoted y [] x []) annos parser

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceannoParser2 parser = bind (\x (Annoted y pos l r) -> Annoted y pos (x++l) r) annos parser

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceemptyAnno :: a -> Annoted a

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceemptyAnno x = Annoted x [] [] []

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- simpleIds for spec- and view-name

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancelogicS = "logic" -- new keyword

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancesimpleId = pToken (reserved (logicS:casl_reserved_words) scanAnyWords)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- logic and encoding names

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- exclude colon (because encoding must be recognized)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- ecclude dot to recognize optional sublogic name

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceotherChars = "_`"

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- better list what is allowed rather than exclude what is forbidden

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- white spaces und non-printables should be not allowed!

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceencodingName = pToken(reserved (funS:casl_reserved_words) (many1

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance (oneOf (otherChars ++ (signChars \\ ":."))

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance <|> scanLPD)))

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- keep these identical in order to

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- decide after seeing ".", ":" or "->" what was meant

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancelogicName = do e <- encodingName

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do string dotS

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance s <- encodingName

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance return (Logic_name e (Just s))

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance <|> return (Logic_name e Nothing)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- parse Logic_code

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseLogic :: GenParser Char AnyLogic Logic_code

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseLogic =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do l <- asKey logicS

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance case e of

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Logic_name f Nothing ->

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do c <- asKey colonS

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance parseLogAfterColon (Just f) [l,c]

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

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance t <- logicName

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseLogAfterColon e l =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do s <- logicName

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance parseOptLogTarget e (Just s) l

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance <|> parseOptLogTarget e Nothing l

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseOptLogTarget e s l =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do f <- asKey funS

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do t <- logicName

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

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- for parsing "," not followed by "logic" within G_mapping

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- thus a single Char.

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancenotFollowedWith :: GenParser tok st a -> GenParser tok st b

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance -> GenParser tok st a

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceplainComma = commaT `notFollowedWith` asKey logicS

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- rearrange list to keep current logic as first element

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- does not consume anything! (may only fail)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance{-switchLogic :: Logic_code -> LogicGraph -> GenParser Char st LogicGraph

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceswitchLogic n l@(Logic i : _) =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance let s = case n of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Logic_code _ _ (Just (Logic_name t _)) _ -> tokStr t

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance _ -> language_name i

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

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance else return (f++r)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseItemsMap :: GenParser Char AnyLogic (G_symb_map_items_list, [Token])

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseItemsMap =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do Logic id <- getState

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance `separatedBy` commaT

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance return (G_symb_map_items_list id cs, ps)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseMapping :: LogicGraph -> GenParser Char AnyLogic ([G_mapping], [Token])

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseMapping l =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do n <- parseLogic

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do c <- commaT

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance (gs, ps) <- parseMapping l

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance return (G_logic_translation n : gs, c:ps)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance <|> return ([G_logic_translation n], [])

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance <|> do (m, ps) <- parseItemsMap

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do c <- commaT

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance (gs, qs) <- parseMapping l

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

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

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

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance------------------------------------------------------------------------

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseItemsList :: LogicGraph -> GenParser Char AnyLogic (G_symb_items_list, [Token])

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceparseItemsList l =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance do Logic id <- getState

67fc6fe7ffa26acdf15b246a26161a5872aff8bcFelix Gabriel Mance (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)) [(sourceLine pos, sourceColumn 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,(sourceLine pos, sourceColumn 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++" ...")