{- |
Module      :  ./TopHybrid/Print_AS.hs
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 :: Named Frm_Wrap -> Doc
printNamedFormula = (Frm_Wrap -> Doc) -> Annoted Frm_Wrap -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted Frm_Wrap -> Doc
printFormula (Annoted Frm_Wrap -> Doc)
-> (Named Frm_Wrap -> Annoted Frm_Wrap) -> Named Frm_Wrap -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Frm_Wrap -> Annoted Frm_Wrap
forall s. Named s -> Annoted s
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 -> Doc
printFormula (Frm_Wrap l :: l
l f :: TH_FORMULA f
f) = case TH_FORMULA f
f of
                               UnderLogic f' :: f
f' -> l -> Named f -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named l
l (Named f -> Doc) -> Named f -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> f -> Named f
forall a s. a -> s -> SenAttr s a
makeNamed "" f
f'
                               f' :: TH_FORMULA f
f' -> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f'

instance (Pretty f) => Pretty (TH_FORMULA f) where
        pretty :: TH_FORMULA f -> Doc
pretty (At n :: NOMINAL
n f :: TH_FORMULA f
f) = [Char] -> Doc
keyword "@" Doc -> Doc -> Doc
<+> NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f
        pretty (Uni n :: NOMINAL
n f :: TH_FORMULA f
f) = [Char] -> Doc
keyword "forall worlds" Doc -> Doc -> Doc
<+> NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f
        pretty (Exist n :: NOMINAL
n f :: TH_FORMULA f
f) = [Char] -> Doc
keyword "exist world" Doc -> Doc -> Doc
<+> NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f
        pretty (UnderLogic f :: f
f) = [Char] -> Doc
keyword "{" Doc -> Doc -> Doc
<+> f -> Doc
forall a. Pretty a => a -> Doc
pretty f
f Doc -> Doc -> Doc
<+> [Char] -> Doc
keyword "}"
        pretty (Box m :: NOMINAL
m f :: TH_FORMULA f
f) = [Char] -> Doc
keyword "[" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
m Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Char] -> Doc
keyword "]" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f
        pretty (Dia m :: NOMINAL
m f :: TH_FORMULA f
f) = [Char] -> Doc
keyword "<" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
m Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Char] -> Doc
keyword ">" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f
        pretty (Conjunction f :: TH_FORMULA f
f f' :: TH_FORMULA f
f') = TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f Doc -> Doc -> Doc
<+> [Char] -> Doc
keyword "/\\" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f'
        pretty (Disjunction f :: TH_FORMULA f
f f' :: TH_FORMULA f
f') = TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f Doc -> Doc -> Doc
<+> [Char] -> Doc
keyword "\\/" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f'
        pretty (Implication f :: TH_FORMULA f
f f' :: TH_FORMULA f
f') = TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f Doc -> Doc -> Doc
<+> [Char] -> Doc
keyword "->" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f'
        pretty (BiImplication f :: TH_FORMULA f
f f' :: TH_FORMULA f
f') = TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f Doc -> Doc -> Doc
<+> [Char] -> Doc
keyword "<->" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f'
        pretty (Here n :: NOMINAL
n) = NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n
        pretty (Neg f :: TH_FORMULA f
f) = [Char] -> Doc
keyword "not" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f
        pretty (Par f :: TH_FORMULA f
f) = [Char] -> Doc
keyword "(" Doc -> Doc -> Doc
<+> TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f Doc -> Doc -> Doc
<+> [Char] -> Doc
keyword ")"
        pretty TrueA = [Char] -> Doc
keyword "True"
        pretty FalseA = [Char] -> Doc
keyword "False"

instance (Pretty s) => Pretty (THybridSign s) where
        pretty :: THybridSign s -> Doc
pretty x :: THybridSign s
x@(THybridSign _ _ s :: s
s) =
                [Char] -> Doc
keyword "Modalities" Doc -> Doc -> Doc
<+> Set NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty (THybridSign s -> Set NOMINAL
forall s. THybridSign s -> Set NOMINAL
modies THybridSign s
x) Doc -> Doc -> Doc
$+$
                [Char] -> Doc
keyword "Nominals" Doc -> Doc -> Doc
<+> Set NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty (THybridSign s -> Set NOMINAL
forall s. THybridSign s -> Set NOMINAL
nomies THybridSign s
x) Doc -> Doc -> Doc
$+$
                [Char] -> Doc
keyword "Under Sig {" Doc -> Doc -> Doc
$+$ s -> Doc
forall a. Pretty a => a -> Doc
pretty s
s Doc -> Doc -> Doc
$+$ [Char] -> Doc
keyword "}"

instance (Pretty b) => Pretty (TH_BSPEC b) where
        pretty :: TH_BSPEC b -> Doc
pretty (Bspec x :: [TH_BASIC_ITEM]
x b :: b
b) = [TH_BASIC_ITEM] -> Doc
forall a. Pretty a => a -> Doc
pretty [TH_BASIC_ITEM]
x
                                Doc -> Doc -> Doc
$+$ [Char] -> Doc
keyword "Under Spec {" Doc -> Doc -> Doc
$+$
                                b -> Doc
forall a. Pretty a => a -> Doc
pretty b
b
                                Doc -> Doc -> Doc
$+$ [Char] -> Doc
keyword "}"

instance Pretty (TH_BASIC_ITEM) where
        pretty :: TH_BASIC_ITEM -> Doc
pretty (Simple_mod_decl x :: [NOMINAL]
x) = [Char] -> Doc
keyword "Modalities" Doc -> Doc -> Doc
<+> [NOMINAL] -> Doc
forall a. Pretty a => a -> Doc
pretty [NOMINAL]
x
        pretty (Simple_nom_decl x :: [NOMINAL]
x) = [Char] -> Doc
keyword "Nominals" Doc -> Doc -> Doc
<+> [NOMINAL] -> Doc
forall a. Pretty a => a -> Doc
pretty [NOMINAL]
x

instance Pretty Frm_Wrap where
        pretty :: Frm_Wrap -> Doc
pretty (Frm_Wrap _ f :: TH_FORMULA f
f) = TH_FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty TH_FORMULA f
f
instance Pretty Spc_Wrap where
        pretty :: Spc_Wrap -> Doc
pretty (Spc_Wrap _ b :: TH_BSPEC bs
b f :: [Annoted Frm_Wrap]
f) = TH_BSPEC bs -> Doc
forall a. Pretty a => a -> Doc
pretty TH_BSPEC bs
b Doc -> Doc -> Doc
$+$ [Annoted Frm_Wrap] -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted Frm_Wrap]
f
instance Pretty Mor where
        pretty :: Mor -> Doc
pretty _ = [Char] -> Doc
forall a. HasCallStack => [Char] -> a
error "Not implemented!"

instance Pretty Sgn_Wrap where
        pretty :: Sgn_Wrap -> Doc
pretty (Sgn_Wrap _ s :: THybridSign sign
s) = THybridSign sign -> Doc
forall a. Pretty a => a -> Doc
pretty THybridSign sign
s
        pretty (Sgn_Wrap
EmptySign) = () -> Doc
forall a. Pretty a => a -> Doc
pretty ()