{- |
Module      :  ./Syntax/Print_AS_Architecture.hs
Description :  pretty printing of CASL architectural specifications
Copyright   :  (c) Klaus Luettich, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Grothendieck)

Pretty printing of CASL architectural specifications
-}

module Syntax.Print_AS_Architecture () where

import Common.Doc
import Common.DocUtils
import Common.Keywords

import Syntax.AS_Architecture
import Syntax.Print_AS_Structured

sp1 :: Doc
sp1 :: Doc
sp1 = String -> Doc
keyword " "

instance PrettyLG ARCH_SPEC where
    prettyLG :: LogicGraph -> ARCH_SPEC -> Doc
prettyLG lg :: LogicGraph
lg a :: ARCH_SPEC
a = case ARCH_SPEC
a of
        Basic_arch_spec aa :: [Annoted UNIT_DECL_DEFN]
aa ab :: Annoted UNIT_EXPRESSION
ab _ -> [Doc] -> Doc
sep [String -> Doc
keyword (String
unitS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS)
                Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Annoted UNIT_DECL_DEFN -> Doc)
-> [Annoted UNIT_DECL_DEFN] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> Annoted UNIT_DECL_DEFN -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg) [Annoted UNIT_DECL_DEFN]
aa)
               , String -> Doc
keyword String
resultS Doc -> Doc -> Doc
<+> LogicGraph -> Annoted UNIT_EXPRESSION -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_EXPRESSION
ab]
        Arch_spec_name aa :: ARCH_SPEC_NAME
aa -> ARCH_SPEC_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty ARCH_SPEC_NAME
aa
        Group_arch_spec aa :: Annoted ARCH_SPEC
aa _ -> Doc -> Doc
specBraces (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
rmTopKey (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Annoted ARCH_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted ARCH_SPEC
aa

instance PrettyLG UNIT_REF where
    prettyLG :: LogicGraph -> UNIT_REF -> Doc
prettyLG lg :: LogicGraph
lg (Unit_ref aa :: ARCH_SPEC_NAME
aa ab :: REF_SPEC
ab _) =
        [Doc] -> Doc
fsep [ARCH_SPEC_NAME -> Doc
structIRI ARCH_SPEC_NAME
aa, String -> Doc
keyword String
toS, LogicGraph -> REF_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg REF_SPEC
ab]

instance PrettyLG UNIT_DECL_DEFN where
    prettyLG :: LogicGraph -> UNIT_DECL_DEFN -> Doc
prettyLG lg :: LogicGraph
lg ud :: UNIT_DECL_DEFN
ud = case UNIT_DECL_DEFN
ud of
        Unit_decl aa :: ARCH_SPEC_NAME
aa ab :: REF_SPEC
ab ac :: [Annoted UNIT_TERM]
ac _ -> [Doc] -> Doc
cat [ARCH_SPEC_NAME -> Doc
structIRI ARCH_SPEC_NAME
aa Doc -> Doc -> Doc
<+> Doc
colon,
            Doc
sp1 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
fsep (LogicGraph -> REF_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg REF_SPEC
ab Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                 if [Annoted UNIT_TERM] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted UNIT_TERM]
ac then [] else
                     String -> Doc
keyword String
givenS Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((Annoted UNIT_TERM -> Doc) -> [Annoted UNIT_TERM] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg) [Annoted UNIT_TERM]
ac))]
        Unit_defn aa :: ARCH_SPEC_NAME
aa ab :: UNIT_EXPRESSION
ab _ ->
            [Doc] -> Doc
cat [ARCH_SPEC_NAME -> Doc
structIRI ARCH_SPEC_NAME
aa Doc -> Doc -> Doc
<+> Doc
equals, Doc
sp1 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> LogicGraph -> UNIT_EXPRESSION -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg UNIT_EXPRESSION
ab]

instance PrettyLG UNIT_SPEC where
    prettyLG :: LogicGraph -> UNIT_SPEC -> Doc
prettyLG lg :: LogicGraph
lg u :: UNIT_SPEC
u = case UNIT_SPEC
u of
        Unit_type aa :: [Annoted SPEC]
aa ab :: Annoted SPEC
ab _ ->
          let ab' :: Doc
ab' = Doc -> Doc
rmTopKey (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Annoted SPEC -> Doc
printGroupSpec LogicGraph
lg Annoted SPEC
ab
          in if [Annoted SPEC] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted SPEC]
aa then Doc
ab' else [Doc] -> Doc
sep
               [ [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
cross)
                          ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted SPEC -> Doc) -> [Annoted SPEC] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
rmTopKey (Doc -> Doc) -> (Annoted SPEC -> Doc) -> Annoted SPEC -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicGraph -> Annoted SPEC -> Doc
printGroupSpec LogicGraph
lg) [Annoted SPEC]
aa
               , Doc
funArrow Doc -> Doc -> Doc
<+> Doc
ab']
        Spec_name aa :: ARCH_SPEC_NAME
aa -> ARCH_SPEC_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty ARCH_SPEC_NAME
aa
        Closed_unit_spec aa :: UNIT_SPEC
aa _ -> [Doc] -> Doc
fsep [String -> Doc
keyword String
closedS, LogicGraph -> UNIT_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg UNIT_SPEC
aa]

instance PrettyLG REF_SPEC where
    prettyLG :: LogicGraph -> REF_SPEC -> Doc
prettyLG lg :: LogicGraph
lg rs :: REF_SPEC
rs = case REF_SPEC
rs of
        Unit_spec u :: UNIT_SPEC
u -> LogicGraph -> UNIT_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg UNIT_SPEC
u
        Refinement b :: Bool
b u :: UNIT_SPEC
u m :: [G_mapping]
m r :: REF_SPEC
r _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
            LogicGraph -> UNIT_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg UNIT_SPEC
u Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (if Bool
b then [] else [String -> Doc
keyword String
behaviourallyS])
            [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
keyword String
refinedS]
            [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (if [G_mapping] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [G_mapping]
m then [] else String -> Doc
keyword String
viaS Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((G_mapping -> Doc) -> [G_mapping] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map G_mapping -> Doc
forall a. Pretty a => a -> Doc
pretty [G_mapping]
m))
            [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
keyword String
toS, LogicGraph -> REF_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg REF_SPEC
r]
        Arch_unit_spec aa :: Annoted ARCH_SPEC
aa _ ->
            [Doc] -> Doc
fsep [String -> Doc
keyword String
archS Doc -> Doc -> Doc
<+> String -> Doc
keyword String
specS, LogicGraph -> Annoted ARCH_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted ARCH_SPEC
aa]
        Compose_ref aa :: [REF_SPEC]
aa _ -> case [REF_SPEC]
aa of
            [] -> Doc
empty
            x :: REF_SPEC
x : xs :: [REF_SPEC]
xs -> [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ LogicGraph -> REF_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg REF_SPEC
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
               (REF_SPEC -> Doc) -> [REF_SPEC] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ s :: REF_SPEC
s -> String -> Doc
keyword String
thenS Doc -> Doc -> Doc
<+> LogicGraph -> REF_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg REF_SPEC
s) [REF_SPEC]
xs
        Component_ref aa :: [UNIT_REF]
aa _ ->
            Doc -> Doc
specBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (UNIT_REF -> Doc) -> [UNIT_REF] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> UNIT_REF -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg) [UNIT_REF]
aa

instance PrettyLG UNIT_EXPRESSION where
    prettyLG :: LogicGraph -> UNIT_EXPRESSION -> Doc
prettyLG lg :: LogicGraph
lg (Unit_expression aa :: [UNIT_BINDING]
aa ab :: Annoted UNIT_TERM
ab _) =
        let ab' :: Doc
ab' = LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
ab
        in if [UNIT_BINDING] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UNIT_BINDING]
aa then Doc
ab'
           else [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
keyword String
lambdaS Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                    Doc -> [Doc] -> [Doc]
punctuate Doc
semi ((UNIT_BINDING -> Doc) -> [UNIT_BINDING] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> UNIT_BINDING -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg) [UNIT_BINDING]
aa)
                    [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> Doc
addBullet Doc
ab']

instance PrettyLG UNIT_BINDING where
    prettyLG :: LogicGraph -> UNIT_BINDING -> Doc
prettyLG lg :: LogicGraph
lg (Unit_binding aa :: ARCH_SPEC_NAME
aa ab :: UNIT_SPEC
ab _) =
        let aa' :: Doc
aa' = ARCH_SPEC_NAME -> Doc
structIRI ARCH_SPEC_NAME
aa
            ab' :: Doc
ab' = LogicGraph -> UNIT_SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg UNIT_SPEC
ab
        in [Doc] -> Doc
fsep [Doc
aa', Doc
colon, Doc
ab']

instance PrettyLG UNIT_TERM where
    prettyLG :: LogicGraph -> UNIT_TERM -> Doc
prettyLG lg :: LogicGraph
lg ut :: UNIT_TERM
ut = case UNIT_TERM
ut of
        Unit_reduction aa :: Annoted UNIT_TERM
aa ab :: RESTRICTION
ab ->
          let aa' :: Doc
aa' = LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
aa
              ab' :: Doc
ab' = RESTRICTION -> Doc
forall a. Pretty a => a -> Doc
pretty RESTRICTION
ab
          in [Doc] -> Doc
fsep [Doc
aa', Doc
ab']
        Unit_translation aa :: Annoted UNIT_TERM
aa ab :: RENAMING
ab ->
          let aa' :: Doc
aa' = LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
aa
              ab' :: Doc
ab' = RENAMING -> Doc
forall a. Pretty a => a -> Doc
pretty RENAMING
ab
          in [Doc] -> Doc
fsep [Doc
aa', Doc
ab']
        Amalgamation aa :: [Annoted UNIT_TERM]
aa _ -> case [Annoted UNIT_TERM]
aa of
            [] -> Doc
empty
            x :: Annoted UNIT_TERM
x : xs :: [Annoted UNIT_TERM]
xs -> [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
               (Annoted UNIT_TERM -> Doc) -> [Annoted UNIT_TERM] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ s :: Annoted UNIT_TERM
s -> String -> Doc
keyword String
andS Doc -> Doc -> Doc
<+> LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
s) [Annoted UNIT_TERM]
xs
        Local_unit aa :: [Annoted UNIT_DECL_DEFN]
aa ab :: Annoted UNIT_TERM
ab _ ->
            [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
keyword String
localS Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Doc -> [Doc] -> [Doc]
punctuate Doc
semi ((Annoted UNIT_DECL_DEFN -> Doc)
-> [Annoted UNIT_DECL_DEFN] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> Annoted UNIT_DECL_DEFN -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg) [Annoted UNIT_DECL_DEFN]
aa)
                        [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
keyword String
withinS, LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
ab]
        Unit_appl aa :: ARCH_SPEC_NAME
aa ab :: [FIT_ARG_UNIT]
ab _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ARCH_SPEC_NAME -> Doc
structIRI ARCH_SPEC_NAME
aa Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (FIT_ARG_UNIT -> Doc) -> [FIT_ARG_UNIT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> FIT_ARG_UNIT -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg) [FIT_ARG_UNIT]
ab
        Group_unit_term aa :: Annoted UNIT_TERM
aa _ -> Doc -> Doc
specBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
aa

instance PrettyLG FIT_ARG_UNIT where
    prettyLG :: LogicGraph -> FIT_ARG_UNIT -> Doc
prettyLG lg :: LogicGraph
lg (Fit_arg_unit aa :: Annoted UNIT_TERM
aa ab :: [G_mapping]
ab _) = Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg Annoted UNIT_TERM
aa Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: if [G_mapping] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [G_mapping]
ab then []
               else String -> Doc
keyword String
fitS Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((G_mapping -> Doc) -> [G_mapping] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map G_mapping -> Doc
forall a. Pretty a => a -> Doc
pretty [G_mapping]
ab)