{- |
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 -> Doc
pretty (ModDefn time :: Bool
time term :: Bool
term id_list :: [Annoted Id]
id_list ax_list :: [Annoted FrameForm]
ax_list _) = [Doc] -> Doc
fsep
          [(if Bool
time then String -> Doc
keyword String
timeS else Doc
empty)
           Doc -> Doc -> Doc
<+> (if Bool
term then String -> Doc
keyword String
termS else Doc
empty)
           Doc -> Doc -> Doc
<+> String -> Doc
keyword String
modalityS
          , (Id -> Doc) -> [Annoted Id] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos Id -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted Id]
id_list
          , if [Annoted FrameForm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted FrameForm]
ax_list then Doc
empty else
                Doc -> Doc
specBraces ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted FrameForm -> Doc) -> [Annoted FrameForm] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted FrameForm -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted FrameForm]
ax_list)]

instance Pretty FrameForm where
  pretty :: FrameForm -> Doc
pretty (FrameForm l :: [VAR_DECL]
l f :: [Annoted (FORMULA EM_FORMULA)]
f _) = case [Annoted (FORMULA EM_FORMULA)]
f of
        [] -> String -> Doc
topSigKey (String
varS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [VAR_DECL] -> String
forall a. ListCheck a => a -> String
pluralS [VAR_DECL]
l) Doc -> Doc -> Doc
<+> [VAR_DECL] -> Doc
printVarDecls [VAR_DECL]
l
        [s :: Annoted (FORMULA EM_FORMULA)
s] | [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
l -> Annoted (FORMULA EM_FORMULA) -> Doc
forall a. Pretty a => a -> Doc
pretty Annoted (FORMULA EM_FORMULA)
s
        _ | [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
l -> [Annoted (FORMULA EM_FORMULA)] -> Doc
forall f. FormExtension f => [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas [Annoted (FORMULA EM_FORMULA)]
f
        _ -> [Doc] -> Doc
fsep [[Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
forallDoc Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [VAR_DECL] -> [Doc]
printVarDeclL [VAR_DECL]
l
                  , [Annoted (FORMULA EM_FORMULA)] -> Doc
forall f. FormExtension f => [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas [Annoted (FORMULA EM_FORMULA)]
f]

instance Pretty EM_BASIC_ITEM where
  pretty :: EM_BASIC_ITEM -> Doc
pretty itm :: EM_BASIC_ITEM
itm = case EM_BASIC_ITEM
itm of
    ModItem md :: ModDefn
md -> ModDefn -> Doc
forall a. Pretty a => a -> Doc
pretty ModDefn
md
    Nominal_decl id_list :: [Annoted SIMPLE_ID]
id_list _ -> [Doc] -> Doc
sep [String -> Doc
keyword String
nominalS, (SIMPLE_ID -> Doc) -> [Annoted SIMPLE_ID] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos SIMPLE_ID -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted SIMPLE_ID]
id_list]

modPrec :: MODALITY -> Int
modPrec :: MODALITY -> Int
modPrec m :: MODALITY
m = case MODALITY
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 :: Bool -> MODALITY -> MODALITY -> Doc
printMPrec b :: Bool
b oP :: MODALITY
oP cP :: MODALITY
cP =
  (if (if Bool
b then Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(>) else Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(>=)) (MODALITY -> Int
modPrec MODALITY
oP) (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ MODALITY -> Int
modPrec MODALITY
cP then Doc -> Doc
forall a. a -> a
id else Doc -> Doc
parens)
  (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ MODALITY -> Doc
forall a. Pretty a => a -> Doc
pretty MODALITY
cP

instance Pretty MODALITY where
        pretty :: MODALITY -> Doc
pretty mdl :: MODALITY
mdl = case MODALITY
mdl of
          SimpleMod idt :: SIMPLE_ID
idt ->
            if SIMPLE_ID -> String
tokStr SIMPLE_ID
idt String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
emptyS then Doc
empty else SIMPLE_ID -> Doc
forall a. Pretty a => a -> Doc
pretty SIMPLE_ID
idt
          TermMod t :: TERM EM_FORMULA
t -> TERM EM_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty TERM EM_FORMULA
t
          Guard sen :: FORMULA EM_FORMULA
sen -> FORMULA EM_FORMULA -> Doc
prJunct FORMULA EM_FORMULA
sen Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
keyword String
quMark
          TransClos md :: MODALITY
md -> Bool -> MODALITY -> MODALITY -> Doc
printMPrec Bool
False MODALITY
mdl MODALITY
md
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
keyword String
tmTransClosS
          ModOp o :: ModOp
o md1 :: MODALITY
md1 md2 :: MODALITY
md2 -> [Doc] -> Doc
fsep [Bool -> MODALITY -> MODALITY -> Doc
printMPrec Bool
True MODALITY
mdl MODALITY
md1
            , String -> Doc
keyword (ModOp -> String
forall a. Show a => a -> String
show ModOp
o) Doc -> Doc -> Doc
<+> Bool -> MODALITY -> MODALITY -> Doc
printMPrec Bool
False MODALITY
mdl MODALITY
md2]

prettyRigor :: Bool -> Doc
prettyRigor :: Bool -> Doc
prettyRigor b :: Bool
b = String -> Doc
keyword (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ if Bool
b then String
rigidS else String
flexibleS

instance Pretty EM_SIG_ITEM where
        pretty :: EM_SIG_ITEM -> Doc
pretty (Rigid_op_items rig :: Bool
rig op_list :: [Annoted (OP_ITEM EM_FORMULA)]
op_list _) =
                [Doc] -> Doc
fsep [Bool -> Doc
prettyRigor Bool
rig Doc -> Doc -> Doc
<+> String -> Doc
keyword (String
opS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted (OP_ITEM EM_FORMULA)] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted (OP_ITEM EM_FORMULA)]
op_list),
                     (OP_ITEM EM_FORMULA -> Doc)
-> [Annoted (OP_ITEM EM_FORMULA)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos OP_ITEM EM_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted (OP_ITEM EM_FORMULA)]
op_list]
        pretty (Rigid_pred_items rig :: Bool
rig pred_list :: [Annoted (PRED_ITEM EM_FORMULA)]
pred_list _) =
                [Doc] -> Doc
fsep [Bool -> Doc
prettyRigor Bool
rig Doc -> Doc -> Doc
<+> String -> Doc
keyword (String
predS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted (PRED_ITEM EM_FORMULA)] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted (PRED_ITEM EM_FORMULA)]
pred_list),
                     (PRED_ITEM EM_FORMULA -> Doc)
-> [Annoted (PRED_ITEM EM_FORMULA)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos PRED_ITEM EM_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted (PRED_ITEM EM_FORMULA)]
pred_list]

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

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

prJunct :: FORMULA EM_FORMULA -> Doc
prJunct :: FORMULA EM_FORMULA -> Doc
prJunct f :: FORMULA EM_FORMULA
f = (if FORMULA EM_FORMULA -> Bool
isEMJunct FORMULA EM_FORMULA
f then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FORMULA EM_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty FORMULA EM_FORMULA
f

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

instance Pretty EM_FORMULA where
  pretty :: EM_FORMULA -> Doc
pretty ef :: EM_FORMULA
ef = case EM_FORMULA
ef of
    PrefixForm p :: FormPrefix
p s :: FORMULA EM_FORMULA
s _ -> (case FormPrefix
p of
      BoxOrDiamond _ m :: MODALITY
m _ _ -> case MODALITY
m of
        SimpleMod _ -> [Doc] -> Doc
hsep
        _ -> [Doc] -> Doc
sep
      _ -> [Doc] -> Doc
hsep) [FormPrefix -> Doc
forall a. Pretty a => a -> Doc
pretty FormPrefix
p, FORMULA EM_FORMULA -> Doc
prJunct FORMULA EM_FORMULA
s]
    UntilSince choice :: Bool
choice s1 :: FORMULA EM_FORMULA
s1 s2 :: FORMULA EM_FORMULA
s2 _ -> Bool -> ([Doc] -> Doc) -> Doc -> Doc -> Doc -> Doc
printInfix Bool
True [Doc] -> Doc
sep (FORMULA EM_FORMULA -> Doc
prJunct FORMULA EM_FORMULA
s1)
      (String -> Doc
keyword (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ if Bool
choice then String
untilS else String
sinceS)
      (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FORMULA EM_FORMULA -> Doc
prJunct FORMULA EM_FORMULA
s2
    ModForm md :: ModDefn
md -> ModDefn -> Doc
forall a. Pretty a => a -> Doc
pretty ModDefn
md

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