1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederModule : $Header$

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederDescription : pretty printing of CASL specification libaries

54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederCopyright : (c) Klaus Luettich, Uni Bremen 2002-2006

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederStability : provisional

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederPortability : non-portable(Grothendieck)

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederPretty printing of CASL specification libaries

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder-}

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maedermodule Syntax.Print_AS_Library () where

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maederimport Data.Maybe (maybeToList)

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maederimport Common.AS_Annotation

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maederimport Common.IRI

f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Lueckeimport Common.Doc

f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Lueckeimport Common.DocUtils

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maederimport Common.Keywords

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Common.LibName

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederimport Logic.Grothendieck

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederimport Syntax.AS_Structured

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederimport Syntax.AS_Library

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederimport Syntax.Print_AS_Architecture ()

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederimport Syntax.Print_AS_Structured

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederinstance PrettyLG LIB_DEFN where

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder prettyLG lg (Lib_defn aa ab _ ad) =

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder let aa' = pretty aa -- lib name

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder ab' = vsep $ printLibItems lg ab -- LIB_ITEMs

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder ad' = vcat $ map pretty ad -- global ANNOTATIONs

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder in (if getLibId aa == nullIRI then empty else

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder keyword libraryS <+> aa') $++$ ad' $++$ ab'

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder

6f08518fe3561930fef290b8e01384a6f1c90598Till MossakowskiprintLibItems :: LogicGraph -> [Annoted LIB_ITEM] -> [Doc]

6f08518fe3561930fef290b8e01384a6f1c90598Till MossakowskiprintLibItems lg is = case is of

6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski [] -> []

6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski i : rs -> prettyLG lg i : printLibItems (case item i of

6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski Logic_decl aa _ -> setLogicName aa lg

6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski _ -> lg) rs

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederinstance PrettyLG VIEW_TYPE where

ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder prettyLG = prettyViewType []

f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Luecke

1e39a4ee4e97d16c48003d49e4af3d181f25ad71Christian MaederprettyViewType :: [a] -> LogicGraph -> VIEW_TYPE -> Doc

1e39a4ee4e97d16c48003d49e4af3d181f25ad71Christian MaederprettyViewType ad lg (View_type frm to _) =

1e39a4ee4e97d16c48003d49e4af3d181f25ad71Christian Maeder sep [ printGroupSpec lg frm <+> keyword toS

f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Luecke , (if null ad then id else (<+> equals))

7ab2df3001654dd1b7a2cfc3da1ccef11c39a503Christian Maeder $ printGroupSpec lg to]

0a65899b09e78455a94af9128455f6613441ab71cmaeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederinstance PrettyLG LIB_ITEM where

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder prettyLG lg li = case li of

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder Spec_defn si (Genericity aa@(Params pl) ab@(Imported il) _) ac' _ ->

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder let las = l_annos ac'

d0642e0d269791a923f2bf86ea249f971f14addbChristian Maeder (sa, ac) = if startsWithSemanticAnno las then

(equals <+> annoDoc (head las),

ac' { l_annos = tail las })

else (equals, ac')

x : r = case skipVoidGroup $ item ac of

Extension e@(_ : _) _ ->

printExtension lg $ moveAnnos ac e

Union u@(_ : _) _ ->

printUnion lg $ moveAnnos ac u

_ -> [prettyLG lg ac]

spid = indexed (iriToStringShortUnsecure si)

sphead = if null il then

if null pl then spid <+> sa

else cat [spid, printPARAMS lg aa <+> sa]

else sep [ cat [spid, printPARAMS lg aa]

, printIMPORTED lg ab <+> sa]

in if null (iriToStringShortUnsecure si) && null pl

then prettyLG lg ac' else

vcat $ (topKey specS <+> vcat [sphead, x]) : r

++ [keyword endS]

View_defn si (Genericity aa@(Params pl) ab@(Imported il) _)

vt ad _ ->

let spid = structIRI si

sphead = if null il then

if null pl then spid <+> colon

else cat [spid, printPARAMS lg aa <+> colon]

else sep [ cat [spid, printPARAMS lg aa]

, printIMPORTED lg ab <+> colon]

in topKey viewS <+>

sep [sphead, prettyViewType ad lg vt, ppWithCommas ad]

$+$ keyword endS

Entail_defn si (Entail_type s1 s2 _) _ -> topKey entailmentS <+>

sep [structIRI si <+> equals

, prettyLG lg s1

, keyword entailsS

, prettyLG lg s2 ]

$+$ keyword endS

Equiv_defn si (Equiv_type as1 as2 _) sp _ -> topKey equivalenceS <+>

sep [structIRI si <+> colon, sep

[ prettyLG lg as1

, text equiS

, prettyLG lg as2]

<+> equals, prettyLG lg sp]

$+$ keyword endS

Align_defn si ar vt corresps _ ->

let spid = indexed (iriToStringShortUnsecure si)

sphead = case ar of

Nothing -> spid <+> colon

Just alignArities -> sep

[spid, printAlignArities alignArities <+> colon ]

in topKey alignmentS <+>

sep ([sphead, prettyViewType [] lg vt]

++ if null corresps then []

else [equals,

printCorrespondences corresps])

$+$ keyword endS

Module_defn mn mt rs _ ->

let spid = indexed (iriToStringShortUnsecure mn)

sphead = spid <+> colon

spmt = case mt of

Module_type sp1 sp2 _ -> sep

[prettyLG lg sp1, text ofS, prettyLG lg sp2]

in topKey moduleS <+>

sep [sphead, spmt, text forS, sep $ map structIRI rs]

Arch_spec_defn si ab _ -> topKey archS <+>

fsep [keyword specS, structIRI si <+> equals, prettyLG lg ab]

$+$ keyword endS

Unit_spec_defn si ab _ -> topKey unitS <+>

fsep [keyword specS, structIRI si <+> equals, prettyLG lg ab]

$+$ keyword endS

Ref_spec_defn si ab _ -> keyword refinementS <+>

fsep [structIRI si <+> equals, prettyLG lg ab]

$+$ keyword endS

Graph_defn si n _ -> keyword networkS <+>

fsep [structIRI si <+> equals, pretty n]

$+$ keyword endS

Download_items l ab _ -> topKey fromS <+>

fsep ((pretty l <+> keyword getS) : prettyDownloadItems ab)

Logic_decl aa _ -> pretty aa

Newlogic_defn nl _ -> pretty nl

Newcomorphism_defn nc _ -> pretty nc

instance PrettyLG OmsOrNetwork where

prettyLG lg s = case s of

MkOms o -> printGroupSpec lg o

MkNetwork n -> pretty n

prettyDownloadItems :: DownloadItems -> [Doc]

prettyDownloadItems d = case d of

ItemMaps l -> punctuate comma $ map pretty l

UniqueItem i -> [mapsto, structIRI i]

instance PrettyLG GENERICITY where

prettyLG lg (Genericity aa ab _) =

sep [printPARAMS lg aa, printIMPORTED lg ab]

printPARAMS :: LogicGraph -> PARAMS -> Doc

printPARAMS lg (Params aa) = cat $ map (brackets . rmTopKey . prettyLG lg ) aa

printIMPORTED :: LogicGraph -> IMPORTED -> Doc

printIMPORTED lg (Imported aa) = case aa of

[] -> empty

_ -> sep [keyword givenS, sepByCommas $ map (printGroupSpec lg) aa]

instance Pretty ALIGN_ARITIES where

pretty = printAlignArities

printAlignArities :: ALIGN_ARITIES -> Doc

printAlignArities (Align_arities f b) =

sep [text alignArityForwardS, printAlignArity f,

text alignArityBackwardS, printAlignArity b]

printAlignArity :: ALIGN_ARITY -> Doc

printAlignArity = text . showAlignArity

printCorrespondences :: [CORRESPONDENCE] -> Doc

printCorrespondences = vsep . punctuate comma . map printCorrespondence

printCorrespondence :: CORRESPONDENCE -> Doc

printCorrespondence Default_correspondence = text "*"

printCorrespondence (Correspondence_block mrref mconf cs) =

sep $ concat

[[text relationS],

map printRelationRef $ maybeToList mrref,

map printConfidence $ maybeToList mconf,

[text "{"],

[printCorrespondences cs],

[text "}"]]

printCorrespondence (Single_correspondence mcid eRef toer mrRef mconf) =

sep $ concat

[[indexed $ show eRef],

map printRelationRef $ maybeToList mrRef,

map printConfidence $ maybeToList mconf,

[pretty toer],

map pretty $ maybeToList mcid]

instance Pretty CORRESPONDENCE where

pretty = printCorrespondence

printConfidence :: CONFIDENCE -> Doc

-- "show" should work in [0,1]

printConfidence = text . ('(' :) . (++ ")") . show

printRelationRef :: RELATION_REF -> Doc

printRelationRef rref = case rref of

Subsumes -> text ">"

IsSubsumed -> text "<"

Equivalent -> text "="

Incompatible -> text "%"

HasInstance -> text "$\\ni$"

InstanceOf -> text "$\\in$"

DefaultRelation -> text "$\\mapsto$"

Iri i -> structIRI i

instance Pretty ItemNameMap where

pretty (ItemNameMap a m) = fsep

$ structIRI a : case m of

Nothing -> []

Just b -> [mapsto, structIRI b]