PrintLe.hs revision e13ee09381f136f5eadaabdb9699773c0052cf3d
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : pretty printing signatures
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniMaintainer : Christian.Maeder@dfki.de
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : experimental
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniPortability : portable
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinipretty printing a HasCASL environment
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinimodule HasCASL.PrintLe (diffTypeMap, diffType, printMap1) where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederimport qualified Data.Map as Map
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Data.Set as Set
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederinstance Pretty ClassInfo where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty (ClassInfo rk ks) = if Set.null ks then colon <+> pretty rk else
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder text lessS <+> printList0 (Set.toList ks)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederprintGenKind :: GenKind -> Doc
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorriniprintGenKind k = case k of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Loose -> empty
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Free -> text freeS
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Generated -> text generatedS
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederinstance Pretty TypeDefn where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder pretty td = case td of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder NoTypeDefn -> empty
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder PreDatatype -> text "%(data type)%"
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder AliasTypeDefn s -> text assignS <+> pretty s
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder DatatypeDefn dd -> text "%[" <> pretty dd <> text "]%"
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederprintAltDefn :: AltDefn -> Doc
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederprintAltDefn (Construct mi ts p sels) = case mi of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Just i -> pretty i <+> fsep (map (parens . semiDs) sels) <> pretty p
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Nothing -> text (typeS ++ sS) <+> ppWithCommas ts
5fd8f2cd4cad1d0f623a50c7f01bda4335f4935bPaolo Torriniinstance Pretty Selector where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder pretty (Select mi t p) =
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Just i -> pretty i <+> (case p of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Partial -> text colonQuMark
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Total -> colon) <> space
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> empty) <> pretty t
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederinstance Pretty TypeInfo where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder pretty (TypeInfo _ ks sups def) =
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder fsep $ [colon, printList0 $ Set.toList ks]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder ++ (if Set.null sups then []
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder else [less, printList0 $ Set.toList sups])
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder ++ case def of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder NoTypeDefn -> []
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder _ -> [pretty def]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederinstance Pretty TypeVarDefn where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder pretty (TypeVarDefn v vk _ i) =
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder printVarKind v vk <+> text ("%(var_" ++ shows i ")%")
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maederinstance Pretty VarDefn where
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini pretty (VarDefn ty) =
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini colon <+> pretty ty
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torriniinstance Pretty ConstrInfo where
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini pretty (ConstrInfo i t) =
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini pretty i <+> colon <+> pretty t
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maederinstance Pretty OpDefn where
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini pretty od = case od of
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder NoOpDefn b -> text $ "%(" ++ shows b ")%"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ConstructData _ -> text "%(constructor)%"
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder SelectData cs _ -> sep [ text "%(selector of constructor(s)"
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini , printList0 (Set.toList cs) <> text ")%" ]
d4655008a003ed9717ba0bb0d7022e166006fca0Christian Maeder Definition b t -> fsep [pretty $ NoOpDefn b, equals, pretty t]
2b827e8e9d6a1196ffaf263dcc991779e5f9c0e9Christian Maederinstance Pretty OpInfo where
2b827e8e9d6a1196ffaf263dcc991779e5f9c0e9Christian Maeder pretty o = let l = Set.toList $ opAttrs o in
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini fsep $ [pretty (opType o) <> if null l then empty else comma]
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder ++ punctuate comma (map pretty l)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder ++ [pretty $ opDefn o]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance Pretty DataEntry where
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini pretty (DataEntry im i k args _ alts) =
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini printGenKind k <+> keyword typeS <+>
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini fsep ([fcat $ pretty i : map (parens . pretty) args
2b827e8e9d6a1196ffaf263dcc991779e5f9c0e9Christian Maeder , defn, cat $ punctuate (space <> bar <> space)
2b827e8e9d6a1196ffaf263dcc991779e5f9c0e9Christian Maeder $ map printAltDefn $ Set.toList alts]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini ++ if Map.null im then []
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini else [text withS, text (typeS ++ sS), printMap1 im])
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance Pretty Sentence where
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini pretty s = case s of
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini Formula t -> (case t of
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini QuantifiedTerm Universal (_ : _) _ _ -> id
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini _ -> addBullet) $ pretty t
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini DatatypeSen ls -> vcat (map pretty ls)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ProgEqSen _ _ pe -> keyword programS <+> pretty pe
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance Pretty Env where
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini { classMap = cm
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini , typeMap = tm
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini , localTypeVars = tvs
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini , assumps = ops
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini , localVars = vs
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini , sentences = se
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini , envDiags=ds } = let
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini oops = foldr Map.delete ops $ map fst bList
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini otm = diffTypeMap cm tm bTypes
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini atm = filterAliases otm
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini header m s = keyword $
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini if Map.size m < 2 then s else
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini if last s == 's' then s ++ "es" else s ++ "s"
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder in noPrint (Map.null cm) (header cm classS)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ printMap0 cm
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ noPrint (Map.null otm) (header otm typeS)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $+$ printMap0 (Map.map (\ ti -> ti
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini { typeDefn = case typeDefn ti of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini AliasTypeDefn _ -> NoTypeDefn
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini d -> d }) otm)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ noPrint (Map.null atm) (header atm typeS)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ printMap0 atm
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ noPrint (Map.null tvs) (header tvs varS)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ printMap0 tvs
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ printSetMap (keyword opS) space oops
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $+$ noPrint (Map.null vs) (header vs varS)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini $+$ printMap0 vs
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder $+$ vcat (map (pretty . fromLabelledSen) $ reverse se)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder $+$ vcat (map pretty $ reverse ds)
d4655008a003ed9717ba0bb0d7022e166006fca0Christian MaederprintMap0 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc
d4655008a003ed9717ba0bb0d7022e166006fca0Christian MaederprintMap0 = printMap id (vcat . punctuate semi) ( \ a b -> fsep $ a : [b])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintMap1 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniprintMap1 = printMap id vcat ( \ a b -> fsep $ a : mapsto : [b])
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederinstance Pretty Morphism where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let tm = typeIdMap m
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini fm = funMap m
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder -- the types in funs are already mapped
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder -- key und value types only differ wrt. partiality
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder ds = Map.foldWithKey ( \ (i, _) (j, t) l ->
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini (pretty i <+> mapsto <+>
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder pretty j <+> colon <+> pretty t) : l)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder in (if Map.null tm then empty
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini else keyword (typeS ++ sS) <+> printMap1 tm)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $+$ (if Map.null fm then empty
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini else keyword (opS ++ sS) <+> sepByCommas ds)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder $+$ colon <+> specBraces (pretty $ msource m)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder <+> specBraces (pretty $ mtarget m)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederinstance Pretty a => Pretty (SymbolType a) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty t = case t of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder OpAsItemType sc -> pretty sc
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder TypeAsItemType k -> pretty k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ClassAsItemType k -> pretty k
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance Pretty Symbol where
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torrini pretty s = keyword (case symType s of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder OpAsItemType _ -> opS
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder TypeAsItemType _ -> typeS
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ClassAsItemType _ -> classS) <+>
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty (symName s) <+> colon <+>
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty (symType s)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederinstance Pretty RawSymbol where
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini pretty rs = case rs of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder AnID i -> pretty i
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini AKindedId k i -> printSK k [i] <> pretty i
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini AQualId i t -> printSK (symbTypeToKind t) [i] <> pretty i <+> colon
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ASymbol s -> pretty s
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinidiffTypeMap :: ClassMap -> TypeMap -> TypeMap -> TypeMap
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinidiffTypeMap cm t1 t2 =
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder let t = Map.differenceWith (diffType cm) t1 t2
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder r = Set.intersection $ Set.union (Map.keysSet t) $ Map.keysSet bTypes
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini in Map.map ( \ ti -> ti { superTypes = r $ superTypes ti }) t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | compute difference of type infos
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffType :: ClassMap -> TypeInfo -> TypeInfo -> Maybe TypeInfo
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinidiffType cm ti1 ti2 =
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini let k1 = otherTypeKinds ti1
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder k2 = otherTypeKinds ti2
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini Set.filter (lesserKind cm k) k2) k1
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder in if Set.null ks then Nothing else
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini Just $ ti1 { otherTypeKinds = ks
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , superTypes = Set.difference (superTypes ti1) $
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini superTypes ti2 }