fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance{- |

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceModule : $Header$

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceDescription : pretty printing (parts of) a LibEnv

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceCopyright : (c) C. Maeder, Uni Bremen 2002-2006

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceMaintainer : Christian.Maeder@dfki.de

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceStability : provisional

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancePortability : non-portable(DevGraph)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mancepretty printing (parts of) a LibEnv

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-}

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mancemodule Static.PrintDevGraph

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance ( prettyLibEnv

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , printTh

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , prettyHistElem

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , prettyHistory

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , prettyGr

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , prettyLEdge

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , showLEdge

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , dgOriginHeader

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , dgOriginSpec

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , showXPath

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , dgLinkOriginHeader

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , dgLinkOriginSpec

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , dgRuleHeader

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , dgRuleEdges

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance ) where

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Syntax.Print_AS_Structured ()

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Syntax.AS_Structured

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Static.GTheory

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Static.DevGraph

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Static.History

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.GlobalAnnotations

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceimport Common.LibName

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceimport Common.Id

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.Consistency

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceimport Common.Doc as Doc

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceimport Common.DocUtils

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.Result

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.Keywords

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.ConvertGlobalAnnos

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.AnalyseAnnos

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport qualified Common.Lib.SizedList as SizedList

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport qualified Common.Lib.Rel as Rel

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport qualified Common.Lib.Graph as Tree

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Data.Graph.Inductive.Graph as Graph

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport qualified Data.Map as Map

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport qualified Data.Set as Set

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Data.List

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Data.Char

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceprintTh :: GlobalAnnos -> SIMPLE_ID -> G_theory -> Doc

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceprintTh oga sn g =

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance let ga = removeProblematicListAnnos oga in

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance useGlobalAnnos ga $ pretty ga $+$ prettyGTheorySL g $+$

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance sep [if null (tokStr sn) then Doc.empty else

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance keyword specS <+> sidDoc sn <+> equals, prettyGTheory g]

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceremoveProblematicListAnnos :: GlobalAnnos -> GlobalAnnos

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceremoveProblematicListAnnos ga = let

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance is = Map.keysSet $ Rel.toMap $ prec_annos ga

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance la = literal_annos ga

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance nla = la { list_lit = Map.filterWithKey ( \ li _ ->

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance let (op, cl, cs) = getListBrackets li in

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Set.null $ Set.filter ( \ (Id ts ics _) ->

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance cs == ics && isPrefixOf op ts && isSuffixOf cl ts) is)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance $ list_lit la }

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Result _ (Just lm) = store_literal_map Map.empty $ convertLiteralAnnos nla

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance in ga { literal_annos = nla

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , literal_map = lm }

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance-- * pretty instances

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceshowXPathComp :: XPathPart -> String

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceshowXPathComp c = case c of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance ElemName s -> s

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance ChildIndex i -> "Spec[" ++ show i ++ "]"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceshowXPath :: [XPathPart] -> String

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceshowXPath l = case l of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance [] -> "/"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance _ -> concatMap (('/' :) . showXPathComp) l

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceshowNodeId :: Node -> String

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceshowNodeId i = "node " ++ show i

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceinstance Pretty NodeSig where

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance pretty (NodeSig n sig) = fsep [ text (showNodeId n) <> colon, pretty sig ]

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancedgOriginSpec :: DGOrigin -> Maybe SIMPLE_ID

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancedgOriginSpec o = case o of

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance DGInst n -> Just n

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance DGFitView n -> Just n

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance _ -> Nothing

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel MancedgOriginHeader :: DGOrigin -> String

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel MancedgOriginHeader o = case o of

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance DGEmpty -> "empty-spec"

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance DGBasic -> "foreign-basic-spec"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGBasicSpec _ _ -> "basic-spec"

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance DGExtension -> "extension"

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance DGLogicCoercion -> "logic-translation"

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance DGTranslation _ -> "translation"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGUnion -> "union"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance DGRestriction _ -> "restriction"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGRevealTranslation -> "translation part of a revealing"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance DGFreeOrCofree v -> map toLower (show v) ++ "-spec"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance DGLocal -> "local-spec"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGClosed -> "closed-spec"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGLogicQual -> "spec with logic qualifier"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGData -> "data-spec"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGFormalParams -> "formal parameters"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGImports -> "arch import"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGInst _ -> "instantiation"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGFitSpec -> "fitting-spec"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGFitView _ -> "fitting-view"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGProof -> "proof-construct"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGNormalForm n -> "normal-form(" ++ shows n ")"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGintegratedSCC -> "OWL spec with integrated strongly connected components"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGFlattening -> "flattening"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Manceinstance Pretty DGOrigin where

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance pretty o = text (dgOriginHeader o) <+> pretty (dgOriginSpec o)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance $+$ case o of

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGBasicSpec gbs syms -> specBraces (pretty gbs) $+$

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance if Set.null syms then Doc.empty else

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance text "new symbols:" $+$ pretty syms

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGTranslation (Renamed r) -> pretty r

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGRestriction (Restricted r) -> pretty r

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ -> Doc.empty

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Manceinstance Pretty DGNodeInfo where

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance pretty c = case c of

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGNode {} -> pretty $ node_origin c

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance DGRef {} ->

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance pretty (getLibId $ ref_libname c) <+> text (showNodeId $ ref_node c)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceprettyDGNodeLab :: DGNodeLab -> Doc

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel ManceprettyDGNodeLab l = sep [ text $ getDGNodeName l, pretty $ nodeInfo l]

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceinstance Pretty DGNodeLab where

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance pretty l = vcat

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance [ text $ "xpath: " ++ showXPath (reverse $ xpath $ dgn_name l)

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , pretty $ getNodeConsStatus l

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , if hasOpenGoals l then text "has open goals" else

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance if hasSenKind (const True) l then Doc.empty else text "locally empty"

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance , if labelHasHiding l then text "has ingoing hiding link" else Doc.empty

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance , case dgn_nf l of

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Nothing -> Doc.empty

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Just n -> text "normal form:" <+> text (showNodeId n)

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , text "origin:" $+$ pretty (nodeInfo l)

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , case dgn_sigma l of

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance Nothing -> Doc.empty

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance Just gm -> text "normal form inclusion:" $+$ pretty gm

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , text "local theory:"

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance , pretty $ dgn_theory l]

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Manceinstance Pretty EdgeId where

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance pretty (EdgeId i) = text $ show i

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancedgLinkOriginSpec :: DGLinkOrigin -> Maybe SIMPLE_ID

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancedgLinkOriginSpec o = case o of

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkMorph n -> Just n

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkInst n _ -> Just n

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkInstArg n -> Just n

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkView n _ -> Just n

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkFitView n -> Just n

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkFitViewImp n -> Just n

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance _ -> Nothing

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancedgLinkMapping :: DGLinkOrigin -> [G_mapping]

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancedgLinkMapping o = case o of

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkInst _ (Fitted l) -> l

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkView _ (Fitted l) -> l

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance _ -> []

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancedgLinkOriginHeader :: DGLinkOrigin -> String

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancedgLinkOriginHeader o = case o of

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance SeeTarget -> "see target"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance TEST -> "test"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance SeeSource -> "see source"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGImpliesLink -> "reversed implies link of extension"

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkExtension -> "extension"

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance DGLinkTranslation -> "OMDoc translation"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkClosedLenv -> "closed spec and local environment"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkImports -> "OWL import"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkMorph _ -> "instantiation morphism of"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkInst _ _ -> "instantiation of"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkInstArg _ -> "actual parameter of"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkView _ _ -> "view"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkFitView _ -> "fit source of"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkFitViewImp _ -> "add import to source of"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkProof -> "proof-link"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkFlatteningUnion -> "flattening non-disjoint union"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGLinkFlatteningRename -> "flattening renaming"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceinstance Pretty DGLinkOrigin where

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance pretty o = text (dgLinkOriginHeader o) <+> pretty (dgLinkOriginSpec o)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance $+$ ppWithCommas (dgLinkMapping o)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-- | only shows the edge and node ids

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceshowLEdge :: LEdge DGLinkLab -> String

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceshowLEdge (s, t, l) = "edge " ++ showEdgeId (dgl_id l)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance ++ " " ++ (showName $ dglName l)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance ++ "(" ++ showNodeId s ++ " --> " ++ show t ++ ")"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-- | only print the origin and parts of the type

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceprettyDGLinkLab :: (DGLinkLab -> Doc) -> DGLinkLab -> Doc

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceprettyDGLinkLab f l = fsep

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance [ case dgl_origin l of

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance SeeTarget -> Doc.empty

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance o -> pretty o

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , f l ]

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-- | print short edge information

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceprettyLEdge :: LEdge DGLinkLab -> Doc

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceprettyLEdge e@(_, _, l) = fsep

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance [ text $ showLEdge e

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , prettyDGLinkLab (text . getDGLinkType) l

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , prettyThmLinkStatus $ dgl_type l ]

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancedgRuleEdges :: DGRule -> [LEdge DGLinkLab]

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancedgRuleEdges r = case r of

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGRuleWithEdge _ l -> [l]

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance Composition ls -> ls

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> []

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancedgRuleHeader :: DGRule -> String

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancedgRuleHeader r = case r of

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGRule str -> str

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGRuleWithEdge str _ -> str

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGRuleLocalInference _ -> "local-inference"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance Composition _ -> "composition"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance BasicInference _ _ -> "basic-inference"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance BasicConsInference _ _ -> "basic-cons-inference"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceinstance Pretty DGRule where

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance pretty r = let es = dgRuleEdges r in fsep

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance DGRuleLocalInference m ->

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

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance BasicInference c bp -> fsep

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , text $ show bp]

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance 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 ($+$)