{- |
Module      :  ./CoCASL/Print_AS.hs
Description :  pretty print abstract syntax of CoCASL
Copyright   :  (c) T. Mossakowski, Uni Bremen 2004-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  hausmann@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

printing AS_CoCASL and CoCASLSign data types
-}

module CoCASL.Print_AS where

import Common.Keywords
import Common.AS_Annotation
import Common.Doc
import Common.DocUtils

import CASL.AS_Basic_CASL
import CASL.ToDoc

import CoCASL.AS_CoCASL
import CoCASL.CoCASLSign

instance Pretty C_BASIC_ITEM where
    pretty :: C_BASIC_ITEM -> Doc
pretty = C_BASIC_ITEM -> Doc
printC_BASIC_ITEM

printC_BASIC_ITEM :: C_BASIC_ITEM -> Doc
printC_BASIC_ITEM :: C_BASIC_ITEM -> Doc
printC_BASIC_ITEM cb :: C_BASIC_ITEM
cb = case C_BASIC_ITEM
cb of
    CoFree_datatype l :: [Annoted CODATATYPE_DECL]
l _ -> String -> Doc
keyword String
cofreeS Doc -> Doc -> Doc
<+> [Annoted CODATATYPE_DECL] -> Doc
printAnnotedCoDatas [Annoted CODATATYPE_DECL]
l
    CoSort_gen l :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
l _ -> case [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
l of
      [Annoted (Ext_SIG_ITEMS (CoDatatype_items l' :: [Annoted CODATATYPE_DECL]
l' _)) _ _ _] ->
        String -> Doc
keyword String
cogeneratedS Doc -> Doc -> Doc
<+> [Annoted CODATATYPE_DECL] -> Doc
printAnnotedCoDatas [Annoted CODATATYPE_DECL]
l'
      _ -> String -> Doc
keyword String
cogeneratedS Doc -> Doc -> Doc
<+> Doc -> Doc
specBraces ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA) -> Doc)
-> [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA) -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
l)

printAnnotedCoDatas :: [Annoted CODATATYPE_DECL] -> Doc
printAnnotedCoDatas :: [Annoted CODATATYPE_DECL] -> Doc
printAnnotedCoDatas l :: [Annoted CODATATYPE_DECL]
l = String -> Doc
keyword (String
cotypeS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted CODATATYPE_DECL] -> String
forall a. [a] -> String
appendS [Annoted CODATATYPE_DECL]
l)
      Doc -> Doc -> Doc
<+> (CODATATYPE_DECL -> Doc) -> [Annoted CODATATYPE_DECL] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos CODATATYPE_DECL -> Doc
printCODATATYPE_DECL [Annoted CODATATYPE_DECL]
l

instance Pretty C_SIG_ITEM where
    pretty :: C_SIG_ITEM -> Doc
pretty = C_SIG_ITEM -> Doc
printC_SIG_ITEM

printC_SIG_ITEM :: C_SIG_ITEM -> Doc
printC_SIG_ITEM :: C_SIG_ITEM -> Doc
printC_SIG_ITEM (CoDatatype_items l :: [Annoted CODATATYPE_DECL]
l _) = [Annoted CODATATYPE_DECL] -> Doc
printAnnotedCoDatas [Annoted CODATATYPE_DECL]
l

instance Pretty CODATATYPE_DECL where
    pretty :: CODATATYPE_DECL -> Doc
pretty = CODATATYPE_DECL -> Doc
printCODATATYPE_DECL

printCODATATYPE_DECL :: CODATATYPE_DECL -> Doc
printCODATATYPE_DECL :: CODATATYPE_DECL -> Doc
printCODATATYPE_DECL (CoDatatype_decl s :: SORT
s a :: [Annoted COALTERNATIVE]
a _) = case [Annoted COALTERNATIVE]
a of
      [] -> SORT -> Doc
idDoc SORT
s
      _ -> [Doc] -> Doc
fsep [SORT -> Doc
idDoc SORT
s, Doc
defn, [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
bar) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                      (Annoted COALTERNATIVE -> Doc) -> [Annoted COALTERNATIVE] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((COALTERNATIVE -> Doc) -> Annoted COALTERNATIVE -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted COALTERNATIVE -> Doc
printCOALTERNATIVE) [Annoted COALTERNATIVE]
a]

instance Pretty COALTERNATIVE where
    pretty :: COALTERNATIVE -> Doc
pretty = COALTERNATIVE -> Doc
printCOALTERNATIVE

printCOALTERNATIVE :: COALTERNATIVE -> Doc
printCOALTERNATIVE :: COALTERNATIVE -> Doc
printCOALTERNATIVE coal :: COALTERNATIVE
coal = case COALTERNATIVE
coal of
    Co_construct k :: OpKind
k n :: Maybe SORT
n l :: [COCOMPONENTS]
l _ -> case Maybe SORT
n of
       Nothing -> Doc
empty
       Just i :: SORT
i -> SORT -> Doc
idDoc SORT
i
       Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (case [COCOMPONENTS]
l of
        [] -> case OpKind
k of
              Total -> Doc
empty
              _ -> Doc -> Doc
parens Doc
empty
        _ -> Doc -> Doc
parens ([Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (COCOMPONENTS -> Doc) -> [COCOMPONENTS] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map COCOMPONENTS -> Doc
printCOCOMPONENTS [COCOMPONENTS]
l))
                Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> case OpKind
k of
                   Total -> Doc
empty
                   _ -> Doc
quMarkD
    CoSubsorts l :: [SORT]
l _ -> String -> Doc
text (String
sortS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String
forall a. ListCheck a => a -> String
pluralS [SORT]
l) Doc -> Doc -> Doc
<+> [SORT] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SORT]
l

instance Pretty COCOMPONENTS where
    pretty :: COCOMPONENTS -> Doc
pretty = COCOMPONENTS -> Doc
printCOCOMPONENTS

printCOCOMPONENTS :: COCOMPONENTS -> Doc
printCOCOMPONENTS :: COCOMPONENTS -> Doc
printCOCOMPONENTS (CoSelect l :: [SORT]
l s :: OP_TYPE
s _) =
    [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc [SORT]
l) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OP_TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty OP_TYPE
s

instance FormExtension C_FORMULA where
  isQuantifierLike :: C_FORMULA -> Bool
isQuantifierLike f :: C_FORMULA
f = case C_FORMULA
f of
    BoxOrDiamond {} -> Bool
False
    CoSort_gen_ax {} -> Bool
True

instance Pretty C_FORMULA where
    pretty :: C_FORMULA -> Doc
pretty = C_FORMULA -> Doc
printC_FORMULA

printC_FORMULA :: C_FORMULA -> Doc
printC_FORMULA :: C_FORMULA -> Doc
printC_FORMULA cf :: C_FORMULA
cf = case C_FORMULA
cf of
    BoxOrDiamond b :: Bool
b t :: MODALITY
t f :: FORMULA C_FORMULA
f _ ->
      let sp :: Doc -> Doc -> Doc
sp = case MODALITY
t of
                 Simple_mod _ -> Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>)
                 _ -> Doc -> Doc -> Doc
(<+>)
          td :: Doc
td = MODALITY -> Doc
printMODALITY MODALITY
t
          fd :: Doc
fd = FORMULA C_FORMULA -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula FORMULA C_FORMULA
f
      in if Bool
b then Doc -> Doc
brackets Doc
td Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
fd else Doc
less Doc -> Doc -> Doc
`sp` Doc
td Doc -> Doc -> Doc
`sp` Doc
greater Doc -> Doc -> Doc
<+> Doc
fd
    CoSort_gen_ax sorts :: [SORT]
sorts ops :: [OP_SYMB]
ops _ -> String -> Doc
keyword String
cogeneratedS Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
         Doc -> Doc
specBraces ([Doc] -> Doc
sep [ String -> Doc
keyword String
sortS Doc -> Doc -> Doc
<+> [SORT] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SORT]
sorts Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
semi
                         , [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> Doc) -> [OP_SYMB] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty [OP_SYMB]
ops])

instance Pretty MODALITY where
    pretty :: MODALITY -> Doc
pretty = MODALITY -> Doc
printMODALITY

printMODALITY :: MODALITY -> Doc
printMODALITY :: MODALITY -> Doc
printMODALITY md :: MODALITY
md = case MODALITY
md of
    Simple_mod ident :: SIMPLE_ID
ident -> SIMPLE_ID -> Doc
sidDoc SIMPLE_ID
ident
    Term_mod t :: TERM C_FORMULA
t -> TERM C_FORMULA -> Doc
forall f. FormExtension f => TERM f -> Doc
printTerm TERM C_FORMULA
t

instance Pretty CoCASLSign where
    pretty :: CoCASLSign -> Doc
pretty = CoCASLSign -> Doc
printCoCASLSign

printCoCASLSign :: CoCASLSign -> Doc
printCoCASLSign :: CoCASLSign -> Doc
printCoCASLSign _ = Doc
empty