{- |
Module      :  ./Static/PrintDevGraph.hs
Description :  pretty printing (parts of) a LibEnv
Copyright   :  (c) C. Maeder, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(DevGraph)

pretty printing (parts of) a LibEnv
-}

module Static.PrintDevGraph
    ( prettyLibEnv
    , printTh
    , prettyHistElem
    , prettyHistory
    , prettyGr
    , prettyLEdge
    , showLEdge
    , dgOriginHeader
    , dgOriginSpec
    , showXPath
    , dgLinkOriginHeader
    , dgLinkOriginSpec
    , dgRuleHeader
    , dgRuleEdges
    ) where

import Syntax.Print_AS_Structured
import Syntax.AS_Structured

import Static.DgUtils
import Static.GTheory
import Static.DevGraph
import Static.History

import Common.GlobalAnnotations
import Common.LibName
import Common.Id
import Common.IRI
import Common.Consistency
import Common.Doc as Doc
import Common.DocUtils
import Common.Result
import Common.Keywords
import Common.ConvertGlobalAnnos
import Common.AnalyseAnnos
import qualified Common.Lib.SizedList as SizedList
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.Graph as Tree

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List
import Data.Char

printTh :: GlobalAnnos -> IRI -> G_theory -> Doc
printTh :: GlobalAnnos -> IRI -> G_theory -> Doc
printTh oga :: GlobalAnnos
oga sn :: IRI
sn g :: G_theory
g =
    let ga :: GlobalAnnos
ga = GlobalAnnos -> GlobalAnnos
removeProblematicListAnnos GlobalAnnos
oga in
    GlobalAnnos -> Doc -> Doc
useGlobalAnnos GlobalAnnos
ga (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Doc
forall a. Pretty a => a -> Doc
pretty GlobalAnnos
ga Doc -> Doc -> Doc
$+$ G_theory -> Doc
prettyGTheorySL G_theory
g Doc -> Doc -> Doc
$+$
    [Doc] -> Doc
sep [ if IRI
sn IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
nullIRI then Doc
Doc.empty else
             String -> Doc
keyword String
specS Doc -> Doc -> Doc
<+> IRI -> Doc
structIRI IRI
sn Doc -> Doc -> Doc
<+> Doc
equals
        , Maybe IRI -> G_theory -> Doc
prettyGTheory (G_theory -> Maybe IRI
gTheorySyntax G_theory
g) G_theory
g]

removeProblematicListAnnos :: GlobalAnnos -> GlobalAnnos
removeProblematicListAnnos :: GlobalAnnos -> GlobalAnnos
removeProblematicListAnnos ga :: GlobalAnnos
ga = let
    is :: Set Id
is = Map Id (Set Id) -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id (Set Id) -> Set Id) -> Map Id (Set Id) -> Set Id
forall a b. (a -> b) -> a -> b
$ Rel Id -> Map Id (Set Id)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel Id -> Map Id (Set Id)) -> Rel Id -> Map Id (Set Id)
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel Id
prec_annos GlobalAnnos
ga
    la :: LiteralAnnos
la = GlobalAnnos -> LiteralAnnos
literal_annos GlobalAnnos
ga
    nla :: LiteralAnnos
nla = LiteralAnnos
la { list_lit :: Map Id (Id, Id)
list_lit = (Id -> (Id, Id) -> Bool) -> Map Id (Id, Id) -> Map Id (Id, Id)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey ( \ li :: Id
li _ ->
        let (op :: [Token]
op, cl :: [Token]
cl, cs :: [Id]
cs) = Id -> ([Token], [Token], [Id])
getListBrackets Id
li in
          Set Id -> Bool
forall a. Set a -> Bool
Set.null (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ (Id -> Bool) -> Set Id -> Set Id
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ( \ (Id ts :: [Token]
ts ics :: [Id]
ics _) ->
              [Id]
cs [Id] -> [Id] -> Bool
forall a. Eq a => a -> a -> Bool
== [Id]
ics Bool -> Bool -> Bool
&& [Token] -> [Token] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [Token]
op [Token]
ts Bool -> Bool -> Bool
&& [Token] -> [Token] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf [Token]
cl [Token]
ts) Set Id
is)
        (Map Id (Id, Id) -> Map Id (Id, Id))
-> Map Id (Id, Id) -> Map Id (Id, Id)
forall a b. (a -> b) -> a -> b
$ LiteralAnnos -> Map Id (Id, Id)
list_lit LiteralAnnos
la }
    Result _ (Just lm :: LiteralMap
lm) = LiteralMap -> [Annotation] -> Result LiteralMap
store_literal_map LiteralMap
forall k a. Map k a
Map.empty ([Annotation] -> Result LiteralMap)
-> [Annotation] -> Result LiteralMap
forall a b. (a -> b) -> a -> b
$ LiteralAnnos -> [Annotation]
convertLiteralAnnos LiteralAnnos
nla
    in GlobalAnnos
ga { literal_annos :: LiteralAnnos
literal_annos = LiteralAnnos
nla
          , literal_map :: LiteralMap
literal_map = LiteralMap
lm }

-- * pretty instances

showXPathComp :: XPathPart -> String
showXPathComp :: XPathPart -> String
showXPathComp c :: XPathPart
c = case XPathPart
c of
  ElemName s :: String
s -> String
s
  ChildIndex i :: Int
i -> "Spec[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"

showXPath :: [XPathPart] -> String
showXPath :: [XPathPart] -> String
showXPath l :: [XPathPart]
l = case [XPathPart]
l of
  [] -> "/"
  _ -> (XPathPart -> String) -> [XPathPart] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (('/' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (XPathPart -> String) -> XPathPart -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XPathPart -> String
showXPathComp) [XPathPart]
l

showNodeId :: Node -> String
showNodeId :: Int -> String
showNodeId i :: Int
i = "node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

instance Pretty NodeSig where
  pretty :: NodeSig -> Doc
pretty (NodeSig n :: Int
n sig :: G_sign
sig) = [Doc] -> Doc
fsep [ String -> Doc
text (Int -> String
showNodeId Int
n) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, G_sign -> Doc
forall a. Pretty a => a -> Doc
pretty G_sign
sig ]

instance Pretty NodeName where
  pretty :: NodeName -> Doc
pretty n :: NodeName
n = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ NodeName -> String
showName NodeName
n

dgOriginSpec :: DGOrigin -> Maybe IRI
dgOriginSpec :: DGOrigin -> Maybe IRI
dgOriginSpec o :: DGOrigin
o = case DGOrigin
o of
    DGInst n :: IRI
n -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    DGFitView n :: IRI
n -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    _ -> Maybe IRI
forall a. Maybe a
Nothing

dgOriginHeader :: DGOrigin -> String
dgOriginHeader :: DGOrigin -> String
dgOriginHeader o :: DGOrigin
o = case DGOrigin
o of
    DGEmpty -> "empty-spec"
    DGBasic -> "foreign-basic-spec"
    DGBasicSpec {} -> "basic-spec"
    DGExtension -> "extension"
    DGLogicCoercion -> "logic-translation"
    DGTranslation _ -> "translation"
    DGUnion -> "union"
    DGIntersect -> "intersection"
    DGExtract -> "extraction"
    DGRestriction _ _ -> "restriction"
    DGRevealTranslation -> "translation part of a revealing"
    DGFreeOrCofree v :: FreeOrCofree
v -> (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FreeOrCofree -> String
forall a. Show a => a -> String
show FreeOrCofree
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-spec"
    DGLocal -> "local-spec"
    DGClosed -> "closed-spec"
    DGLogicQual -> "spec with logic qualifier"
    DGData -> "data-spec"
    DGFormalParams -> "formal parameters"
    DGVerificationGeneric -> "verification for application of generic units"
    DGImports -> "arch import"
    DGInst _ -> "instantiation"
    DGFitSpec -> "fitting-spec"
    DGFitView _ -> "fitting-view"
    DGProof -> "proof-construct"
    DGNormalForm n :: Int
n -> "normal-form(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
n ")"
    DGintegratedSCC -> "OWL spec with integrated strongly connected components"
    DGFlattening -> "flattening"
    DGTest -> "testing"
    DGAlignment -> "alignment"

instance Pretty DGOrigin where
  pretty :: DGOrigin -> Doc
pretty o :: DGOrigin
o = let prettySyms :: String -> Set a -> Doc
prettySyms headr :: String
headr syms :: Set a
syms = if Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
syms then Doc
Doc.empty
                   else String -> Doc
text String
headr Doc -> Doc -> Doc
$+$ Set a -> Doc
forall a. Pretty a => a -> Doc
pretty Set a
syms
    in String -> Doc
text (DGOrigin -> String
dgOriginHeader DGOrigin
o) Doc -> Doc -> Doc
<+> Maybe IRI -> Doc
forall a. Pretty a => a -> Doc
pretty (DGOrigin -> Maybe IRI
dgOriginSpec DGOrigin
o)
      Doc -> Doc -> Doc
$+$ case DGOrigin
o of
          DGFreeOrCofree forc :: FreeOrCofree
forc -> String -> Doc
text "FreeOrCofree:" Doc -> Doc -> Doc
<+> (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ FreeOrCofree -> String
forall a. Show a => a -> String
show FreeOrCofree
forc)
          DGInst iri :: IRI
iri -> String -> Doc
text "Inst:" Doc -> Doc -> Doc
<+> IRI -> Doc
forall a. Pretty a => a -> Doc
pretty IRI
iri
          DGFitView iri :: IRI
iri -> String -> Doc
text "View:" Doc -> Doc -> Doc
<+> IRI -> Doc
forall a. Pretty a => a -> Doc
pretty IRI
iri
          DGNormalForm node :: Int
node -> String -> Doc
text "Node:" Doc -> Doc -> Doc
<+> (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
node)
          DGBasicSpec mgbs :: Maybe G_basic_spec
mgbs _ syms :: Set G_symbol
syms -> case Maybe G_basic_spec
mgbs of
              Nothing -> Doc
Doc.empty
              Just gbs :: G_basic_spec
gbs -> Doc -> Doc
specBraces (G_basic_spec -> Doc
forall a. Pretty a => a -> Doc
pretty G_basic_spec
gbs)
            Doc -> Doc -> Doc
$+$ String -> Set G_symbol -> Doc
forall a. Pretty a => String -> Set a -> Doc
prettySyms "new symbols:" Set G_symbol
syms
          DGTranslation (Renamed r :: RENAMING
r) -> RENAMING -> Doc
forall a. Pretty a => a -> Doc
pretty RENAMING
r
          DGRestriction rst :: MaybeRestricted
rst syms :: Set G_symbol
syms -> let
              prtS :: Doc
prtS = String -> Set G_symbol -> Doc
forall a. Pretty a => String -> Set a -> Doc
prettySyms "hidden symbols:" Set G_symbol
syms
              in case MaybeRestricted
rst of
                Restricted r :: RESTRICTION
r -> RESTRICTION -> Doc
forall a. Pretty a => a -> Doc
pretty RESTRICTION
r Doc -> Doc -> Doc
$+$ Doc
prtS
                NoRestriction -> Doc
prtS
          v :: DGOrigin
v@DGOrigin
_ -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ DGOrigin -> String
forall a. Show a => a -> String
show DGOrigin
v

instance Pretty DGNodeInfo where
  pretty :: DGNodeInfo -> Doc
pretty c :: DGNodeInfo
c = case DGNodeInfo
c of
    DGNode {} -> DGOrigin -> Doc
forall a. Pretty a => a -> Doc
pretty (DGOrigin -> Doc) -> DGOrigin -> Doc
forall a b. (a -> b) -> a -> b
$ DGNodeInfo -> DGOrigin
node_origin DGNodeInfo
c
    DGRef {} ->
      IRI -> Doc
forall a. Pretty a => a -> Doc
pretty (LibName -> IRI
getLibId (LibName -> IRI) -> LibName -> IRI
forall a b. (a -> b) -> a -> b
$ DGNodeInfo -> LibName
ref_libname DGNodeInfo
c) Doc -> Doc -> Doc
<+> String -> Doc
text (Int -> String
showNodeId (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ DGNodeInfo -> Int
ref_node DGNodeInfo
c)

prettyDGNodeLab :: DGNodeLab -> Doc
prettyDGNodeLab :: DGNodeLab -> Doc
prettyDGNodeLab l :: DGNodeLab
l = [Doc] -> Doc
sep [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> String
getDGNodeName DGNodeLab
l, DGNodeInfo -> Doc
forall a. Pretty a => a -> Doc
pretty (DGNodeInfo -> Doc) -> DGNodeInfo -> Doc
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
l]

instance Pretty DGNodeLab where
  pretty :: DGNodeLab -> Doc
pretty l :: DGNodeLab
l = [Doc] -> Doc
vcat
    [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "xpath: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [XPathPart] -> String
showXPath ([XPathPart] -> [XPathPart]
forall a. [a] -> [a]
reverse ([XPathPart] -> [XPathPart]) -> [XPathPart] -> [XPathPart]
forall a b. (a -> b) -> a -> b
$ NodeName -> [XPathPart]
xpath (NodeName -> [XPathPart]) -> NodeName -> [XPathPart]
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
l)
    , ConsStatus -> Doc
forall a. Pretty a => a -> Doc
pretty (ConsStatus -> Doc) -> ConsStatus -> Doc
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> ConsStatus
getNodeConsStatus DGNodeLab
l
    , if DGNodeLab -> Bool
hasOpenGoals DGNodeLab
l then String -> Doc
text "has open goals" else
      if (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> DGNodeLab -> Bool
hasSenKind (Bool -> SenStatus a (AnyComorphism, BasicProof) -> Bool
forall a b. a -> b -> a
const Bool
True) DGNodeLab
l then Doc
Doc.empty else String -> Doc
text "locally empty"
    , if DGNodeLab -> Bool
labelHasHiding DGNodeLab
l then String -> Doc
text "has ingoing hiding link" else Doc
Doc.empty
    , case DGNodeLab -> Maybe Int
dgn_nf DGNodeLab
l of
        Nothing -> Doc
Doc.empty
        Just n :: Int
n -> String -> Doc
text "normal form:" Doc -> Doc -> Doc
<+> String -> Doc
text (Int -> String
showNodeId Int
n)
    , String -> Doc
text "origin:" Doc -> Doc -> Doc
$+$ DGNodeInfo -> Doc
forall a. Pretty a => a -> Doc
pretty (DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
l)
    , case DGNodeLab -> Maybe GMorphism
dgn_sigma DGNodeLab
l of
        Nothing -> Doc
Doc.empty
        Just gm :: GMorphism
gm -> String -> Doc
text "normal form inclusion:" Doc -> Doc -> Doc
$+$ GMorphism -> Doc
forall a. Pretty a => a -> Doc
pretty GMorphism
gm
    , String -> Doc
text "local theory:"
    , G_theory -> Doc
forall a. Pretty a => a -> Doc
pretty (G_theory -> Doc) -> G_theory -> Doc
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
l]

instance Pretty EdgeId where
   pretty :: EdgeId -> Doc
pretty (EdgeId i :: Int
i) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
i

dgLinkOriginSpec :: DGLinkOrigin -> Maybe IRI
dgLinkOriginSpec :: DGLinkOrigin -> Maybe IRI
dgLinkOriginSpec o :: DGLinkOrigin
o = case DGLinkOrigin
o of
    DGLinkMorph n :: IRI
n -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    DGLinkInst n :: IRI
n _ -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    DGLinkInstArg n :: IRI
n -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    DGLinkView n :: IRI
n _ -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    DGLinkFitView n :: IRI
n -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    DGLinkFitViewImp n :: IRI
n -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    DGLinkRefinement n :: IRI
n -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
n
    _ -> Maybe IRI
forall a. Maybe a
Nothing

dgLinkMapping :: DGLinkOrigin -> [G_mapping]
dgLinkMapping :: DGLinkOrigin -> [G_mapping]
dgLinkMapping o :: DGLinkOrigin
o = case DGLinkOrigin
o of
    DGLinkInst _ (Fitted l :: [G_mapping]
l) -> [G_mapping]
l
    DGLinkView _ (Fitted l :: [G_mapping]
l) -> [G_mapping]
l
    _ -> []

dgLinkOriginHeader :: DGLinkOrigin -> String
dgLinkOriginHeader :: DGLinkOrigin -> String
dgLinkOriginHeader o :: DGLinkOrigin
o = case DGLinkOrigin
o of
    SeeTarget -> "see target"
    DGLinkVerif -> "architectural verification condition"
    SeeSource -> "see source"
    DGImpliesLink -> "reversed implies link of extension"
    DGLinkExtension -> "extension"
    DGLinkTranslation -> "OMDoc translation"
    DGLinkClosedLenv -> "closed spec and local environment"
    DGLinkImports -> "OWL import"
    DGLinkIntersect -> "inclusion of intersection"
    DGLinkMorph _ -> "instantiation morphism of"
    DGLinkInst _ _ -> "instantiation of"
    DGLinkInstArg _ -> "actual parameter of"
    DGLinkView _ _ -> "view"
    DGLinkAlign _ -> "alignment"
    DGLinkFitView _ -> "fit source of"
    DGLinkFitViewImp _ -> "add import to source of"
    DGLinkProof -> "proof-link"
    DGLinkFlatteningUnion -> "flattening non-disjoint union"
    DGLinkFlatteningRename -> "flattening renaming"
    DGLinkRefinement _ -> "refinement"
    TEST -> "test"

instance Pretty DGLinkOrigin where
  pretty :: DGLinkOrigin -> Doc
pretty o :: DGLinkOrigin
o = String -> Doc
text (DGLinkOrigin -> String
dgLinkOriginHeader DGLinkOrigin
o) Doc -> Doc -> Doc
<+> Maybe IRI -> Doc
forall a. Pretty a => a -> Doc
pretty (DGLinkOrigin -> Maybe IRI
dgLinkOriginSpec DGLinkOrigin
o)
    Doc -> Doc -> Doc
$+$ [G_mapping] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas (DGLinkOrigin -> [G_mapping]
dgLinkMapping DGLinkOrigin
o)

-- | only shows the edge and node ids
showLEdge :: LEdge DGLinkLab -> String
showLEdge :: LEdge DGLinkLab -> String
showLEdge (s :: Int
s, t :: Int
t, l :: DGLinkLab
l) = "edge " String -> String -> String
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
l)
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGLinkLab -> String
dglName DGLinkLab
l
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
showNodeId Int
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " --> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

-- | only print the origin and parts of the type
prettyDGLinkLab :: (DGLinkLab -> Doc) -> DGLinkLab -> Doc
prettyDGLinkLab :: (DGLinkLab -> Doc) -> DGLinkLab -> Doc
prettyDGLinkLab f :: DGLinkLab -> Doc
f l :: DGLinkLab
l = [Doc] -> Doc
fsep
  [ case DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
l of
      SeeTarget -> Doc
Doc.empty
      o :: DGLinkOrigin
o -> DGLinkOrigin -> Doc
forall a. Pretty a => a -> Doc
pretty DGLinkOrigin
o
  , DGLinkLab -> Doc
f DGLinkLab
l ]

-- | print short edge information
prettyLEdge :: LEdge DGLinkLab -> Doc
prettyLEdge :: LEdge DGLinkLab -> Doc
prettyLEdge e :: LEdge DGLinkLab
e@(_, _, l :: DGLinkLab
l) = [Doc] -> Doc
fsep
  [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> String
showLEdge LEdge DGLinkLab
e
  , (DGLinkLab -> Doc) -> DGLinkLab -> Doc
prettyDGLinkLab (String -> Doc
text (String -> Doc) -> (DGLinkLab -> String) -> DGLinkLab -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> String
getDGLinkType) DGLinkLab
l
  , DGLinkType -> Doc
prettyThmLinkStatus (DGLinkType -> Doc) -> DGLinkType -> Doc
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l ]

dgRuleEdges :: DGRule -> [EdgeId]
dgRuleEdges :: DGRule -> [EdgeId]
dgRuleEdges r :: DGRule
r = case DGRule
r of
    DGRuleWithEdge _ l :: EdgeId
l -> [EdgeId
l]
    Composition ls :: [EdgeId]
ls -> [EdgeId]
ls
    _ -> []

dgRuleHeader :: DGRule -> String
dgRuleHeader :: DGRule -> String
dgRuleHeader r :: DGRule
r = case DGRule
r of
    DGRule str :: String
str -> String
str
    DGRuleWithEdge str :: String
str _ -> String
str
    DGRuleLocalInference _ -> "local-inference"
    Composition _ -> "composition"

instance Pretty DGRule where
  pretty :: DGRule -> Doc
pretty r :: DGRule
r = let es :: [EdgeId]
es = DGRule -> [EdgeId]
dgRuleEdges DGRule
r in [Doc] -> Doc
fsep
    [ String -> Doc
text (DGRule -> String
dgRuleHeader DGRule
r) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> if [EdgeId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EdgeId]
es then Doc
Doc.empty else Doc
colon, case DGRule
r of
    DGRuleLocalInference m :: [(String, String)]
m ->
        Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((String, String) -> Doc) -> [(String, String)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: String
t) ->
          let d :: Doc
d = String -> Doc
text String
s in if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
t then Doc
d else Doc -> Doc -> Doc
pairElems Doc
d (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
t) [(String, String)]
m
    _ -> case [EdgeId]
es of
      [] -> Doc
Doc.empty
      _ -> Set EdgeId -> Doc
forall a. Pretty a => a -> Doc
pretty (Set EdgeId -> Doc) -> Set EdgeId -> Doc
forall a b. (a -> b) -> a -> b
$ [EdgeId] -> Set EdgeId
forall a. Ord a => [a] -> Set a
Set.fromList [EdgeId]
es]

instance Pretty ThmLinkStatus where
  pretty :: ThmLinkStatus -> Doc
pretty tls :: ThmLinkStatus
tls = case ThmLinkStatus
tls of
        LeftOpen -> Doc
Doc.empty
        Proven r :: DGRule
r ls :: ProofBasis
ls -> let s :: Set EdgeId
s = ProofBasis -> Set EdgeId
proofBasis ProofBasis
ls in
          [Doc] -> Doc
fcat [Doc -> Doc
parens (DGRule -> Doc
forall a. Pretty a => a -> Doc
pretty DGRule
r), if Set EdgeId -> Bool
forall a. Set a -> Bool
Set.null Set EdgeId
s then Doc
Doc.empty else Set EdgeId -> Doc
forall a. Pretty a => a -> Doc
pretty Set EdgeId
s]

prettyThmLinkStatus :: DGLinkType -> Doc
prettyThmLinkStatus :: DGLinkType -> Doc
prettyThmLinkStatus = Doc -> (ThmLinkStatus -> Doc) -> Maybe ThmLinkStatus -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
Doc.empty ThmLinkStatus -> Doc
forall a. Pretty a => a -> Doc
pretty (Maybe ThmLinkStatus -> Doc)
-> (DGLinkType -> Maybe ThmLinkStatus) -> DGLinkType -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus

instance Pretty ConsStatus where
   pretty :: ConsStatus -> Doc
pretty (ConsStatus cons :: Conservativity
cons pc :: Conservativity
pc thm :: ThmLinkStatus
thm) = case Conservativity -> Conservativity -> Conservativity
forall a. Ord a => a -> a -> a
max Conservativity
cons Conservativity
pc of
     None -> Doc
Doc.empty
     c :: Conservativity
c -> String -> Doc
text (Conservativity -> String
forall a. Show a => a -> String
show Conservativity
c) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> ThmLinkStatus -> Doc
forall a. Pretty a => a -> Doc
pretty ThmLinkStatus
thm

instance Pretty DGLinkType where
    pretty :: DGLinkType -> Doc
pretty t :: DGLinkType
t = (case DGLinkType
t of
       FreeOrCofreeDefLink v :: FreeOrCofree
v _ -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ FreeOrCofree -> String
forall a. Show a => a -> String
show FreeOrCofree
v
       _ -> Doc
Doc.empty)
         Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (DGEdgeTypeModInc -> String
getDGEdgeTypeModIncName (DGEdgeTypeModInc -> String) -> DGEdgeTypeModInc -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc
getHomEdgeType Bool
False Bool
True DGLinkType
t)
               Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> DGLinkType -> Doc
prettyThmLinkStatus DGLinkType
t
               Doc -> Doc -> Doc
$+$ ConsStatus -> Doc
forall a. Pretty a => a -> Doc
pretty (DGLinkType -> ConsStatus
getLinkConsStatus DGLinkType
t)

instance Pretty DGLinkLab where
  pretty :: DGLinkLab -> Doc
pretty l :: DGLinkLab
l = let mor :: Doc
mor = GMorphism -> Doc
forall a. Pretty a => a -> Doc
pretty (GMorphism -> Doc) -> GMorphism -> Doc
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l in [Doc] -> Doc
vcat
    [ String -> Doc
text "Origin:" Doc -> Doc -> Doc
<+> DGLinkOrigin -> Doc
forall a. Pretty a => a -> Doc
pretty (DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
l)
    , String -> Doc
text "Type:" Doc -> Doc -> Doc
<+> DGLinkType -> Doc
forall a. Pretty a => a -> Doc
pretty (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l)
    , if DGLinkLab -> Bool
dglPending DGLinkLab
l then String -> Doc
text "proof chain incomplete" else Doc
Doc.empty
    , case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l of
        HidingFreeOrCofreeThm k :: Maybe FreeOrCofree
k n :: Int
n gm :: GMorphism
gm _ -> let nstr :: String
nstr = Int -> String
showNodeId Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":" in
          String -> Doc
text ("Signature morphism from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nstr)
          Doc -> Doc -> Doc
$+$ Doc
mor
          Doc -> Doc -> Doc
$+$ String -> Doc
text ("with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (case Maybe FreeOrCofree
k of
          Nothing -> "hiding"
          Just v :: FreeOrCofree
v -> (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FreeOrCofree -> String
forall a. Show a => a -> String
show FreeOrCofree
v))
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " morphism:") Doc -> Doc -> Doc
$+$ GMorphism -> Doc
forall a. Pretty a => a -> Doc
pretty GMorphism
gm
        _ -> String -> Doc
text "Signature morphism:" Doc -> Doc -> Doc
$+$ Doc
mor ]

-- | pretty print a labelled node
prettyGenLNode :: (a -> Doc) -> LNode a -> Doc
prettyGenLNode :: (a -> Doc) -> LNode a -> Doc
prettyGenLNode f :: a -> Doc
f (n :: Int
n, l :: a
l) = [Doc] -> Doc
fsep [String -> Doc
text (Int -> String
showNodeId Int
n) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, a -> Doc
f a
l]

prettyLNode :: LNode DGNodeLab -> Doc
prettyLNode :: LNode DGNodeLab -> Doc
prettyLNode = (DGNodeLab -> Doc) -> LNode DGNodeLab -> Doc
forall a. (a -> Doc) -> LNode a -> Doc
prettyGenLNode DGNodeLab -> Doc
prettyDGNodeLab

dgChangeType :: DGChange -> String
dgChangeType :: DGChange -> String
dgChangeType c :: DGChange
c = case DGChange
c of
    InsertNode _ -> "insert"
    DeleteNode _ -> "delete"
    InsertEdge _ -> "insert"
    DeleteEdge _ -> "delete"
    SetNodeLab _ _ -> "change"

instance Pretty DGChange where
  pretty :: DGChange -> Doc
pretty c :: DGChange
c = String -> Doc
text (DGChange -> String
dgChangeType DGChange
c) Doc -> Doc -> Doc
<+> case DGChange
c of
    InsertNode n :: LNode DGNodeLab
n -> LNode DGNodeLab -> Doc
prettyLNode LNode DGNodeLab
n
    DeleteNode n :: LNode DGNodeLab
n -> LNode DGNodeLab -> Doc
prettyLNode LNode DGNodeLab
n
    InsertEdge e :: LEdge DGLinkLab
e -> LEdge DGLinkLab -> Doc
prettyLEdge LEdge DGLinkLab
e
    DeleteEdge e :: LEdge DGLinkLab
e -> LEdge DGLinkLab -> Doc
prettyLEdge LEdge DGLinkLab
e
    SetNodeLab _ n :: LNode DGNodeLab
n -> LNode DGNodeLab -> Doc
prettyLNode LNode DGNodeLab
n

prettyGr :: Tree.Gr DGNodeLab DGLinkLab -> Doc
prettyGr :: Gr DGNodeLab DGLinkLab -> Doc
prettyGr g :: Gr DGNodeLab DGLinkLab
g = [Doc] -> Doc
vcat ((LNode DGNodeLab -> Doc) -> [LNode DGNodeLab] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LNode DGNodeLab -> Doc
prettyLNode ([LNode DGNodeLab] -> [Doc]) -> [LNode DGNodeLab] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr DGNodeLab DGLinkLab
g)
  Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((LEdge DGLinkLab -> Doc) -> [LEdge DGLinkLab] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> Doc
prettyLEdge ([LEdge DGLinkLab] -> [Doc]) -> [LEdge DGLinkLab] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr DGNodeLab DGLinkLab
g)

prettyImport :: MaybeNode -> Doc
prettyImport :: MaybeNode -> Doc
prettyImport imp :: MaybeNode
imp = case MaybeNode
imp of
  EmptyNode _ -> Doc
Doc.empty
  JustNode n :: NodeSig
n -> String -> Doc
keyword String
givenS Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty (NodeSig -> Int
getNode NodeSig
n)

prettyAllParams :: MaybeNode -> Doc
prettyAllParams :: MaybeNode -> Doc
prettyAllParams ps :: MaybeNode
ps = case MaybeNode
ps of
  EmptyNode _ -> Doc
Doc.empty
  JustNode n :: NodeSig
n -> Int -> Doc
forall a. Pretty a => a -> Doc
pretty (NodeSig -> Int
getNode NodeSig
n)

instance Pretty ExtGenSig where
  pretty :: ExtGenSig -> Doc
pretty (ExtGenSig (GenSig imp :: MaybeNode
imp params :: [NodeSig]
params allParamSig :: MaybeNode
allParamSig) body :: NodeSig
body) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    Int -> Doc
forall a. Pretty a => a -> Doc
pretty (NodeSig -> Int
getNode NodeSig
body) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
    (if [NodeSig] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NodeSig]
params then [] else
         [ [Int] -> Doc
forall a. Pretty a => a -> Doc
pretty ([Int] -> Doc) -> [Int] -> Doc
forall a b. (a -> b) -> a -> b
$ (NodeSig -> Int) -> [NodeSig] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> Int
getNode [NodeSig]
params
         , MaybeNode -> Doc
prettyAllParams MaybeNode
allParamSig ]) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
    [ MaybeNode -> Doc
prettyImport MaybeNode
imp ]

instance Pretty ExtViewSig where
  pretty :: ExtViewSig -> Doc
pretty (ExtViewSig src :: NodeSig
src gmor :: GMorphism
gmor ptar :: ExtGenSig
ptar) = [Doc] -> Doc
fsep
    [ Int -> Doc
forall a. Pretty a => a -> Doc
pretty (NodeSig -> Int
getNode NodeSig
src) Doc -> Doc -> Doc
<+> String -> Doc
text String
toS
    , ExtGenSig -> Doc
forall a. Pretty a => a -> Doc
pretty ExtGenSig
ptar
    , GMorphism -> Doc
forall a. Pretty a => a -> Doc
pretty GMorphism
gmor ]

instance Pretty UnitSig where
  pretty :: UnitSig -> Doc
pretty (UnitSig params :: [NodeSig]
params usig :: NodeSig
usig _) =
    (if [NodeSig] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NodeSig]
params then Doc
Doc.empty else [G_sign] -> Doc
forall a. Pretty a => a -> Doc
pretty ([G_sign] -> Doc) -> [G_sign] -> Doc
forall a b. (a -> b) -> a -> b
$ (NodeSig -> G_sign) -> [NodeSig] -> [G_sign]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> G_sign
getSig [NodeSig]
params)
    Doc -> Doc -> Doc
<+> G_sign -> Doc
forall a. Pretty a => a -> Doc
pretty (NodeSig -> G_sign
getSig NodeSig
usig)

instance Pretty ImpUnitSigOrSig where
  pretty :: ImpUnitSigOrSig -> Doc
pretty iu :: ImpUnitSigOrSig
iu = case ImpUnitSigOrSig
iu of
    ImpUnitSig imp :: MaybeNode
imp usig :: UnitSig
usig -> [Doc] -> Doc
fsep
      [ UnitSig -> Doc
forall a. Pretty a => a -> Doc
pretty UnitSig
usig, MaybeNode -> Doc
prettyImport MaybeNode
imp ]
    Sig n :: NodeSig
n -> String -> Doc
keyword String
specS Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty (NodeSig -> Int
getNode NodeSig
n)

instance Pretty RTNodeType where
 pretty :: RTNodeType -> Doc
pretty (RTPlain usig :: UnitSig
usig) = UnitSig -> Doc
forall a. Pretty a => a -> Doc
pretty UnitSig
usig
 pretty (RTRef n :: Int
n) = Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
n

instance Pretty RTNodeLab where
 pretty :: RTNodeLab -> Doc
pretty rlab :: RTNodeLab
rlab = [Doc] -> Doc
fsep [String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ RTNodeLab -> String
rtn_name RTNodeLab
rlab,
                     String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ RTNodeLab -> String
rtn_diag RTNodeLab
rlab,
                     RTNodeType -> Doc
forall a. Pretty a => a -> Doc
pretty (RTNodeType -> Doc) -> RTNodeType -> Doc
forall a b. (a -> b) -> a -> b
$ RTNodeLab -> RTNodeType
rtn_type RTNodeLab
rlab
                     ]

instance Pretty RefSig where
  pretty :: RefSig -> Doc
pretty = String -> Doc
text (String -> Doc) -> (RefSig -> String) -> RefSig -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefSig -> String
forall a. Show a => a -> String
show -- missing

instance Pretty AlignSig where
  pretty :: AlignSig -> Doc
pretty = String -> Doc
text (String -> Doc) -> (AlignSig -> String) -> AlignSig -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignSig -> String
forall a. Show a => a -> String
show -- missing

instance Pretty GlobalEntry where
  pretty :: GlobalEntry -> Doc
pretty ge :: GlobalEntry
ge = case GlobalEntry
ge of
    SpecEntry se :: ExtGenSig
se -> String -> Doc
topKey String
specS Doc -> Doc -> Doc
<+> ExtGenSig -> Doc
forall a. Pretty a => a -> Doc
pretty ExtGenSig
se
    ViewOrStructEntry b :: Bool
b ve :: ExtViewSig
ve -> String -> Doc
topKey (if Bool
b then String
viewS else String
structS)
      Doc -> Doc -> Doc
<+> ExtViewSig -> Doc
forall a. Pretty a => a -> Doc
pretty ExtViewSig
ve
    UnitEntry ue :: UnitSig
ue -> String -> Doc
topKey String
unitS Doc -> Doc -> Doc
<+> UnitSig -> Doc
forall a. Pretty a => a -> Doc
pretty UnitSig
ue
    AlignEntry ae :: AlignSig
ae -> AlignSig -> Doc
forall a. Pretty a => a -> Doc
pretty AlignSig
ae
    ArchOrRefEntry b :: Bool
b ae :: RefSig
ae -> (if Bool
b then String -> Doc
topKey String
archS else String -> Doc
keyword String
refinementS)
      Doc -> Doc -> Doc
<+> RefSig -> Doc
forall a. Pretty a => a -> Doc
pretty RefSig
ae
    _ -> Doc
Doc.empty

instance Pretty DGraph where
  pretty :: DGraph -> Doc
pretty dg :: DGraph
dg = [Doc] -> Doc
vcat
    [ Gr DGNodeLab DGLinkLab -> Doc
prettyGr (Gr DGNodeLab DGLinkLab -> Doc) -> Gr DGNodeLab DGLinkLab -> Doc
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
    , String -> Doc
text "global environment:"
    , (Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map IRI GlobalEntry
-> Doc
forall a b.
(Pretty a, Pretty b) =>
(Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
printMap Doc -> Doc
forall a. a -> a
id [Doc] -> Doc
vcat (\ k :: Doc
k v :: Doc
v -> [Doc] -> Doc
fsep [Doc
k Doc -> Doc -> Doc
<+> Doc
mapsto, Doc
v]) (Map IRI GlobalEntry -> Doc) -> Map IRI GlobalEntry -> Doc
forall a b. (a -> b) -> a -> b
$ DGraph -> Map IRI GlobalEntry
globalEnv DGraph
dg
    , String -> Doc
text "history:"
    , ProofHistory -> Doc
prettyHistory (ProofHistory -> Doc) -> ProofHistory -> Doc
forall a b. (a -> b) -> a -> b
$ ProofHistory -> ProofHistory
reverseHistory (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> ProofHistory
proofHistory DGraph
dg
    , String -> Doc
text "redoable history:"
    , ProofHistory -> Doc
prettyHistory (ProofHistory -> Doc) -> ProofHistory -> Doc
forall a b. (a -> b) -> a -> b
$ ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a
SizedList.reverse (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> a -> b
$ ProofHistory -> ProofHistory
reverseHistory (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> ProofHistory
redoHistory DGraph
dg
    , String -> Doc
text "next edge:" Doc -> Doc -> Doc
<+> EdgeId -> Doc
forall a. Pretty a => a -> Doc
pretty (DGraph -> EdgeId
getNewEdgeId DGraph
dg) ]

prettyHistElem :: HistElem -> Doc
prettyHistElem :: HistElem -> Doc
prettyHistElem he :: HistElem
he = case HistElem
he of
  HistElem c :: DGChange
c -> DGChange -> Doc
forall a. Pretty a => a -> Doc
pretty DGChange
c
  HistGroup r :: DGRule
r l :: ProofHistory
l -> String -> Doc
text "rule:" Doc -> Doc -> Doc
<+> DGRule -> Doc
forall a. Pretty a => a -> Doc
pretty DGRule
r Doc -> Doc -> Doc
$+$ Doc
space Doc -> Doc -> Doc
<+> ProofHistory -> Doc
prettyHistory ProofHistory
l

prettyHistory :: ProofHistory -> Doc
prettyHistory :: ProofHistory -> Doc
prettyHistory = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (ProofHistory -> [Doc]) -> ProofHistory -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HistElem -> Doc) -> [HistElem] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map HistElem -> Doc
prettyHistElem ([HistElem] -> [Doc])
-> (ProofHistory -> [HistElem]) -> ProofHistory -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofHistory -> [HistElem]
forall a. SizedList a -> [a]
SizedList.toList

prettyLibEnv :: LibEnv -> Doc
prettyLibEnv :: LibEnv -> Doc
prettyLibEnv = (Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> LibEnv -> Doc
forall a b.
(Pretty a, Pretty b) =>
(Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
printMap Doc -> Doc
forall a. a -> a
id [Doc] -> Doc
vsep Doc -> Doc -> Doc
($+$)