hets/COL/Print_AS.hs

	Print_AS.hs revision 88ece6e49930670e8fd3ee79c89a2e918d2fbd0c
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa{-
649fdc0d0502d62d160c150684356fef2c273484Eugen KuksaModule      :  $Header$
649fdc0d0502d62d160c150684356fef2c273484Eugen KuksaCopyright   :  (c) Wiebke Herding, C. Maeder, Uni Bremen 2004
649fdc0d0502d62d160c150684356fef2c273484Eugen KuksaLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa
649fdc0d0502d62d160c150684356fef2c273484Eugen KuksaMaintainer  :  hets@tzi.de
649fdc0d0502d62d160c150684356fef2c273484Eugen KuksaStability   :  provisional
649fdc0d0502d62d160c150684356fef2c273484Eugen KuksaPortability :  portable
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa  printing AS_Modal ModalSign data types
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa-}
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksamodule Modal.Print_AS where
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Common.Id
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Common.Keywords
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport qualified Common.Lib.Set as Set
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Common.Lib.Pretty
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Common.PrettyPrint
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Common.PPUtils
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport CASL.Print_AS_Basic
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport CASL.Sign
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Modal.AS_Modal
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Modal.ModalSign
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksainstance PrettyPrint M_BASIC_ITEM where
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    printText0 ga (Simple_mod_decl is fs _) =
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    ptext modalityS <+> semiAnno_text ga is
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa          <> braces (semiAnno_text ga fs)
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    printText0 ga (Term_mod_decl ss fs _) =
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    ptext termS <+> ptext modalityS <+> semiAnno_text ga ss
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa          <> braces (semiAnno_text ga fs)
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksainstance PrettyPrint RIGOR where
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    printText0 _ Rigid = ptext rigidS
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    printText0 _ Flexible = ptext flexibleS
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksainstance PrettyPrint M_SIG_ITEM where
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    printText0 ga (Rigid_op_items r ls _) =
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa    hang (printText0 ga r <+> ptext opS <> pluralS_doc ls) 4 $
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa         semiAnno_text ga ls
    printText0 ga (Rigid_pred_items r ls _) =
    hang (printText0 ga r <+> ptext predS <> pluralS_doc ls) 4 $
         semiAnno_text ga ls

instance PrettyPrint M_FORMULA where
    printText0 ga (Box t f _) =
       brackets (printText0 ga t) <> printText0 ga f
    printText0 ga (Diamond t f _) =
    let sp = case t of
             Simple_mod _ -> (<>)
             _ -> (<+>)
        in ptext lessS `sp` printText0 ga t `sp` ptext greaterS
           <+> printText0 ga f

instance PrettyPrint MODALITY where
    printText0 ga (Simple_mod ident) =
    if tokStr ident == emptyS then empty
       else printText0 ga ident
    printText0 ga (Term_mod t) = printText0 ga t

instance PrettyPrint ModalSign where
    printText0 ga s =
    let ms = modies s
        tms = termModies s in
    printSetMap (ptext rigidS <+> ptext opS) empty ga (rigidOps s)
    $$
    printSetMap (ptext rigidS <+> ptext predS)
            space ga (rigidPreds s)
    $$ (if Set.null ms then empty else
    ptext modalitiesS <+> semiT_text ga (Set.toList ms))
    $$ (if Set.null tms then empty else
    ptext termS <+> ptext modalityS <+> semiT_text ga (Set.toList tms))