{- |

Module : $Header$

Description : pretty printing signatures

Copyright : (c) Christian Maeder, Uni Bremen, DFKI GmbH 2002-2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : experimental

Portability : portable

pretty printing a HasCASL environment

-}

module HasCASL.PrintLe

( diffClass

, diffClassMap

, mergeClassInfo

, mergeClassMap

, addClassMap

, addCpoMap

, minimizeClassMap

, mergeMap

, improveDiag

, diffTypeMap

, diffType

, printMap1

, mostSyms

, delPreDefs

) where

import HasCASL.As

import HasCASL.AsUtils

import HasCASL.PrintAs

import HasCASL.Le

import HasCASL.Builtin

import HasCASL.ClassAna

import Common.AS_Annotation

import Common.Doc

import Common.DocUtils

import Common.Id

import qualified Data.Map as Map

import qualified Data.Set as Set

import Common.Keywords

import Common.Result

import Control.Monad (foldM)

import Data.List

import Data.Maybe

instance Pretty ClassInfo where

pretty (ClassInfo rk ks) = less <+>

if Set.null ks then pretty (rawToKind rk) else

printList0 (Set.toList ks)

printGenKind :: 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 <+> pretty s

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

printAltDefn :: AltDefn -> Doc

printAltDefn (Construct mi ts p sels) = case mi of

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

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

instance Pretty Selector where

pretty (Select mi t p) = let d = pretty t in case mi of

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

Partial -> text colonQuMark

<+> if isSimpleType t then d else parens d

Total -> colon

<+> if isPrefixOf "?" $ show d then parens d else d

Nothing -> d

instance Pretty TypeInfo where

pretty (TypeInfo _ _ _ def) = 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 _ -> empty

ConstructData _ -> text "%(constructor)%"

SelectData cs _ -> sep

[ text "%(selector of constructor(s)"

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

Definition b t ->

sep [text $ "%[ " ++ if isPred b then "<=>" else "="

, pretty t <+> text "]%" ]

isOpDefn :: OpBrand -> OpDefn -> Bool

isOpDefn b od = case od of

NoOpDefn c -> c == b

Definition c _ -> c == b

_ -> False

isPredOpDefn :: OpDefn -> Bool

isPredOpDefn = isOpDefn Pred

isFunOpDefn :: OpDefn -> Bool

isFunOpDefn = isOpDefn Fun

instance Pretty OpInfo where

pretty o = let od = opDefn o in

sep [pretty $ (if isPredOpDefn od then unPredTypeScheme else id)

$ opType o, pretty od]

instance Pretty DataEntry where

pretty (DataEntry im j k args _ talts) = let

i = Map.findWithDefault j j im

mapAlt (Construct mi tys p sels) = Construct mi

(map (mapType im) tys) p $ map (map mapSel) sels

mapSel (Select mi ty p) = Select mi (mapType im ty) p

alts = Set.map mapAlt talts

in printGenKind k <+> keyword typeS <+>

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

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

$ map printAltDefn $ Set.toList alts]

instance Pretty Sentence where

pretty s = case s of

Formula t -> (case t of

QuantifiedTerm Universal (_ : _) _ _ -> id

_ -> addBullet) $ pretty t

DatatypeSen ls -> vcat (map pretty ls)

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

delPreDefs :: Env -> Env

delPreDefs e =

let cm = classMap e

tm = typeMap e

ops = assumps e

ocm = diffClassMap cm cpoMap

in e

{ classMap = ocm

, typeMap = diffTypeMap ocm tm bTypes

, assumps = foldr (Map.delete . fst) ops bList }

getSuperClasses :: ClassMap -> [(Id, Kind)]

getSuperClasses = concatMap

( \ (i, ci) -> map ( \ s -> (i, s))

. Set.toList $ Set.delete (rawToKind $ rawKind ci) $ classKinds ci)

. Map.toList

getSuperTypes :: TypeMap -> [(Id, Id)]

getSuperTypes = concatMap

( \ (i, ti) -> map ( \ s -> (i, s))

. Set.toList $ superTypes ti)

. Map.toList

getTypeKinds :: TypeMap -> [(Id, Kind)]

getTypeKinds = concatMap

( \ (i, ti) -> map ( \ k -> (i, k))

. Set.toList $ otherTypeKinds ti)

. Map.toList

getTypeAliases :: TypeMap -> [(Id, Type)]

getTypeAliases = foldr

( \ (i, td) -> case typeDefn td of

AliasTypeDefn ty -> ((i, ty) :)

_ -> id) [] . Map.toList

instance Pretty Env where

pretty env = let

d = delPreDefs env

cm = classMap d

tm = typeMap d

tvs = localTypeVars d

vs = localVars d

poMap = Map.map (Set.partition (isPredOpDefn . opDefn)) $ assumps d

pMap = Map.map fst poMap

aoMap = Map.map snd poMap

foMap = Map.map (Set.partition (isFunOpDefn . opDefn)) aoMap

fMap = Map.map fst foMap

oMap = Map.map snd foMap

ltm = getTypeKinds tm

stm = getSuperTypes tm

atm = getTypeAliases tm

scm = getSuperClasses cm

bas = map (\ (b, o) -> Unparsed_anno (Annote_word "binder")

(Line_anno $ " " ++ show b ++ ", " ++ show o) $ posOfId b)

$ Map.toList $ binders d

mkPlural s = s ++ if last s == 's' then "es" else "s"

header2 l s = keyword $ case l of

_ : _ : _ -> mkPlural s

_ -> s

header m s = keyword $

if Map.size m < 2 then s else mkPlural s

in noPrint (Map.null cm) (header cm classS)

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

$+$ noPrint (null scm) (header2 scm classS)

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

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

$+$ noPrint (null ltm) (header2 ltm typeS)

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

pretty i <+> colon <+> pretty k) ltm)

$+$ noPrint (null stm) (header2 stm typeS)

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

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

$+$ noPrint (null atm) (header2 atm typeS)

$+$ printAliasTypes atm

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

$+$ printMap0 tvs

$+$ vcat (map annoDoc bas)

$+$ printSetMap (keyword opS) space oMap

$+$ printSetMap (keyword predS) space pMap

$+$ printSetMap (keyword functS) space fMap

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

$+$ printMap0 vs

$+$ vcat (map (pretty . fromLabelledSen) . reverse $ sentences d)

$+$ vcat (map pretty . reverse $ envDiags d)

mostSyms :: Env -> [Symbol]

mostSyms e = let

d = delPreDefs e

cm = classMap d

tm = typeMap d

in map (\ (i, k) -> idToClassSymbol i $ rawKind k) (Map.toList cm)

++ map (\ (i, s) -> Symbol i $ SuperClassSymbol s) (getSuperClasses cm)

++ map (\ (i, s) -> Symbol i $ TypeKindInstance s) (getTypeKinds tm)

++ map (\ (i, s) -> Symbol i $ SuperTypeSymbol s) (getSuperTypes tm)

++ map (\ (i, s) -> Symbol i $ TypeAliasSymbol s) (getTypeAliases tm)

++ concatMap (\ (i, ts) ->

map (\ t -> (if isPredOpDefn $ opDefn t then

Symbol i . PredAsItemType . unPredTypeScheme

else idToOpSymbol i) $ opType t) $ Set.toList ts)

(Map.toList $ assumps d)

printAliasType :: Type -> Doc

printAliasType ty =

let (args, t) = getArgsAndType ty in

fsep $ map (parens . pretty) args ++ [text assignS, pretty t]

printAliasTypes :: [(Id, Type)] -> Doc

printAliasTypes = vcat . punctuate semi .

map (\ (i, ty) -> sep [pretty i, printAliasType ty])

getArgsAndType :: Type -> ([TypeArg], Type)

getArgsAndType ty = case ty of

TypeAbs arg t _ -> let (l, r) = getArgsAndType t in (arg : l, r)

_ -> ([], ty)

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

cm = classIdMap 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) ->

((pretty i <+> mapsto <+>

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

[] fm

in (if Map.null tm then empty

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

$+$ (if Map.null cm then empty

else keyword (classS ++ sS) <+> printMap1 cm)

$+$ (if Map.null fm then empty

else keyword (opS ++ sS) <+> sepByCommas ds)

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

$+$ mapsto

<+> specBraces (pretty $ mtarget m)

instance Pretty Symbol where

pretty s = let ty = symType s in

printSK (symbTypeToKind ty) [()] <+> pretty (symName s) <+> case ty of

SuperTypeSymbol sty -> less <+> pretty sty

SuperClassSymbol k -> less <+> pretty k

TypeAliasSymbol t -> printAliasType t

TypeKindInstance k -> colon <+> pretty k

OpAsItemType sc -> colon <+> pretty sc

TypeAsItemType k -> colon <+> pretty (rawToKind k)

ClassAsItemType k -> colon <+> pretty (rawToKind k)

PredAsItemType sc -> colon <+> pretty sc

instance Pretty RawSymbol where

pretty rs = case rs of

AnID i -> pretty i

AKindedId k i -> printSK k [i] <+> pretty i

ASymbol s -> pretty s

improveDiag :: (GetRange a, Pretty a) => a -> Diagnosis -> Diagnosis

improveDiag v d = d

{ diagString = let f : l = lines $ diagString d in

unlines $ (f ++ " of '" ++ showDoc v "'") : l

, diagPos = getRange v }

mergeMap :: (Ord a, GetRange a, Pretty a) => (b -> b -> Result b)

-> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)

mergeMap f m1 = foldM ( \ m (k, v) -> case Map.lookup k m of

Nothing -> return $ Map.insert k v m

Just w -> let

Result ds r = do

u <- f w v

return $ Map.insert k u m

in Result (map (improveDiag k) ds) r) m1 . Map.toList

mergeClassInfo :: ClassInfo -> ClassInfo -> Result ClassInfo

mergeClassInfo c1 c2 = do

k <- minRawKind "class raw kind" (rawKind c1) $ rawKind c2

return $ ClassInfo k $ Set.union (classKinds c1) $ classKinds c2

minimizeClassMap :: ClassMap -> ClassMap

minimizeClassMap cm = Map.map (\ ci -> ci { classKinds =

keepMinKinds cm [classKinds ci] }) cm

mergeClassMap :: ClassMap -> ClassMap -> Result ClassMap

mergeClassMap c = fmap minimizeClassMap . mergeMap mergeClassInfo c

addClassMap :: ClassMap -> ClassMap -> ClassMap

addClassMap c = fromMaybe (error "addClassMap") . maybeResult . mergeClassMap c

addCpoMap :: ClassMap -> ClassMap

addCpoMap = addClassMap cpoMap

diffClassMap :: ClassMap -> ClassMap -> ClassMap

diffClassMap c1 c2 =

let ce = addClassMap c1 c2

in Map.differenceWith (diffClass ce) c1 c2

-- | compute difference of class infos

diffClass :: ClassMap -> ClassInfo -> ClassInfo -> Maybe ClassInfo

diffClass cm (ClassInfo r1 k1) (ClassInfo _ k2) =

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

Set.filter (flip (lesserKind cm) k) k2) k1

in if Set.null ks then Nothing else

Just $ ClassInfo r1 ks

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

diffTypeMap = Map.differenceWith . diffType

-- | 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 (flip (lesserKind cm) k) k2) k1

sups = Set.difference (superTypes ti1) $ superTypes ti2

in if Set.null ks && Set.null sups then Nothing else

Just $ ti1 { otherTypeKinds = ks

, superTypes = sups }