1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaModule : $Header$

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaMaintainer : maeder@tzi.de

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuStability : experimental

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaPortability : portable

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovapretty printing a HasCASL environment

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-}

99c3239092cab05eaca2f021e5edef2eab00ba01Christian Maeder

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovamodule HasCASL.PrintLe where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport HasCASL.As

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport HasCASL.AsUtils

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport HasCASL.PrintAs

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport HasCASL.Le

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport HasCASL.Builtin

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Id

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport qualified Common.Lib.Map as Map

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport qualified Common.Lib.Set as Set

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Keywords

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.PrettyPrint

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Result ()

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Data.List

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrettyPrint Morphism where

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder printText0 ga = toText ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrettyPrint Env where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printText0 ga = toText (addBuiltins ga) . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrettyPrint Sentence where

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder printText0 ga = toText (addBuiltins ga) . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrettyPrint SymbMapItems where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printText0 ga = toText ga . pretty

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrettyPrint SymbItems where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printText0 ga = toText ga . pretty

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrettyPrint RawSymbol where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printText0 ga = toText ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

1a38107941725211e7c3f051f7a8f5e12199f03acmaederinstance PrettyPrint Symbol where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printText0 ga = toText ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrintLaTeX Morphism where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printLatex0 ga = toLatex ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrintLaTeX Env where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printLatex0 ga = toLatex (addBuiltins ga) . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrintLaTeX Sentence where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printLatex0 ga = toLatex (addBuiltins ga) . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrintLaTeX SymbMapItems where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printLatex0 ga = toLatex ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrintLaTeX SymbItems where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printLatex0 ga = toLatex ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrintLaTeX RawSymbol where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printLatex0 ga = toLatex ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance PrintLaTeX Symbol where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova printLatex0 ga = toLatex ga . pretty

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance Pretty ClassInfo where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova pretty (ClassInfo rk ks) = case ks of

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova [] -> colon <+> pretty rk

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova _ -> text lessS <+> printList0 ks

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintGenKind :: GenKind -> Doc

printGenKind k = case k of

Loose -> empty

Free -> text freeS

Generated -> text generatedS

instance Pretty TypeDefn where

pretty td = case td of

NoTypeDefn -> empty

PreDatatype -> text "%(data type)%"

AliasTypeDefn s -> text assignS <+> printPseudoType s

DatatypeDefn dd -> text " %[" <> pretty dd <> text "]%"

printAltDefn :: Id -> [TypeArg] -> RawKind -> AltDefn -> Doc

printAltDefn dt tArgs rk (Construct mi ts p sels) = case mi of

Just i -> fcat $ [pretty i <> space, colon <> space,

pretty (createConstrType dt tArgs rk p ts)]

++ map (parens . semiDs) sels

Nothing -> text (typeS ++ sS) <+> commaDs ts

instance Pretty Selector where

pretty (Select mi t p) =

(case mi of

Just i -> pretty i <+> (case p of

Partial -> text (colonS++quMark)

Total -> colon) <> space

Nothing -> empty) <> pretty t

instance Pretty TypeInfo where

pretty (TypeInfo _ ks sups def) =

fsep $ [colon, printList0 ks]

++ (if Set.null sups then []

else [less, printList0 $ Set.toList sups])

++ case def of

NoTypeDefn -> []

_ -> [pretty def]

instance Pretty TypeVarDefn where

pretty (TypeVarDefn v vk _ i) =

printVarKind v vk <+> text ("%(var_" ++ shows i ")%")

instance Pretty VarDefn where

pretty (VarDefn ty) =

colon <+> pretty ty

instance Pretty ConstrInfo where

pretty (ConstrInfo i t) =

pretty i <+> colon <+> pretty t

instance Pretty OpDefn where

pretty od = case od of

NoOpDefn b -> text $ "%(" ++ shows b ")%"

ConstructData i -> text $ "%(construct " ++ showId i ")%"

SelectData c i -> text ("%(select from " ++ showId i " constructed by")

$+$ printList0 c <> text ")%"

Definition b t -> fsep [pretty $ NoOpDefn b, equals, pretty t]

instance Pretty OpInfo where

pretty o = let l = opAttrs o in

fsep $ [ colon

, pretty (opType o) <> if null l then empty else comma]

++ punctuate comma (map pretty l)

++ [pretty $ opDefn o]

instance Pretty OpInfos where

pretty (OpInfos l) = vcat $ map pretty l

instance Pretty DataEntry where

pretty (DataEntry im i k args rk alts) =

printGenKind k <+> keyword typeS <+>

fsep ([fcat $ pretty i : map (parens . pretty) args

, defn, vcat $ map (printAltDefn i args rk) alts]

++ if Map.null im then []

else [text withS, text (typeS ++ sS), printMap0 im])

instance Pretty Sentence where

pretty s = case s of

Formula t -> pretty t

DatatypeSen ls -> vcat (map pretty ls)

ProgEqSen _ _ pe -> keyword programS <+> pretty pe

instance Pretty Env where

pretty (Env{classMap=cm, typeMap=tm, localTypeVars=tvs,

assumps=ops, localVars=vs,

sentences=se, envDiags=ds}) =

let oops = foldr Map.delete ops $ map fst bList

otm = Map.difference tm $ addUnit Map.empty

header s = text "%%" <+> text s

<+> text (replicate (70 - length s) '-')

in noPrint (Map.null cm) (header "Classes")

$+$ printMap0 cm

$+$ noPrint (Map.null otm) (header "Type Constructors")

$+$ printMap0 otm

$+$ noPrint (Map.null tvs) (header "Type Variables")

$+$ printMap0 tvs

$+$ noPrint (Map.null oops) (header "Assumptions")

$+$ printMap0 oops

$+$ noPrint (Map.null vs) (header "Variables")

$+$ printMap0 vs

$+$ noPrint (null se) (header "Sentences")

$+$ vcat (map pretty $ reverse se)

$+$ noPrint (null ds) (header "Diagnostics")

$+$ vcat (map pretty $ reverse ds)

printMap0 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc

printMap0 = printMap []

printMap1 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc

printMap1 = printMap [mapsto]

printMap :: (Pretty a, Ord a, Pretty b) => [Doc] -> Map.Map a b -> Doc

printMap d m = vcat $ map (\ (a, b) -> fsep $

pretty a : d ++ [pretty b]) $ Map.toList m

instance Pretty Morphism where

pretty m =

let tm = typeIdMap m

fm = funMap m

ds = Map.foldWithKey ( \ (i, s) (j, t) l ->

(pretty i <+> colon <+> pretty s

<+> mapsto <+>

pretty j <+> colon <+> pretty t) : l)

[] fm

in (if Map.null tm then empty

else keyword (typeS ++ sS) <+> printMap0 tm)

$+$ (if Map.null fm then empty

else keyword (opS ++ sS) <+> fsep (punctuate comma ds))

$+$ colon <+> specBraces (pretty $ msource m)

$+$ mapsto

<+> specBraces (pretty $ mtarget m)

instance Pretty a => Pretty (SymbolType a) where

pretty t = case t of

OpAsItemType sc -> pretty sc

TypeAsItemType k -> pretty k

ClassAsItemType k -> pretty k

instance Pretty Symbol where

pretty s = keyword (case symType s of

OpAsItemType _ -> opS

TypeAsItemType _ -> typeS

ClassAsItemType _ -> classS) <+>

pretty (symName s) <+> colon <+>

pretty (symType s)

instance Pretty RawSymbol where

pretty rs = case rs of

AnID i -> pretty i

AKindedId k i -> printSK k <> pretty i

AQualId i t -> printSK (symbTypeToKind t) <> pretty i <+> colon

<+> pretty t

ASymbol s -> pretty s