PrintDevGraph.hs revision 3f9fabb8ac5cfd9234431ecf19b51ff3e985595a
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweModule : $Header$
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweDescription : pretty printing (parts of) a LibEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweCopyright : (c) C. Maeder, Uni Bremen 2002-2006
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweMaintainer : Christian.Maeder@dfki.de
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweStability : provisional
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowePortability : non-portable(DevGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowepretty printing (parts of) a LibEnv
5dbfd19ad5fcc2b779f40f80fa05c1bd28fd0b4eTheo Schlossnagle ( prettyLibEnv
ead9bb4b1be81d7bbf8ed86ee41d6c1e58b069a3Yuri Pankov , prettyHistElem
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , prettyHistory
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , prettyLEdge
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dgOriginHeader
fc2512cfb727d49529d8ed99164db871f4829b73Robert Mustacchi , dgOriginSpec
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dgLinkOriginHeader
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dgLinkOriginSpec
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport qualified Common.Lib.SizedList as SizedList
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport qualified Common.Lib.Rel as Rel
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport qualified Common.Lib.Graph as Tree
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport qualified Data.Map as Map
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport qualified Data.Set as Set
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprintTh :: GlobalAnnos -> SIMPLE_ID -> G_theory -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprintTh oga sn g =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let ga = removeProblematicListAnnos oga in
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe useGlobalAnnos ga $ pretty ga $+$ prettyGTheorySL g $+$
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe sep [keyword specS <+> sidDoc sn <+> equals, prettyGTheory g]
fc2512cfb727d49529d8ed99164db871f4829b73Robert MustacchiremoveProblematicListAnnos :: GlobalAnnos -> GlobalAnnos
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweremoveProblematicListAnnos ga = let
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe la = literal_annos ga
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe nla = la { list_lit = Map.filterWithKey ( \ li _ ->
89b9271284be1a4e3e3053d7bc12f9bbf8145b06Robert Mustacchi let (op, cl, cs) = getListBrackets li in
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe cs == ics && isPrefixOf op ts && isSuffixOf cl ts) is)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ list_lit la }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Result _ (Just lm) = store_literal_map Map.empty $ convertLiteralAnnos nla
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in ga { literal_annos = nla
fc2512cfb727d49529d8ed99164db871f4829b73Robert Mustacchi , literal_map = lm }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- * pretty instances
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowXPathComp :: XPathPart -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowXPathComp c = case c of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ElemName s -> s
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ChildIndex i -> show i
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowXPath :: [XPathPart] -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowXPath = intercalate "/" . map showXPathComp . reverse
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowNodeId :: Node -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowNodeId i = "node " ++ show i
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty NodeSig where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (NodeSig n sig) = fsep [ text (showNodeId n) <> colon, pretty sig ]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgOriginSpec :: DGOrigin -> Maybe SIMPLE_ID
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgOriginSpec o = case o of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGSpecInst n -> Just n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGFitView n -> Just n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGFitViewA n -> Just n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe _ -> Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgOriginHeader :: DGOrigin -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgOriginHeader o = case o of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGEmpty -> "empty-spec"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGBasic -> "foreign-basic-spec"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGBasicSpec _ -> "basic-spec"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGExtension -> "extension"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGTranslation -> "translation"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGUnion -> "union"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGHiding -> "hiding"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGRevealing -> "revealing"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGRevealTranslation -> "translation part of a revealing"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGFreeOrCofree v -> map toLower (show v) ++ "-spec"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLocal -> "local-spec"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGClosed -> "closed-spec"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLogicQual -> "spec with logic qualifier"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGData -> "data-spec"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGFormalParams -> "formal parameters"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGImports -> "arch import"
7dc9a163b382daee1ce43b6588dd1b507363dae5Robert Mustacchi DGSpecInst _ -> "instantiation"
a5eb7107f06a6e23e8e77e8d3a84c1ff90a73ac6Bryan Cantrill DGFitSpec -> "fitting-spec"
a5eb7107f06a6e23e8e77e8d3a84c1ff90a73ac6Bryan Cantrill DGFitView _ -> "fitting-view"
a5eb7107f06a6e23e8e77e8d3a84c1ff90a73ac6Bryan Cantrill DGFitViewA _ -> "fitting view (actual parameters)"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGProof -> "proof-construct"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGNormalForm n -> "normal-form(" ++ shows n ")"
1767006bb066ef500b90b432fba79d63d0d09b36Bryan Cantrill DGintegratedSCC -> "OWL spec with integrated strongly connected components"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGFlattening -> "flattening"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGOrigin where
ce83b99835cc4643ab0fefd88dea62427d9ced5eRobert Mustacchi pretty o = text (dgOriginHeader o) <+> pretty (dgOriginSpec o)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe <+> case o of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGBasicSpec syms -> if Set.null syms then Doc.empty else pretty syms
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGNodeInfo where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty c = case c of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGNode {} -> pretty $ node_origin c
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (getLIB_ID $ ref_libname c) <+> text (showNodeId $ ref_node c)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyDGNodeLab :: DGNodeLab -> Doc
7a5aac98bc37534537d4896efd4efd30627d221eJerry JelinekprettyDGNodeLab l = sep [ text $ getDGNodeName l, pretty $ nodeInfo l]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGNodeLab where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty l = vcat
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ text "Origin:" <+> pretty (nodeInfo l)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , pretty $ getNodeConsStatus l
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , if hasOpenGoals l then text "has open goals" else
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if hasSenKind (const True) l then Doc.empty else text "locally empty"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , if labelHasHiding l then text "has ingoing hiding link" else Doc.empty
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , case dgn_nf l of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just n -> text "normal form:" <+> text (showNodeId n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , case dgn_sigma l of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just gm -> text "normal form inclusion:" $+$ pretty gm
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text "Local Theory:"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , pretty $ dgn_theory l]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty EdgeId where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (EdgeId i) = text $ show i
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgLinkOriginSpec :: DGLinkOrigin -> Maybe SIMPLE_ID
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgLinkOriginSpec o = case o of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkSpecInst n -> Just n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkView n -> Just n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFitView n -> Just n
9d12795f87b63c2e39e87bff369182edd34677d3Robert Mustacchi DGLinkFitViewImp n -> Just n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFitViewAImp n -> Just n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe _ -> Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgLinkOriginHeader :: DGLinkOrigin -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgLinkOriginHeader o = case o of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe SeeTarget -> "see target"
296749875bd503e7a14e25b4c57d3142cb496df1Joshua M. Clulow SeeSource -> "see source"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGImpliesLink -> "reversed implies link of extension"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkExtension -> "extension"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkTranslation -> "OMDoc translation"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkClosedLenv -> "closed spec and local environment"
d2b9ba291ef0d1dc8807b6d46996674c723924d0Robert Mustacchi DGLinkImports -> "OWL import"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkSpecInst _ -> "instantiation-link"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFitSpec -> "fitting-spec-link"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkView _ -> "view"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFitView _ -> "fitting view to"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFitViewImp _ -> "fitting view (import)"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFitViewAImp _ -> "fitting view (actual parameter)"
b65dd972486b1f5913d705d2a0cb9c3fb189a9e0Robert Mustacchi DGLinkProof -> "proof-link"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFlatteningUnion -> "flattening non-disjoint union"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGLinkFlatteningRename -> "flattening renaming"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGLinkOrigin where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty o = text (dgLinkOriginHeader o) <+> pretty (dgLinkOriginSpec o)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | only shows the edge and node ids
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowLEdge :: LEdge DGLinkLab -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweshowLEdge (s, t, l) = "edge " ++ showEdgeId (dgl_id l)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ++ " (" ++ showNodeId s ++ " --> " ++ show t ++ ")"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | only print the origin and some notion of the tye of the label
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyDGLinkLab :: (DGLinkLab -> Doc) -> DGLinkLab -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyDGLinkLab f l = fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ case dgl_origin l of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe o -> pretty o
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | print short edge information
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyLEdge :: LEdge DGLinkLab -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyLEdge e@(_, _, l) = fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ text $ showLEdge e
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , prettyDGLinkLab (text . getDGLinkType) l
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , prettyThmLinkStatus $ dgl_type l ]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgRuleEdges :: DGRule -> [LEdge DGLinkLab]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgRuleEdges r = case r of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGRuleWithEdge _ l -> [l]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Composition ls -> ls
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgRuleHeader :: DGRule -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgRuleHeader r = case r of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGRule str -> str
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGRuleWithEdge str _ -> str
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGRuleLocalInference _ -> "Local-Inference"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Composition _ -> "Composition"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe BasicInference _ _ -> "Basic-Inference"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe BasicConsInference _ _ -> "Basic-Cons-Inference"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGRule where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty r = let es = dgRuleEdges r in fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ text (dgRuleHeader r) <> if null es then Doc.empty else colon, case r of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DGRuleLocalInference m ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe braces $ sepByCommas $ map (\ (s, t) ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let d = text s in if s == t then d else pairElems d $ text t) m
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe BasicInference c bp -> fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ text $ "using comorphism '" ++ show c ++ "' with proof tree:"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text $ show bp]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe BasicConsInference c bp -> fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ text $ "using comorphism '" ++ show c ++ "' with proof tree:"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text $ show bp]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe _ -> case es of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [(_, _, l)] -> prettyDGLinkLab (const Doc.empty) l
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe _ -> pretty $ Set.fromList $ map (\ (_, _, l) -> dgl_id l) es]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty ThmLinkStatus where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty tls = case tls of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Proven r ls -> let s = proofBasis ls in
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe fcat [parens (pretty r), if Set.null s then Doc.empty else pretty s]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyThmLinkStatus :: DGLinkType -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyThmLinkStatus = maybe Doc.empty pretty . thmLinkStatus
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty ConsStatus where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (ConsStatus cons pc thm) = case max cons pc of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe c -> text (show c) <> pretty thm
fc2512cfb727d49529d8ed99164db871f4829b73Robert Mustacchiinstance Pretty DGLinkType where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty t = text (getDGEdgeTypeModIncName $ getHomEdgeType True t)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe <> prettyThmLinkStatus t
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $+$ pretty (getLinkConsStatus t)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGLinkLab where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty l = vcat
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ text "Origin:" <+> pretty (dgl_origin l)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text "Type:" <+> pretty (dgl_type l)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text "Signature Morphism:"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , pretty $ dgl_morphism l
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , case dgl_type l of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe HidingFreeOrCofreeThm Nothing gm _ ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe text "with hiding morphism:" $+$ pretty gm
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | pretty print a labelled node
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyGenLNode :: (a -> Doc) -> LNode a -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyGenLNode f (n, l) = fsep [text (showNodeId n) <> colon, f l]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyLNode :: LNode DGNodeLab -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyLNode = prettyGenLNode prettyDGNodeLab
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgChangeType :: DGChange -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowedgChangeType c = case c of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe InsertNode _ -> "insert"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DeleteNode _ -> "delete"
462453d2d0c563559a4caf186db76954e563bd1aMatthew Ahrens InsertEdge _ -> "insert"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DeleteEdge _ -> "delete"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe SetNodeLab _ _ -> "change"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGChange where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty c = text (dgChangeType c) <+> case c of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe InsertNode n -> prettyLNode n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DeleteNode n -> prettyLNode n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe InsertEdge e -> prettyLEdge e
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe DeleteEdge e -> prettyLEdge e
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe SetNodeLab _ n -> prettyLNode n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyGr :: Tree.Gr DGNodeLab DGLinkLab -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyGr g = vcat (map prettyLNode $ labNodes g)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $+$ vcat (map prettyLEdge $ labEdges g)
e56998eefc33ead0f12b364be915dd6bfc12a3f5Robert MustacchiprettyImport :: MaybeNode -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyImport imp = case imp of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe EmptyNode _ -> Doc.empty
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe JustNode n -> keyword givenS <+> pretty (getNode n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyAllParams :: MaybeNode -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyAllParams ps = case ps of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe EmptyNode _ -> Doc.empty
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe JustNode n -> pretty (getNode n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty ExtGenSig where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (ExtGenSig (GenSig imp params allParamSig) body) = fsep $
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (getNode body) :
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (if null params then [] else
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ pretty $ map getNode params
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , prettyAllParams allParamSig ]) ++
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ prettyImport imp ]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty ExtViewSig where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (ExtViewSig src gmor ptar) = fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ pretty (getNode src) <+> text toS
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , pretty ptar
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , pretty gmor ]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty UnitSig where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty (UnitSig params usig) =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (if null params then Doc.empty else pretty $ map getNode params)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe <+> pretty (getNode usig)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty ImpUnitSigOrSig where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty iu = case iu of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ImpUnitSig imp usig -> fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ pretty usig, prettyImport imp ]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Sig n -> keyword specS <+> pretty (getNode n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty ArchSig where
ad0ef8fd06d1ac28108685495a9ba1244a20a5caRobert Mustacchi pretty (ArchSig m usig) = fsep
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ printMap id vcat (\ k v -> fsep [keyword unitS <+> k <+> mapsto, v]) m
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , pretty usig ]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty GlobalEntry where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty ge = case ge of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe SpecEntry se -> topKey specS <+> pretty se
ad0ef8fd06d1ac28108685495a9ba1244a20a5caRobert Mustacchi ViewEntry ve -> topKey viewS <+> pretty ve
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe UnitEntry ue -> topKey unitS <+> pretty ue
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ArchEntry ae -> topKey archS <+> pretty ae
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe RefEntry -> keyword refinementS
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweinstance Pretty DGraph where
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pretty dg = vcat
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [ prettyGr $ dgBody dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text "Global Environment"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , printMap id vcat (\ k v -> fsep [k <+> mapsto, v]) $ globalEnv dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text "History"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , prettyHistory $ reverseHistory $ proofHistory dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text "Redoable History"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , prettyHistory $ SizedList.reverse $ reverseHistory $ redoHistory dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , text "next edge:" <+> pretty (getNewEdgeId dg) ]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyHistElem :: HistElem -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyHistElem he = case he of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe HistElem c -> pretty c
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe HistGroup r l -> text "rule:" <+> pretty r $+$ space <+> prettyHistory l
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyHistory :: ProofHistory -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyHistory = vcat . map prettyHistElem . SizedList.toList
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyLibEnv :: LibEnv -> Doc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweprettyLibEnv = printMap id vsep ($+$)