PrintLe.hs revision c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian MaederMaintainer : maeder@tzi.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederpretty printing a HasCASL environment
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder-}
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.PrintLe where
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport HasCASL.HToken
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.Id
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederimport HasCASL.PrintAs
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederimport HasCASL.Le
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederimport Data.Maybe
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederimport Common.GlobalAnnotations
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport Common.PrettyPrint
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport Common.PPUtils
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport Common.Lib.Pretty as Pretty
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Common.Lib.Map as Map
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederimport Common.Keywords
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederinstance PrettyPrint ClassInfo where
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder printText0 ga (ClassInfo ks) =
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder space <> text lessS <+> printList0 ga ks
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederprintGenKind :: GenKind -> Doc
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederprintGenKind k = case k of
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Loose -> empty
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Free -> text freeS <> space
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Generated -> text generatedS <> space
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederinstance PrettyPrint TypeDefn where
986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian Maeder printText0 _ NoTypeDefn = empty
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 _ PreDatatype = space <> text "%(data type)%"
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 _ TypeVarDefn = space <> text "%(var)%"
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga (AliasTypeDefn s) = space <> text assignS
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> printPseudoType ga s
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga (Supertype v t f) = space <> text equalS <+>
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder braces (printText0 ga v
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> colon
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> printText0 ga t
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> text dotS
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> printText0 ga f)
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga (DatatypeDefn k args alts) = text " %[" <>
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printGenKind k <> (text typeS <+> text place
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> printList0 ga args
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> text defnS $$
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder vcat (map (printText0 ga) alts)) <> text "]%"
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederinstance PrettyPrint AltDefn where
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga (Construct i ts p sels) =
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga i <+> colon
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> listSep_text (space<>text funS<>space) ga ts <+>
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder text (case p of
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Partial -> funS ++ quMark
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Total -> funS) <+> text place
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> hcat (map (parens . printText0 ga) sels)
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederinstance PrettyPrint Selector where
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga (Select i t p) =
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga i <+> (case p of
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Partial -> text ":?"
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Total -> colon) <+> printText0 ga t
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederinstance PrettyPrint TypeInfo where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder printText0 ga (TypeInfo _ ks sups defn) =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder space <> colon <+> printList0 ga ks
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder <> noPrint (null sups)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (space <> text lessS <+> printList0 ga sups)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder <> printText0 ga defn
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederinstance PrettyPrint ConstrInfo where
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder printText0 ga (ConstrInfo i t) =
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder printText0 ga i <+> colon <+> printText0 ga t
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederinstance PrettyPrint OpDefn where
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 _ (NoOpDefn b) = space <> text ("%(" ++ show b ++ ")%")
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 _ VarDefn = space <> text "%(var)%"
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 _ (ConstructData i) = space <> text ("%(construct " ++
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder showId i ")%")
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 ga (SelectData c i) = space <> text ("%(select from " ++
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder showId i " constructed by")
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder $$ printList0 ga c <> text ")%"
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 ga (Definition b t) = printText0 ga (NoOpDefn b) <+>
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder text equalS <+> printText0 ga t
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederinstance PrettyPrint OpInfo where
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 ga o = space <> colon <+> printText0 ga (opType o)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder <> (case opAttrs o of
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder [] -> empty
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder l -> comma <> commaT_text ga l)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder <> printText0 ga (opDefn o)
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederinstance PrettyPrint OpInfos where
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 ga (OpInfos l) = vcat $ map (printText0 ga) l
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maederinstance PrettyPrint a => PrettyPrint (Maybe a) where
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder printText0 _ Nothing = empty
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder printText0 ga (Just c) = printText0 ga c
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederinstance PrettyPrint DatatypeDefn where
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder printText0 ga (DatatypeConstr i1 i2 k args alts) =
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder printGenKind k <> text typeS
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder <+> printText0 ga i1 <+> parens
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder (text mapsTo <+> printText0 ga i2)
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder <+> (printList0 ga args
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder <+> text defnS $$
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder vcat (map (printText0 ga) alts))
0205259ae45f1fc559cef00e69ca54a3aea10acaChristian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederinstance PrettyPrint Sentence where
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 ga s = case s of
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder Formula t -> printText0 ga t
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder DatatypeSen ls -> vcat (map (printText0 ga) ls)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder ProgEqSen _ _ pe -> text programS <+> printText0 ga pe
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederinstance PrettyPrint Env where
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder printText0 ga (Env{classMap=cm, typeMap=tm,
bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian Maeder assumps=as, sentences=se, envDiags=ds}) =
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder noPrint (Map.isEmpty cm) (header "Classes")
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder $$ printMap0 ga cm
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder $$ noPrint (Map.isEmpty tm) (header "Type Constructors")
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder $$ printMap0 ga tm
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder $$ noPrint (Map.isEmpty as) (header "Assumptions")
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder $$ printMap0 ga as
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder $$ noPrint (null se) (header "Sentences")
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder $$ vcat (map (printText0 ga) se)
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder $$ noPrint (null ds) (header "Diagnostics")
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder $$ vcat (map (printText0 ga) $ reverse ds)
where header s = text "%%" <+> text s
<+> text (replicate (70 - length s) '-')
printMap0 :: (PrettyPrint a, Ord a, PrettyPrint b)
=> GlobalAnnos -> Map.Map a b -> Doc
printMap0 g m =
let l = Map.toList m in
vcat(map (\ (a, b) -> printText0 g a
<> printText0 g b) l)
instance PrettyPrint SymbolType where
printText0 ga t = case t of
OpAsItemType sc -> printText0 ga sc
TypeAsItemType k -> printText0 ga k
ClassAsItemType k -> printText0 ga k
instance PrettyPrint Symbol where
printText0 ga s = text (case symType s of
OpAsItemType _ -> opS
TypeAsItemType _ -> typeS
ClassAsItemType _ -> classS) <+>
printText0 ga (symName s) <+> text colonS <+>
printText0 ga (symType s)
instance PrettyPrint RawSymbol where
printText0 ga rs = case rs of
AnID i -> printText0 ga i
AKindedId k i -> printSK k <> printText0 ga i
AQualId i t -> printSK (symbTypeToKind t) <> printText0 ga i <+> colon
<+> printText0 ga t