PrintLe.hs revision ad270004874ce1d0697fb30d7309f180553bb315
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederModule : $Header$
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederMaintainer : maeder@tzi.de
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : experimental
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederPortability : portable
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederpretty printing a HasCASL environment
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-}
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.PrintLe where
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport HasCASL.AsUtils
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.PrintAs
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.Le
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport HasCASL.Builtin
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Common.Id
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Doc
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maederimport Common.DocUtils
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Keywords
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Data.List
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty ClassInfo where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (ClassInfo rk ks) = case ks of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [] -> colon <+> pretty rk
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> text lessS <+> printList0 ks
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederprintGenKind :: GenKind -> Doc
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederprintGenKind k = case k of
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Loose -> empty
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Free -> text freeS
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Generated -> text generatedS
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeDefn where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty td = case td of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder NoTypeDefn -> empty
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder PreDatatype -> text "%(data type)%"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder AliasTypeDefn s -> text assignS <+> printPseudoType s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder DatatypeDefn dd -> text " %[" <> pretty dd <> text "]%"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintAltDefn :: Id -> [TypeArg] -> RawKind -> AltDefn -> Doc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintAltDefn dt tArgs rk (Construct mi ts p sels) = case mi of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just i -> fcat $ [pretty i <> space, colon <> space,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (createConstrType dt tArgs rk p ts)]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ map (parens . semiDs) sels
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder Nothing -> text (typeS ++ sS) <+> ppWithCommas ts
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Selector where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (Select mi t p) =
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder (case mi of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just i -> pretty i <+> (case p of
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder Partial -> text colonQuMark
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Total -> colon) <> space
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> empty) <> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeInfo where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (TypeInfo _ ks sups def) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep $ [colon, printList0 ks]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ (if Set.null sups then []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else [less, printList0 $ Set.toList sups])
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ++ case def of
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder NoTypeDefn -> []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> [pretty def]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeVarDefn where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (TypeVarDefn v vk _ i) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder printVarKind v vk <+> text ("%(var_" ++ shows i ")%")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty VarDefn where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (VarDefn ty) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder colon <+> pretty ty
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty ConstrInfo where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (ConstrInfo i t) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty i <+> colon <+> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty OpDefn where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty od = case od of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder NoOpDefn b -> text $ "%(" ++ shows b ")%"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ConstructData i -> text $ "%(construct " ++ showId i ")%"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder SelectData c i -> text ("%(select from " ++ showId i " constructed by")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ printList0 c <> text ")%"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Definition b t -> fsep [pretty $ NoOpDefn b, equals, pretty t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty OpInfo where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty o = let l = opAttrs o in
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep $ [ colon
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , pretty (opType o) <> if null l then empty else comma]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ punctuate comma (map pretty l)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ [pretty $ opDefn o]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty OpInfos where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (OpInfos l) = vcat $ map pretty l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty DataEntry where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (DataEntry im i k args rk alts) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder printGenKind k <+> keyword typeS <+>
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep ([fcat $ pretty i : map (parens . pretty) args
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , defn, vcat $ map (printAltDefn i args rk) alts]
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ++ if Map.null im then []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else [text withS, text (typeS ++ sS), printMap0 im])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Sentence where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty s = case s of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Formula t -> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder DatatypeSen ls -> vcat (map pretty ls)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ProgEqSen _ _ pe -> keyword programS <+> pretty pe
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Env where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (Env{classMap=cm, typeMap=tm, localTypeVars=tvs,
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder assumps=ops, localVars=vs,
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder sentences=se, envDiags=ds}) =
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder let oops = foldr Map.delete ops $ map fst bList
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder otm = Map.difference tm $ addUnit Map.empty
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder header s = text "%%" <+> text s
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder <+> text (replicate (70 - length s) '-')
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder in noPrint (Map.null cm) (header "Classes")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ printMap0 cm
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder $+$ noPrint (Map.null otm) (header "Type Constructors")
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder $+$ printMap0 otm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ noPrint (Map.null tvs) (header "Type Variables")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ printMap0 tvs
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder $+$ noPrint (Map.null oops) (header "Assumptions")
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder $+$ printMap0 oops
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ noPrint (Map.null vs) (header "Variables")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ printMap0 vs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ noPrint (null se) (header "Sentences")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ vcat (map pretty $ reverse se)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ noPrint (null ds) (header "Diagnostics")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ vcat (map pretty $ reverse ds)
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintMap0 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian MaederprintMap0 = printMyMap []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintMap1 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian MaederprintMap1 = printMyMap [mapsto]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian MaederprintMyMap :: (Pretty a, Ord a, Pretty b) => [Doc] -> Map.Map a b -> Doc
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian MaederprintMyMap d = printMap id vcat ( \ a b -> fsep $ a : d ++ [b])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Morphism where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty m =
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder let tm = typeIdMap m
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder fm = funMap m
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ds = Map.foldWithKey ( \ (i, s) (j, t) l ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (pretty i <+> colon <+> pretty s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <+> mapsto <+>
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty j <+> colon <+> pretty t) : l)
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder [] fm
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder in (if Map.null tm then empty
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else keyword (typeS ++ sS) <+> printMap0 tm)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ (if Map.null fm then empty
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder else keyword (opS ++ sS) <+> sepByCommas ds)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ colon <+> specBraces (pretty $ msource m)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $+$ mapsto
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <+> specBraces (pretty $ mtarget m)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty a => Pretty (SymbolType a) where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty t = case t of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder OpAsItemType sc -> pretty sc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypeAsItemType k -> pretty k
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ClassAsItemType k -> pretty k
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Symbol where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty s = keyword (case symType s of
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder OpAsItemType _ -> opS
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder TypeAsItemType _ -> typeS
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ClassAsItemType _ -> classS) <+>
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (symName s) <+> colon <+>
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (symType s)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty RawSymbol where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty rs = case rs of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder AnID i -> pretty i
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder AKindedId k i -> printSK k [i] <> pretty i
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder AQualId i t -> printSK (symbTypeToKind t) [i] <> pretty i <+> colon
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <+> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ASymbol s -> pretty s