content: {- |
  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 = printC_BASIC_ITEM
  
  printC_BASIC_ITEM :: C_BASIC_ITEM -> Doc
  printC_BASIC_ITEM cb = case cb of
      CoFree_datatype l _ -> keyword cofreeS <+> printAnnotedCoDatas l
      CoSort_gen l _ -> case l of
        [Annoted (Ext_SIG_ITEMS (CoDatatype_items l' _)) _ _ _] ->
          keyword cogeneratedS <+> printAnnotedCoDatas l'
        _ -> keyword cogeneratedS <+> specBraces (vcat $ map pretty l)
  
  printAnnotedCoDatas :: [Annoted CODATATYPE_DECL] -> Doc
  printAnnotedCoDatas l = keyword (cotypeS ++ appendS l)
        <+> semiAnnos printCODATATYPE_DECL l
  
  instance Pretty C_SIG_ITEM where
      pretty = printC_SIG_ITEM
  
  printC_SIG_ITEM :: C_SIG_ITEM -> Doc
  printC_SIG_ITEM (CoDatatype_items l _) = printAnnotedCoDatas l
  
  instance Pretty CODATATYPE_DECL where
      pretty = printCODATATYPE_DECL
  
  printCODATATYPE_DECL :: CODATATYPE_DECL -> Doc
  printCODATATYPE_DECL (CoDatatype_decl s a _) = case a of
        [] -> idDoc s
        _ -> fsep [idDoc s, defn, sep $ punctuate (space <> bar) $
                        map (printAnnoted printCOALTERNATIVE) a]
  
  instance Pretty COALTERNATIVE where
      pretty = printCOALTERNATIVE
  
  printCOALTERNATIVE :: COALTERNATIVE -> Doc
  printCOALTERNATIVE coal = case coal of
      Co_construct k n l _ -> case n of
         Nothing -> empty
         Just i -> idDoc i
         <> (case l of
          [] -> case k of
                Total -> empty
                _ -> parens empty
          _ -> parens (fsep $ punctuate semi $ map printCOCOMPONENTS l))
                  <> case k of
                     Total -> empty
                     _ -> quMarkD
      CoSubsorts l _ -> text (sortS ++ pluralS l) <+> ppWithCommas l
  
  instance Pretty COCOMPONENTS where
      pretty = printCOCOMPONENTS
  
  printCOCOMPONENTS :: COCOMPONENTS -> Doc
  printCOCOMPONENTS (CoSelect l s _) =
      fsep (punctuate comma $ map idDoc l) <> colon <> pretty s
  
  instance FormExtension C_FORMULA where
    isQuantifierLike f = case f of
      BoxOrDiamond {} -> False
      CoSort_gen_ax {} -> True
  
  instance Pretty C_FORMULA where
      pretty = printC_FORMULA
  
  printC_FORMULA :: C_FORMULA -> Doc
  printC_FORMULA cf = case cf of
      BoxOrDiamond b t f _ ->
        let sp = case t of
                   Simple_mod _ -> (<>)
                   _ -> (<+>)
            td = printMODALITY t
            fd = printFormula f
        in if b then brackets td <> fd else less `sp` td `sp` greater <+> fd
      CoSort_gen_ax sorts ops _ -> keyword cogeneratedS <>
           specBraces (sep [ keyword sortS <+> ppWithCommas sorts <> semi
                           , fsep $ punctuate semi $ map pretty ops])
  
  instance Pretty MODALITY where
      pretty = printMODALITY
  
  printMODALITY :: MODALITY -> Doc
  printMODALITY md = case md of
      Simple_mod ident -> sidDoc ident
      Term_mod t -> printTerm t
  
  instance Pretty CoCASLSign where
      pretty = printCoCASLSign
  
  printCoCASLSign :: CoCASLSign -> Doc
  printCoCASLSign _ = empty
  