7a8401ce858002b67e8f4198fde45a1562696ccbChristian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian MaederCopyright : DFKI GmbH 2009

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

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichMaintainer : codruta.liliana@gmail.com

50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederStability : experimental

50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederPortability : portable

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederprinting AS_ExtModal ExtModalSign data types

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding-}

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdingmodule ExtModal.Print_AS where

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Common.Keywords

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Common.AS_Annotation

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Common.Doc

2bb4c0b7bc54ce51e68bff86b3a19be16e0f0449Christian Maederimport Common.DocUtils

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maederimport qualified Common.Lib.MapSet as MapSet

40f1a7ea3e3ed12cbeca205918b645dabed0402aChristian Maeder

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Map as Map

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Set as Set

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport ExtModal.AS_ExtModal

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport ExtModal.ExtModalSign

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport ExtModal.Keywords

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

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

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport CASL.ToDoc

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maederinstance Pretty EM_BASIC_ITEM where

99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder pretty (Simple_mod_decl time id_list ax_list _) = fsep

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder [(if time then keyword timeS else empty) <+> keyword modalityS

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang , semiAnnos pretty id_list

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang , if null ax_list then empty else

99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder specBraces (semiAnnos pretty ax_list)]

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder pretty (Nominal_decl id_list _) = sep

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang [ keyword nominalS, semiAnnos pretty id_list ]

c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maederinstance Pretty MODALITY where

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder pretty (Simple_modality idt) = pretty idt

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Composition md1 md2) = (keyword tmOParanthS) <> (pretty md1) <>

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (keyword tmCompositionS) <> (pretty md2)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang <> (keyword tmCParanthS)

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder pretty (Union md1 md2) = (keyword tmOParanthS) <> (pretty md1) <> (keyword tmUnionS)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang <> (pretty md2) <> (keyword tmCParanthS)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (TransitiveClosure md) = (keyword tmOParanthS) <> (pretty md) <>

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder (keyword (tmTransClosS ++ tmCParanthS))

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder pretty (Guard sen) = (keyword tmOParanthS) <> (pretty sen) <> (keyword (tmGuardS ++ tmCParanthS))

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maederinstance Pretty RIGOR where

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder pretty Rigid = keyword rigidS

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder pretty Flexible = keyword flexibleS

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty EM_SIG_ITEM where

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder pretty (Rigid_op_items rig op_list _) =

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder cat [pretty rig <+> keyword (opS ++ pluralS op_list),

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder space <> semiAnnos pretty op_list]

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Rigid_pred_items rig pred_list _) =

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder cat [pretty rig <+> keyword (predS ++ pluralS pred_list),

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder space <> semiAnnos pretty pred_list]

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance Pretty NOMINAL where

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty (Nominal idt) = pretty idt

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederinstance FormExtension EM_FORMULA

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty EM_FORMULA where

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder pretty (BoxOrDiamond choice modality leq_geq number em_sentence _) =

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang let sp = case modality of

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Simple_modality _ -> (<>)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang _ -> (<+>)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang mdl = pretty modality

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder in sep $ (if choice then brackets mdl else less `sp` mdl `sp` greater)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang : (if leq_geq then keyword lessEq else keyword greaterEq)

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder : (text (show number)) : space : [condParensInnerF printFormula parens em_sentence]

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty (Hybrid choice nom em_sentence _) =

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang sep $ (if choice then keyword atS else keyword hereS) : space : (pretty nom) : space

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder : [condParensInnerF printFormula parens em_sentence]

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder pretty (UntilSince choice sentence1 sentence2 _) =

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder sep $ ([condParensInnerF printFormula parens sentence1]

a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder ++ ( space : (if choice then keyword untilS else keyword sinceS) : space

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang : [condParensInnerF printFormula parens sentence2]))

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder pretty (PathQuantification choice em_sentence _) =

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder sep $ (if choice then keyword allPathsS else keyword somePathsS) : space

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang : [condParensInnerF printFormula parens em_sentence]

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder pretty (NextY choice em_sentence _) =

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder sep $ (if choice then keyword nextS else keyword yesterdayS) : space

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder : [condParensInnerF printFormula parens em_sentence]

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder pretty (StateQuantification dir_choice choice em_sentence _) =

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang let kw = case dir_choice of

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder True -> if choice then keyword generallyS else keyword eventuallyS

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder _ -> if choice then keyword hithertoS else keyword previouslyS

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder in sep $ kw : space : [condParensInnerF printFormula parens em_sentence]

bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich pretty (FixedPoint choice p_var em_sentence _) =

bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich sep $ (if choice then keyword muS else keyword nuS) : space : (pretty p_var) : space

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder : [condParensInnerF printFormula parens em_sentence]

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercondParensInnerF :: Pretty f => (FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian MaedercondParensInnerF frm_print parens_fun frm =

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder case frm of

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Quantification _ _ _ _ -> frm'

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder True_atom _ -> frm'

180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder False_atom _ -> frm'

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder Predication _ _ _ -> frm'

Definedness _ _ -> frm'

Existl_equation _ _ _ -> frm'

Strong_equation _ _ _ -> frm'

Membership _ _ _ -> frm'

ExtFORMULA _ -> frm'

_ -> parens_fun frm'

where frm' = frm_print frm

instance Pretty EModalSign where

pretty = printEModalSign id

printEModalSign :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA) -> EModalSign

-> Doc

printEModalSign sim sign =

let mds = modalities sign

tms = time_modalities sign

nms = nominals sign in

printSetMap (keyword rigidS <+> keyword opS) empty

(MapSet.toMap $ rigidOps sign)

$+$

printSetMap (keyword rigidS <+> keyword predS) empty

(MapSet.toMap $ rigidPreds sign)

$+$

(if Map.null mds then empty else fsep

[ keyword modalitiesS

, sepBySemis (map sidDoc (Map.keys mds))

, let fs = Map.elems mds in if null $ concat fs then empty else

specBraces $ printFormulaOfEModalSign sim fs ])

$+$

(if Set.null tms then empty else

keyword timeS <+> keyword modalitiesS

<+> sepBySemis (map sidDoc (Set.toList tms)))

$+$

(if Set.null nms then empty else

keyword nominalsS <+> sepBySemis (map sidDoc (Set.toList nms)))

printFormulaOfEModalSign :: FormExtension f => (FORMULA f -> FORMULA f)

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

printFormulaOfEModalSign sim = vcat . map

(sepBySemis . map (printAnnoted $ pretty . sim))