c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule : $Header$

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederDescription : pretty printing (parts of) a LibEnv

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) C. Maeder, Uni Bremen 2002-2006

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederMaintainer : Christian.Maeder@dfki.de

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable(DevGraph)

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederpretty printing (parts of) a LibEnv

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule Static.PrintDevGraph

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder ( prettyLibEnv

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder , printTh

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , prettyHistElem

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , prettyHistory

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , prettyGr

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , prettyLEdge

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , showLEdge

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder , dgOriginHeader

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder , dgOriginSpec

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder , showXPath

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , dgLinkOriginHeader

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , dgLinkOriginSpec

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , dgRuleHeader

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder , dgRuleEdges

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder ) where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Syntax.Print_AS_Structured ()

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Syntax.AS_Structured

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Static.GTheory

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Static.DevGraph

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Static.History

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.GlobalAnnotations

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Common.LibName

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Common.Id

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Common.Consistency

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport Common.Doc as Doc

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Common.DocUtils

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Common.Result

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Keywords

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Common.ConvertGlobalAnnos

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Common.AnalyseAnnos

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport qualified Common.Lib.SizedList as SizedList

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport qualified Common.Lib.Rel as Rel

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport qualified Common.Lib.Graph as Tree

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Data.Graph.Inductive.Graph as Graph

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport qualified Data.Map as Map

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport qualified Data.Set as Set

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Data.List

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Data.Char

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederprintTh :: GlobalAnnos -> SIMPLE_ID -> G_theory -> Doc

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederprintTh oga sn g =

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder let ga = removeProblematicListAnnos oga in

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder useGlobalAnnos ga $ pretty ga $+$ prettyGTheorySL g $+$

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder sep [if null (tokStr sn) then Doc.empty else

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder keyword specS <+> sidDoc sn <+> equals, prettyGTheory g]

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederremoveProblematicListAnnos :: GlobalAnnos -> GlobalAnnos

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederremoveProblematicListAnnos ga = let

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder is = Map.keysSet $ Rel.toMap $ prec_annos ga

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder la = literal_annos ga

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder nla = la { list_lit = Map.filterWithKey ( \ li _ ->

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder let (op, cl, cs) = getListBrackets li in

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Set.null $ Set.filter ( \ (Id ts ics _) ->

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder cs == ics && isPrefixOf op ts && isSuffixOf cl ts) is)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder $ list_lit la }

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Result _ (Just lm) = store_literal_map Map.empty $ convertLiteralAnnos nla

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder in ga { literal_annos = nla

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , literal_map = lm }

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- * pretty instances

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaedershowXPathComp :: XPathPart -> String

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedershowXPathComp c = case c of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ElemName s -> s

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ChildIndex i -> "Spec[" ++ show i ++ "]"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedershowXPath :: [XPathPart] -> String

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedershowXPath l = case l of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder [] -> "/"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder _ -> concatMap (('/' :) . showXPathComp) l

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedershowNodeId :: Node -> String

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedershowNodeId i = "node " ++ show i

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederinstance Pretty NodeSig where

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder pretty (NodeSig n sig) = fsep [ text (showNodeId n) <> colon, pretty sig ]

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederdgOriginSpec :: DGOrigin -> Maybe SIMPLE_ID

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederdgOriginSpec o = case o of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGInst n -> Just n

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGFitView n -> Just n

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder _ -> Nothing

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaederdgOriginHeader :: DGOrigin -> String

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederdgOriginHeader o = case o of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGEmpty -> "empty-spec"

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder DGBasic -> "foreign-basic-spec"

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder DGBasicSpec _ _ -> "basic-spec"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGExtension -> "extension"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGLogicCoercion -> "logic-translation"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGTranslation _ -> "translation"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGUnion -> "union"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGRestriction _ -> "restriction"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGRevealTranslation -> "translation part of a revealing"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGFreeOrCofree v -> map toLower (show v) ++ "-spec"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLocal -> "local-spec"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGClosed -> "closed-spec"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGLogicQual -> "spec with logic qualifier"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGData -> "data-spec"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGFormalParams -> "formal parameters"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGImports -> "arch import"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGInst _ -> "instantiation"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGFitSpec -> "fitting-spec"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGFitView _ -> "fitting-view"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGProof -> "proof-construct"

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder DGNormalForm n -> "normal-form(" ++ shows n ")"

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder DGintegratedSCC -> "OWL spec with integrated strongly connected components"

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder DGFlattening -> "flattening"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Pretty DGOrigin where

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder pretty o = text (dgOriginHeader o) <+> pretty (dgOriginSpec o)

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder $+$ case o of

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder DGBasicSpec gbs syms -> specBraces (pretty gbs) $+$

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder if Set.null syms then Doc.empty else

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder text "new symbols:" $+$ pretty syms

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder DGTranslation (Renamed r) -> pretty r

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder DGRestriction (Restricted r) -> pretty r

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder _ -> Doc.empty

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Pretty DGNodeInfo where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder pretty c = case c of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGNode {} -> pretty $ node_origin c

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder DGRef {} ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder pretty (getLibId $ ref_libname c) <+> text (showNodeId $ ref_node c)

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederprettyDGNodeLab :: DGNodeLab -> Doc

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederprettyDGNodeLab l = sep [ text $ getDGNodeName l, pretty $ nodeInfo l]

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederinstance Pretty DGNodeLab where

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder pretty l = vcat

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder [ text $ "xpath: " ++ showXPath (reverse $ xpath $ dgn_name l)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , pretty $ getNodeConsStatus l

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder , if hasOpenGoals l then text "has open goals" else

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder if hasSenKind (const True) l then Doc.empty else text "locally empty"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder , if labelHasHiding l then text "has ingoing hiding link" else Doc.empty

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , case dgn_nf l of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Nothing -> Doc.empty

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just n -> text "normal form:" <+> text (showNodeId n)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , text "origin:" $+$ pretty (nodeInfo l)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , case dgn_sigma l of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Nothing -> Doc.empty

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just gm -> text "normal form inclusion:" $+$ pretty gm

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder , text "local theory:"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , pretty $ dgn_theory l]

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederinstance Pretty EdgeId where

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder pretty (EdgeId i) = text $ show i

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederdgLinkOriginSpec :: DGLinkOrigin -> Maybe SIMPLE_ID

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederdgLinkOriginSpec o = case o of

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder DGLinkMorph n -> Just n

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder DGLinkInst n _ -> Just n

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder DGLinkInstArg n -> Just n

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkView n _ -> Just n

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder DGLinkFitView n -> Just n

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder DGLinkFitViewImp n -> Just n

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder _ -> Nothing

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederdgLinkMapping :: DGLinkOrigin -> [G_mapping]

962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederdgLinkMapping o = case o of

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder DGLinkInst _ (Fitted l) -> l

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkView _ (Fitted l) -> l

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder _ -> []

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder

962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederdgLinkOriginHeader :: DGLinkOrigin -> String

962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederdgLinkOriginHeader o = case o of

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder SeeTarget -> "see target"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder TEST -> "test"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder SeeSource -> "see source"

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder DGImpliesLink -> "reversed implies link of extension"

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder DGLinkExtension -> "extension"

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder DGLinkTranslation -> "OMDoc translation"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkClosedLenv -> "closed spec and local environment"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkImports -> "OWL import"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkMorph _ -> "instantiation morphism of"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkInst _ _ -> "instantiation of"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkInstArg _ -> "actual parameter of"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkView _ _ -> "view"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkFitView _ -> "fit source of"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkFitViewImp _ -> "add import to source of"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkProof -> "proof-link"

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder DGLinkFlatteningUnion -> "flattening non-disjoint union"

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder DGLinkFlatteningRename -> "flattening renaming"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Pretty DGLinkOrigin where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder pretty o = text (dgLinkOriginHeader o) <+> pretty (dgLinkOriginSpec o)

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder $+$ ppWithCommas (dgLinkMapping o)

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder-- | only shows the edge and node ids

15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaedershowLEdge :: LEdge DGLinkLab -> String

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaedershowLEdge (s, t, l) = "edge " ++ showEdgeId (dgl_id l)

++ " " ++ (showName $ dglName l)

++ "(" ++ showNodeId s ++ " --> " ++ show t ++ ")"

-- | only print the origin and parts of the type

prettyDGLinkLab :: (DGLinkLab -> Doc) -> DGLinkLab -> Doc

prettyDGLinkLab f l = fsep

[ case dgl_origin l of

SeeTarget -> Doc.empty

o -> pretty o

, f l ]

-- | print short edge information

prettyLEdge :: LEdge DGLinkLab -> Doc

prettyLEdge e@(_, _, l) = fsep

[ text $ showLEdge e

, prettyDGLinkLab (text . getDGLinkType) l

, prettyThmLinkStatus $ dgl_type l ]

dgRuleEdges :: DGRule -> [LEdge DGLinkLab]

dgRuleEdges r = case r of

DGRuleWithEdge _ l -> [l]

Composition ls -> ls

_ -> []

dgRuleHeader :: DGRule -> String

dgRuleHeader r = case r of

DGRule str -> str

DGRuleWithEdge str _ -> str

DGRuleLocalInference _ -> "local-inference"

Composition _ -> "composition"

BasicInference _ _ -> "basic-inference"

BasicConsInference _ _ -> "basic-cons-inference"

instance Pretty DGRule where

pretty r = let es = dgRuleEdges r in fsep

[ text (dgRuleHeader r) <> if null es then Doc.empty else colon, case r of

DGRuleLocalInference m ->

braces $ sepByCommas $ map (\ (s, t) ->

let d = text s in if s == t then d else pairElems d $ text t) m

BasicInference c bp -> fsep

[ text $ "using comorphism '" ++ show c ++ "' with proof tree:"

, text $ show bp]

BasicConsInference c bp -> fsep

[ text $ "using comorphism '" ++ show c ++ "' with proof tree:"

, text $ show bp]

_ -> case es of

[] -> Doc.empty

[(_, _, l)] -> prettyDGLinkLab (const Doc.empty) l

_ -> pretty $ Set.fromList $ map (\ (_, _, l) -> dgl_id l) es]

instance Pretty ThmLinkStatus where

pretty tls = case tls of

LeftOpen -> Doc.empty

Proven r ls -> let s = proofBasis ls in

fcat [parens (pretty r), if Set.null s then Doc.empty else pretty s]

prettyThmLinkStatus :: DGLinkType -> Doc

prettyThmLinkStatus = maybe Doc.empty pretty . thmLinkStatus

instance Pretty ConsStatus where

pretty (ConsStatus cons pc thm) = case max cons pc of

None -> Doc.empty

c -> text (show c) <> pretty thm

instance Pretty DGLinkType where

pretty t = (case t of

FreeOrCofreeDefLink v _ -> text $ show v

_ -> Doc.empty)

<> text (getDGEdgeTypeModIncName $ getHomEdgeType False True t)

<> prettyThmLinkStatus t

$+$ pretty (getLinkConsStatus t)

instance Pretty DGLinkLab where

pretty l = vcat

[ text "Origin:" <+> pretty (dgl_origin l)

, text "Type:" <+> pretty (dgl_type l)

, text "Signature Morphism:"

, if dglPending l then text "proof chain incomplete" else Doc.empty

, pretty $ dgl_morphism l

, case dgl_type l of

HidingFreeOrCofreeThm k gm _ -> text ("with " ++ (case k of

Nothing -> "hiding"

Just v -> map toLower (show v))

++ " morphism:") $+$ pretty gm

_ -> Doc.empty ]

-- | pretty print a labelled node

prettyGenLNode :: (a -> Doc) -> LNode a -> Doc

prettyGenLNode f (n, l) = fsep [text (showNodeId n) <> colon, f l]

prettyLNode :: LNode DGNodeLab -> Doc

prettyLNode = prettyGenLNode prettyDGNodeLab

dgChangeType :: DGChange -> String

dgChangeType c = case c of

InsertNode _ -> "insert"

DeleteNode _ -> "delete"

InsertEdge _ -> "insert"

DeleteEdge _ -> "delete"

SetNodeLab _ _ -> "change"

instance Pretty DGChange where

pretty c = text (dgChangeType c) <+> case c of

InsertNode n -> prettyLNode n

DeleteNode n -> prettyLNode n

InsertEdge e -> prettyLEdge e

DeleteEdge e -> prettyLEdge e

SetNodeLab _ n -> prettyLNode n

prettyGr :: Tree.Gr DGNodeLab DGLinkLab -> Doc

prettyGr g = vcat (map prettyLNode $ labNodes g)

$+$ vcat (map prettyLEdge $ labEdges g)

prettyImport :: MaybeNode -> Doc

prettyImport imp = case imp of

EmptyNode _ -> Doc.empty

JustNode n -> keyword givenS <+> pretty (getNode n)

prettyAllParams :: MaybeNode -> Doc

prettyAllParams ps = case ps of

EmptyNode _ -> Doc.empty

JustNode n -> pretty (getNode n)

instance Pretty ExtGenSig where

pretty (ExtGenSig (GenSig imp params allParamSig) body) = fsep $

pretty (getNode body) :

(if null params then [] else

[ pretty $ map getNode params

, prettyAllParams allParamSig ]) ++

[ prettyImport imp ]

instance Pretty ExtViewSig where

pretty (ExtViewSig src gmor ptar) = fsep

[ pretty (getNode src) <+> text toS

, pretty ptar

, pretty gmor ]

instance Pretty UnitSig where

pretty (UnitSig params usig) =

(if null params then Doc.empty else pretty $ map getNode params)

<+> pretty (getNode usig)

instance Pretty ImpUnitSigOrSig where

pretty iu = case iu of

ImpUnitSig imp usig -> fsep

[ pretty usig, prettyImport imp ]

Sig n -> keyword specS <+> pretty (getNode n)

-- instance Pretty ArchSig where

-- pretty (ArchSig m usig) = fsep

-- [ printMap id vcat (\ k v -> fsep [keyword unitS <+> k <+> mapsto, v]) m

-- , pretty usig ]

instance Pretty RefSig where

pretty _ = keyword refinementS

instance Pretty GlobalEntry where

pretty ge = case ge of

SpecEntry se -> topKey specS <+> pretty se

StructEntry ve -> topKey structS <+> pretty ve

ViewEntry ve -> topKey viewS <+> pretty ve

UnitEntry ue -> topKey unitS <+> pretty ue

ArchEntry ae -> topKey archS <+> pretty ae

RefEntry re -> keyword refinementS

instance Pretty DGraph where

pretty dg = vcat

[ prettyGr $ dgBody dg

, text "global environment:"

, printMap id vcat (\ k v -> fsep [k <+> mapsto, v]) $ globalEnv dg

, text "history:"

, prettyHistory $ reverseHistory $ proofHistory dg

, text "redoable history:"

, prettyHistory $ SizedList.reverse $ reverseHistory $ redoHistory dg

, text "next edge:" <+> pretty (getNewEdgeId dg) ]

prettyHistElem :: HistElem -> Doc

prettyHistElem he = case he of

HistElem c -> pretty c

HistGroup r l -> text "rule:" <+> pretty r $+$ space <+> prettyHistory l

prettyHistory :: ProofHistory -> Doc

prettyHistory = vcat . map prettyHistElem . SizedList.toList

prettyLibEnv :: LibEnv -> Doc

prettyLibEnv = printMap id vsep ($+$)