{- |
Module      :  ./ExtModal/Print_AS.hs
Copyright   :  DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

printing AS_ExtModal ExtModalSign data types
-}

module ExtModal.Print_AS where

import Common.Keywords
import Common.Doc
import Common.DocUtils
import Common.Id
import qualified Common.Lib.MapSet as MapSet

import qualified Data.Set as Set

import ExtModal.AS_ExtModal
import ExtModal.ExtModalSign
import ExtModal.Keywords

import CASL.AS_Basic_CASL (FORMULA (..))
import CASL.ToDoc

instance Pretty ModDefn where
  pretty (ModDefn time term id_list ax_list _) = fsep
          [(if time then keyword timeS else empty)
           <+> (if term then keyword termS else empty)
           <+> keyword modalityS
          , semiAnnos pretty id_list
          , if null ax_list then empty else
                specBraces (vcat $ map pretty ax_list)]

instance Pretty FrameForm where
  pretty (FrameForm l f _) = case f of
        [] -> topSigKey (varS ++ pluralS l) <+> printVarDecls l
        [s] | null l -> pretty s
        _ | null l -> printAnnotedBulletFormulas f
        _ -> fsep [fsep $ forallDoc : printVarDeclL l
                  , printAnnotedBulletFormulas f]

instance Pretty EM_BASIC_ITEM where
  pretty itm = case itm of
    ModItem md -> pretty md
    Nominal_decl id_list _ -> sep [keyword nominalS, semiAnnos pretty id_list]

modPrec :: MODALITY -> Int
modPrec m = case m of
  SimpleMod _ -> 0 -- strongest
  TermMod _ -> 0 -- strongest
  Guard _ -> 1
  TransClos _ -> 2
  ModOp Composition _ _ -> 3
  ModOp Intersection _ _ -> 4
  ModOp Union _ _ -> 5
  ModOp OrElse _ _ -> 6 -- weakest

printMPrec :: Bool -> MODALITY -> MODALITY -> Doc
printMPrec b oP cP =
  (if (if b then (>) else (>=)) (modPrec oP) $ modPrec cP then id else parens)
  $ pretty cP

instance Pretty MODALITY where
        pretty mdl = case mdl of
          SimpleMod idt ->
            if tokStr idt == emptyS then empty else pretty idt
          TermMod t -> pretty t
          Guard sen -> prJunct sen <> keyword quMark
          TransClos md -> printMPrec False mdl md
            <> keyword tmTransClosS
          ModOp o md1 md2 -> fsep [printMPrec True mdl md1
            , keyword (show o) <+> printMPrec False mdl md2]

prettyRigor :: Bool -> Doc
prettyRigor b = keyword $ if b then rigidS else flexibleS

instance Pretty EM_SIG_ITEM where
        pretty (Rigid_op_items rig op_list _) =
                fsep [prettyRigor rig <+> keyword (opS ++ pluralS op_list),
                     semiAnnos pretty op_list]
        pretty (Rigid_pred_items rig pred_list _) =
                fsep [prettyRigor rig <+> keyword (predS ++ pluralS pred_list),
                     semiAnnos pretty pred_list]

instance FormExtension EM_FORMULA where
  isQuantifierLike ef = case ef of
    UntilSince {} -> False
    PrefixForm _ f _ -> isQuant f
    _ -> True
  prefixExt ef = case ef of
    ModForm _ -> id
    _ -> (bullet <+>)

isEMJunct :: FORMULA EM_FORMULA -> Bool
isEMJunct f = case f of
  ExtFORMULA (UntilSince {}) -> True
  _ -> isJunct f

prJunct :: FORMULA EM_FORMULA -> Doc
prJunct f = (if isEMJunct f then parens else id) $ pretty f

instance Pretty FormPrefix where
  pretty fp = case fp of
    BoxOrDiamond choice modality gEq number ->
      let sp = case modality of
                 SimpleMod _ -> (<>)
                 _ -> (<+>)
          mdl = pretty modality
      in (case choice of
                  Box -> brackets mdl
                  Diamond -> less `sp` mdl `sp` greater
                  EBox -> text oB <> mdl <> text cB)
               <+> if gEq && number == 1 then empty else
                (if gEq then empty else keyword lessEq)
                <> text (show number)
    Hybrid choice nom ->
      keyword (if choice then atS else hereS) <+> pretty nom
    PathQuantification choice ->
      keyword (if choice then allPathsS else somePathsS)
    NextY choice ->
      keyword (if choice then nextS else yesterdayS)
    StateQuantification dir_choice choice ->
      keyword (if dir_choice then if choice then generallyS else eventuallyS
               else if choice then hithertoS else previouslyS)
    FixedPoint choice p_var ->
      keyword (if choice then muS else nuS) <+> pretty p_var <+> bullet

instance Pretty EM_FORMULA where
  pretty ef = case ef of
    PrefixForm p s _ -> (case p of
      BoxOrDiamond _ m _ _ -> case m of
        SimpleMod _ -> hsep
        _ -> sep
      _ -> hsep) [pretty p, prJunct s]
    UntilSince choice s1 s2 _ -> printInfix True sep (prJunct s1)
      (keyword $ if choice then untilS else sinceS)
      $ prJunct s2
    ModForm md -> pretty md

instance Pretty EModalSign where
    pretty sign =
        let mds = modalities sign
            tims = timeMods sign
            terms = termMods sign
            nms = nominals sign in
        printSetMap (keyword flexibleS <+> keyword opS) empty
            (MapSet.toMap $ flexOps sign)
        $+$
        printSetMap (keyword flexibleS <+> keyword predS) space
            (MapSet.toMap $ flexPreds sign)
        $+$
        vcat (map (\ i -> fsep
          $ [keyword timeS | Set.member i tims]
          ++ [keyword termS | Set.member i terms]
          ++ [keyword modalityS, idDoc i])
            $ Set.toList mds)
        $+$
        (if Set.null nms then empty else
        keyword nominalS <+> sepBySemis (map idDoc (Set.toList nms)))