switched over to new Doc

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6478 cec4b9c1-7d33-0410-9eda-942365e851bb
spechub · Jun 22, 2006 · c438c79 · c438c79
1 parent 7d201e2
commit c438c79
Show file tree

Hide file tree

Showing 36 changed files with 859 additions and 844 deletions.
diff --git a/CASL/Inject.hs b/CASL/Inject.hs
@@ -9,7 +9,7 @@ Portability :  portable
 
 This module replaces Sorted_term(s) with explicit injection
    functions.  Don't do this after simplification since crucial sort
-   information may be missing 
+   information may be missing
 -}
 
 module CASL.Inject where
@@ -19,25 +19,25 @@ import CASL.Sign
 import CASL.Overload
 import CASL.Fold
 import Common.Id
-import Common.PrettyPrint
+import Common.Doc
 
 -- | the name of injections
 injName :: Id
 injName = mkId [mkSimpleId "g__inj"]
 
 inject :: Range -> TERM f -> SORT -> TERM f
 inject pos argument result_type = let argument_type = term_sort argument in
-    if argument_type == result_type then argument else 
+    if argument_type == result_type then argument else
     Application (injOpSymb pos argument_type result_type) [argument] nullRange
 
 injOpSymb :: Range -> SORT -> SORT -> OP_SYMB
 injOpSymb pos s1 s2 =
     Qual_op_name injName (Op_type Total [s1] s2 pos) pos
 
 injRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)
-injRecord mf = (mapRecord mf) 
+injRecord mf = (mapRecord mf)
      { foldApplication = \ _ o ts ps -> case o of
-         Qual_op_name _ ty _ -> Application o 
+         Qual_op_name _ ty _ -> Application o
              (zipWith (inject ps) ts $ args_OP_TYPE ty) ps
          _ -> error "injApplication"
      , foldSorted_term = \ _ st s ps -> inject ps st s
@@ -54,15 +54,15 @@ injFormula :: (f -> f) -> FORMULA f -> FORMULA f
 injFormula = foldFormula . injRecord
 
 
--- | takes a list of OP_SYMB generated by 
+-- | takes a list of OP_SYMB generated by
 -- 'CASL.AS_Basic_CASL.recover_Sort_gen_ax' and inserts these operations into
 -- the signature; unqualified OP_SYMBs yield an error
-insertInjOps ::(PrettyPrint f) => Sign f e -> [OP_SYMB] -> Sign f e
+insertInjOps ::(Pretty f) => Sign f e -> [OP_SYMB] -> Sign f e
 insertInjOps = foldl insOp
-    where insOp sign o = 
+    where insOp sign o =
               case o of
               (Qual_op_name i ot _)
-                  | i == injName -> 
+                  | i == injName ->
                        sign { opMap = addOpTo i (toOpType ot) (opMap sign)}
                   | otherwise -> sign
               _ -> error "CASL.Inject.insertInjOps: Wrong constructor."
diff --git a/CASL/MixfixParser.hs b/CASL/MixfixParser.hs
@@ -25,8 +25,9 @@ import Common.Id
 import qualified Common.Lib.Set as Set
 import qualified Common.Lib.Map as Map
 import Common.Earley
-import Common.ConvertLiteral
-import Common.PrettyPrint
+import Common.ConvertMixfixToken
+import Common.Doc
+import Common.DocUtils
 import Common.AS_Annotation
 import CASL.ShowMixfix
 import CASL.Print_AS_Basic()
@@ -234,7 +235,7 @@ addType tt t =
 -- | the type for mixfix resolution
 type MixResolve f = GlobalAnnos -> (Token -> [Rule], Rules) -> f -> Result f
 
-iterateCharts :: PrettyPrint f => (f -> f)
+iterateCharts :: Pretty f => (f -> f)
               -> MixResolve f -> GlobalAnnos -> [TERM f]
               -> Chart (TERM f) -> Chart (TERM f)
 iterateCharts par extR g terms c =
@@ -303,31 +304,31 @@ mkIdSets ops preds =
     in (f ops, f preds)
 
 -- | top-level resolution like 'resolveMixTrm' that fails in case of diags
-resolveMixfix :: PrettyPrint f => (f -> f)
+resolveMixfix :: Pretty f => (f -> f)
               -> MixResolve f -> MixResolve (TERM f)
 resolveMixfix par extR g ruleS t =
     let r@(Result ds _) = resolveMixTrm par extR g ruleS t
         in if null ds then r else Result ds Nothing
 
 -- | basic term resolution that supports recursion without failure
-resolveMixTrm :: PrettyPrint f => (f -> f)
+resolveMixTrm :: Pretty f => (f -> f)
               -> MixResolve f -> MixResolve (TERM f)
 resolveMixTrm par extR ga (adder, ruleS) trm =
         getResolved (showTerm par ga) (posOfTerm trm) toAppl
            $ iterateCharts par extR ga [trm] $ initChart adder ruleS
 
-showTerm :: PrettyPrint f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
-showTerm par ga = shows . printText0 ga . mapTerm par
+showTerm :: Pretty f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
+showTerm par ga = showGlobalDoc ga . mapTerm par
 
 -- | top-level resolution like 'resolveMixFrm' that fails in case of diags
-resolveFormula :: PrettyPrint f => (f -> f)
+resolveFormula :: Pretty f => (f -> f)
                -> MixResolve f -> MixResolve (FORMULA f)
 resolveFormula par extR g ruleS f =
     let r@(Result ds _) = resolveMixFrm par extR g ruleS f
         in if null ds then r else Result ds Nothing
 
 -- | basic formula resolution that supports recursion without failure
-resolveMixFrm :: PrettyPrint f => (f -> f)
+resolveMixFrm :: Pretty f => (f -> f)
               -> MixResolve f -> MixResolve (FORMULA f)
 resolveMixFrm par extR g ids frm =
     let self = resolveMixFrm par extR g ids

diff --git a/CASL/Morphism.hs b/CASL/Morphism.hs
@@ -32,7 +32,7 @@ import Control.Monad
 import Common.PrettyPrint
 import Control.Exception (assert)
 import Common.Doc
-import Common.DocUtils
+import Common.DocUtils ()
 import Common.Print_AS_Annotation
 
 data SymbType = OpAsItemType OpType
@@ -69,7 +69,7 @@ data RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id
                  deriving (Show, Eq, Ord)
 
 instance PosItem RawSymbol where
-    getRange rs = 
+    getRange rs =
         case rs of
         ASymbol s -> getRange s
         AnID i -> getRange i
@@ -395,8 +395,7 @@ legalMor mor =
   && isSubMapSet mpreds (predMap s2)
   && legalSign s2
 
-sigInclusion :: (PrettyPrint e, PrettyPrint f)
-             => Ext f e m -- ^ compute extended morphism
+sigInclusion :: Ext f e m -- ^ compute extended morphism
              -> (e -> e -> Bool) -- ^ subsignature test of extensions
              -> Sign f e -> Sign f e -> Result (Morphism f e m)
 sigInclusion extEm isSubExt sigma1 sigma2 =
@@ -487,7 +486,7 @@ instance Pretty Symbol where
     case symbType sy of
        SortAsItemType -> empty
        st -> space <> colon <> pretty st
-    
+
 
 instance PrettyPrint SymbType where
   -- op types try to place a question mark immediately after a colon
@@ -498,12 +497,12 @@ instance Pretty SymbType where
      OpAsItemType ot -> pretty ot
      PredAsItemType pt -> space <> pretty pt
      SortAsItemType -> empty
- 
+
 instance PrettyPrint Kind where
     printText0 ga = toText ga . pretty
 
 instance Pretty Kind where
-  pretty k = keyword $ case k of 
+  pretty k = keyword $ case k of
       SortKind -> sortS
       FunKind -> opS
       PredKind -> predS
@@ -519,21 +518,17 @@ instance Pretty RawSymbol where
 
 instance (PrettyPrint e, PrettyPrint f, PrettyPrint m) =>
     PrettyPrint (Morphism f e m) where
-        printText0 ga = toText ga . 
+        printText0 ga = toText ga .
           printMorphism (fromText ga) (fromText ga) (fromText ga)
 
 printMorphism :: (f->Doc) -> (e->Doc) -> (m->Doc) -> Morphism f e m -> Doc
 printMorphism fF fE fM mor =
-    printSymbolMap (Map.filterWithKey (/=) $ morphismToSymbMap mor)
+    pretty (Map.filterWithKey (/=) $ morphismToSymbMap mor)
     $+$ fM (extended_map mor) $+$ colon $+$
     specBraces (space <> printSign fF fE (msource mor) <> space)
-    $+$ text funS $+$ 
+    $+$ text funS $+$
     specBraces (space <> printSign fF fE (mtarget mor) <> space)
 
 instance (Pretty e, Pretty f, Pretty m) =>
     Pretty (Morphism f e m) where
        pretty = printMorphism pretty pretty pretty
-
-printSymbolMap :: SymbolMap -> Doc
-printSymbolMap = printMap specBraces (fsep . punctuate comma) 
-    (\ a b -> a <+> mapsto <+> b)
diff --git a/CASL/Overload.hs b/CASL/Overload.hs
@@ -30,7 +30,8 @@ import Common.Lib.State
 
 import Common.Id
 import Common.GlobalAnnotations
-import Common.PrettyPrint
+import Common.Doc
+import Common.DocUtils
 import Common.Result
 import Common.Partial
 
@@ -50,7 +51,7 @@ type Min f e = Sign f e -> f -> Result f
     + Definedness is handled by expanding the subterm.
     + Membership is handled like Cast
 -----------------------------------------------------------}
-minExpFORMULA :: PrettyPrint f => Min f e -> Sign f e -> FORMULA f
+minExpFORMULA :: Pretty f => Min f e -> Sign f e -> FORMULA f
               -> Result (FORMULA f)
 minExpFORMULA mef sign formula = case formula of
     Quantification q vars f pos -> do
@@ -101,7 +102,7 @@ minExpFORMULA mef sign formula = case formula of
     _ -> return formula -- do not fail even for unresolved cases
 
 -- | test if a term can be uniquely resolved
-oneExpTerm :: PrettyPrint f => Min f e -> Sign f e
+oneExpTerm :: Pretty f => Min f e -> Sign f e
            -> TERM f -> Result (TERM f)
 oneExpTerm minF sign term = do
     ts <- minExpTerm minF sign term
@@ -111,7 +112,7 @@ oneExpTerm minF sign term = do
     - Minimal expansion of an equation formula -
   see minExpTerm_cond
 -----------------------------------------------------------}
-minExpFORMULA_eq :: PrettyPrint f => Min f e -> Sign f e
+minExpFORMULA_eq :: Pretty f => Min f e -> Sign f e
                  -> (TERM f -> TERM f -> Range -> FORMULA f)
                  -> TERM f -> TERM f -> Range -> Result (FORMULA f)
 minExpFORMULA_eq mef sign eq term1 term2 pos = do
@@ -120,23 +121,23 @@ minExpFORMULA_eq mef sign eq term1 term2 pos = do
     is_unambiguous (globAnnos sign) (eq term1 term2 pos) ps pos
 
 -- | check if there is at least one solution
-hasSolutions :: PrettyPrint f => GlobalAnnos -> f -> [[f]] -> Range
+hasSolutions :: Pretty f => GlobalAnnos -> f -> [[f]] -> Range
              -> Result [[f]]
 hasSolutions ga topterm ts pos = let terms = filter (not . null) ts in
    if null terms then Result
-    [Diag Error ("no typing for: " ++ show (printText0 ga topterm))
+    [Diag Error ("no typing for: " ++ showGlobalDoc ga topterm "")
           pos] Nothing
     else return terms
 
 -- | check if there is a unique equivalence class
-is_unambiguous :: PrettyPrint f => GlobalAnnos -> f -> [[f]] -> Range
+is_unambiguous :: Pretty f => GlobalAnnos -> f -> [[f]] -> Range
                -> Result f
 is_unambiguous ga topterm ts pos = do
     terms <- hasSolutions ga topterm ts pos
     case terms of
         [ term : _ ] -> return term
         _ -> Result [Diag Error ("ambiguous term\n  " ++
-                showSepList (showString "\n  ") (shows . printText0 ga)
+                showSepList (showString "\n  ") (showGlobalDoc ga)
                 (take 5 $ map head terms) "") pos] Nothing
 
 checkIdAndArgs :: Id -> [a] -> Range -> Result Int
@@ -146,30 +147,30 @@ checkIdAndArgs ide args poss =
     in if isMixfix ide && pargs /= nargs then
     Result [Diag Error
        ("expected " ++ shows pargs " argument(s) of mixfix identifier '"
-         ++ showPretty ide "' but found " ++ shows nargs " argument(s)")
+         ++ showDoc ide "' but found " ++ shows nargs " argument(s)")
        poss] Nothing
     else return nargs
 
 
-noOpOrPred :: PrettyPrint t => [a] -> String -> Maybe t -> Id -> Range
+noOpOrPred :: Pretty t => [a] -> String -> Maybe t -> Id -> Range
            -> Int -> Result ()
 noOpOrPred ops str mty ide pos nargs =
     if null ops then case mty of
            Nothing -> Result [Diag Error
              ("no " ++ str ++ " with " ++ shows nargs " argument"
               ++ (if nargs == 1 then "" else "s") ++ " found for '"
-              ++ showPretty ide "'") pos] Nothing
+              ++ showDoc ide "'") pos] Nothing
            Just ty -> Result [Diag Error
              ("no " ++ str ++ " with profile '"
-              ++ showPretty ty "' found for '"
-              ++ showPretty ide "'") pos] Nothing
+              ++ showDoc ty "' found for '"
+              ++ showDoc ide "'") pos] Nothing
        else return ()
 
 {-----------------------------------------------------------
     - Minimal expansion of a predication formula -
     see minExpTerm_appl
 -----------------------------------------------------------}
-minExpFORMULA_pred :: PrettyPrint f => Min f e -> Sign f e -> Id
+minExpFORMULA_pred :: Pretty f => Min f e -> Sign f e -> Id
                    -> Maybe PredType -> [TERM f] -> Range
                    -> Result (FORMULA f)
 minExpFORMULA_pred mef sign ide mty args pos = do
@@ -208,7 +209,7 @@ qualify_pred ide pos (pred', terms') =
     Predication (Qual_pred_name ide (toPRED_TYPE pred') pos) terms' pos
 
 -- | expansions of an equation formula or a conditional
-minExpTerm_eq :: PrettyPrint f =>  Min f e -> Sign f e -> TERM f -> TERM f
+minExpTerm_eq :: Pretty f =>  Min f e -> Sign f e -> TERM f -> TERM f
               -> Result [[(TERM f, TERM f)]]
 minExpTerm_eq mef sign term1 term2 = do
     exps1 <- minExpTerm mef sign term1
@@ -231,7 +232,7 @@ minimize_eq s l = keepMinimals s (term_sort . snd) $
   * 'Application' terms are handled by 'minExpTerm_op'.
   * 'Conditional' terms are handled by 'minExpTerm_cond'.
 -----------------------------------------------------------}
-minExpTerm :: PrettyPrint f => Min f e -> Sign f e -> TERM f
+minExpTerm :: Pretty f => Min f e -> Sign f e -> TERM f
            -> Result [[TERM f]]
 minExpTerm mef sign top = let ga = globAnnos sign in case top of
     Qual_var var sort _ -> let ts = minExpTerm_var sign var (Just sort) in
@@ -273,7 +274,7 @@ minExpTerm_var sign tok ms = case Map.lookup tok $ varMap sign of
               Just s2 -> if s == s2 then qv else []
 
 -- | minimal expansion of an (possibly qualified) operator application
-minExpTerm_appl :: PrettyPrint f => Min f e -> Sign f e -> Id
+minExpTerm_appl :: Pretty f => Min f e -> Sign f e -> Id
                 -> Maybe OpType -> [TERM f] -> Range -> Result [[TERM f]]
 minExpTerm_appl mef sign ide mty args pos = do
     nargs <- checkIdAndArgs ide args pos
@@ -330,7 +331,7 @@ qualify_op ide pos (op', terms') =
   7. Transform each term in the minimized set into a qualified function
     application term.
 -----------------------------------------------------------}
-minExpTerm_op :: PrettyPrint f => Min f e -> Sign f e -> OP_SYMB -> [TERM f]
+minExpTerm_op :: Pretty f => Min f e -> Sign f e -> OP_SYMB -> [TERM f]
               -> Range -> Result [[TERM f]]
 minExpTerm_op mef sign (Op_name ide@(Id (tok:_) _ _)) args pos =
     let res = minExpTerm_appl mef sign ide Nothing args pos in
@@ -358,7 +359,7 @@ minExpTerm_op _ _ _ _ _ = error "minExpTerm_op"
   Finally transform the eq. classes into lists of
   conditionals with equally sorted terms.
 -----------------------------------------------------------}
-minExpTerm_cond :: PrettyPrint f => Min f e -> Sign f e
+minExpTerm_cond :: Pretty f => Min f e -> Sign f e
                 -> (TERM f -> TERM f -> a) -> TERM f -> TERM f -> Range
                 -> Result [[a]]
 minExpTerm_cond mef sign f term1 term2 pos = do

diff --git a/CASL/Print_AS_Basic.hs b/CASL/Print_AS_Basic.hs
@@ -28,26 +28,20 @@ import CASL.ToDoc
 
 instance (PrettyPrint b, PrettyPrint s, PrettyPrint f) =>
     PrettyPrint (BASIC_SPEC b s f) where
-    printText0 ga = Doc.toText ga . 
+    printText0 ga = Doc.toText ga .
          printBASIC_SPEC (fromText ga) (fromText ga) (fromText ga)
 
 instance (PrettyPrint b, PrettyPrint s, PrettyPrint f) =>
     PrettyPrint (BASIC_ITEMS b s f) where
-    printText0 ga = Doc.toText ga . 
+    printText0 ga = Doc.toText ga .
          printBASIC_ITEMS (fromText ga) (fromText ga) (fromText ga)
 
-
-printFormulaAux :: PrettyPrint f => GlobalAnnos -> [Annoted (FORMULA f)] -> Doc
-printFormulaAux ga f =
-  vcat $ map (printAnnotedFormula_Text0 ga True) f
-
-printAnnotedFormula_Text0 :: PrettyPrint f =>
-                             GlobalAnnos -> Bool -> Annoted (FORMULA f) -> Doc
-printAnnotedFormula_Text0 ga withDot = Doc.toText ga . Doc.printAnnoted 
-           ((if withDot then (Doc.bullet Doc.<+>) else id) . fromText ga)
+printAnnotedFormula :: Doc.Pretty f => Bool -> Annoted (FORMULA f) -> Doc.Doc
+printAnnotedFormula withDot = Doc.printAnnoted
+           ((if withDot then (Doc.bullet Doc.<+>) else id) . Doc.pretty)
 
 instance (PrettyPrint s, PrettyPrint f) => PrettyPrint (SIG_ITEMS s f) where
-    printText0 ga = Doc.toText ga . printSIG_ITEMS (fromText ga) (fromText ga) 
+    printText0 ga = Doc.toText ga . printSIG_ITEMS (fromText ga) (fromText ga)
 
 
 instance PrettyPrint f => PrettyPrint (SORT_ITEM f) where
@@ -96,12 +90,12 @@ instance PrettyPrint VAR_DECL where
 printFORMULA :: PrettyPrint f => GlobalAnnos -> FORMULA f -> Doc
 printFORMULA ga = Doc.toText ga . printFormula (fromText ga)
 
-printTheoryFormula :: PrettyPrint f => GlobalAnnos -> Named (FORMULA f) -> Doc
-printTheoryFormula ga f = printAnnotedFormula_Text0 ga
+printTheoryFormula :: Doc.Pretty f => Named (FORMULA f) -> Doc.Doc
+printTheoryFormula f = printAnnotedFormula
     (case sentence f of
     Quantification Universal _ _ _ -> False
     Sort_gen_ax _ _ -> False
-    _ -> True) $ Doc.fromLabelledSen f 
+    _ -> True) $ Doc.fromLabelledSen f
 
 instance PrettyPrint f => PrettyPrint (FORMULA f) where
     printText0 = printFORMULA