7a8401ce858002b67e8f4198fde45a1562696ccbChristian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Modal/Print_AS.hs

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian MaederCopyright : (c) Wiebke Herding, C. Maeder, Uni Bremen 2004-2006

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichMaintainer : luecke@informatik.uni-bremen.de

50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederStability : provisional

50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederPortability : portable

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederprinting AS_Modal ModalSign data types

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding-}

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdingmodule Modal.Print_AS where

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport CASL.AS_Basic_CASL (FORMULA (..))

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport CASL.ToDoc

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

2bb4c0b7bc54ce51e68bff86b3a19be16e0f0449Christian Maederimport Common.AS_Annotation

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maederimport Common.Doc

40f1a7ea3e3ed12cbeca205918b645dabed0402aChristian Maederimport Common.DocUtils

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Common.Id

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Common.Keywords

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport Modal.AS_Modal

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport Modal.ModalSign

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Map as Map

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintFormulaOfModalSign :: FormExtension f => (FORMULA f -> FORMULA f)

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder -> [[Annoted (FORMULA f)]] -> Doc

99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian MaederprintFormulaOfModalSign sim = semiAnnos (pretty . sim) . concat

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty M_BASIC_ITEM where

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Simple_mod_decl is fs _) =

99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder cat [keyword modalityS <+> semiAnnos pretty is

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder , space <> specBraces (semiAnnos pretty fs)]

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Term_mod_decl ss fs _) =

c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder cat [keyword termS <+> keyword modalityS <+> semiAnnos pretty ss

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder , space <> specBraces (semiAnnos pretty fs)]

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty RIGOR where

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty Rigid = keyword rigidS

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty Flexible = keyword flexibleS

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty M_SIG_ITEM where

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Rigid_op_items r ls _) =

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder cat [pretty r <+> keyword (opS ++ pluralS ls),

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder space <> semiAnnos pretty ls]

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Rigid_pred_items r ls _) =

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder cat [pretty r <+> keyword (predS ++ pluralS ls),

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder space <> semiAnnos pretty ls]

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty M_FORMULA where

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (BoxOrDiamond b t f _) =

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder let sp = case t of

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Simple_mod _ -> (<>)

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder _ -> (<+>)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang td = pretty t

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder in sep $ (if b then brackets td

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder else less `sp` td `sp` greater)

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder : [condParensInnerF printFormula parens f]

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension M_FORMULA where

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder isQuantifierLike _ = False

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty MODALITY where

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Simple_mod ident) =

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder if tokStr ident == emptyS then empty

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang else pretty ident

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Term_mod t) = pretty t

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty ModalSign where

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder pretty = printModalSign id

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian MaederprintModalSign :: (FORMULA M_FORMULA -> FORMULA M_FORMULA) -> ModalSign -> Doc

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian MaederprintModalSign sim s =

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang let ms = modies s

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang tms = termModies s in

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder printSetMap (keyword flexibleS <+> keyword opS) empty

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder (MapSet.toMap $ flexOps s)

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder $+$ printSetMap (keyword flexibleS <+> keyword predS) space

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder (MapSet.toMap $ flexPreds s)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang $+$ (if Map.null ms then empty else

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder cat [keyword modalitiesS <+> sepBySemis (map sidDoc $ Map.keys ms)

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder , specBraces (printFormulaOfModalSign sim $ Map.elems ms)])

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang $+$ (if Map.null tms then empty else

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder cat [keyword termS <+> keyword modalityS <+> sepBySemis

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder (map idDoc $ Map.keys tms)

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder , specBraces (printFormulaOfModalSign sim $ Map.elems tms)])

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangcondParensInnerF :: Pretty f => (FORMULA f -> Doc)

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder -> (Doc -> Doc) {- ^ a function that surrounds

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder the given Doc with appropiate parens -}

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -> FORMULA f -> Doc

bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus LuettichcondParensInnerF pf parens_fun f =

bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich case f of

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Quantification {} -> f'

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Atom _ _ -> f'

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Predication {} -> f'

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder Definedness _ _ -> f'

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Equation {} -> f'

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Membership {} -> f'

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder ExtFORMULA _ -> f'

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder _ -> parens_fun f'

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder where f' = pf f