ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederCopyright : (c) Renato Neves
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederMaintainer : nevrenato@gmail.com
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederStability : provisional
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederPortability : portable
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederprinting Hybrid data types
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport CASL.AS_Basic_CASL (FORMULA (..))
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport qualified Common.Lib.MapSet as MapSet
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport qualified Data.Map as Map
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederprintFormulaOfHybridSign :: FormExtension f => (FORMULA f -> FORMULA f)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -> [[Annoted (FORMULA f)]] -> Doc
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederprintFormulaOfHybridSign sim = semiAnnos (pretty . sim) . concat
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Pretty H_BASIC_ITEM where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Simple_mod_decl is fs _) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [keyword modalityS <+> semiAnnos pretty is
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , space <> specBraces (semiAnnos pretty fs)]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Term_mod_decl ss fs _) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [keyword termS <+> keyword modalityS <+> semiAnnos pretty ss
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , space <> specBraces (semiAnnos pretty fs)]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Simple_nom_decl is fs _) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [keyword nominalS <+> semiAnnos pretty is
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , space <> specBraces (semiAnnos pretty fs)]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Pretty RIGOR where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty Rigid = keyword rigidS
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty Flexible = keyword flexibleS
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Pretty H_SIG_ITEM where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Rigid_op_items r ls _) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [pretty r <+> keyword (opS ++ pluralS ls),
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder space <> semiAnnos pretty ls]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Rigid_pred_items r ls _) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [pretty r <+> keyword (predS ++ pluralS ls),
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder space <> semiAnnos pretty ls]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Pretty H_FORMULA where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (BoxOrDiamond b t f _) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let sp = case t of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Simple_mod _ -> (<>)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder in sep $ (if b then brackets td
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder else less `sp` td `sp` greater)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder : [condParensInnerF printFormula parens f]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (At n f _) =
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder in sep $ (prettyAt `sp` td) : [condParensInnerF printFormula parens f]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Univ n f _) =
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder in sep $ (prettyUniv `sp` td) : [condParensInnerF printFormula parens f]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Exist n f _) =
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder in sep $ (prettyExist `sp` td) :
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder [condParensInnerF printFormula parens f]
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder pretty (Here n _) =
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder in sep [prettyHere `sp` td]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance FormExtension H_FORMULA where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder isQuantifierLike _ = False
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Pretty MODALITY where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Simple_mod ident) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder if tokStr ident == emptyS then empty
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder else pretty ident
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty (Term_mod t) = pretty t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Pretty NOMINAL where
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder pretty (Simple_nom i) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder if tokStr i == emptyS then empty
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Pretty HybridSign where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pretty = printHybridSign id
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederprintHybridSign :: (FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederprintHybridSign sim s =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let ms = modies s
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder tms = termModies s
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ns = nomies s in
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder printSetMap (keyword rigidS <+> keyword opS) empty
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $+$ printSetMap (keyword rigidS <+> keyword predS) space
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $+$ (if Map.null ms then empty else
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [keyword modalitiesS <+> sepBySemis (map sidDoc $ Map.keys ms)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , specBraces (printFormulaOfHybridSign sim $ Map.elems ms)])
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $+$ (if Map.null tms then empty else
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [keyword termS <+> keyword modalityS <+> sepBySemis
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (map idDoc $ Map.keys tms)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , specBraces (printFormulaOfHybridSign sim $ Map.elems tms)])
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $+$ (if Map.null ns then empty else
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder cat [keyword nominalsS <+> sepBySemis (map sidDoc $ Map.keys ns)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , specBraces (printFormulaOfHybridSign sim $ Map.elems ns)])
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedercondParensInnerF :: Pretty f => (FORMULA f -> Doc)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -> (Doc -> Doc) {- ^ a function that surrounds
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder the given Doc with appropiate parens -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -> FORMULA f -> Doc
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedercondParensInnerF pf parens_fun f =
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder Quantification {} -> f'
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder Predication {} -> f'
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder Definedness {} -> f'
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder Membership {} -> f'
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ExtFORMULA _ -> f'
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder _ -> parens_fun f'
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder where f' = pf f