b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt{-|

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntModule : $Header$

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntCopyright : (c) C. Maeder, Uni Bremen 2002-2004

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntMaintainer : till@tzi.de

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntStability : provisional

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntPortability : non-portable(Logic)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt dumping a LibEnv

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-}

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntmodule Static.PrintDevGraph where

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Logic.Logic

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Logic.Grothendieck

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Syntax.AS_Library

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Syntax.Print_AS_Library

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.AS_Annotation

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.GlobalAnnotations

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport qualified Common.Lib.Map as Map

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Id

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.PrettyPrint

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.PPUtils

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Result

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Keywords

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Lib.Pretty as P

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Static.DevGraph

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Static.DGToSpec

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntinstance PrettyPrint LibEnv where

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt printText0 _ le = vcat (map (printLibrary le) $ Map.toList le)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntprintLibrary :: LibEnv -> (LIB_NAME, GlobalContext) -> Doc

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntprintLibrary le (ln, (ga, ge, dg)) =

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt text libraryS <+> printText0 ga ln $$

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt foldr (aboveWithNLs 2) P.empty

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt (map (printTheory le ln ga dg) $ Map.toList ge)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntprintTheory :: LibEnv -> LIB_NAME -> GlobalAnnos -> DGraph

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> (SIMPLE_ID, GlobalEntry) -> Doc

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntprintTheory le ln ga dg (sn, ge) = case ge of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt SpecEntry (_,_,_, e) -> case getNode e of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> P.empty

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just n -> case maybeResult $ computeTheory le ln dg n of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> P.empty

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just (G_theory lid sign sens) ->

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt text specS <+> printText0 ga sn $$

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt printText0 ga sign $$ text "" $$

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt vsep (map (print_named lid ga .

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mapNamed (simplify_sen lid sign)) sens)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> P.empty

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt