Print_AS_Library.hs revision 8d901fd5053fb152680165ed98a5e53a0e1b69f7
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder{- |
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederModule : $Header$
7895bc4f90d3ea250877c02a897f5dcca4590a89Christian MaederDescription : pretty printing of CASL specification libaries
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederCopyright : (c) Klaus Luettich, Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederMaintainer : Christian.Maeder@dfki.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederPortability : non-portable(Grothendieck)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederPretty printing of CASL specification libaries
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-}
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maedermodule Syntax.Print_AS_Library () where
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maeder
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maederimport Data.Maybe (maybeToList)
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maeder
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maederimport Common.AS_Annotation
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maederimport Common.IRI
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maederimport Common.Doc
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maederimport Common.DocUtils
9ba43c9323dc1a4bb1e684d87370b43468ab9096Christian Maederimport Common.Keywords
cbe26e1cedf1e305b077afa82cb5f46850cdb8b1Christian Maederimport Common.LibName
21095d13d876edd444df223f34d14efa85ba58c1Christian Maeder
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maederimport Logic.Grothendieck
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescuimport Syntax.AS_Structured
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maederimport Syntax.AS_Library
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maeder
3b5d1e9f95905d6595b3bb01b54499a37a3d82acChristian Maederimport Syntax.Print_AS_Architecture ()
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maederimport Syntax.Print_AS_Structured
434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maederinstance PrettyLG LIB_DEFN where
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maeder prettyLG lg (Lib_defn aa ab _ ad) =
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maeder let aa' = pretty aa -- lib name
0d72630889db51ffe7a0336cbb7fde5dbe415e9dEwaryst Schulz ab' = vsep $ printLibItems lg ab -- LIB_ITEMs
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly ad' = vcat $ map pretty ad -- global ANNOTATIONs
0d72630889db51ffe7a0336cbb7fde5dbe415e9dEwaryst Schulz in (if aa == emptyLibName "" then empty else
3b5d1e9f95905d6595b3bb01b54499a37a3d82acChristian Maeder keyword libraryS <+> aa') $++$ ad' $++$ ab'
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder
b2542911be8b16ffb988c3abe09ee63be98e119fChristian MaederprintLibItems :: LogicGraph -> [Annoted LIB_ITEM] -> [Doc]
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian MaederprintLibItems lg is = case is of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder [] -> []
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder i : rs -> prettyLG lg i : printLibItems (case item i of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Logic_decl aa _ -> setLogicName aa lg
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder _ -> lg) rs
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wanginstance PrettyLG LIB_ITEM where
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang prettyLG lg li = case li of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Spec_defn si (Genericity aa@(Params pl) ab@(Imported il) _) ac' _ ->
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let las = l_annos ac'
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder (sa, ac) = if startsWithSemanticAnno las then
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder (equals <+> annoDoc (head las),
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder ac' { l_annos = tail las })
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder else (equals, ac')
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder x : r = case skipVoidGroup $ item ac of
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maeder Extension e@(_ : _) _ ->
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder printExtension lg $ moveAnnos ac e
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang Union u@(_ : _) _ ->
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder printUnion lg $ moveAnnos ac u
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang _ -> [prettyLG lg ac]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder spid = indexed (iriToStringShortUnsecure si)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sphead = if null il then
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder if null pl then spid <+> sa
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder else cat [spid, printPARAMS lg aa <+> sa]
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder else sep [ cat [spid, printPARAMS lg aa]
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder , printIMPORTED lg ab <+> sa]
9ba43c9323dc1a4bb1e684d87370b43468ab9096Christian Maeder in if null (iriToStringShortUnsecure si) && null pl
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder then prettyLG lg ac' else
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder vcat $ (topKey specS <+> vcat [sphead, x]) : r
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maeder ++ [keyword endS]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder View_defn si (Genericity aa@(Params pl) ab@(Imported il) _)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder (View_type frm to _) ad _ ->
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder let spid = structIRI si
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder sphead = if null il then
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang if null pl then spid <+> colon
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder else cat [spid, printPARAMS lg aa <+> colon]
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder else sep [ cat [spid, printPARAMS lg aa]
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder , printIMPORTED lg ab <+> colon]
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder in topKey viewS <+>
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder sep ([sphead, sep [ printGroupSpec lg frm <+> keyword toS
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder , (if null ad then id else (<+> equals))
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder $ printGroupSpec lg to]]
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder ++ [ppWithCommas ad])
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder $+$ keyword endS
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder Equiv_defn si (Equiv_type as1 as2 _) sp _ -> topKey equivalenceS <+>
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sep [structIRI si <+> colon, sep
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder [ printGroupSpec lg $ emptyAnno as1
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang , text equiS
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang , printGroupSpec lg $ emptyAnno as2]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder <+> equals, prettyLG lg sp]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder $+$ keyword endS
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder Align_defn si ar (Align_type frm to _) corresps _ ->
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder let spid = indexed (iriToStringShortUnsecure si)
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder sphead = case ar of
a571b691ac0da91a895c33f250509622004dcf03Christian Maeder Nothing -> spid <+> colon
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang Just alignArities -> sep
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder [spid, printAlignArities alignArities <+> colon ]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder in topKey alignmentS <+>
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang sep ([sphead, sep [ printGroupSpec lg frm <+> keyword toS,
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder printGroupSpec lg to]]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder ++ if null corresps then []
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder else [equals,
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder printCorrespondences corresps])
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder $+$ keyword endS
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder Module_defn mn mt rs _ ->
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder let spid = indexed (iriToStringShortUnsecure mn)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sphead = spid <+> colon
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder spmt = case mt of
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder Module_type sp1 sp2 _ -> sep
a571b691ac0da91a895c33f250509622004dcf03Christian Maeder [prettyLG lg sp1, text ofS, prettyLG lg sp2]
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder in topKey moduleS <+>
a571b691ac0da91a895c33f250509622004dcf03Christian Maeder sep [sphead, spmt, text forS, sep $ map structIRI rs]
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder Arch_spec_defn si ab _ -> topKey archS <+>
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder fsep [keyword specS, structIRI si <+> equals, prettyLG lg ab]
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder $+$ keyword endS
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder Unit_spec_defn si ab _ -> topKey unitS <+>
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder fsep [keyword specS, structIRI si <+> equals, prettyLG lg ab]
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder $+$ keyword endS
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder Ref_spec_defn si ab _ -> keyword refinementS <+>
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder fsep [structIRI si <+> equals, prettyLG lg ab]
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder $+$ keyword endS
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang Download_items l ab _ -> topKey fromS <+>
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder fsep ((pretty l <+> keyword getS) : prettyDownloadItems ab)
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang Logic_decl aa _ -> sep [keyword logicS, pretty aa]
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder Newlogic_defn nl _ -> pretty nl
fef03b64e3b1d7d3a8e098f62ef2e7687a433f09Christian Maeder Newcomorphism_defn nc _ -> pretty nc
9aef2f9a1f6d7557bc31bf4f9db235f7f0d5170dChristian Maeder
fef03b64e3b1d7d3a8e098f62ef2e7687a433f09Christian MaederprettyDownloadItems :: DownloadItems -> [Doc]
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian MaederprettyDownloadItems d = case d of
ade1f65c2bb98fbf45f8ef16bed4fa50802225a4Christian Maeder ItemMaps l -> punctuate comma $ map pretty l
9aef2f9a1f6d7557bc31bf4f9db235f7f0d5170dChristian Maeder UniqueItem i -> [mapsto, structIRI i]
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wanginstance PrettyLG GENERICITY where
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang prettyLG lg (Genericity aa ab _) =
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang sep [printPARAMS lg aa, printIMPORTED lg ab]
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder
57d9ffd4f0d821632c5dd116a5301c3305599b19Christian MaederprintPARAMS :: LogicGraph -> PARAMS -> Doc
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian MaederprintPARAMS lg (Params aa) = cat $ map (brackets . rmTopKey . prettyLG lg ) aa
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangprintIMPORTED :: LogicGraph -> IMPORTED -> Doc
eab576044505ba1fbc64610323053490fbd9e82cChristian MaederprintIMPORTED lg (Imported aa) = case aa of
57d9ffd4f0d821632c5dd116a5301c3305599b19Christian Maeder [] -> empty
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang _ -> sep [keyword givenS, sepByCommas $ map (printGroupSpec lg) aa]
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangprintAlignArities :: ALIGN_ARITIES -> Doc
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangprintAlignArities (Align_arities f b) =
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder sep [text alignArityForwardS, printAlignArity f,
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder text alignArityBackwardS, printAlignArity b]
8519df804b37f95a2394a6cd5662da02efa3400bChristian Maeder
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian MaederprintAlignArity :: ALIGN_ARITY -> Doc
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian MaederprintAlignArity ar = text $ case ar of
8519df804b37f95a2394a6cd5662da02efa3400bChristian Maeder AA_InjectiveAndTotal -> "1"
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang AA_Injective -> "?"
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang AA_Total -> "+"
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder AA_NeitherInjectiveNorTotal -> "*"
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder
8519df804b37f95a2394a6cd5662da02efa3400bChristian MaederprintCorrespondences :: [CORRESPONDENCE] -> Doc
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangprintCorrespondences = vsep . punctuate comma . map printCorrespondence
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangprintCorrespondence :: CORRESPONDENCE -> Doc
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangprintCorrespondence Default_correspondence = text "*"
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintCorrespondence (Correspondence_block mrref mconf cs) =
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sep $ concat
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian Maeder [[text relationS],
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder map printRelationRef $ maybeToList mrref,
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder map printConfidence $ maybeToList mconf,
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian Maeder [text "{"],
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder [printCorrespondences cs],
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder [text "}"]]
184449040f3b741bbb6a2e881415b30d624e2c63Christian Maeder
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian MaederprintCorrespondence (Single_correspondence mcid eRef toer mrRef mconf) =
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sep $ concat
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder [[indexed $ show eRef],
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang map printRelationRef $ maybeToList mrRef,
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder map printConfidence $ maybeToList mconf,
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder [pretty toer],
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder map pretty $ maybeToList mcid]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintConfidence :: CONFIDENCE -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -- "show" should work in [0,1]
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederprintConfidence = text . ('(' :) . (++ ")") . show
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder
e92e93922166c81167de83cc7400403c5d9bb26cChristian MaederprintRelationRef :: RELATION_REF -> Doc
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederprintRelationRef rref = case rref of
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder Subsumes -> text ">"
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder IsSubsumed -> text "<"
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder Equivalent -> text "="
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder Incompatible -> text "%"
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder HasInstance -> text "$\\ni$"
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder InstanceOf -> text "$\\in$"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder DefaultRelation -> text "$\\mapsto$"
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder Iri i -> structIRI i
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
6c4ee04931dded62728f3a9954b2799beed536e9Christian Maederinstance Pretty ItemNameMap where
6c4ee04931dded62728f3a9954b2799beed536e9Christian Maeder pretty (ItemNameMap a m) = fsep
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder $ structIRI a : case m of
434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder Nothing -> []
434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder Just b -> [mapsto, structIRI b]
434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder