hets/Syntax/Print_AS_Structured.hs

{- |
Module      :  ./Syntax/Print_AS_Structured.hs
Description :  pretty printing of CASL structured 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 structured specifications
-}

module Syntax.Print_AS_Structured
    ( structIRI
    , printGroupSpec
    , skipVoidGroup
    , printUnion
    , printExtension
    , moveAnnos
    , PrettyLG (..)
    ) where

import Common.Id
import Common.IRI
import Common.Keywords
import Common.Doc
import Common.DocUtils
import Common.AS_Annotation

import Logic.Grothendieck
import Logic.Logic

import Syntax.AS_Structured

sublogicId :: SIMPLE_ID -> Doc
sublogicId = structId . tokStr

structIRI :: IRI -> Doc
structIRI = structId . iriToStringShortUnsecure -- also print user information

class PrettyLG a where
  prettyLG :: LogicGraph -> a -> Doc

instance PrettyLG a => PrettyLG (Annoted a) where
    prettyLG lg = printAnnoted $ prettyLG lg

instance PrettyLG SPEC where
    prettyLG = printSPEC

printUnion :: LogicGraph -> [Annoted SPEC] -> [Doc]
printUnion lg = prepPunctuate (topKey andS <> space) . map (condBracesAnd lg)

printIntersection :: LogicGraph -> [Annoted SPEC] -> [Doc]
printIntersection lg = prepPunctuate (topKey intersectS <> space) . map (condBracesAnd lg)

moveAnnos :: Annoted SPEC -> [Annoted SPEC] -> [Annoted SPEC]
moveAnnos x l = appAnno $ case l of
    [] -> error "moveAnnos"
    h : r -> h { l_annos = l_annos x ++ l_annos h } : r
    where appAnno a = case a of
                 [] -> []
                 [h] -> [appendAnno h (r_annos x)]
                 h : r -> h : appAnno r

printOptUnion :: LogicGraph -> Annoted SPEC -> [Doc]
printOptUnion lg x = case skipVoidGroup $ item x of
        Union e@(_ : _) _ -> printUnion lg $ moveAnnos x e
        Extension e@(_ : _) _ -> printExtension lg $ moveAnnos x e
        _ -> [prettyLG lg x]

printExtension :: LogicGraph -> [Annoted SPEC] -> [Doc]
printExtension lg l = case l of
    [] -> []
    x : r -> printOptUnion lg x ++
             concatMap ((\ u -> case u of
                            [] -> []
                            d : s -> (topKey thenS <+> d) : s) .
                        printOptUnion lg) r

printSPEC :: LogicGraph -> SPEC -> Doc
printSPEC lg spec = case spec of
    Basic_spec (G_basic_spec lid basic_spec) _ ->
        case lookupCurrentSyntax "" lg of
      Just (Logic lid2, sm) -> if language_name lid2 /= language_name lid
          then error "printSPEC: logic mismatch"
          else case basicSpecPrinter sm lid of
        Just p -> p basic_spec
        _ -> error $ "printSPEC: no basic spec printer for "
             ++ showSyntax lid sm
      _ -> error "printSPEC: incomplete logic graph"
    EmptySpec _ -> specBraces empty
    Extraction aa ab -> sep [condBracesTransReduct lg aa, printEXTRACTION ab]
    Translation aa ab -> sep [condBracesTransReduct lg aa, printRENAMING ab]
    Reduction aa ab -> sep [condBracesTransReduct lg aa, printRESTRICTION ab]
    Approximation aa ab ->
      sep [condBracesTransReduct lg aa, printAPPROXIMATION ab]
    Minimization aa ab ->
      sep [condBracesTransReduct lg aa, printMINIMIZATION ab]
    Filtering aa ab -> sep [condBracesTransReduct lg aa, printFILTERING ab]
    Union aa _ -> sep $ printUnion lg aa
    Intersection aa _ -> sep $ printIntersection lg aa
    Extension aa _ -> sep $ printExtension lg aa
    Free_spec aa _ -> sep [keyword freeS, printGroupSpec lg aa]
    Cofree_spec aa _ -> sep [keyword cofreeS, printGroupSpec lg aa]
    Minimize_spec aa _ -> sep [keyword minimizeS, printGroupSpec lg aa]
    Local_spec aa ab _ -> fsep
      [keyword localS, prettyLG lg aa, keyword withinS, condBracesWithin lg ab]
    Closed_spec aa _ -> sep [keyword closedS, printGroupSpec lg aa]
    Group aa _ -> prettyLG lg aa
    Spec_inst aa ab mi _ -> let
      r = cat [structIRI aa, print_fit_arg_list lg ab]
      in maybe r (\ i -> sep [r, pretty i]) mi
    Qualified_spec ln asp _ -> pretty ln <> colon
      $+$ prettyLG (setLogicName ln lg) asp
    Data ld _ s1 s2 _ -> keyword dataS
        <+> printGroupSpec (setCurLogic (show ld) lg) s1
        $+$ prettyLG lg s2
    Combination n _ -> sep [keyword combineS, pretty n]
    Apply i bs _ ->
      sep [keyword "apply" <+> pretty i, prettyLG lg $ Basic_spec bs nullRange]
    Bridge s1 rs s2 _ -> fsep $ [condBraces lg s1, keyword "bridge"]
      ++ map pretty rs ++ [condBraces lg s2]

instance Pretty Network where
    pretty (Network cs es _) = fsep $ ppWithCommas cs
      : if null es then [] else [keyword excludingS, ppWithCommas es]

instance Pretty FILTERING where
    pretty = printFILTERING

printFILTERING :: FILTERING -> Doc
printFILTERING (FilterBasicSpec b aa _) =
   keyword (if b then selectS else rejectS) <+> pretty aa
printFILTERING (FilterSymbolList b aa _) =
   keyword (if b then selectS else rejectS) <+> pretty aa

instance Pretty MINIMIZATION where
    pretty = printMINIMIZATION

printMINIMIZATION :: MINIMIZATION -> Doc
printMINIMIZATION (Mini kw cms cvs _) =
   fsep $ keyword (tokStr kw) : map pretty cms ++ if null cvs then [] else
     keyword "vars" : map pretty cvs

instance Pretty APPROXIMATION where
    pretty = printAPPROXIMATION

printAPPROXIMATION :: APPROXIMATION -> Doc
printAPPROXIMATION (ForgetOrKeep b syms ml _) =
   fsep $ keyword (if b then forgetS else keepS)
   : ppWithCommas syms : maybe [] (\ i -> [keyword withS, pretty i]) ml

instance Pretty EXTRACTION where
    pretty = printEXTRACTION

printEXTRACTION :: EXTRACTION -> Doc
printEXTRACTION (ExtractOrRemove b aa _) =
   keyword (if b then "extract" else "remove") <+> fsep (map pretty aa)

instance Pretty RENAMING where
    pretty = printRENAMING

printRENAMING :: RENAMING -> Doc
printRENAMING (Renaming aa _) =
   keyword withS <+> ppWithCommas aa

instance Pretty RESTRICTION where
    pretty = printRESTRICTION

printRESTRICTION :: RESTRICTION -> Doc
printRESTRICTION rest = case rest of
    Hidden aa _ -> keyword hideS <+> ppWithCommas aa
    Revealed aa _ -> keyword revealS <+> pretty aa

printLogicEncoding :: (Pretty a) => a -> Doc
printLogicEncoding enc = keyword logicS <+> pretty enc

instance Pretty G_mapping where
    pretty = printG_mapping

printG_mapping :: G_mapping -> Doc
printG_mapping gma = case gma of
    G_symb_map gsmil -> pretty gsmil
    G_logic_translation enc -> printLogicEncoding enc

instance Pretty G_hiding where
    pretty = printG_hiding

printG_hiding :: G_hiding -> Doc
printG_hiding ghid = case ghid of
    G_symb_list gsil -> pretty gsil
    G_logic_projection enc -> printLogicEncoding enc

instance PrettyLG FIT_ARG where
    prettyLG = printFIT_ARG

printFIT_ARG :: LogicGraph -> FIT_ARG -> Doc
printFIT_ARG lg fit = case fit of
    Fit_spec aa ab _ ->
        let aa' = rmTopKey $ prettyLG lg aa
        in if null ab then aa' else
               fsep $ aa' : keyword fitS
                        : punctuate comma (map printG_mapping ab)
    Fit_view si ab _ ->
        sep [keyword viewS, cat [structIRI si, print_fit_arg_list lg ab]]

instance Pretty Logic_code where
    pretty = printLogic_code

printLogic_code :: Logic_code -> Doc
printLogic_code (Logic_code menc msrc mtar _) =
   let pm = maybe [] ((: []) . printLogic_name) in
   fsep $ maybe [] ((: [colon]) . pretty) menc
        ++ pm msrc ++ funArrow : pm mtar

instance Pretty LogicDescr where
    pretty ld = case ld of
      LogicDescr n s _ -> sep [keyword logicS, pretty n,
        maybe empty (\ r -> sep [keyword serializationS, pretty r]) s]
      SyntaxQual i -> sep [keyword serializationS, pretty i]
      LanguageQual i -> sep [keyword "language", pretty i]

instance Pretty Logic_name where
    pretty = printLogic_name

printLogic_name :: Logic_name -> Doc
printLogic_name (Logic_name mlog slog ms) = let d = structId mlog in
    case slog of
      Nothing -> d
      Just sub -> d <> dot <> sublogicId sub
    <> maybe empty (parens . pretty) ms

instance Pretty LABELED_ONTO_OR_INTPR_REF where
    pretty = printLIRI

printLIRI :: LABELED_ONTO_OR_INTPR_REF -> Doc
printLIRI (Labeled n i) = case n of
    Just x -> pretty x <+> colon <+> pretty i
    Nothing -> pretty i

{- |
  specialized printing of 'FIT_ARG's
-}
print_fit_arg_list :: LogicGraph -> [Annoted FIT_ARG] -> Doc
print_fit_arg_list lg = cat . map (brackets . prettyLG lg)

{- |
   conditional generation of grouping braces for Union and Extension
-}
printGroupSpec :: LogicGraph -> Annoted SPEC -> Doc
printGroupSpec lg s = let d = prettyLG lg s in
    case skip_Group $ item s of
                 Spec_inst {} -> d
                 _ -> specBraces d

{- |
  generate grouping braces for Tanslations and Reductions
-}
condBracesTransReduct :: LogicGraph -> Annoted SPEC -> Doc
condBracesTransReduct lg s = let d = prettyLG lg s in
    case skip_Group $ item s of
                 Bridge {} -> specBraces d
                 Extension {} -> specBraces d
                 Union {} -> specBraces d
                 Intersection {} -> specBraces d
                 Local_spec {} -> specBraces d
                 _ -> d

{- |
  generate grouping braces for Within
-}
condBracesWithin :: LogicGraph -> Annoted SPEC -> Doc
condBracesWithin lg s = let d = prettyLG lg s in
    case skip_Group $ item s of
                 Bridge {} -> specBraces d
                 Extension {} -> specBraces d
                 Union {} -> specBraces d
                 Intersection {} -> specBraces d
                 _ -> d
{- |
  only Extensions inside of Unions (and) need grouping braces
-}
condBracesAnd :: LogicGraph -> Annoted SPEC -> Doc
condBracesAnd lg s = let d = prettyLG lg s in
    case skip_Group $ item s of
                 Bridge {} -> specBraces d
                 Extension {} -> specBraces d
                 _ -> d

-- bridges inside bridges need grouping
condBraces :: LogicGraph -> Annoted SPEC -> Doc
condBraces lg s = let d = prettyLG lg s in
    case skip_Group $ item s of
                 Bridge {} -> specBraces d
                 _ -> d

-- | only skip groups without annotations
skipVoidGroup :: SPEC -> SPEC
skipVoidGroup sp =
    case sp of
            Group g _ | null (l_annos g) && null (r_annos g)
                          -> skipVoidGroup $ item g
            _ -> sp

-- | skip nested groups
skip_Group :: SPEC -> SPEC
skip_Group sp =
    case sp of
            Group g _ -> skip_Group $ item g
            _ -> sp