ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova{- |

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaModule : $Header$

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaDescription : pretty printing (parts of) a LibEnv

b43458b4d81f7451112cecbd757f3a05216e7088Kristina SojakovaCopyright : (c) C. Maeder, Uni Bremen 2002-2006

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaStability : provisional

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaPortability : non-portable(DevGraph)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovapretty printing (parts of) a LibEnv

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova-}

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovamodule Static.PrintDevGraph

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova ( prettyLibEnv

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , printTh

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , prettyHistElem

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , prettyHistory

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , prettyGr

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova , prettyLEdge

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova , showLEdge

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova , dgOriginHeader

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , dgOriginSpec

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , showXPath

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , dgLinkOriginHeader

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova , dgLinkOriginSpec

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova , dgRuleHeader

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova , dgRuleEdges

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova ) where

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Syntax.Print_AS_Structured ()

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Syntax.AS_Structured

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Static.GTheory

b43458b4d81f7451112cecbd757f3a05216e7088Kristina Sojakovaimport Static.DevGraph

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Static.History

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Common.GlobalAnnotations

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Common.LibName

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Common.Id

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Common.Consistency

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Common.Doc as Doc

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Common.DocUtils

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Result

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Keywords

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.ConvertGlobalAnnos

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.AnalyseAnnos

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport qualified Common.Lib.SizedList as SizedList

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakovaimport qualified Common.Lib.Rel as Rel

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakovaimport qualified Common.Lib.Graph as Tree

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakovaimport Data.Graph.Inductive.Graph as Graph

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakovaimport qualified Data.Map as Map

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakovaimport qualified Data.Set as Set

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maederimport Data.List

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakovaimport Data.Char

b43458b4d81f7451112cecbd757f3a05216e7088Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintTh :: GlobalAnnos -> SIMPLE_ID -> G_theory -> Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintTh oga sn g =

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova let ga = removeProblematicListAnnos oga in

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova useGlobalAnnos ga $ pretty ga $+$ prettyGTheorySL g $+$

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova sep [if null (tokStr sn) then Doc.empty else

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova keyword specS <+> sidDoc sn <+> equals, prettyGTheory g]

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaremoveProblematicListAnnos :: GlobalAnnos -> GlobalAnnos

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaremoveProblematicListAnnos ga = let

abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova is = Map.keysSet $ Rel.toMap $ prec_annos ga

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova la = literal_annos ga

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova nla = la { list_lit = Map.filterWithKey ( \ li _ ->

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova let (op, cl, cs) = getListBrackets li in

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova Set.null $ Set.filter ( \ (Id ts ics _) ->

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova cs == ics && isPrefixOf op ts && isSuffixOf cl ts) is)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova $ list_lit la }

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova Result _ (Just lm) = store_literal_map Map.empty $ convertLiteralAnnos nla

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova in ga { literal_annos = nla

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , literal_map = lm }

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova-- * pretty instances

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaedershowXPathComp :: XPathPart -> String

80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian MaedershowXPathComp c = case c of

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder ElemName s -> s

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova ChildIndex i -> "Spec[" ++ show i ++ "]"

168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaedershowXPath :: [XPathPart] -> String

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaedershowXPath l = case l of

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova [] -> "/"

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova _ -> concatMap (('/' :) . showXPathComp) l

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova

abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovashowNodeId :: Node -> String

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovashowNodeId i = "node " ++ show i

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maederinstance Pretty NodeSig where

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova pretty (NodeSig n sig) = fsep [ text (showNodeId n) <> colon, pretty sig ]

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaederdgOriginSpec :: DGOrigin -> Maybe SIMPLE_ID

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovadgOriginSpec o = case o of

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova DGInst n -> Just n

abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova DGFitView n -> Just n

168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova _ -> Nothing

80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovadgOriginHeader :: DGOrigin -> String

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovadgOriginHeader o = case o of

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGEmpty -> "empty-spec"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGBasic -> "foreign-basic-spec"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGBasicSpec _ _ -> "basic-spec"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGExtension -> "extension"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGLogicCoercion -> "logic-translation"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGTranslation _ -> "translation"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGUnion -> "union"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGRestriction _ -> "restriction"

abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova DGRevealTranslation -> "translation part of a revealing"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGFreeOrCofree v -> map toLower (show v) ++ "-spec"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova DGLocal -> "local-spec"

5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova DGClosed -> "closed-spec"

5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova DGLogicQual -> "spec with logic qualifier"

5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova DGData -> "data-spec"

DGFormalParams -> "formal parameters"

DGImports -> "arch import"

DGInst _ -> "instantiation"

DGFitSpec -> "fitting-spec"

DGFitView _ -> "fitting-view"

DGProof -> "proof-construct"

DGNormalForm n -> "normal-form(" ++ shows n ")"

DGintegratedSCC -> "OWL spec with integrated strongly connected components"

DGFlattening -> "flattening"

instance Pretty DGOrigin where

pretty o = text (dgOriginHeader o) <+> pretty (dgOriginSpec o)

$+$ case o of

DGBasicSpec gbs syms -> specBraces (pretty gbs) $+$

if Set.null syms then Doc.empty else

text "new symbols:" $+$ pretty syms

DGTranslation (Renamed r) -> pretty r

DGRestriction (Restricted r) -> pretty r

_ -> Doc.empty

instance Pretty DGNodeInfo where

pretty c = case c of

DGNode {} -> pretty $ node_origin c

DGRef {} ->

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

prettyDGNodeLab :: DGNodeLab -> Doc

prettyDGNodeLab l = sep [ text $ getDGNodeName l, pretty $ nodeInfo l]

instance Pretty DGNodeLab where

pretty l = vcat

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

, pretty $ getNodeConsStatus l

, if hasOpenGoals l then text "has open goals" else

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

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

, case dgn_nf l of

Nothing -> Doc.empty

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

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

, case dgn_sigma l of

Nothing -> Doc.empty

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

, text "local theory:"

, pretty $ dgn_theory l]

instance Pretty EdgeId where

pretty (EdgeId i) = text $ show i

dgLinkOriginSpec :: DGLinkOrigin -> Maybe SIMPLE_ID

dgLinkOriginSpec o = case o of

DGLinkMorph n -> Just n

DGLinkInst n _ -> Just n

DGLinkInstArg n -> Just n

DGLinkView n _ -> Just n

DGLinkFitView n -> Just n

DGLinkFitViewImp n -> Just n

_ -> Nothing

dgLinkMapping :: DGLinkOrigin -> [G_mapping]

dgLinkMapping o = case o of

DGLinkInst _ (Fitted l) -> l

DGLinkView _ (Fitted l) -> l

_ -> []

dgLinkOriginHeader :: DGLinkOrigin -> String

dgLinkOriginHeader o = case o of

SeeTarget -> "see target"

TEST -> "test"

SeeSource -> "see source"

DGImpliesLink -> "reversed implies link of extension"

DGLinkExtension -> "extension"

DGLinkTranslation -> "OMDoc translation"

DGLinkClosedLenv -> "closed spec and local environment"

DGLinkImports -> "OWL import"

DGLinkMorph _ -> "instantiation morphism of"

DGLinkInst _ _ -> "instantiation of"

DGLinkInstArg _ -> "actual parameter of"

DGLinkView _ _ -> "view"

DGLinkFitView _ -> "fit source of"

DGLinkFitViewImp _ -> "add import to source of"

DGLinkProof -> "proof-link"

DGLinkFlatteningUnion -> "flattening non-disjoint union"

DGLinkFlatteningRename -> "flattening renaming"

instance Pretty DGLinkOrigin where

pretty o = text (dgLinkOriginHeader o) <+> pretty (dgLinkOriginSpec o)

$+$ ppWithCommas (dgLinkMapping o)

-- | only shows the edge and node ids

showLEdge :: LEdge DGLinkLab -> String

showLEdge (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 ($+$)