Parse_AS_Structured.hs revision 3b4439aa37e4229ad6e83d46bd303c2799784c80
$Id$
Author: Till Mossakowski, Christian Maeder
Year: 2002/2003
Parsing the Structured part of hetrogenous specifications.
from 25 March 2001
C.2.2 Structured Specifications
todo:
fixing of details concerning annos
logic translations and implicit coercions
"and" should do union of involved logics
therefore, logic should be explicit argument instead of kept in the state
arch specs
-}
module Parse_AS_Structured where
import Grothendieck
import Logic
import Logic_CASL -- we need the default logic
import AS_Structured
import AS_Library
import AS_Annotation
import Anno_Parser
import Id(tokPos)
import Keywords
import Lexer
import Token
import Parsec
import ParsecChar (digit)
import Id
import List
import Maybe(maybeToList)
import Print_AS_Structured -- for test purposes
import Print_HetCASL
------------------------------------------------------------------------
-- annotation adapter
------------------------------------------------------------------------
asKey = pToken . toKey
-- skip to leading annotation and read many
annos :: GenParser Char st [Annotation]
annos = skip >> many (annotationL << skip)
annoParser parser = bind (\x y -> Annoted y [] x []) annos parser
annoParser2 parser = bind (\x (Annoted y pos l r) -> Annoted y pos (x++l) r) annos parser
emptyAnno :: a -> Annoted a
emptyAnno x = Annoted x [] [] []
------------------------------------------------------------------------
-- simpleIds for spec- and view-name
------------------------------------------------------------------------
logicS = "logic" -- new keyword
simpleId = pToken (reserved (logicS:casl_reserved_words) scanAnyWords)
------------------------------------------------------------------------
-- logic and encoding names
------------------------------------------------------------------------
-- exclude colon (because encoding must be recognized)
-- ecclude dot to recognize optional sublogic name
otherChars = "_`"
-- better list what is allowed rather than exclude what is forbidden
-- white spaces und non-printables should be not allowed!
encodingName = pToken(reserved (funS:casl_reserved_words) (many1
(oneOf (otherChars ++ (signChars \\ ":."))
<|> scanLPD)))
-- keep these identical in order to
-- decide after seeing ".", ":" or "->" what was meant
logicName = do e <- encodingName
do string dotS
s <- encodingName
return (Logic_name e (Just s))
<|> return (Logic_name e Nothing)
------------------------------------------------------------------------
-- parse Logic_code
------------------------------------------------------------------------
parseLogic :: GenParser Char AnyLogic Logic_code
parseLogic =
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 lid <- getState
(cs, ps) <- callParser (parse_symb_map_items lid) (language_name lid) "symbol maps"
`separatedBy` commaT
-- ??? should be plainComma, but does not work for reveal s,t!
return (G_symb_map_items_list lid 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 lid <- getState
(cs, ps) <- callParser (parse_symb_items lid) (language_name lid) "symbols"
`separatedBy` plainComma
return (G_symb_items_list lid 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
<|> {-do lookAhead (oBraceT <|> ((simpleId << annos)
`followedWith`
(asKey withS <|> asKey hideS
<|> asKey revealS <|> asKey andS
<|> asKey thenS <|> cBraceT
<|> asKey withinS <|> asKey endS
<|> oBracketT <|> cBracketT
<|> (eof >> return (Token "" nullPos)))
))-}
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 lid <- getState
bspec <- callParser (parse_basic_spec lid) (language_name lid)
"basic specification"
return (Basic_spec (G_basic_spec lid bspec))
logicSpec :: LogicGraph -> GenParser Char AnyLogic SPEC
logicSpec l = do
s1 <- asKey logicS
log <- logicName
let Logic_name t _ = log
s2 <- asKey ":"
oldlog <- getState
let newlog = lookupLogic log l
logtrans = coercelog newlog oldlog
setState newlog
sp <- annoParser (specE l)
setState oldlog
let sp1 = Qualified_spec log sp (map tokPos [s1,t,s2])
return (logtrans sp1)
lookupLogic (Logic_name log sublog) (logics,_) =
case find (\(Logic lid) -> language_name lid == tokStr log) logics of
Nothing -> error ("logic "++tokStr log++" unknown")
Just (Logic lid) ->
case sublog of
Nothing -> Logic lid
Just s ->
case find (\sub -> tokStr s `elem` sublogic_names lid sub)
(all_sublogics lid) of
Nothing -> error ("sublogic "++tokStr s++
" in logic "++tokStr log++" unknown")
Just sub -> Logic lid -- ??? can we throw away sublogic?
coercelog (Logic newlid) (Logic oldlid) =
if newlang == oldlang then id
else error ("Cannot coerce from "++newlang++" to "++oldlang)
where newlang = language_name newlid
oldlang = language_name oldlid
-- \sp -> Translation (emptyAnno sp) (Renaming [G_logic_translation (Logic_code...)] [])
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 ps)
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 lid <- getState
(symbit,ps) <- option (G_symb_map_items_list lid [],[])
(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 libid <- libId
v <- option Nothing (fmap Just version)
return (case v of
Nothing -> Lib_id libid
Just v1 -> Lib_version libid 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++" ...")