content: {- |
  Module      :  ./Hybrid/Print_AS.hs
  Copyright   :  (c) Renato Neves
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  nevrenato@gmail.com
  Stability   :  provisional
  Portability :  portable
  
  printing Hybrid data types
  -}
  
  module Hybrid.Print_AS where
  
  import CASL.AS_Basic_CASL (FORMULA (..))
  import CASL.ToDoc
  
  import Common.AS_Annotation
  import Common.Doc
  import Common.DocUtils
  import Common.Id
  import Common.Keywords
  import qualified Common.Lib.MapSet as MapSet
  
  import Hybrid.AS_Hybrid
  import Hybrid.HybridSign
  import Hybrid.Keywords
  import qualified Data.Map as Map
  
  
  printFormulaOfHybridSign :: FormExtension f => (FORMULA f -> FORMULA f)
                          -> [[Annoted (FORMULA f)]] -> Doc
  printFormulaOfHybridSign sim = semiAnnos (pretty . sim) . concat
  
  instance Pretty H_BASIC_ITEM where
      pretty (Simple_mod_decl is fs _) =
          cat [keyword modalityS <+> semiAnnos pretty is
              , space <> specBraces (semiAnnos pretty fs)]
      pretty (Term_mod_decl ss fs _) =
          cat [keyword termS <+> keyword modalityS <+> semiAnnos pretty ss
              , space <> specBraces (semiAnnos pretty fs)]
      pretty (Simple_nom_decl is fs _) =
          cat [keyword nominalS <+> semiAnnos pretty is
              , space <> specBraces (semiAnnos pretty fs)]
  
  instance Pretty RIGOR where
      pretty Rigid = keyword rigidS
      pretty Flexible = keyword flexibleS
  
  instance Pretty H_SIG_ITEM where
      pretty (Rigid_op_items r ls _) =
          cat [pretty r <+> keyword (opS ++ pluralS ls),
               space <> semiAnnos pretty ls]
      pretty (Rigid_pred_items r ls _) =
          cat [pretty r <+> keyword (predS ++ pluralS ls),
               space <> semiAnnos pretty ls]
  
  instance Pretty H_FORMULA where
      pretty (BoxOrDiamond b t f _) =
          let sp = case t of
                           Simple_mod _ -> (<>)
                           _ -> (<+>)
              td = pretty t
          in sep $ (if b then brackets td
                    else less `sp` td `sp` greater)
                 : [condParensInnerF printFormula parens f]
      pretty (At n f _) =
          let sp = (<>)
              td = pretty n
          in sep $ (prettyAt `sp` td) : [condParensInnerF printFormula parens f]
      pretty (Univ n f _) =
          let sp = (<+>)
              td = pretty n
          in sep $ (prettyUniv `sp` td) : [condParensInnerF printFormula parens f]
      pretty (Exist n f _) =
          let sp = (<+>)
              td = pretty n
          in sep $ (prettyExist `sp` td) :
                    [condParensInnerF printFormula parens f]
      pretty (Here n _) =
          let sp = (<+>)
              td = pretty n
          in sep [prettyHere `sp` td]
  
  instance FormExtension H_FORMULA where
    isQuantifierLike _ = False
  
  instance Pretty MODALITY where
      pretty (Simple_mod ident) =
          if tokStr ident == emptyS then empty
             else pretty ident
      pretty (Term_mod t) = pretty t
  
  instance Pretty NOMINAL where
      pretty (Simple_nom i) =
          if tokStr i == emptyS then empty
             else pretty i
  
  instance Pretty HybridSign where
      pretty = printHybridSign id
  
  printHybridSign :: (FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc
  printHybridSign sim s =
      let ms = modies s
          tms = termModies s
          ns = nomies s in
      printSetMap (keyword rigidS <+> keyword opS) empty
                  (MapSet.toMap $ rigidOps s)
      $+$ printSetMap (keyword rigidS <+> keyword predS) space
          (MapSet.toMap $ rigidPreds s)
      $+$ (if Map.null ms then empty else
          cat [keyword modalitiesS <+> sepBySemis (map sidDoc $ Map.keys ms)
              , specBraces (printFormulaOfHybridSign sim $ Map.elems ms)])
      $+$ (if Map.null tms then empty else
          cat [keyword termS <+> keyword modalityS <+> sepBySemis
                  (map idDoc $ Map.keys tms)
              , specBraces (printFormulaOfHybridSign sim $ Map.elems tms)])
      $+$ (if Map.null ns then empty else
          cat [keyword nominalsS <+> sepBySemis (map sidDoc $ Map.keys ns)
              , specBraces (printFormulaOfHybridSign sim $ Map.elems ns)])
  
  condParensInnerF :: Pretty f => (FORMULA f -> Doc)
                      -> (Doc -> Doc)    {- ^ a function that surrounds
                                         the given Doc with appropiate parens -}
                      -> FORMULA f -> Doc
  condParensInnerF pf parens_fun f =
      case f of
      Quantification {} -> f'
      Atom {} -> f'
      Predication {} -> f'
      Definedness {} -> f'
      Membership {} -> f'
      ExtFORMULA _ -> f'
      _ -> parens_fun f'
      where f' = pf f
  