{- |
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 :: (FORMULA f -> FORMULA f) -> [[Annoted (FORMULA f)]] -> Doc
printFormulaOfHybridSign sim :: FORMULA f -> FORMULA f
sim = (FORMULA f -> Doc) -> [Annoted (FORMULA f)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos (FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty (FORMULA f -> Doc) -> (FORMULA f -> FORMULA f) -> FORMULA f -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> FORMULA f
sim) ([Annoted (FORMULA f)] -> Doc)
-> ([[Annoted (FORMULA f)]] -> [Annoted (FORMULA f)])
-> [[Annoted (FORMULA f)]]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Annoted (FORMULA f)]] -> [Annoted (FORMULA f)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

instance Pretty H_BASIC_ITEM where
    pretty :: H_BASIC_ITEM -> Doc
pretty (Simple_mod_decl is :: [Annoted SIMPLE_ID]
is fs :: [AnHybFORM]
fs _) =
        [Doc] -> Doc
cat [String -> Doc
keyword String
modalityS Doc -> Doc -> Doc
<+> (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]
is
            , Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
specBraces ((FORMULA H_FORMULA -> Doc) -> [AnHybFORM] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos FORMULA H_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [AnHybFORM]
fs)]
    pretty (Term_mod_decl ss :: [Annoted SORT]
ss fs :: [AnHybFORM]
fs _) =
        [Doc] -> Doc
cat [String -> Doc
keyword String
termS Doc -> Doc -> Doc
<+> String -> Doc
keyword String
modalityS Doc -> Doc -> Doc
<+> (SORT -> Doc) -> [Annoted SORT] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos SORT -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted SORT]
ss
            , Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
specBraces ((FORMULA H_FORMULA -> Doc) -> [AnHybFORM] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos FORMULA H_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [AnHybFORM]
fs)]
    pretty (Simple_nom_decl is :: [Annoted SIMPLE_ID]
is fs :: [AnHybFORM]
fs _) =
        [Doc] -> Doc
cat [String -> Doc
keyword String
nominalS Doc -> Doc -> Doc
<+> (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]
is
            , Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
specBraces ((FORMULA H_FORMULA -> Doc) -> [AnHybFORM] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos FORMULA H_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [AnHybFORM]
fs)]

instance Pretty RIGOR where
    pretty :: RIGOR -> Doc
pretty Rigid = String -> Doc
keyword String
rigidS
    pretty Flexible = String -> Doc
keyword String
flexibleS

instance Pretty H_SIG_ITEM where
    pretty :: H_SIG_ITEM -> Doc
pretty (Rigid_op_items r :: RIGOR
r ls :: [Annoted (OP_ITEM H_FORMULA)]
ls _) =
        [Doc] -> Doc
cat [RIGOR -> Doc
forall a. Pretty a => a -> Doc
pretty RIGOR
r Doc -> Doc -> Doc
<+> String -> Doc
keyword (String
opS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted (OP_ITEM H_FORMULA)] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted (OP_ITEM H_FORMULA)]
ls),
             Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (OP_ITEM H_FORMULA -> Doc) -> [Annoted (OP_ITEM H_FORMULA)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos OP_ITEM H_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted (OP_ITEM H_FORMULA)]
ls]
    pretty (Rigid_pred_items r :: RIGOR
r ls :: [Annoted (PRED_ITEM H_FORMULA)]
ls _) =
        [Doc] -> Doc
cat [RIGOR -> Doc
forall a. Pretty a => a -> Doc
pretty RIGOR
r Doc -> Doc -> Doc
<+> String -> Doc
keyword (String
predS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted (PRED_ITEM H_FORMULA)] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted (PRED_ITEM H_FORMULA)]
ls),
             Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (PRED_ITEM H_FORMULA -> Doc)
-> [Annoted (PRED_ITEM H_FORMULA)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos PRED_ITEM H_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted (PRED_ITEM H_FORMULA)]
ls]

instance Pretty H_FORMULA where
    pretty :: H_FORMULA -> Doc
pretty (BoxOrDiamond b :: Bool
b t :: MODALITY
t f :: FORMULA H_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
forall a. Pretty a => a -> Doc
pretty MODALITY
t
        in [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (if Bool
b then Doc -> Doc
brackets Doc
td
                  else Doc
less Doc -> Doc -> Doc
`sp` Doc
td Doc -> Doc -> Doc
`sp` Doc
greater)
               Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [(FORMULA H_FORMULA -> Doc)
-> (Doc -> Doc) -> FORMULA H_FORMULA -> Doc
forall f.
Pretty f =>
(FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc
condParensInnerF FORMULA H_FORMULA -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula Doc -> Doc
parens FORMULA H_FORMULA
f]
    pretty (At n :: NOMINAL
n f :: FORMULA H_FORMULA
f _) =
        let sp :: Doc -> Doc -> Doc
sp = Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>)
            td :: Doc
td = NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n
        in [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
prettyAt Doc -> Doc -> Doc
`sp` Doc
td) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [(FORMULA H_FORMULA -> Doc)
-> (Doc -> Doc) -> FORMULA H_FORMULA -> Doc
forall f.
Pretty f =>
(FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc
condParensInnerF FORMULA H_FORMULA -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula Doc -> Doc
parens FORMULA H_FORMULA
f]
    pretty (Univ n :: NOMINAL
n f :: FORMULA H_FORMULA
f _) =
        let sp :: Doc -> Doc -> Doc
sp = Doc -> Doc -> Doc
(<+>)
            td :: Doc
td = NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n
        in [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
prettyUniv Doc -> Doc -> Doc
`sp` Doc
td) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [(FORMULA H_FORMULA -> Doc)
-> (Doc -> Doc) -> FORMULA H_FORMULA -> Doc
forall f.
Pretty f =>
(FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc
condParensInnerF FORMULA H_FORMULA -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula Doc -> Doc
parens FORMULA H_FORMULA
f]
    pretty (Exist n :: NOMINAL
n f :: FORMULA H_FORMULA
f _) =
        let sp :: Doc -> Doc -> Doc
sp = Doc -> Doc -> Doc
(<+>)
            td :: Doc
td = NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n
        in [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
prettyExist Doc -> Doc -> Doc
`sp` Doc
td) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                  [(FORMULA H_FORMULA -> Doc)
-> (Doc -> Doc) -> FORMULA H_FORMULA -> Doc
forall f.
Pretty f =>
(FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc
condParensInnerF FORMULA H_FORMULA -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula Doc -> Doc
parens FORMULA H_FORMULA
f]
    pretty (Here n :: NOMINAL
n _) =
        let sp :: Doc -> Doc -> Doc
sp = Doc -> Doc -> Doc
(<+>)
            td :: Doc
td = NOMINAL -> Doc
forall a. Pretty a => a -> Doc
pretty NOMINAL
n
        in [Doc] -> Doc
sep [Doc
prettyHere Doc -> Doc -> Doc
`sp` Doc
td]

instance FormExtension H_FORMULA where
  isQuantifierLike :: H_FORMULA -> Bool
isQuantifierLike _ = Bool
False

instance Pretty MODALITY where
    pretty :: MODALITY -> Doc
pretty (Simple_mod ident :: SIMPLE_ID
ident) =
        if SIMPLE_ID -> String
tokStr SIMPLE_ID
ident 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
ident
    pretty (Term_mod t :: TERM H_FORMULA
t) = TERM H_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty TERM H_FORMULA
t

instance Pretty NOMINAL where
    pretty :: NOMINAL -> Doc
pretty (Simple_nom i :: SIMPLE_ID
i) =
        if SIMPLE_ID -> String
tokStr SIMPLE_ID
i 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
i

instance Pretty HybridSign where
    pretty :: HybridSign -> Doc
pretty = (FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc
printHybridSign FORMULA H_FORMULA -> FORMULA H_FORMULA
forall a. a -> a
id

printHybridSign :: (FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc
printHybridSign :: (FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc
printHybridSign sim :: FORMULA H_FORMULA -> FORMULA H_FORMULA
sim s :: HybridSign
s =
    let ms :: Map SIMPLE_ID [AnHybFORM]
ms = HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
s
        tms :: Map SORT [AnHybFORM]
tms = HybridSign -> Map SORT [AnHybFORM]
termModies HybridSign
s
        ns :: Map SIMPLE_ID [AnHybFORM]
ns = HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
s in
    Doc -> Doc -> Map SORT (Set OpType) -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap (String -> Doc
keyword String
rigidS Doc -> Doc -> Doc
<+> String -> Doc
keyword String
opS) Doc
empty
                (MapSet SORT OpType -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet SORT OpType -> Map SORT (Set OpType))
-> MapSet SORT OpType -> Map SORT (Set OpType)
forall a b. (a -> b) -> a -> b
$ HybridSign -> MapSet SORT OpType
rigidOps HybridSign
s)
    Doc -> Doc -> Doc
$+$ Doc -> Doc -> Map SORT (Set PredType) -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap (String -> Doc
keyword String
rigidS Doc -> Doc -> Doc
<+> String -> Doc
keyword String
predS) Doc
space
        (MapSet SORT PredType -> Map SORT (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet SORT PredType -> Map SORT (Set PredType))
-> MapSet SORT PredType -> Map SORT (Set PredType)
forall a b. (a -> b) -> a -> b
$ HybridSign -> MapSet SORT PredType
rigidPreds HybridSign
s)
    Doc -> Doc -> Doc
$+$ (if Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a. Map k a -> Bool
Map.null Map SIMPLE_ID [AnHybFORM]
ms then Doc
empty else
        [Doc] -> Doc
cat [String -> Doc
keyword String
modalitiesS Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepBySemis ((SIMPLE_ID -> Doc) -> [SIMPLE_ID] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> Doc
sidDoc ([SIMPLE_ID] -> [Doc]) -> [SIMPLE_ID] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID]
forall k a. Map k a -> [k]
Map.keys Map SIMPLE_ID [AnHybFORM]
ms)
            , Doc -> Doc
specBraces ((FORMULA H_FORMULA -> FORMULA H_FORMULA) -> [[AnHybFORM]] -> Doc
forall f.
FormExtension f =>
(FORMULA f -> FORMULA f) -> [[Annoted (FORMULA f)]] -> Doc
printFormulaOfHybridSign FORMULA H_FORMULA -> FORMULA H_FORMULA
sim ([[AnHybFORM]] -> Doc) -> [[AnHybFORM]] -> Doc
forall a b. (a -> b) -> a -> b
$ Map SIMPLE_ID [AnHybFORM] -> [[AnHybFORM]]
forall k a. Map k a -> [a]
Map.elems Map SIMPLE_ID [AnHybFORM]
ms)])
    Doc -> Doc -> Doc
$+$ (if Map SORT [AnHybFORM] -> Bool
forall k a. Map k a -> Bool
Map.null Map SORT [AnHybFORM]
tms then Doc
empty else
        [Doc] -> Doc
cat [String -> Doc
keyword String
termS Doc -> Doc -> Doc
<+> String -> Doc
keyword String
modalityS Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepBySemis
                ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc ([SORT] -> [Doc]) -> [SORT] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map SORT [AnHybFORM] -> [SORT]
forall k a. Map k a -> [k]
Map.keys Map SORT [AnHybFORM]
tms)
            , Doc -> Doc
specBraces ((FORMULA H_FORMULA -> FORMULA H_FORMULA) -> [[AnHybFORM]] -> Doc
forall f.
FormExtension f =>
(FORMULA f -> FORMULA f) -> [[Annoted (FORMULA f)]] -> Doc
printFormulaOfHybridSign FORMULA H_FORMULA -> FORMULA H_FORMULA
sim ([[AnHybFORM]] -> Doc) -> [[AnHybFORM]] -> Doc
forall a b. (a -> b) -> a -> b
$ Map SORT [AnHybFORM] -> [[AnHybFORM]]
forall k a. Map k a -> [a]
Map.elems Map SORT [AnHybFORM]
tms)])
    Doc -> Doc -> Doc
$+$ (if Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a. Map k a -> Bool
Map.null Map SIMPLE_ID [AnHybFORM]
ns then Doc
empty else
        [Doc] -> Doc
cat [String -> Doc
keyword String
nominalsS Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepBySemis ((SIMPLE_ID -> Doc) -> [SIMPLE_ID] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> Doc
sidDoc ([SIMPLE_ID] -> [Doc]) -> [SIMPLE_ID] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID]
forall k a. Map k a -> [k]
Map.keys Map SIMPLE_ID [AnHybFORM]
ns)
            , Doc -> Doc
specBraces ((FORMULA H_FORMULA -> FORMULA H_FORMULA) -> [[AnHybFORM]] -> Doc
forall f.
FormExtension f =>
(FORMULA f -> FORMULA f) -> [[Annoted (FORMULA f)]] -> Doc
printFormulaOfHybridSign FORMULA H_FORMULA -> FORMULA H_FORMULA
sim ([[AnHybFORM]] -> Doc) -> [[AnHybFORM]] -> Doc
forall a b. (a -> b) -> a -> b
$ Map SIMPLE_ID [AnHybFORM] -> [[AnHybFORM]]
forall k a. Map k a -> [a]
Map.elems Map SIMPLE_ID [AnHybFORM]
ns)])

condParensInnerF :: Pretty f => (FORMULA f -> Doc)
                    -> (Doc -> Doc)    {- ^ a function that surrounds
                                       the given Doc with appropiate parens -}
                    -> FORMULA f -> Doc
condParensInnerF :: (FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc
condParensInnerF pf :: FORMULA f -> Doc
pf parens_fun :: Doc -> Doc
parens_fun f :: FORMULA f
f =
    case FORMULA f
f of
    Quantification {} -> Doc
f'
    Atom {} -> Doc
f'
    Predication {} -> Doc
f'
    Definedness {} -> Doc
f'
    Membership {} -> Doc
f'
    ExtFORMULA _ -> Doc
f'
    _ -> Doc -> Doc
parens_fun Doc
f'
    where f' :: Doc
f' = FORMULA f -> Doc
pf FORMULA f
f