switched to Common.Doc.Pretty

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6181 cec4b9c1-7d33-0410-9eda-942365e851bb

Comorphisms/HasCASL2IsabelleHOL.hs

@@ -20,7 +20,6 @@ import qualified Common.Lib.Map as Map
 import Data.List
 import Data.Maybe
 import Common.AS_Annotation (Named(..))
-import Common.PrettyPrint
 
 -- HasCASL
 import HasCASL.Logic_HasCASL

HasCASL/As.der.hs

@@ -215,23 +215,10 @@ data Component = Selector UninstOpId Partiality Type SeparatorKind Range
 
 -- | the possible quantifiers
 data Quantifier = Universal | Existential | Unique
-                  deriving (Eq, Ord)
-
-instance Show Quantifier where
-    show q = case q of
-        Universal -> forallS
-        Existential -> existsS
-        Unique -> existsUnique
+                  deriving (Eq, Ord, Show)
 
 -- | the possibly type annotations of terms
-data TypeQual = OfType | AsType | InType | Inferred deriving (Eq, Ord)
-
-instance Show TypeQual where
-    show q = case q of
-        OfType -> colonS
-        AsType -> asS
-        InType -> inS
-        Inferred -> colonS
+data TypeQual = OfType | AsType | InType | Inferred deriving (Eq, Ord, Show)
 
 -- | an indicator of (otherwise equivalent) let or where equations
 data LetBrand = Let | Where | Program deriving (Show, Eq, Ord)

HasCASL/AsUtils.hs

@@ -16,7 +16,9 @@ module HasCASL.AsUtils where
 import HasCASL.As
 import Common.Id
 import Common.Keywords
-import Common.PrettyPrint
+import Common.Doc
+import qualified Common.Lib.Pretty as Pretty
+import Common.GlobalAnnotations
 import qualified Common.Lib.Set as Set
 
 -- | the string for the universe type
@@ -304,8 +306,14 @@ toKind vk = case vk of
         _ -> error "toKind: Downset"
     MissingKind -> error "toKind: Missing"
 
+showPretty :: Pretty a => a -> ShowS
+showPretty = shows . toOldDoc . pretty
+
+toOldDoc :: Doc -> Pretty.Doc
+toOldDoc = toText emptyGlobalAnnos
+
 -- | generate a comparison string
-expected :: PrettyPrint a => a -> a -> String
+expected :: Pretty a => a -> a -> String
 expected a b =
     "\n  expected: " ++ showPretty a
     "\n     found: " ++ showPretty b "\n"

HasCASL/ClassAna.hs

@@ -17,10 +17,10 @@ import HasCASL.AsUtils
 import HasCASL.PrintAs()
 import Common.Id
 import HasCASL.Le
-import Common.PrettyPrint
 import qualified Common.Lib.Map as Map
 import Common.Lib.State
 import Common.Result
+import Common.Doc
 
 -- * analyse kinds
 
@@ -104,15 +104,15 @@ invertVariance v = case v of
 -- * diagnostic messages
 
 -- | create message for different kinds 
-diffKindDiag :: (PosItem a, PrettyPrint a) => 
+diffKindDiag :: (PosItem a, Pretty a) => 
                  a -> RawKind -> RawKind -> [Diagnosis]
 diffKindDiag a k1 k2 = 
            [ Diag Error
               ("incompatible kind of: " ++ showPretty a "" ++ expected k1 k2)
             $ getRange a ]
 
 -- | check if raw kinds are equal
-checkKinds :: (PosItem a, PrettyPrint a) => 
+checkKinds :: (PosItem a, Pretty a) => 
               a -> RawKind -> RawKind -> [Diagnosis]
 checkKinds p k1 k2 =
        if k1 == k2 then []

HasCASL/Constrain.hs

@@ -8,7 +8,6 @@ Stability   :  experimental
 Portability :  portable 
 
 constraint resolution
-
 -}
 
 module HasCASL.Constrain where
@@ -24,11 +23,10 @@ import qualified Common.Lib.Set as Set
 import qualified Common.Lib.Map as Map
 import qualified Common.Lib.Rel as Rel
 import Common.Lib.State
-import Common.PrettyPrint
-import Common.Lib.Pretty
-import Common.Keywords
+import qualified Common.PrettyPrint as PP
 import Common.Id
 import Common.Result
+import Common.Doc
 
 import Control.Exception(assert)
 
@@ -39,12 +37,13 @@ data Constrain = Kinding Type Kind
                | Subtyping Type Type 
                  deriving (Eq, Ord, Show)
 
-instance PrettyPrint Constrain where
-    printText0 ga c = case c of 
-       Kinding ty k -> printText0 ga ty <+> colon 
-                                      <+> printText0 ga k
-       Subtyping t1 t2 -> printText0 ga t1 <+> text lessS
-                                      <+> printText0 ga t2
+instance PP.PrettyPrint Constrain where
+    printText0 ga = toText ga . pretty 
+
+instance Pretty Constrain where
+    pretty c = case c of 
+       Kinding ty k -> fsep [pretty ty, colon, pretty k]
+       Subtyping t1 t2 -> fsep [pretty t1, less, pretty t2]
 
 instance PosItem Constrain where
   getRange c = case c of 
@@ -86,7 +85,8 @@ entail te p =
 
 byInst :: Monad m => TypeEnv -> Constrain -> m Constraints
 byInst te c = let cm = classMap te in case c of 
-    Kinding ty k -> if k == universe then assert (rawKindOfType ty == ClassKind ())
+    Kinding ty k -> if k == universe then 
+                        assert (rawKindOfType ty == ClassKind ())
                     $ return noC else 
       let Result _ds mk = inferKinds (Just True) ty te in
                    case mk of 
@@ -97,7 +97,8 @@ byInst te c = let cm = classMap te in case c of
                              else fail $ "constrain '" ++ 
                                   showPretty c "' is unprovable"
                                   ++ "\n  known kinds are: " ++
-                                  showPretty ks ""
+                                  concat (intersperse ", " $ 
+                                          map (flip showPretty "") ks) 
     Subtyping t1 t2 -> if lesserType te t1 t2 then return noC
                        else fail ("unable to prove: " ++ showPretty t1 " < " 
                                   ++ showPretty t2 "")
@@ -326,5 +327,4 @@ fromTypeMap :: TypeMap -> Rel.Rel Type
 fromTypeMap = Map.foldWithKey (\ t ti r -> let k = typeKind ti in
                     Set.fold ( \ j -> Rel.insert (TypeName t k 0)
                                 $ TypeName j k 0) r
-                                    $ superTypes ti) Rel.empty 
-
+                                    $ superTypes ti) Rel.empty

HasCASL/Logic_HasCASL.hs

@@ -23,7 +23,6 @@ import HasCASL.Symbol
 import HasCASL.ParseItem
 import HasCASL.Morphism
 import HasCASL.ATC_HasCASL()
-import HasCASL.LaTeX_HasCASL()
 import HasCASL.SymbolMapAnalysis
 import HasCASL.Sublogic
 import HasCASL.SimplifyTerm

HasCASL/Merge.hs

@@ -13,7 +13,7 @@ merging parts of local environment
 module HasCASL.Merge where
 
 import Common.Id
-import Common.PrettyPrint
+import Common.Doc
 import Common.Result
 
 import HasCASL.As
@@ -34,17 +34,17 @@ import Data.List
 class Mergeable a where
     merge :: a -> a -> Result a 
 
-instance (Ord a, PosItem a, PrettyPrint a, Mergeable b) 
+instance (Ord a, PosItem a, Pretty a, Mergeable b) 
     => Mergeable (Map.Map a b) where
     merge = mergeMap id merge
 
-improveDiag :: (PosItem a, PrettyPrint a) => a -> Diagnosis -> Diagnosis
+improveDiag :: (PosItem a, Pretty a) => a -> Diagnosis -> Diagnosis
 improveDiag v d = d { diagString = let f:l = lines $ diagString d in 
                       unlines $ (f ++ " of '" ++ showPretty v "'") : l
                     , diagPos = getRange v
                     }
 
-mergeMap :: (Ord a, PosItem a, PrettyPrint a) => 
+mergeMap :: (Ord a, PosItem a, Pretty a) => 
             (b -> b) -> (b -> b -> Result b) 
          -> Map.Map a b -> Map.Map a b -> Result  (Map.Map a b)
 mergeMap e f m1 m2 = foldM ( \ m (k, v) -> 
@@ -69,7 +69,7 @@ instance Mergeable a => Mergeable (Maybe a) where
 instance Mergeable ClassInfo where
     merge = mergeA "super classes"
 
-instance (PrettyPrint a, Eq a) => Mergeable (AnyKind a) where
+instance (Pretty a, Eq a) => Mergeable (AnyKind a) where
     merge = mergeA "super kinds" 
 
 mergeTypeInfo :: TypeInfo -> TypeInfo -> Result TypeInfo 
@@ -191,7 +191,7 @@ instance Mergeable Env where
                              , typeMap = tMap
                              , assumps = as }
 
-mergeA :: (PrettyPrint a, Eq a) => String -> a -> a -> Result a
+mergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
 mergeA str t1 t2 = if t1 == t2 then return t1 else 
     fail ("different " ++ str ++ expected t1 t2)
 

HasCASL/MixAna.hs

@@ -24,7 +24,7 @@ import qualified Common.Lib.Set as Set
 
 import HasCASL.As
 import HasCASL.AsUtils
-import HasCASL.PrintAs
+import HasCASL.PrintAs()
 import HasCASL.Unify
 import HasCASL.VarDecl
 import HasCASL.Le
@@ -202,7 +202,7 @@ resolver isPat ga trm =
                  $ Set.union (Rel.keysSet ass) $ Rel.keysSet vs
        chart <- iterateCharts ga [trm] $ initChart addRule ruleS
        let Result ds mr = getResolved
-              (shows . printTerm emptyGlobalAnnos . parenTerm) (getRange trm)
+              (showPretty . parenTerm) (getRange trm)
                           toMixTerm chart
        addDiags ds
        if isPat then case mr of