2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder{- |

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederModule : $Header$

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederDescription : pretty printing of CASL structured specifications

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

54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiMaintainer : Christian.Maeder@dfki.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability : non-portable(Grothendieck)

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederPretty printing of CASL structured specifications

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder-}

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedermodule Syntax.Print_AS_Structured

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder ( structIRI

da955132262baab309a50fdffe228c9efe68251dCui Jian , printGroupSpec

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder , skipVoidGroup

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder , printUnion

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder , printExtension

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder , moveAnnos

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder , PrettyLG (..)

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder ) where

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederimport Common.Id

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.IRI

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Keywords

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Doc

14c89b2d830777bf4db2850f038c9f60acaca486Christian Maederimport Common.DocUtils

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Common.AS_Annotation

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport Logic.Grothendieck

9175e29c044318498a40f323f189f9dfd50378efChristian Maederimport Logic.Logic

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyerimport Syntax.AS_Structured

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaedersublogicId :: SIMPLE_ID -> Doc

c0c2380bced8159ff0297ece14eba948bd236471Christian MaedersublogicId = structId . tokStr

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning

c0c2380bced8159ff0297ece14eba948bd236471Christian MaederstructIRI :: IRI -> Doc

6352f3c31da3043783a13be6594aacb2147378baRazvan PascanustructIRI = structId . iriToStringShortUnsecure -- also print user information

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maederclass PrettyLG a where

a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder prettyLG :: LogicGraph -> a -> Doc

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder

66a774f13272fde036481edd2298081ab3d04678Razvan Pascanuinstance PrettyLG a => PrettyLG (Annoted a) where

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross prettyLG lg = printAnnoted $ prettyLG lg

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederinstance PrettyLG SPEC where

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder prettyLG = printSPEC

6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian Maeder

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin KühlprintUnion :: LogicGraph -> [Annoted SPEC] -> [Doc]

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovaprintUnion lg = prepPunctuate (topKey andS <> space) . map (condBracesAnd lg)

63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian MaedermoveAnnos :: Annoted SPEC -> [Annoted SPEC] -> [Annoted SPEC]

14c89b2d830777bf4db2850f038c9f60acaca486Christian MaedermoveAnnos x l = appAnno $ case l of

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder [] -> error "moveAnnos"

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder h : r -> h { l_annos = l_annos x ++ l_annos h } : r

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder where appAnno a = case a of

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder [] -> []

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder [h] -> [appendAnno h (r_annos x)]

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl h : r -> h : appAnno r

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

2b873214c9ab511bbca437c036371ab664aedaceChristian MaederprintOptUnion :: LogicGraph -> Annoted SPEC -> [Doc]

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian MaederprintOptUnion lg x = case skipVoidGroup $ item x of

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Union e@(_ : _) _ -> printUnion lg $ moveAnnos x e

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Extension e@(_ : _) _ -> printExtension lg $ moveAnnos x e

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder _ -> [prettyLG lg x]

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossprintExtension :: LogicGraph -> [Annoted SPEC] -> [Doc]

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossprintExtension lg l = case l of

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder [] -> []

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder x : r -> printOptUnion lg x ++

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder concatMap ((\ u -> case u of

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder [] -> []

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder d : s -> (topKey thenS <+> d) : s) .

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder printOptUnion lg) r

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder

9175e29c044318498a40f323f189f9dfd50378efChristian MaederprintSPEC :: LogicGraph -> SPEC -> Doc

9175e29c044318498a40f323f189f9dfd50378efChristian MaederprintSPEC lg spec = case spec of

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder Basic_spec (G_basic_spec lid basic_spec) _ ->

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder case lookupCurrentSyntax "" lg of

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder Just (Logic lid2, sm) -> if language_name lid2 /= language_name lid

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder then error "printSPEC: logic mismatch"

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder else case basicSpecPrinter sm lid of

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder Just p -> p basic_spec

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder _ -> error $ "printSPEC: no basic spec printer for "

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder ++ showSyntax lid sm

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder _ -> error "printSPEC: incomplete logic graph"

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder EmptySpec _ -> specBraces empty

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl Translation aa ab -> sep [condBracesTransReduct lg aa, printRENAMING ab]

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl Reduction aa ab -> sep [condBracesTransReduct lg aa, printRESTRICTION ab]

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Union aa _ -> sep $ printUnion lg aa

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Extension aa _ -> sep $ printExtension lg aa

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Free_spec aa _ -> sep [keyword freeS, printGroupSpec lg aa]

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Cofree_spec aa _ -> sep [keyword cofreeS, printGroupSpec lg aa]

bdc103981a28a51938de98a956d8a3767f6cf43dAivaras Jakubauskas Local_spec aa ab _ -> fsep

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder [keyword localS, prettyLG lg aa, keyword withinS, condBracesWithin lg ab]

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder Closed_spec aa _ -> sep [keyword closedS, printGroupSpec lg aa]

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder Group aa _ -> prettyLG lg aa

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder Spec_inst aa ab _ -> cat [structIRI aa, print_fit_arg_list lg ab]

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder Qualified_spec ln asp _ -> printLogicEncoding ln <> colon

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder $+$ prettyLG (setLogicName ln lg) asp

7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder Data ld _ s1 s2 _ -> keyword dataS

fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder <+> printGroupSpec (setCurLogic (show ld) lg) s1

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $+$ prettyLG lg s2

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Combination cs es _ -> fsep $ keyword combineS : ppWithCommas cs

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder : if null es then [] else [keyword excludingS, ppWithCommas es]

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühlinstance Pretty RENAMING where

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova pretty = printRENAMING

72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz

a461314c811f4187dff85c8be079a41b2f13f176Christian MaederprintRENAMING :: RENAMING -> Doc

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederprintRENAMING (Renaming aa _) =

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder keyword withS <+> ppWithCommas aa

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maederinstance Pretty RESTRICTION where

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder pretty = printRESTRICTION

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossprintRESTRICTION :: RESTRICTION -> Doc

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossprintRESTRICTION rest = case rest of

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer Hidden aa _ -> keyword hideS <+> ppWithCommas aa

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer Revealed aa _ -> keyword revealS <+> pretty aa

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder

9175e29c044318498a40f323f189f9dfd50378efChristian MaederprintLogicEncoding :: (Pretty a) => a -> Doc

9175e29c044318498a40f323f189f9dfd50378efChristian MaederprintLogicEncoding enc = keyword logicS <+> pretty enc

f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich

9175e29c044318498a40f323f189f9dfd50378efChristian Maederinstance Pretty G_mapping where

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder pretty = printG_mapping

printG_mapping :: G_mapping -> Doc

printG_mapping gma = case gma of

G_symb_map gsmil -> pretty gsmil

G_logic_translation enc -> printLogicEncoding enc

instance Pretty G_hiding where

pretty = printG_hiding

printG_hiding :: G_hiding -> Doc

printG_hiding ghid = case ghid of

G_symb_list gsil -> pretty gsil

G_logic_projection enc -> printLogicEncoding enc

instance PrettyLG FIT_ARG where

prettyLG = printFIT_ARG

printFIT_ARG :: LogicGraph -> FIT_ARG -> Doc

printFIT_ARG lg fit = case fit of

Fit_spec aa ab _ ->

let aa' = rmTopKey $ prettyLG lg aa

in if null ab then aa' else

fsep $ aa' : keyword fitS

: punctuate comma (map printG_mapping ab)

Fit_view si ab _ ->

sep [keyword viewS, cat [structIRI si, print_fit_arg_list lg ab]]

instance Pretty Logic_code where

pretty = printLogic_code

printLogic_code :: Logic_code -> Doc

printLogic_code (Logic_code menc msrc mtar _) =

let pm = maybe [] ((: []) . printLogic_name) in

fsep $ maybe [] ((: [colon]) . pretty) menc

++ pm msrc ++ funArrow : pm mtar

instance Pretty LogicDescr where

pretty (LogicDescr n s _) = sep [pretty n,

maybe empty (\ r -> sep [keyword serializationS, pretty r]) s]

instance Pretty Logic_name where

pretty = printLogic_name

printLogic_name :: Logic_name -> Doc

printLogic_name (Logic_name mlog slog ms) = let d = structId mlog in

case slog of

Nothing -> d

Just sub -> d <> dot <> sublogicId sub

<> maybe empty (parens . pretty) ms

{- |

specialized printing of 'FIT_ARG's

-}

print_fit_arg_list :: LogicGraph -> [Annoted FIT_ARG] -> Doc

print_fit_arg_list lg = cat . map (brackets . prettyLG lg)

{- |

conditional generation of grouping braces for Union and Extension

-}

printGroupSpec :: LogicGraph -> Annoted SPEC -> Doc

printGroupSpec lg s = let d = prettyLG lg s in

case skip_Group $ item s of

Spec_inst {} -> d

_ -> specBraces d

{- |

generate grouping braces for Tanslations and Reductions

-}

condBracesTransReduct :: LogicGraph -> Annoted SPEC -> Doc

condBracesTransReduct lg s = let d = prettyLG lg s in

case skip_Group $ item s of

Extension {} -> specBraces d

Union {} -> specBraces d

Local_spec {} -> specBraces d

_ -> d

{- |

generate grouping braces for Within

-}

condBracesWithin :: LogicGraph -> Annoted SPEC -> Doc

condBracesWithin lg s = let d = prettyLG lg s in

case skip_Group $ item s of

Extension _ _ -> specBraces d

Union _ _ -> specBraces d

_ -> d

{- |

only Extensions inside of Unions (and) need grouping braces

-}

condBracesAnd :: LogicGraph -> Annoted SPEC -> Doc

condBracesAnd lg s = let d = prettyLG lg s in

case skip_Group $ item s of

Extension _ _ -> specBraces d

_ -> d

-- | only skip groups without annotations

skipVoidGroup :: SPEC -> SPEC

skipVoidGroup sp =

case sp of

Group g _ | null (l_annos g) && null (r_annos g)

-> skipVoidGroup $ item g

_ -> sp

-- | skip nested groups

skip_Group :: SPEC -> SPEC

skip_Group sp =

case sp of

Group g _ -> skip_Group $ item g

_ -> sp