{- |
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