01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- |

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Klaus L�ttich, Christian Maeder and Uni Bremen 2002-2003

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicence : All rights reserved.

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : hets@tzi.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable (rank-2-polymorphism)

351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder pretty printing data types of 'BASIC_SPEC'

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski-}

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedermodule CASL.Print_AS_Basic where

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder-- debugging

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Data.List (mapAccumL)

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport Data.Char (isDigit)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Id

5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport CASL.AS_Basic_CASL

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Common.AS_Annotation

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.GlobalAnnotations

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport CASL.LiteralFuns

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Common.Print_AS_Annotation

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederimport Common.Keywords

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport Common.Lib.Pretty

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Common.PrettyPrint

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Common.PPUtils

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederinstance PrettyPrint BASIC_SPEC where

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder printText0 ga (Basic_spec l) =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if null l then braces empty else vcat (map (printText0 ga) l)

90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder where _just_avoid_unused_import_warning = smallSpace_latex

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich printLatex0 ga (Basic_spec l) =

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder if null l then braces_latex empty else vcat (map (printLatex0 ga) l)

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance PrettyPrint BASIC_ITEMS where

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printText0 ga (Sig_items s) = printText0 ga s

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga (Free_datatype l _) =

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder hang (ptext freeS <+> ptext typeS<>pluralS_doc l) 4 $

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu semiAnno_text ga l

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder printText0 ga (Sort_gen l _) =

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder hang (ptext generatedS <+> condTypeS) 4 $

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder condBraces (vcat (map (printText0 ga) l))

8e80792f474d154ff11762fac081a422e34f1accChristian Maeder where condTypeS =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if isOnlyDatatype then ptext typeS<>pluralS_doc l

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else empty

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder condBraces d =

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder if isOnlyDatatype then

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case l of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [x] -> case x of

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder Annoted (Datatype_items l' _) _ lans _ ->

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder vcat (map (printText0 ga) lans)

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder $$ semiAnno_text ga l'

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder _ -> error "wrong implementation of isOnlyDatatype"

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder _ -> error "wrong implementation of isOnlyDatatype"

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder else braces d

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder isOnlyDatatype =

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder case l of

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder [x] -> case x of

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Annoted (Datatype_items _ _) _ _ _ -> True

351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder _ -> False

351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder _ -> False

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder printText0 ga (Var_items l _) =

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder text varS<>pluralS_doc l <+> semiT_text ga l

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder printText0 ga (Local_var_axioms l f p) =

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder text forallS <+> semiT_text ga l

351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder $$ printText0 ga (Axiom_items f p)

351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder printText0 ga (Axiom_items f _) =

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder vcat $ map (printAnnotedFormula_Text0 ga) f

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder printLatex0 ga (Sig_items s) = printLatex0 ga s

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder printLatex0 ga (Free_datatype l _) =

351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder hang_latex (hc_sty_plain_keyword "free"

351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder <~> setTab_latex

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder <> hc_sty_plain_keyword ("type"++ pluralS l)) 9 $

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder tabbed_nest_latex $ semiAnno_latex ga l

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder printLatex0 ga (Sort_gen l _) =

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder hang_latex (hc_sty_plain_keyword generatedS

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder <~> setTab_latex<> condTypeS) 9 $

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder tabbed_nest_latex $ condBraces

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder (vcat (map (printLatex0 ga) l))

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder where condTypeS =

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder if isOnlyDatatype then

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder hc_sty_plain_keyword (typeS++pluralS l)

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder else empty

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder condBraces d =

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder if isOnlyDatatype then

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder case l of

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder [x] -> case x of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Annoted (Datatype_items l' _) _ lans _ ->

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder vcat (map (printLatex0 ga) lans)

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder $$ semiAnno_latex ga l'

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder _ -> error "wrong implementation of isOnlyDatatype"

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> error "wrong implementation of isOnlyDatatype"

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski else braces_latex d

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder isOnlyDatatype =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case l of

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder [x] -> case x of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Annoted (Datatype_items _ _) _ _ _ -> True

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> False

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder _ -> False

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder printLatex0 ga (Var_items l _) =

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder hc_sty_plain_keyword (varS++pluralS l) <\+>

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder semiT_latex ga l

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printLatex0 ga (Local_var_axioms l f p) =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski hc_sty_axiom "\\forall" <\+> semiT_latex ga l

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder $$ printLatex0 ga (Axiom_items f p)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printLatex0 ga (Axiom_items f _) =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski vcat $ map (printAnnotedFormula_Latex0 ga) f

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederprintAnnotedFormula_Text0 :: GlobalAnnos -> Annoted FORMULA -> Doc

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederprintAnnotedFormula_Text0 ga (Annoted i _ las ras) =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let i' = char '.' <+> printText0 ga i

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder las' = if not $ null las then

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ptext "\n" <> printAnnotationList_Text0 ga las

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder else

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder empty

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder (la,rras) = case ras of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [] -> (empty,[])

26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder r@(l:xs)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | isLabel l -> (printText0 ga l,xs)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | otherwise -> (empty,r)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ras' = printAnnotationList_Text0 ga rras

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder in las' $+$ (hang i' 0 la) $$ ras'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederprintAnnotedFormula_Latex0 :: GlobalAnnos -> Annoted FORMULA -> Doc

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprintAnnotedFormula_Latex0 ga (Annoted i _ las ras) =

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder let i' = hc_sty_axiom "\\bullet" <\+> printLatex0 ga i

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder las' = if not $ null las then

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder sp_text 0 "\n" <> printAnnotationList_Latex0 ga las

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder else

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder empty

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder (la,rras) = case ras of

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder [] -> (empty,[])

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder r@(l:xs)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder | isLabel l -> (printLatex0 ga l,xs)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | otherwise -> (empty,r)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ras' = printAnnotationList_Latex0 ga rras

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in las' $+$ (hang_latex i' 0 la) $$ ras'

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance PrettyPrint SIG_ITEMS where

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printText0 ga (Sort_items l _) =

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder text sortS<>pluralS_doc l <+> semiAnno_text ga l

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski printText0 ga (Op_items l _) =

74d9a385499bf903b24848dff450a153f525bda7Christian Maeder text opS<>pluralS_doc l <+> semiAnno_text ga l

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printText0 ga (Pred_items l _) =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder text predS<>pluralS_doc l <+> semiAnno_text ga l

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printText0 ga (Datatype_items l _) =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder text typeS<>pluralS_doc l <+> semiAnno_text ga l

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printLatex0 ga (Sort_items l _) =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder hc_sty_casl_keyword (sortS++pluralS l) <\+>

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder set_tabbed_nest_latex (semiAnno_latex ga l)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printLatex0 ga (Op_items l _) =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder hc_sty_casl_keyword (opS++pluralS l) <\+>

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder set_tabbed_nest_latex (semiAnno_latex ga l)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printLatex0 ga (Pred_items l _) =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder hc_sty_casl_keyword (predS++pluralS l) <\+>

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder set_tabbed_nest_latex (semiAnno_latex ga l)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printLatex0 ga (Datatype_items l _) =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder hc_sty_casl_keyword (typeS++pluralS l) <\+>

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder set_tabbed_nest_latex (semiAnno_latex ga l)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint SORT_ITEM where

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga (Sort_decl l _) = commaT_text ga l

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printText0 ga (Subsort_decl l t _) =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder hang (commaT_text ga l) 4 $ text lessS <+> printText0 ga t

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printText0 ga (Subsort_defn s v t f _) =

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder -- TODO: lannos of f should printed after the equal sign

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printText0 ga s <+> ptext equalS <+>

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder braces (hang (printText0 ga v <+> colon <+> printText0 ga t)

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder 4 (ptext "." <+> printText0 ga f))

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printText0 ga (Iso_decl l _) =

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder fsep $ punctuate (space <>text equalS) $ map (printText0 ga) l

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printLatex0 ga (Sort_decl l _) = commaT_latex ga l

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printLatex0 ga (Subsort_decl l t _) =

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder hang_latex (commaT_latex ga l) 8 $

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder hc_sty_axiom lessS <\+> printLatex0 ga t

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printLatex0 ga (Subsort_defn s v t f _) =

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printLatex0 ga s <\+> equals_latex <\+>

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder braces_latex (hang_latex ( printLatex0 ga v

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <\+> colon_latex

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder <\+> printLatex0 ga t)

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder 8 (hc_sty_axiom "\\bullet" <\+> printLatex0 ga f))

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder printLatex0 ga (Iso_decl l _) =

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder fsep_latex $ punctuate (space_latex<>equals_latex) $

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski map (printLatex0 ga) l

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder

ab642ff136ce716af9e609b667e3f06d766c4ad7Christian Maederinstance PrettyPrint OP_ITEM where

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder printText0 ga (Op_decl l t a _) =

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder hang (hang (commaT_text ga l)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder 4

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (colon <> printText0 ga t <> condComma))

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder 4 $

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder if na then empty

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder else commaT_text ga a

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder where na = null a

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder condComma = if na then empty

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder else comma

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printText0 ga (Op_defn n h t _) = printText0 ga n

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <> printText0 ga h

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <+> text equalS

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder <+> printText0 ga t

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printLatex0 ga (Op_decl l t a _) =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder {-cat [ cat [commaT_latex ga l

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ,colon_latex <> printLatex0 ga t <> condComma]

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder , if na then empty

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder else commaT_latex ga a

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ]-}

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder if na then ids_sig

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder else setTabWithSpaces_latex 4

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder <>

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder (tab_hang_latex ids_sig

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder 4 $ commaT_latex ga a)

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder where ids_sig = setTabWithSpaces_latex 6

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <> tab_hang_latex (commaT_latex ga l)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder 6

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (if na then sig

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else sig <> comma_latex)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sig = colon_latex <> printLatex0 ga t

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder na = null a

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printLatex0 ga (Op_defn n h t _) = printLatex0 ga n

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder <> printLatex0 ga h

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder <\+> equals_latex

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder <\+> printLatex0 ga t

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance PrettyPrint OP_TYPE where

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder printText0 ga (Total_op_type l s _) = (if null l then empty

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder else space

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder <> crossT_text ga l

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <+> text funS)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <> space <> printText0 ga s

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga (Partial_op_type l s _) = (if null l then text quMark

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else space

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder <> crossT_text ga l

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder <+> text (funS ++ quMark))

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder <+> printText0 ga s

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printLatex0 ga (Total_op_type l s _) =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (if null l then empty

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else space_latex <>

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder set_tabbed_nest_latex (crossT_latex ga l

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <\+> hc_sty_axiom "\\rightarrow"))

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <~> printLatex0 ga s

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printLatex0 ga (Partial_op_type l s _) =

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (if null l then hc_sty_axiom quMark

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder else space_latex

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder <> crossT_latex ga l

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder <\+> hc_sty_axiom ("\\rightarrow" ++ quMark))

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder <~> printLatex0 ga s

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance PrettyPrint OP_HEAD where

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder printText0 ga (Total_op_head l s _) =

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (if null l then empty

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else parens(semiT_text ga l))

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder <> colon

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <+> printText0 ga s

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printText0 ga (Partial_op_head l s _) =

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (if null l then empty

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else parens(semiT_text ga l))

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder <> text (colonS ++ quMark)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <+> printText0 ga s

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder printLatex0 ga (Total_op_head l s _) =

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (if null l then empty

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else parens_latex (semiT_latex ga l))

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <> colon_latex

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <\+> printLatex0 ga s

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder printLatex0 ga (Partial_op_head l s _) =

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (if null l then empty

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else parens_latex(semiT_latex ga l))

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <> colon_latex <> hc_sty_axiom quMark

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder <\+> printLatex0 ga s

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederinstance PrettyPrint ARG_DECL where

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printText0 ga (Arg_decl l s _) = commaT_text ga l

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder <+> colon

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <> printText0 ga s

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder printLatex0 ga (Arg_decl l s _) = commaT_latex ga l

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder <\+> colon_latex

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder <> printLatex0 ga s

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederinstance PrettyPrint OP_ATTR where

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printText0 _ (Assoc_op_attr) = text assocS

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder printText0 _ (Comm_op_attr) = text commS

0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder printText0 _ (Idem_op_attr) = text idemS

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder printText0 ga (Unit_op_attr t) = text unitS <+> printText0 ga t

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printLatex0 _ (Assoc_op_attr) = hc_sty_id assocS

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printLatex0 _ (Comm_op_attr) = hc_sty_id commS

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder printLatex0 _ (Idem_op_attr) = hc_sty_id idemS

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printLatex0 ga (Unit_op_attr t) = hc_sty_id unitS <\+> printLatex0 ga t

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederinstance PrettyPrint PRED_ITEM where

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printText0 ga (Pred_decl l t _) = commaT_text ga l

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder <+> colon <+> printText0 ga t

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printText0 ga (Pred_defn n h f _) = printText0 ga n

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder <> printText0 ga h

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <+> text equivS

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder <+> printText0 ga f

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printLatex0 ga (Pred_decl l t _) = commaT_latex ga l

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder <\+> colon_latex <\+> printLatex0 ga t

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printLatex0 ga (Pred_defn n h f _) = printLatex0 ga n

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder <> printLatex0 ga h

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder <\+> hc_sty_axiom "\\Leftrightarrow"

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder <\+> printLatex0 ga f

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederinstance PrettyPrint PRED_TYPE where

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printText0 _ (Pred_type [] _) = parens empty

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printText0 ga (Pred_type l _) = crossT_text ga l

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printLatex0 _ (Pred_type [] _) = parens_latex empty

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printLatex0 ga (Pred_type l _) = crossT_latex ga l

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederinstance PrettyPrint PRED_HEAD where

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printText0 ga (Pred_head l _) = parens (semiT_text ga l)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printLatex0 ga (Pred_head l _) =

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder parens_latex (semiT_latex ga l)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance PrettyPrint DATATYPE_DECL where

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder printText0 ga (Datatype_decl s a _) =

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder printText0 ga s <+>

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder sep ((hang (text defnS) 4 (printText0 ga $ head a)):

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder (map (\x -> nest 2 $ ptext barS <+> nest 2 (printText0 ga x)) $

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder tail a))

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder printLatex0 ga (Datatype_decl s a _) =

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder printLatex0 ga s <\+>

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder sep_latex

caf021dd48c90ff6b26117f13e1d8c0ef1ca618aChristian Maeder ((hang_latex (hc_sty_axiom defnS) 8 (printLatex0 ga $ head a)):

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (map (\x -> nest_latex 4 $ casl_normal_latex "\\textbar"

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski <\+> nest_latex 4 (printLatex0 ga x)) $

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder tail a))

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maederinstance PrettyPrint ALTERNATIVE where

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder printText0 ga (Total_construct n l _) = printText0 ga n

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder <> if null l then empty

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder else parens(semiT_text ga l)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printText0 ga (Partial_construct n l _) = printText0 ga n

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder <> parens(semiT_text ga l)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder <> text quMark

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder printText0 ga (Subsorts l _) = text sortS <+> commaT_text ga l

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printLatex0 ga (Total_construct n l _) =

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder printLatex0 ga n <> if null l then empty

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else parens_latex (semiT_latex ga l)

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder printLatex0 ga (Partial_construct n l _) = printLatex0 ga n

44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder <> parens_latex (semiT_latex ga l)

44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder <> hc_sty_axiom quMark

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder printLatex0 ga (Subsorts l _) =

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder hc_sty_plain_keyword sortS <\+> commaT_latex ga l

4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance PrettyPrint COMPONENTS where

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder printText0 ga (Total_select l s _) = commaT_text ga l

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <> colon

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder <> printText0 ga s

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printText0 ga (Partial_select l s _) = commaT_text ga l

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <> text (colonS ++ quMark)

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder <> printText0 ga s

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printText0 ga (Sort s) = printText0 ga s

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder

4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder printLatex0 ga (Total_select l s _) =

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder commaT_latex ga l <> colon_latex <> printLatex0 ga s

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printLatex0 ga (Partial_select l s _) =

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder commaT_latex ga l

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder <> colon_latex <> hc_sty_axiom quMark

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder <> printLatex0 ga s

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder printLatex0 ga (Sort s) = printLatex0 ga s

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederinstance PrettyPrint VAR_DECL where

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder printText0 ga (Var_decl l s _) = commaT_text ga l

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder <> colon

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder <> printText0 ga s

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder printLatex0 ga (Var_decl l s _) = commaT_latex ga l

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski <> colon_latex

74d9a385499bf903b24848dff450a153f525bda7Christian Maeder <> printLatex0 ga s

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance PrettyPrint FORMULA where

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder printText0 ga (Quantification q l f _) =

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski hang (printText0 ga q <+> semiT_text ga l) 4 $

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder char '.' <+> printText0 ga f

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski printText0 ga (Conjunction l _) =

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sep $ prepPunctuate (ptext lAnd <> space) $

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski map (condParensXjunction printText0 parens ga) l

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski printText0 ga (Disjunction l _) =

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sep $ prepPunctuate (ptext lOr <> space) $

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder map (condParensXjunction printText0 parens ga) l

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printText0 ga i@(Implication f g _) =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder hang (condParensImplEquiv printText0 parens ga i f

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski <+> ptext implS) 4 $

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder condParensImplEquiv printText0 parens ga i g

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder printText0 ga e@(Equivalence f g _) =

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder hang (condParensImplEquiv printText0 parens ga e f

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder <+> ptext equivS) 4 $

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder condParensImplEquiv printText0 parens ga e g

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder printText0 ga (Negation f _) = ptext "not" <+> printText0 ga f

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder printText0 _ (True_atom _) = ptext trueS

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder printText0 _ (False_atom _) = ptext falseS

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder printText0 ga (Predication p l _) =

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder let (p_id,isQual) =

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder case p of

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Pred_name i -> (i,False)

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Qual_pred_name i _ _ -> (i,True)

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder p' = printText0 ga p

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder in if isQual then

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder print_prefix_appl_text ga p' l

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder else condPrint_Mixfix_text ga p_id l

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printText0 ga (Definedness f _) = text defS <+> printText0 ga f

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder printText0 ga (Existl_equation f g _) =

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder hang (printText0 ga f <+> ptext exEqual) 4 $ printText0 ga g

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printText0 ga (Strong_equation f g _) =

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder hang (printText0 ga f <+> ptext equalS) 4 $ printText0 ga g

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder printText0 ga (Membership f g _) =

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder printText0 ga f <+> ptext inS <+> printText0 ga g

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printText0 ga (Mixfix_formula t) = printText0 ga t

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder printText0 _ (Unparsed_formula s _) = text s

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder printLatex0 ga (Quantification q l f _) =

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder hang_latex (printLatex0 ga q <\+> semiT_latex ga l) 8 $

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder hc_sty_axiom "\\bullet" <\+> printLatex0 ga f

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski printLatex0 ga (Conjunction l _) =

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder sep_latex $ prepPunctuate (hc_sty_axiom "\\wedge" <> space_latex) $

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder map (condParensXjunction printLatex0 parens_latex ga) l

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder printLatex0 ga (Disjunction l _) =

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder sep_latex $ prepPunctuate (hc_sty_axiom "\\vee" <> space_latex) $

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder map (condParensXjunction printLatex0 parens_latex ga) l

5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder printLatex0 ga i@(Implication f g _) =

5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder hang_latex (condParensImplEquiv printLatex0 parens_latex ga i f

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <\+> hc_sty_axiom "\\Rightarrow") 8 $

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder condParensImplEquiv printLatex0 parens_latex ga i g

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder printLatex0 ga e@(Equivalence f g _) =

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski hang_latex (condParensImplEquiv printLatex0 parens_latex ga e f

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <\+> hc_sty_axiom "\\Leftrightarrow") 8 $

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder condParensImplEquiv printLatex0 parens_latex ga e g

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder printLatex0 ga (Negation f _) = hc_sty_axiom "\\neg" <\+> printLatex0 ga f

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder printLatex0 _ (True_atom _) = hc_sty_id trueS

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder printLatex0 _ (False_atom _) = hc_sty_id falseS

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder printLatex0 ga (Predication p l _) =

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder let (p_id,isQual) =

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder case p of

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder Pred_name i -> (i,False)

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Qual_pred_name i _ _ -> (i,True)

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder p' = printLatex0 ga p

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder in if isQual then

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder print_prefix_appl_latex ga p' l

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder else condPrint_Mixfix_latex ga p_id l

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder printLatex0 ga (Definedness f _) = hc_sty_id defS <\+> printLatex0 ga f

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder printLatex0 ga (Existl_equation f g _) =

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder hang_latex (printLatex0 ga f

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder <\+> sp_text (axiom_width "=")

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder "\\Ax{\\stackrel{e}{=}}") 8

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder $ printLatex0 ga g

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder printLatex0 ga (Strong_equation f g _) =

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder hang_latex (printLatex0 ga f <\+> hc_sty_axiom "=") 8

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder $ printLatex0 ga g

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder printLatex0 ga (Membership f g _) =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printLatex0 ga f <\+> hc_sty_axiom "\\in" <\+> printLatex0 ga g

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printLatex0 ga (Mixfix_formula t) = printLatex0 ga t

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printLatex0 _ (Unparsed_formula s _) = text s

32562a567baac248a00782d2727716c13117dc4aChristian Maeder

32562a567baac248a00782d2727716c13117dc4aChristian Maederinstance PrettyPrint QUANTIFIER where

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printText0 _ (Universal) = ptext forallS

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printText0 _ (Existential) = ptext existsS

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder printText0 _ (Unique_existential) = ptext (existsS ++ exMark)

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printLatex0 _ (Universal) = hc_sty_axiom "\\forall"

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printLatex0 _ (Existential) = hc_sty_axiom "\\exists"

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printLatex0 _ (Unique_existential) = hc_sty_axiom "\\exists!"

32562a567baac248a00782d2727716c13117dc4aChristian Maeder

32562a567baac248a00782d2727716c13117dc4aChristian Maederinstance PrettyPrint PRED_SYMB where

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printText0 ga (Pred_name n) = printText0 ga n

746440cc1b984a852f5864235b8fa3930963a081Christian Maeder printText0 ga (Qual_pred_name n t _) =

32562a567baac248a00782d2727716c13117dc4aChristian Maeder parens $ ptext predS <+> printText0 ga n <+> colon <+> printText0 ga t

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printLatex0 ga (Pred_name n) = printLatex0 ga n

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printLatex0 ga (Qual_pred_name n t _) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder parens_latex $ hc_sty_id predS

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder <\+> printLatex0 ga n

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder <\+> colon_latex <\+> printLatex0 ga t

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederinstance PrettyPrint TERM where

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Simple_id i) = printText0 ga i

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Qual_var n t _) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder parens $ text varS <+> printText0 ga n <+> colon <+> printText0 ga t

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder printText0 ga (Application o l _) =

4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder let (o_id,isQual) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder case o of

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Op_name i -> (i,False)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Qual_op_name i _ _ -> (i,True)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder o' = printText0 ga o

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder in if isQual then

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder print_prefix_appl_text ga o' l

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder else

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder if isLiteral ga o_id l then

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder {-trace ("a literal application: "

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ++ show (Application o l [])) $ -}

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder print_Literal_text ga o_id l

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder else

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder condPrint_Mixfix_text ga o_id l

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Sorted_term t s _) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga t <+> colon <+> printText0 ga s

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Cast t s _) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga t <+> text asS <+> printText0 ga s

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga(Conditional u f v _) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder hang (printText0 ga u) 4 $

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder sep ((text whenS <+> printText0 ga f):

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder [text elseS <+> printText0 ga v])

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 _ (Unparsed_term s _) = text s

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder printText0 ga (Mixfix_qual_pred p) = printText0 ga p

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Mixfix_term l) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder cat(punctuate space (map (printText0 ga) l))

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder printText0 ga (Mixfix_token t) = printText0 ga t

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Mixfix_sorted_term s _) = colon

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder <> printText0 ga s

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Mixfix_cast s _) = text asS

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder <+> printText0 ga s

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Mixfix_parenthesized l _) = parens (commaT_text ga l)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Mixfix_bracketed l _) = brackets (commaT_text ga l)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printText0 ga (Mixfix_braced l _) = braces (commaT_text ga l)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder printLatex0 ga (Simple_id i) = printLatex0 ga i

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder printLatex0 ga (Qual_var n t _) = -- HERE

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder parens_latex $ hc_sty_id varS

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder <\+> printLatex0 ga n

32562a567baac248a00782d2727716c13117dc4aChristian Maeder <\+> colon_latex <\+> printLatex0 ga t

32562a567baac248a00782d2727716c13117dc4aChristian Maeder printLatex0 ga (Application o l _) =

32562a567baac248a00782d2727716c13117dc4aChristian Maeder let (o_id,isQual) =

32562a567baac248a00782d2727716c13117dc4aChristian Maeder case o of

32562a567baac248a00782d2727716c13117dc4aChristian Maeder Op_name i -> (i,False)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder Qual_op_name i _ _ -> (i,True)

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder o' = printLatex0 ga o

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder in if isQual then

32562a567baac248a00782d2727716c13117dc4aChristian Maeder print_prefix_appl_latex ga o' l

32562a567baac248a00782d2727716c13117dc4aChristian Maeder else

32562a567baac248a00782d2727716c13117dc4aChristian Maeder if isLiteral ga o_id l then

32562a567baac248a00782d2727716c13117dc4aChristian Maeder print_Literal_latex ga o_id l

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else

3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski condPrint_Mixfix_latex ga o_id l

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printLatex0 ga (Sorted_term t s _) =

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga t <\+> colon_latex <\+> printLatex0 ga s

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga (Cast t s _) =

3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski printLatex0 ga t <\+> hc_sty_id asS <\+> printLatex0 ga s

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga(Conditional u f v _) =

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder hang_latex (printLatex0 ga u) 8 $

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder sep_latex ((hc_sty_id whenS <\+> printLatex0 ga f):

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder [hc_sty_id elseS <\+> printLatex0 ga v])

ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski printLatex0 _ (Unparsed_term s _) = text s

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga (Mixfix_qual_pred p) = printLatex0 ga p

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga (Mixfix_term l) =

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder cat(punctuate space (map (printLatex0 ga) l))

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga (Mixfix_token t) = printLatex0 ga t

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga (Mixfix_sorted_term s _) = colon

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <> printLatex0 ga s

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder printLatex0 ga (Mixfix_cast s _) = text asS

ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski <\+> printLatex0 ga s

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang printLatex0 ga (Mixfix_parenthesized l _) =

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang parens_latex (commaT_latex ga l)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang printLatex0 ga (Mixfix_bracketed l _) =

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder brackets_latex (commaT_latex ga l)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printLatex0 ga (Mixfix_braced l _) =

5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder braces_latex (commaT_latex ga l)

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder

5824312cc0cfccce61f195fbe92307a21a467049Christian Maederinstance PrettyPrint OP_SYMB where

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder printText0 ga (Op_name o) = printText0 ga o

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder printText0 ga (Qual_op_name o t _) = parens(text opS

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <+> printText0 ga o

5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder <+> (colon

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder <> printText0 ga t))

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder printLatex0 ga (Op_name o) = printLatex0 ga o

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder printLatex0 ga (Qual_op_name o t _) =

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder parens_latex

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder (hc_sty_id opS

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder <\+> printLatex0 ga o <\+> colon_latex <> printLatex0 ga t)

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maederinstance PrettyPrint SYMB_ITEMS where

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder printText0 ga (Symb_items k l _) =

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder printText0 ga k <> ptext (pluralS_symb_list k l)

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder <+> commaT_text ga l

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder printLatex0 ga (Symb_items k l _) =

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder print_kind_latex ga k l <\+> commaT_latex ga l

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

5824312cc0cfccce61f195fbe92307a21a467049Christian Maederinstance PrettyPrint SYMB_ITEMS_LIST where

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang printText0 ga (Symb_items_list l _) = commaT_text ga l

5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder

printLatex0 ga (Symb_items_list l _) = commaT_latex ga l

instance PrettyPrint SYMB_MAP_ITEMS where

printText0 ga (Symb_map_items k l _) =

printText0 ga k <> ptext (pluralS_symb_list k l)

<+> commaT_text ga l

printLatex0 ga (Symb_map_items k l _) =

print_kind_latex ga k l <\+> commaT_latex ga l

instance PrettyPrint SYMB_MAP_ITEMS_LIST where

printText0 ga (Symb_map_items_list l _) = commaT_text ga l

printLatex0 ga (Symb_map_items_list l _) = commaT_latex ga l

instance PrettyPrint SYMB_KIND where

printText0 _ Implicit = empty

printText0 _ Sorts_kind = ptext sortS

printText0 _ Ops_kind = ptext opS

printText0 _ Preds_kind = ptext predS

printLatex0 _ Implicit = empty

printLatex0 _ Sorts_kind = casl_keyword_latex sortS

printLatex0 _ Ops_kind = casl_keyword_latex opS

printLatex0 _ Preds_kind = casl_keyword_latex predS

instance PrettyPrint SYMB where

printText0 ga (Symb_id i) = printText0 ga i

printText0 ga (Qual_id i t _) =

printText0 ga i <+> colon <+> printText0 ga t

printLatex0 ga (Symb_id i) = printLatex0 ga i

printLatex0 ga (Qual_id i t _) =

printLatex0 ga i <\+> colon_latex <\+> printLatex0 ga t

instance PrettyPrint TYPE where

printText0 ga (O_type t) = printText0 ga t

printText0 ga (P_type t) = printText0 ga t

printText0 ga (A_type t) = printText0 ga t

printLatex0 ga (O_type t) = printLatex0 ga t

printLatex0 ga (P_type t) = printLatex0 ga t

printLatex0 ga (A_type t) = printLatex0 ga t

instance PrettyPrint SYMB_OR_MAP where

printText0 ga (Symb s) = printText0 ga s

printText0 ga (Symb_map s t _) =

printText0 ga s <+> text mapsTo <+> printText0 ga t

printLatex0 ga (Symb s) = printLatex0 ga s

printLatex0 ga (Symb_map s t _) =

printLatex0 ga s <\+> hc_sty_axiom "\\mapsto" <\+> printLatex0 ga t

---- helpers ----------------------------------------------------------------

pluralS_symb_list :: SYMB_KIND -> [a] -> String

pluralS_symb_list k l = case k of

Implicit -> ""

_ -> if length l > 1

then "s"

else ""

print_kind_latex :: GlobalAnnos -> SYMB_KIND -> [a] -> Doc

print_kind_latex ga k l = latex_macro "\\KW{"<>kw<>s<>latex_macro "}"

where kw = printLatex0 ga k

s = case pluralS_symb_list k l of

"" -> empty

s' -> casl_keyword_latex s'

condPrint_Mixfix :: (forall a .PrettyPrint a => GlobalAnnos -> a -> Doc)

-> (Doc -> Doc) -- ^ a function that surrounds

-- the given Doc with appropiate

-- parens

-> (Doc -> Doc -> Doc) -- ^ a beside with space

-- like <+> or <\+>

-> ([Doc] -> Doc) -- ^ a list concat with space and

-- fill the line policy like

-- fsep or fsep_latex

-> (forall b . PrettyPrint b =>

GlobalAnnos -> [b] -> Doc)

-- ^ a function that prints a nice

-- comma seperated list like commaT

-- or commaT_latex

-> GlobalAnnos -> Id -> [TERM] -> Doc

condPrint_Mixfix pf parens_fun

beside_fun fsep_fun commaT_fun

ga i l =

if isMixfix i then

if length (filter isPlace tops) == length l then

print_mixfix_appl pf parens_fun

beside_fun fsep_fun ga i l

else

print_prefix_appl parens_fun commaT_fun ga o' l

else print_prefix_appl parens_fun commaT_fun ga o' l

where tops = case i of Id tp _ _ -> tp

o' = pf ga i

{- TODO: consider string-, number-, list- and floating-annotations -}

condPrint_Mixfix_text :: GlobalAnnos -> Id -> [TERM] -> Doc

condPrint_Mixfix_text =

condPrint_Mixfix printText0 parens

(<+>) fsep (commaT_text)

condPrint_Mixfix_latex :: GlobalAnnos -> Id -> [TERM] -> Doc

condPrint_Mixfix_latex =

condPrint_Mixfix printLatex0 parens_latex

(<\+>) fsep_latex (commaT_latex)

-- printing consistent prefix application and predication

print_prefix_appl :: (Doc -> Doc) -- ^ a function that surrounds

-- the given Doc with appropiate

-- parens

-> (forall b . PrettyPrint b =>

GlobalAnnos -> [b] -> Doc)

-- ^ a function that prints a nice

-- comma seperated list like commaT

-- or commaT_latex

-> GlobalAnnos -> Doc -> [TERM] -> Doc

print_prefix_appl parens_fun commaT_fun ga po' l = po' <>

(if null l then empty

else parens_fun (commaT_fun ga l))

print_prefix_appl_text :: GlobalAnnos -> Doc -> [TERM] -> Doc

print_prefix_appl_text =

print_prefix_appl parens (commaT_text)

print_prefix_appl_latex :: GlobalAnnos -> Doc -> [TERM] -> Doc

print_prefix_appl_latex =

print_prefix_appl parens_latex (commaT_latex)

print_Literal :: (forall a .PrettyPrint a => GlobalAnnos -> a -> Doc)

-> (Doc -> Doc) -- ^ a function that surrounds

-- the given Doc with appropiate

-- parens

-> (Doc -> Doc -> Doc) -- ^ a beside with space

-- like <+> or <\+>

-> ([Doc] -> Doc) -- ^ a list concat with space and

-- fill the line policy like

-- fsep or fsep_latex

-> (forall b . PrettyPrint b =>

GlobalAnnos -> [b] -> Doc)

-- ^ a function that prints a nice

-- comma seperated list like commaT

-- or commaT_latex

-> Doc -- ^ a document containing the dot for a Fraction

-> Doc -- ^ a document containing the 'E' of a Floating

-> GlobalAnnos -> Id -> [TERM] -> Doc

print_Literal pf parens_fun

beside_fun fsep_fun commaT_fun dot_doc e_doc

ga li ts

| isSignedNumber ga li ts = let [t_ts] = ts

in pf ga li <>

((uncurry p_l) (splitAppl t_ts))

| isNumber ga li ts = hcat $ map (pf ga) $ toksNumber li

| isFrac ga li ts = let [lt,rt] = ts

(lni,lnt) = splitAppl lt

(rni,rnt) = splitAppl rt

ln = p_l lni lnt

rn = p_l rni rnt

in ln <> dot_doc <> rn

| isFloat ga li ts = let [bas,ex] = ts

(bas_i,bas_t) = splitAppl bas

(ex_i,ex_t) = splitAppl ex

bas_d = p_l bas_i bas_t

ex_d = p_l ex_i ex_t

in bas_d <> e_doc <> ex_d

| isList ga li ts = let list_body = commaT_fun ga $ listElements li

(openL, closeL, comps) = getListBrackets $

listBrackets li

in hcat(map (pf ga) openL) <+> list_body

<+> hcat(map (pf ga) closeL)

<> pf ga (Id [] comps [])

| isString ga li ts = ptext $

(\s -> let r = '"':(s ++ "\"") in seq r r) $

concatMap convCASLChar $ toksString li

| otherwise = condPrint_Mixfix pf parens_fun

beside_fun fsep_fun commaT_fun

ga li ts

where p_l = print_Literal pf parens_fun

beside_fun fsep_fun

commaT_fun dot_doc e_doc ga

toksNumber i = if tokIsDigit then

[tok]

else

map (termToTok "number") $

collectElements Nothing i ts

where tok = case i of

Id [] _ _ -> error "malformed Id!!!"

Id [tokk] [] _ -> tokk

Id (x:_) _ _ -> x

tokIsDigit = (isDigit $ head $ tokStr $ tok) && null ts

toksString i = case getLiteralType ga i of

StringNull -> []

StringCons n -> map (termToTok "string") $

collectElements (Just n) i ts

_ -> error "toksString"

termToTok tokType x = case basicTerm x of

Just tokk -> tokk

Nothing -> error ("malformed " ++ tokType)

listElements i = case getLiteralType ga i of

ListNull _ -> []

ListCons _ n -> collectElements (Just n) i ts

_ -> error "listElements"

listBrackets i = case getLiteralType ga i of

ListNull b -> b

ListCons b _ -> b

_ -> error "listBrackets"

print_Literal_text :: GlobalAnnos -> Id -> [TERM] -> Doc

print_Literal_text =

print_Literal printText0 parens (<+>) fsep (commaT_text)

(char '.') (char 'E')

print_Literal_latex :: GlobalAnnos -> Id -> [TERM] -> Doc

print_Literal_latex =

print_Literal printLatex0 parens_latex

(<\+>) fsep_latex (commaT_latex)

(casl_normal_latex ".") (casl_normal_latex "E")

-- printing consitent mixfix application or predication

{- TODO: consider string-, number-, list- and floating-annotations -}

print_mixfix_appl :: (forall a .PrettyPrint a => GlobalAnnos -> a -> Doc)

-> (Doc -> Doc) -- ^ a function that surrounds

-- the given Doc with appropiate

-- parens

-> (Doc -> Doc -> Doc) -- ^ a beside with space

-- like <+> or <\+>

-> ([Doc] -> Doc) -- ^ a list concat with space and

-- fill the line policy like

-- fsep or fsep_latex

-> GlobalAnnos -> Id -> [TERM] -> Doc

print_mixfix_appl pf parens_fun

beside_fun fsep_fun

ga oid terms =

d_terms_b_comp <> c `beside_fun` d_terms_a_comp

where (tops,cs) = case oid of Id x1 x2 _ -> (x1,x2)

c = if null cs then text "" -- an empty String works for ASCII

-- and LaTeX ensuring a space after

-- the last token of the identifier

-- if the compound is empty

else pf ga (Id [] cs [])

(tps_b_comp,places) = splitMixToken tops

nr_places = length $ filter isPlace tps_b_comp

(terms_b_comp,terms_a_comp) = splitAt nr_places terms

d_terms_b_comp = fsep_fun (first_term

: fillIn tps_b_comp' terms_b_comp')

d_terms_a_comp = fsep_fun (fillIn places' terms_a_comp'

++ [last_term])

isL3 = length tops >= 3

tps_b_comp' :: [Token]

terms_b_comp' :: [TERM]

first_term :: Doc

(tps_b_comp',terms_b_comp',first_term) =

if isL3 && (isPlace $ head tps_b_comp)

then

(tail tps_b_comp,

tail terms_b_comp,

condParensAppl pf parens_fun

ga oid (head terms_b_comp)

(Just ALeft))

else

(tps_b_comp,terms_b_comp,empty)

(places',terms_a_comp',last_term) =

if isL3 && (not $ null places)

then

(init places,init terms_a_comp,

condParensAppl pf parens_fun

ga oid (last terms_a_comp)

(Just ARight))

else

(places,terms_a_comp,empty)

fillIn :: [Token] -> [TERM] -> [Doc]

fillIn tps ts = let (_,nl) = mapAccumL pr ts tps in nl

pr :: [TERM] -> Token -> ([TERM],Doc)

pr [] top = ([], pf ga top)

pr tS@(t:ts) top

| isPlace top = (ts,pf ga t)

| otherwise = (tS,pf ga top)

condParensAppl :: (GlobalAnnos -> TERM -> Doc)

-> (Doc -> Doc) -- ^ a function that surrounds

-- the given Doc with appropiate

-- parens

-> GlobalAnnos -> Id -> TERM -> Maybe AssocEither -> Doc

condParensAppl pf parens_fun ga o_i t mdir =

case t of

Simple_id _ -> t'

Application _ [] _ -> t'

Application o it _

| isLiteral ga i_i it -> t'

-- ordinary appl (no place)

| isOrdAppl i_i -> t'

-- postfix appl

| isOrdAppl o_i && isPostfix i_i -> t'

| isMixfix o_i && isPostfix i_i -> t'

-- prefix appl w/o parens

| isOrdAppl o_i && isPrefix i_i -> t'

| isPostfix o_i && isPrefix i_i -> parens_fun t'

-- infix appl (left and right arg/place)

| (isInfix i_i && isSurround o_i)

|| (isInfix o_i && isSurround i_i) -> t'

| isInfix i_i && o_i == i_i ->

case mdir of

Nothing -> condParensPrec

Just ass | isAssoc ass amap o_i -> t'

| otherwise -> parens_fun t'

| otherwise -> condParensPrec

where i_i = case o of

Op_name i -> i

Qual_op_name i _ _ -> i

condParensPrec = case precRel (prec_annos ga) o_i i_i of

Lower -> t'

_ -> parens_fun t'

amap = assoc_annos ga

Sorted_term _ _ _ -> t'

Cast _ _ _ -> t'

_ -> parens_fun t'

where t' = pf ga t

condParensImplEquiv :: (GlobalAnnos -> FORMULA -> Doc)

-> (Doc -> Doc) -- ^ a function that surrounds

-- the given Doc with appropiate

-- parens

-> GlobalAnnos -> FORMULA -> FORMULA -> Doc

condParensImplEquiv pf parens_fun ga e_i f =

case e_i of

Implication _ _ _ -> case f of Implication _ _ _ -> f'

Disjunction _ _ -> f'

Conjunction _ _ -> f'

Negation _ _ -> f'

True_atom _ -> f'

False_atom _ -> f'

Predication _ _ _ -> f'

Existl_equation _ _ _ -> f'

Strong_equation _ _ _ -> f'

_ -> parens_fun f'

Equivalence _ _ _ -> case f of Disjunction _ _ -> f'

Conjunction _ _ -> f'

Negation _ _ -> f'

True_atom _ -> f'

False_atom _ -> f'

Predication _ _ _ -> f'

Quantification _ _ _ _ -> f'

Existl_equation _ _ _ -> f'

Strong_equation _ _ _ -> f'

_ -> parens_fun f'

_ -> error "Wrong call: condParensImplEquiv"

where f' = pf ga f

condParensXjunction :: (GlobalAnnos -> FORMULA -> Doc)

-> (Doc -> Doc) -- ^ a function that surrounds

-- the given Doc with appropiate

-- parens

-> GlobalAnnos -> FORMULA -> Doc

condParensXjunction pf parens_fun ga x =

case x of Negation _ _ -> x'

True_atom _ -> x'

False_atom _ -> x'

Predication _ _ _ -> x'

Existl_equation _ _ _ -> x'

Strong_equation _ _ _ -> x'

_ -> parens_fun x'

where x' = pf ga x

---- instances of ListCheck for various data types of AS_Basic_CASL ---

instance ListCheck SIG_ITEMS where

(Sort_items l _) `innerListGT` i = length l > i

(Op_items l _) `innerListGT` i = length l > i

(Pred_items l _) `innerListGT` i = length l > i

(Datatype_items l _) `innerListGT` i = length l > i

instance ListCheck SORT_ITEM where

(Sort_decl l _) `innerListGT` i = length l > i

(Subsort_decl l _ _) `innerListGT` i = length l > i

(Subsort_defn _ _ _ _ _) `innerListGT` _ = False

(Iso_decl _ _) `innerListGT` _ = False

instance ListCheck OP_ITEM where

(Op_decl l _ _ _) `innerListGT` i = length l > i

(Op_defn _ _ _ _) `innerListGT` _ = False

instance ListCheck PRED_ITEM where

(Pred_decl l _ _) `innerListGT` i = length l > i

(Pred_defn _ _ _ _) `innerListGT` _ = False

instance ListCheck DATATYPE_DECL where

(Datatype_decl _ _ _) `innerListGT` _ = False

instance ListCheck VAR_DECL where

(Var_decl l _ _) `innerListGT` i = length l > i

-----------------------------------------------------------------------------