Print_AS.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
4169N/A{- |
1178N/AModule : $Header$
1178N/ACopyright : DFKI GmbH 2009
1178N/ALicense : GPLv2 or higher, see LICENSE.txt
1178N/A
1178N/AMaintainer : codruta.liliana@gmail.com
1178N/AStability : experimental
1178N/APortability : portable
1178N/A
1178N/Aprinting AS_ExtModal ExtModalSign data types
1178N/A-}
1178N/A
1178N/Amodule ExtModal.Print_AS where
1178N/A
1178N/Aimport Common.Keywords
1178N/Aimport qualified Data.Map as Map
1178N/Aimport qualified Data.Set as Set
2362N/Aimport Common.AS_Annotation
2362N/Aimport Common.Doc
2362N/Aimport Common.DocUtils
1178N/A
4169N/Aimport ExtModal.AS_ExtModal
1178N/Aimport ExtModal.ExtModalSign
1178N/Aimport ExtModal.Keywords
4033N/Aimport ExtModal.MorphismExtension
4033N/A
1178N/Aimport CASL.AS_Basic_CASL (FORMULA(..))
1178N/Aimport CASL.ToDoc
1178N/A
1178N/Ainstance Pretty EM_BASIC_ITEM where
1178N/A pretty (Simple_mod_decl time id_list ax_list _) =
1178N/A cat[if time then (keyword timeS) else empty
4033N/A , keyword modalityS <+> semiAnnos pretty id_list
1178N/A , space <> specBraces (semiAnnos pretty ax_list)]
1178N/A pretty (Nominal_decl id_list _) = keyword nominalS <+> semiAnnos pretty id_list
4033N/A
1178N/Ainstance Pretty MODALITY where
1178N/A pretty (Simple_modality idt) = pretty idt
1178N/A pretty (Composition md1 md2) = (keyword tmOParanthS) <> (pretty md1) <>
4033N/A (keyword tmCompositionS) <> (pretty md2)
1178N/A <> (keyword tmCParanthS)
1178N/A pretty (Union md1 md2) = (keyword tmOParanthS) <> (pretty md1) <> (keyword tmUnionS)
4033N/A <> (pretty md2) <> (keyword tmCParanthS)
1178N/A pretty (TransitiveClosure md) = (keyword tmOParanthS) <> (pretty md) <>
1178N/A (keyword (tmTransClosS ++ tmCParanthS))
4033N/A pretty (Guard sen) = (keyword tmOParanthS) <> (pretty sen) <> (keyword (tmGuardS ++ tmCParanthS))
1178N/A
1178N/Ainstance Pretty RIGOR where
4033N/A pretty Rigid = keyword rigidS
0N/A pretty Flexible = keyword flexibleS
1178N/A
1178N/Ainstance Pretty EM_SIG_ITEM where
1178N/A pretty (Rigid_op_items rig op_list _) =
4033N/A cat [pretty rig <+> keyword (opS ++ pluralS op_list),
1178N/A space <> semiAnnos pretty op_list]
1178N/A pretty (Rigid_pred_items rig pred_list _) =
1178N/A cat [pretty rig <+> keyword (predS ++ pluralS pred_list),
1178N/A space <> semiAnnos pretty pred_list]
1178N/A
1178N/Ainstance Pretty NOMINAL where
1178N/A pretty (Nominal idt) = pretty idt
1178N/A
1178N/Ainstance Pretty EM_FORMULA where
1178N/A pretty (BoxOrDiamond choice modality leq_geq number em_sentence _) =
1178N/A let sp = case modality of
1178N/A Simple_modality _ -> (<>)
1178N/A _ -> (<+>)
4033N/A mdl = pretty modality
1178N/A in sep $ (if choice then brackets mdl else less `sp` mdl `sp` greater)
1178N/A : (if leq_geq then keyword lessEq else keyword greaterEq)
4033N/A : (text (show number)) : space : [condParensInnerF (printFormula pretty) parens em_sentence]
1178N/A
1178N/A pretty (Hybrid choice nom em_sentence _) =
1178N/A sep $ (if choice then keyword atS else keyword hereS) : space : (pretty nom) : space
1178N/A : [condParensInnerF (printFormula pretty) parens em_sentence]
4033N/A pretty (UntilSince choice sentence1 sentence2 _) =
1178N/A sep $ ([condParensInnerF (printFormula pretty) parens sentence1]
1178N/A ++ ( space : (if choice then keyword untilS else keyword sinceS) : space
1178N/A : [condParensInnerF (printFormula pretty) parens sentence2]))
1178N/A pretty (PathQuantification choice em_sentence _) =
1178N/A sep $ (if choice then keyword allPathsS else keyword somePathsS) : space
1178N/A : [condParensInnerF (printFormula pretty) parens em_sentence]
4033N/A pretty (NextY choice em_sentence _) =
1178N/A sep $ (if choice then keyword nextS else keyword yesterdayS) : space
1178N/A : [condParensInnerF (printFormula pretty) parens em_sentence]
1178N/A pretty (StateQuantification dir_choice choice em_sentence _) =
4033N/A let kw = case dir_choice of
1178N/A True -> if choice then keyword generallyS else keyword eventuallyS
1178N/A _ -> if choice then keyword hithertoS else keyword previouslyS
1178N/A in sep $ kw : space : [condParensInnerF (printFormula pretty) parens em_sentence]
4033N/A pretty (FixedPoint choice p_var em_sentence _) =
1178N/A sep $ (if choice then keyword muS else keyword nuS) : space : (pretty p_var) : space
1178N/A : [condParensInnerF (printFormula pretty) parens em_sentence]
1178N/A
4033N/AcondParensInnerF :: Pretty f => (FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc
1178N/AcondParensInnerF frm_print parens_fun frm =
1178N/A case frm of
1178N/A Quantification _ _ _ _ -> frm'
4033N/A True_atom _ -> frm'
1178N/A False_atom _ -> frm'
1178N/A Predication _ _ _ -> frm'
4033N/A Definedness _ _ -> frm'
0N/A Existl_equation _ _ _ -> frm'
0N/A Strong_equation _ _ _ -> frm'
0N/A Membership _ _ _ -> frm'
0N/A ExtFORMULA _ -> frm'
0N/A _ -> parens_fun frm'
0N/A where frm' = frm_print frm
0N/A
0N/Ainstance Pretty EModalSign where
0N/A pretty = printEModalSign id
0N/A
0N/AprintEModalSign :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA) -> EModalSign -> Doc
0N/AprintEModalSign sim sign =
1178N/A let mds = modalities sign
4033N/A tms = time_modalities sign
4033N/A nms = nominals sign in
0N/A printSetMap (keyword rigidS <+> keyword opS) empty (rigidOps sign)
4033N/A $+$
0N/A printSetMap (keyword rigidS <+> keyword predS) empty (rigidPreds sign)
4033N/A $+$
0N/A (if Map.null mds then empty else
1178N/A cat [keyword modalitiesS <+> (fsep $ punctuate semi $ map sidDoc (Map.keys mds))
0N/A , specBraces (printFormulaOfEModalSign sim $ Map.elems mds)])
0N/A $+$
4033N/A (if Set.null tms then empty else
1178N/A keyword timeS <+> keyword modalitiesS <+> (fsep $ punctuate semi $ map sidDoc (Set.toList tms)))
1178N/A $+$
4033N/A (if Set.null nms then empty else
1178N/A keyword nominalsS <+> (fsep $ punctuate semi $ map sidDoc (Set.toList nms)))
4033N/A
1178N/A
4033N/AprintFormulaOfEModalSign :: Pretty f => (FORMULA f -> FORMULA f) -> [[Annoted (FORMULA f)]] -> Doc
0N/AprintFormulaOfEModalSign sim =
0N/A vcat . map (\ tf -> fsep $ punctuate semi $ map (printAnnoted $ pretty . sim) tf)
4033N/A
0N/Ainstance Pretty MorphExtension where
1178N/A pretty me = pretty (source me) <+> pretty (target me) <+>
4033N/A text (show (Map.toList (mod_map me))) <+> text (show (Map.toList (nom_map me)))
0N/A
0N/A