{- |

Module : $Header$

License : GPLv2 or higher, see LICENSE.txt

Maintainer : nevrenato@gmail.com

Stability : provisional

Portability : portable

Description :

Instance of class Pretty for hybrid logic

with an arbitrary logic below.

-}

module TopHybrid.Print_AS (printNamedFormula) where

import Common.Doc

import Common.DocUtils

import Common.AS_Annotation

import TopHybrid.AS_TopHybrid

import TopHybrid.TopHybridSign

import Logic.Logic

printNamedFormula :: Named Frm_Wrap -> Doc

printNamedFormula = printAnnoted printFormula . fromLabelledSen

-- the use of the function makeNamed is vacuous, it is only needed

-- to satisfy the types of the print_named function

printFormula :: Frm_Wrap -> Doc

printFormula (Frm_Wrap l f) = case f of

UnderLogic f' -> print_named l $ makeNamed "" f'

f' -> pretty f'

instance (Pretty f) => Pretty (TH_FORMULA f) where

pretty (At n f) = keyword "@" <+> (pretty n) <+> (pretty f)

pretty (Uni n f) = keyword "forall worlds" <+> (pretty n) <+> (pretty f)

pretty (Exist n f) = keyword "exist world" <+> (pretty n) <+> (pretty f)

pretty (UnderLogic f) = keyword "{" <+> (pretty f) <+> (keyword "}")

pretty (Box m f) = keyword "[" <> (pretty m) <> keyword "]" <+> (pretty f)

pretty (Dia m f) = keyword "<" <> (pretty m) <> keyword ">" <+> (pretty f)

pretty (Conjunction f f') = pretty f <+> (keyword "/\\") <+> (pretty f')

pretty (Disjunction f f') = pretty f <+> (keyword "\\/") <+> (pretty f')

pretty (Implication f f') = pretty f <+> (keyword "->") <+> (pretty f')

pretty (BiImplication f f') = pretty f <+> (keyword "<->") <+> (pretty f')

pretty (Here n) = pretty n

pretty (Neg f) = keyword "not" <+> (pretty f)

pretty (Par f) = keyword "(" <+> (pretty f) <+> (keyword ")")

pretty TrueA = keyword "True"

pretty FalseA = keyword "False"

instance (Pretty s) => Pretty (THybridSign s) where

pretty x@(THybridSign _ _ s) =

keyword "Modalities" <+> (pretty $ modies x) $+$

keyword "Nominals" <+> (pretty $ nomies x) $+$

keyword "Under Sig {" $+$ (pretty s) $+$ (keyword "}")

instance (Pretty b) => Pretty (TH_BSPEC b) where

pretty (Bspec x b) = pretty x

$+$ keyword "Under Spec {" $+$

(pretty b)

$+$ keyword "}"

instance Pretty (TH_BASIC_ITEM) where

pretty (Simple_mod_decl x) = keyword "Modalities" <+> (pretty x)

pretty (Simple_nom_decl x) = keyword "Nominals" <+> (pretty x)

instance Pretty Frm_Wrap where

pretty (Frm_Wrap _ f) = pretty f

instance Pretty Spc_Wrap where

pretty (Spc_Wrap _ b f) = pretty b $+$ (pretty f)

instance Pretty Mor where

instance Pretty Sgn_Wrap where

pretty (Sgn_Wrap _ s) = pretty s

pretty (EmptySign) = pretty ()