a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder{- |

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederModule : $Header$

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederDescription : pretty printing signatures

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederMaintainer : Christian.Maeder@dfki.de

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederStability : experimental

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederPortability : portable

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederpretty printing a HasCASL environment

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder-}

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maedermodule HasCASL.PrintLe (diffTypeMap, diffType, printMap1) where

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport HasCASL.As

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport HasCASL.PrintAs

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport HasCASL.Le

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport HasCASL.Builtin

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport HasCASL.ClassAna

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport Common.Doc

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport Common.DocUtils

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport qualified Data.Map as Map

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.Set as Set

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport Common.Keywords

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport Data.List

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederinstance Pretty ClassInfo where

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder pretty (ClassInfo rk ks) =

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder if Set.null ks then colon <+> pretty (rawToKind rk) else

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder text lessS <+> printList0 (Set.toList ks)

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian MaederprintGenKind :: GenKind -> Doc

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian MaederprintGenKind k = case k of

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Loose -> empty

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Free -> text freeS

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Generated -> text generatedS

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederinstance Pretty TypeDefn where

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder pretty td = case td of

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder NoTypeDefn -> empty

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder PreDatatype -> text "%(data type)%"

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder AliasTypeDefn s -> text assignS <+> pretty s

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder DatatypeDefn dd -> text "%[" <> pretty dd <> text "]%"

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder

06f58a67e6df999858bf4f97d5e0786956562d29Christian MaederprintAltDefn :: AltDefn -> Doc

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian MaederprintAltDefn (Construct mi ts p sels) = case mi of

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Just i -> pretty i <+> fsep (map (parens . semiDs) sels) <> pretty p

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Nothing -> text (typeS ++ sS) <+> ppWithCommas ts

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederinstance Pretty Selector where

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder pretty (Select mi t p) =

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder (case mi of

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder Just i -> pretty i <+> case p of

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Partial -> text colonQuMark

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Total -> colon

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Nothing -> empty) <+> pretty t

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederinstance Pretty TypeInfo where

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder pretty (TypeInfo _ _ _ def) = pretty def

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederinstance Pretty TypeVarDefn where

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder pretty (TypeVarDefn v vk _ i) =

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

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederinstance Pretty VarDefn where

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder pretty (VarDefn ty) =

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder colon <+> pretty ty

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maederinstance Pretty ConstrInfo where

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder pretty (ConstrInfo i t) =

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder pretty i <+> colon <+> pretty t

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederinstance Pretty OpDefn where

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder pretty od = case od of

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

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder ConstructData _ -> text "%(constructor)%"

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder SelectData cs _ -> sep

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder [ text "%(selector of constructor(s)"

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , printList0 (Set.toList cs) <> text ")%" ]

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder Definition b t ->

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder sep [text $ "%[" ++ shows b "=", pretty t <> text "]%" ]

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederinstance Pretty OpInfo where

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder pretty o = sep [pretty $ opType o, pretty $ opDefn o]

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederinstance Pretty DataEntry where

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder pretty (DataEntry im i k args _ alts) =

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder printGenKind k <+> keyword typeS <+>

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

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder , defn, cat $ punctuate (space <> bar <> space)

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder $ map printAltDefn $ Set.toList alts]

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder ++ if Map.null im then []

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder else [text withS, text (typeS ++ sS), printMap1 im])

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maederinstance Pretty Sentence where

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder pretty s = case s of

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Formula t -> (case t of

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder QuantifiedTerm Universal (_ : _) _ _ -> id

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder _ -> addBullet) $ pretty t

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder DatatypeSen ls -> vcat (map pretty ls)

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder ProgEqSen _ _ pe -> keyword programS <+> pretty pe

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederinstance Pretty Env where

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder pretty Env

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder { classMap = cm

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , typeMap = tm

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , localTypeVars = tvs

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , assumps = ops

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , localVars = vs

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , sentences = se

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , envDiags=ds } = let

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder oops = foldr Map.delete ops $ map fst bList

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder otm = diffTypeMap cm tm bTypes

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder ltm = concatMap ( \ (i, ti) -> map ( \ k -> (i, k))

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder $ Set.toList $ otherTypeKinds ti) $ Map.toList otm

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder stm = concatMap ( \ (i, ti) -> map ( \ s -> (i, s))

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder $ Set.toList $ superTypes ti) $ Map.toList otm

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder atm = Map.filter ( \ td -> case typeDefn td of

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder AliasTypeDefn _ -> True

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder _ -> False) otm

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder scm = concatMap ( \ (i, ci) -> map ( \ s -> (i, s))

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder $ Set.toList $ Set.delete (rawToKind $ rawKind ci) $ classKinds ci)

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder $ Map.toList cm

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder mkPlural s = if last s == 's' then s ++ "es" else s ++ "s"

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder header2 l s = keyword $ case l of

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder _ : _ : _ -> mkPlural s

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder _ -> s

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder header m s = keyword $

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder if Map.size m < 2 then s else mkPlural s

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder in noPrint (Map.null cm) (header cm classS)

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder $+$ printMap0 (Map.map ( \ ci -> ci { classKinds = Set.empty }) cm)

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder $+$ noPrint (null scm) (header2 scm classS)

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder $+$ vcat (punctuate semi $ map ( \ (i, s) ->

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder pretty i <+> text lessS <+> pretty s) scm)

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder $+$ noPrint (null ltm) (header2 ltm typeS)

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder $+$ vcat (punctuate semi $ map ( \ (i, k) ->

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder pretty i <+> colon <+> pretty k) ltm)

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder $+$ noPrint (null stm) (header2 stm typeS)

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder $+$ vcat (punctuate semi $ map ( \ (i, s) ->

pretty i <+> text lessS <+> pretty s) stm)

$+$ noPrint (Map.null atm) (header atm typeS)

$+$ printMap0 atm

$+$ noPrint (Map.null tvs) (header tvs varS)

$+$ printMap0 tvs

$+$ printSetMap (keyword opS) space oops

$+$ noPrint (Map.null vs) (header vs varS)

$+$ printMap0 vs

$+$ vcat (map (pretty . fromLabelledSen) $ reverse se)

$+$ vcat (map pretty $ reverse ds)

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

printMap0 = printMap id (vcat . punctuate semi) ( \ a b -> fsep $ a : [b])

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

printMap1 = printMap id vcat ( \ a b -> fsep $ a : mapsto : [b])

instance Pretty Morphism where

pretty m =

let tm = typeIdMap m

fm = funMap m

-- the types in funs are already mapped

-- key und value types only differ wrt. partiality

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

(pretty i <+> mapsto <+>

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

[] fm

in (if Map.null tm then empty

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

$+$ (if Map.null fm then empty

else keyword (opS ++ sS) <+> sepByCommas 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 [i] <> pretty i

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

<+> pretty t

ASymbol s -> pretty s

diffTypeMap :: ClassMap -> TypeMap -> TypeMap -> TypeMap

diffTypeMap cm t1 t2 =

let t = Map.differenceWith (diffType cm) t1 t2

r = Set.intersection $ Set.union (Map.keysSet t) $ Map.keysSet bTypes

in Map.map ( \ ti -> ti { superTypes = r $ superTypes ti }) t

-- | compute difference of type infos

diffType :: ClassMap -> TypeInfo -> TypeInfo -> Maybe TypeInfo

diffType cm ti1 ti2 =

let k1 = otherTypeKinds ti1

k2 = otherTypeKinds ti2

ks = Set.filter (\ k -> Set.null $

Set.filter (lesserKind cm k) k2) k1

in if Set.null ks then Nothing else

Just $ ti1 { otherTypeKinds = ks

, superTypes = Set.difference (superTypes ti1) $

superTypes ti2 }