PrintAs.hs revision 6cb518d88084543c13aa7e56db767c14ee97ab77
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder{- |
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : print the abstract syntax so that it can be re-parsed
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : experimental
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederprinting data types of the abstract syntax
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-}
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.PrintAs where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As
d48085f765fca838c1d972d2123601997174583dChristian Maederimport HasCASL.AsUtils
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport HasCASL.FoldTerm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport HasCASL.Builtin
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Common.Id
d48085f765fca838c1d972d2123601997174583dChristian Maederimport Common.Keywords
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederimport Common.DocUtils
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.Doc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.AS_Annotation
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederimport Data.List (groupBy, mapAccumL)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder-- | short cut for: if b then empty else d
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian MaedernoPrint :: Bool -> Doc -> Doc
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian MaedernoPrint b d = if b then empty else d
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedernoNullPrint :: [a] -> Doc -> Doc
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedernoNullPrint = noPrint . null
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersemiDs :: Pretty a => [a] -> Doc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersemiDs = fsep . punctuate semi . map pretty
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersemiAnnoted :: Pretty a => [Annoted a] -> Doc
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Variance where
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder pretty = sidDoc . mkSimpleId . show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty a => Pretty (AnyKind a) where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty knd = case knd of
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder ClassKind ci -> pretty ci
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder FunKind v k1 k2 _ -> fsep
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [ pretty v <> (case k1 of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder FunKind _ _ _ _ -> parens
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> id) (pretty k1)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , funArrow, pretty k2]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
120efeede54a5f7650cda8e91363bd6832eac9a9Christian MaedervarOfTypeArg :: TypeArg -> Id
120efeede54a5f7650cda8e91363bd6832eac9a9Christian MaedervarOfTypeArg (TypeArg i _ _ _ _ _ _) = i
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypePattern where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty tp = case tp of
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder TypePattern name@(Id ts cs _) args _ ->
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder let ds = map (pretty . varOfTypeArg) args in
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder if placeCount name == length args then
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder let (ras, dts) = mapAccumL ( \ l t -> if isPlace t then
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder case l of
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder x : r -> (r, x)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder _ -> error "Pretty TypePattern"
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder else (l, printTypeToken t)) ds ts
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder in fsep $ dts ++ (if null cs then [] else
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder [brackets $ sepByCommas $ map printTypeId cs])
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder ++ ras
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder else printTypeId name <+> fsep ds
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder TypePatternToken t -> printTypeToken t
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder MixfixTypePattern ts -> fsep $ map pretty ts
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypePatternArg t _ -> parens $ pretty t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- | put proper brackets around a document
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederbracket :: BracketKind -> Doc -> Doc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederbracket b = case b of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Parens -> parens
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Squares -> brackets
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Braces -> specBraces
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder NoBrackets -> id
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maeder-- | print a 'Kind' plus a preceding colon (or nothing)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintKind :: Kind -> Doc
d92635f998347112e5d5803301c2abfe7832ab65Christian MaederprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | print the kind of a variable with its variance and a preceding colon
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintVarKind :: Variance -> VarKind -> Doc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintVarKind e vk = case vk of
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder Downset t -> less <+> pretty t
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder VarKind k -> colon <+> pretty e <> pretty k
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder MissingKind -> empty
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maederdata TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder deriving (Eq, Ord)
d48085f765fca838c1d972d2123601997174583dChristian Maeder
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederparenPrec p1 (p2, d) = if p2 < p1 then d else parens d
d48085f765fca838c1d972d2123601997174583dChristian Maeder
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederprintTypeToken :: Token -> Doc
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederprintTypeToken t = let
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder l = ("*", cross) : map ( \ (a, d) -> (show a, d) )
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder [ (FunArr, funArrow)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder , (PFunArr, pfun)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder , (ContFunArr, cfun)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder , (PContFunArr, pcfun) ]
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder in case lookup (tokStr t) l of
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Just d -> d
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder _ -> pretty t
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder
df33a9af92444f63ad545da6bb326aac9284318eChristian MaederprintTypeId :: Id -> Doc
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederprintTypeId (Id ts cs _) = let (toks, pls) = splitMixToken ts in
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder fcat $ map printTypeToken toks
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ++ map printTypeToken pls
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedertoMixType :: Type -> (TypePrec, Doc)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedertoMixType typ = case typ of
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder TypeName name _ _ -> (Outfix, printTypeId name)
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder TypeToken tt -> (Outfix, printTypeToken tt)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder TypeAbs v t _ ->
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder BracketType k l _ ->
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (Outfix, bracket k $ sepByCommas $ map (snd . toMixType) l)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder KindedType t kind _ ->
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (Lazyfix, fsep [parenPrec Lazyfix $ toMixType t, colon, pretty kind])
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder TypeAppl t1 t2 -> let
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder (topTy, tyArgs) = getTypeApplAux False typ
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder , parenPrec Prefix $ toMixType t2 ])
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder in case topTy of
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder TypeName name@(Id ts cs _) _k _i ->
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder case map toMixType tyArgs of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [dArg] -> case ts of
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder [e] | name == lazyTypeId ->
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder (Lazyfix, pretty e <+> parenPrec Lazyfix dArg)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder [e1, e2, e3] | not (isPlace e1) && isPlace e2
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder && not (isPlace e3) && null cs ->
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (Outfix, fsep [pretty e1, snd dArg, pretty e3])
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder _ -> aArgs
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [dArg1, dArg2] -> case ts of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [_, e2, _] | isInfix name && null cs ->
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder if tokStr e2 == prodS then
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (ProdInfix, fsep
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [ parenPrec ProdInfix dArg1
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , cross, parenPrec ProdInfix dArg2])
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder else -- assume fun type
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (FunInfix, fsep
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [ parenPrec FunInfix dArg1
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , printTypeToken e2, snd dArg2])
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder _ -> aArgs
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder dArgs -> if isProductIdWithArgs name $ length tyArgs then
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (ProdInfix, fsep $ punctuate (space <> cross) $
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder map (parenPrec ProdInfix) dArgs) else aArgs
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder _ -> aArgs
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Type where
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder pretty = snd . toMixType
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder-- no curried notation for bound variables
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeScheme where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (TypeScheme vs t _) = let tdoc = pretty t in
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder if null vs then tdoc else
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder fsep [forallDoc, semiDs vs, bullet <+> tdoc]
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Partiality where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty p = case p of
37354e3ed68875fb527338105a610df481f98cb0Christian Maeder Partial -> quMarkD
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Total -> empty
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Quantifier where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty q = case q of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Universal -> forallDoc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Existential -> exists
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Unique -> unique
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeQual where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty q = case q of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder OfType -> colon
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder AsType -> text asS
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder InType -> inDoc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Inferred -> colon
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Term where
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder pretty = printTerm . rmSomeTypes
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederisSimpleTerm :: Term -> Bool
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederisSimpleTerm trm = case trm of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder QualVar _ -> True
9d75ab580dbf51b7ca60903fb32e7f38d939d326Christian Maeder QualOp _ _ _ _ _ -> True
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm _ _ _ _ -> True
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ApplTerm _ _ _ -> True
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TupleTerm _ _ -> True
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TermToken _ -> True
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder BracketTerm _ _ _ -> True
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder _ -> False
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder-- | used only to produce CASL applications
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaederisSimpleArgTerm :: Term -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaederisSimpleArgTerm trm = case trm of
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder QualVar vd -> not (isPatVarDecl vd)
9d75ab580dbf51b7ca60903fb32e7f38d939d326Christian Maeder QualOp _ _ _ _ _ -> True
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm n _ l _ -> placeCount n /= 0 || not (null l)
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder TupleTerm _ _ -> True
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder BracketTerm _ _ _ -> True
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder _ -> False
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaederhasRightQuant :: Term -> Bool
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaederhasRightQuant t = case t of
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder QuantifiedTerm {} -> True
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder LambdaTerm {} -> True
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder CaseTerm {} -> True
79bf169bcae16ce390683c698bae248c1ed6ab13Christian Maeder LetTerm Let _ _ _ -> True
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder -> hasRightQuant (last ts)
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder case t2 of
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder _ -> hasRightQuant t2
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder ApplTerm _ t2 _ -> hasRightQuant t2
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder _ -> False
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaederzipArgs :: Id -> [Term] -> [Doc] -> [Doc]
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaederzipArgs n ts ds = case (ts, ds) of
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder (t : r, d : s) -> let
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder p = parenTermDoc t d
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder e = if hasRightQuant t then parens d else p
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder in if null r && null s && endPlace n then
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder [if hasRightQuant t then d else p]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder else e : zipArgs n r s
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder _ -> []
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian MaederisPatVarDecl :: VarDecl -> Bool
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederisPatVarDecl (VarDecl v ty _ _) = case ty of
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder TypeName t _ _ -> isSimpleId v && take 2 (show t) == "_v"
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder _ -> False
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederparenTermDoc :: Term -> Doc -> Doc
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian MaederparenTermDoc trm = if isSimpleTerm trm then id else parens
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintTermRec :: FoldRec Doc (Doc, Doc)
ce3928e71520030ad0275b72050a8f4377f9313cChristian MaederprintTermRec = FoldRec
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder { foldQualVar = \ _ vd@(VarDecl v _ _ _) ->
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder if isPatVarDecl vd then pretty v
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder else parens $ keyword varS <+> pretty vd
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder , foldQualOp = \ _ br n t tys _ -> (if null tys then id else
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder (<> brackets (ppWithCommas tys))) $
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder parens $ fsep [pretty br, pretty n, colon, pretty $
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if isPred br then unPredTypeScheme t else t]
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder , foldResolvedMixTerm =
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder \ (ResolvedMixTerm _ _ os _) n@(Id toks cs ps) tys ts _ ->
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder let pn = placeCount n in if pn == length ts || null ts then
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder let ds = zipArgs n os ts in
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder if null tys then idApplDoc n ds
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder else let (ftoks, _) = splitMixToken toks
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder fId = Id ftoks cs ps
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder (fts, rts) = splitAt (placeCount fId) $ if null ts
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder then replicate pn $ pretty placeTok else ds
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder in fsep $ (idApplDoc fId fts <> brackets (ppWithCommas tys))
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder : rts
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder else idApplDoc applId [idDoc n, parens $ sepByCommas ts]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldApplTerm = \ (ApplTerm o1 o2 _) t1 t2 _ ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case (o1, o2) of
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder -- comment out the following two guards for CASL applications
84e7cfca5b97aef300acdaa8cf63a3572f9151c0Christian Maeder (ResolvedMixTerm n _ [] _, TupleTerm ts@(_ : _) _)
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder | placeCount n == length ts ->
84e7cfca5b97aef300acdaa8cf63a3572f9151c0Christian Maeder idApplDoc n (zipArgs n ts $ map printTerm ts)
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder (ResolvedMixTerm n _ [] _, _) | placeCount n == 1
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder -> idApplDoc n $ zipArgs n [o2] [t2]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder _ -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder , foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder , foldTypedTerm = \ (TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder LambdaTerm {} -> parens
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder LetTerm {} -> parens
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder CaseTerm {} -> parens
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder QuantifiedTerm {} -> parens
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder _ -> id) t, pretty q, pretty typ]
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder , foldQuantifiedTerm = \ _ q vs t _ ->
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder fsep [pretty q, printGenVarDecls vs, bullet <+> t]
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder , foldLambdaTerm = \ _ ps q t _ ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep [ lambda
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , case ps of
a53f4b7cb8bedee4fb7a8b386efcb47246467948Christian Maeder [p] -> if show p == "()" then empty else p
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> fcat $ map parens ps
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder , (case q of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Partial -> bullet
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder Total -> bullet <> text exMark) <+> t]
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder , foldCaseTerm = \ _ t es _ ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep [text caseS, t, text ofS,
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder cat $ punctuate (space <> bar <> space) $
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (printEq0 funArrow) es]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldLetTerm = \ _ br es t _ ->
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder let des = sep $ punctuate semi $ map (printEq0 equals) es
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder in case br of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Let -> fsep [sep [text letS <+> des, text inS], t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Where -> fsep [sep [t, text whereS], des]
966e627a1c06b302a06d59d08b8ab45905f3509cChristian Maeder Program -> text programS <+> des
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldTermToken = \ _ t -> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldMixfixTerm = \ _ ts -> fsep ts
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder , foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder fsep [pretty v, text asP, p]
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , foldProgEq = \ _ p t _ -> (p, t) }
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintTerm :: Term -> Doc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintTerm = foldTerm printTermRec
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrmTypeRec :: MapRec
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrmTypeRec = mapRec
9d75ab580dbf51b7ca60903fb32e7f38d939d326Christian Maeder { foldQualOp = \ t _ i _ _ ps ->
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder if elem i $ map fst bList then
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm i [] [] ps else t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldTypedTerm = \ _ nt q ty ps ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case q of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Inferred -> nt
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> case nt of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder QualVar (VarDecl _ oty _ _) | oty == ty -> nt
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> TypedTerm nt q ty ps }
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrmSomeTypes :: Term -> Term
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrmSomeTypes = foldTerm rmTypeRec
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder-- | put parenthesis around applications
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaederparenTermRec :: MapRec
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaederparenTermRec = let
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder addParAppl t = case t of
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm _ _ [] _ -> t
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder QualVar _ -> t
9d75ab580dbf51b7ca60903fb32e7f38d939d326Christian Maeder QualOp _ _ _ _ _ -> t
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder TermToken _ -> t
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder BracketTerm _ _ _ -> t
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder TupleTerm _ _ -> t
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder _ -> TupleTerm [t] nullRange
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder in mapRec
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder { foldApplTerm = \ _ t1 t2 ps ->
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder ApplTerm (addParAppl t1) (addParAppl t2) ps
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder , foldResolvedMixTerm = \ _ n tys ts ps ->
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm n tys (map addParAppl ts) ps
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder , foldTypedTerm = \ _ t q typ ps ->
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder TypedTerm (addParAppl t) q typ ps
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder , foldMixfixTerm = \ _ ts -> MixfixTerm $ map addParAppl ts
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder , foldAsPattern = \ _ v p ps -> AsPattern v (addParAppl p) ps
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder }
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaederparenTerm :: Term -> Term
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaederparenTerm = foldTerm parenTermRec
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- | print an equation with different symbols between 'Pattern' and 'Term'
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintEq0 :: Doc -> (Doc, Doc) -> Doc
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederprintEq0 s (p, t) = sep [p, hsep [s, t]]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian MaederprintGenVarDecls :: [GenVarDecl] -> Doc
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederprintGenVarDecls = fsep . punctuate semi . map
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder ( \ l -> case l of
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder [x] -> pretty x
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder GenVarDecl (VarDecl _ t _ _) : _ -> sep
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder [ ppWithCommas (map ( \ (GenVarDecl (VarDecl v _ _ _)) -> v) l)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder , printVarDeclType t]
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder GenTypeVarDecl (TypeArg _ e c _ _ _ _) : _ -> sep
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder [ ppWithCommas (map ( \ (GenTypeVarDecl v) -> varOfTypeArg v) l)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder , printVarKind e c]
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder _ -> error "printGenVarDecls") . groupBy sameType
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian MaedersameType :: GenVarDecl -> GenVarDecl -> Bool
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedersameType g1 g2 = case (g1, g2) of
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder (GenVarDecl (VarDecl _ t1 Comma _), GenVarDecl (VarDecl _ t2 _ _))
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder | t1 == t2 -> True
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder (GenTypeVarDecl (TypeArg _ e1 c1 _ _ Comma _),
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder GenTypeVarDecl (TypeArg _ e2 c2 _ _ _ _)) | e1 == e2 && c1 == c2 -> True
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder _ -> False
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian MaederprintVarDeclType :: Type -> Doc
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian MaederprintVarDeclType t = case t of
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder MixfixType [] -> empty
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder _ -> colon <+> pretty t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maederinstance Pretty VarDecl where
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder pretty (VarDecl v t _ _) = pretty v <+> printVarDeclType t
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty GenVarDecl where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty gvd = case gvd of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GenVarDecl v -> pretty v
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GenTypeVarDecl tv -> pretty tv
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeArg where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (TypeArg v e c _ _ _ _) =
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder pretty v <+> printVarKind e c
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- | don't print an empty list and put parens around longer lists
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintList0 :: (Pretty a) => [a] -> Doc
d92635f998347112e5d5803301c2abfe7832ab65Christian MaederprintList0 l = case l of
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder [] -> empty
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [x] -> pretty x
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder _ -> parens $ ppWithCommas l
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty BasicSpec where
32a2f5f00ff72c095b39629101043db4407974f9Christian Maeder pretty (BasicSpec l) = if null l then specBraces empty else
32a2f5f00ff72c095b39629101043db4407974f9Christian Maeder changeGlobalAnnos addBuiltins . vcat $ map pretty l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty ProgEq where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty = printEq0 equals . foldEq printTermRec
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty BasicItem where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty bi = case bi of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder SigItems s -> pretty s
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder ProgItems l _ -> sep [keyword programS, semiAnnoted l]
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder ClassItems i l _ -> let
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder b = semiAnnos pretty l
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder p = plClass l
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder in case i of
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder Plain -> topSigKey (classS ++ if p then "es" else "") <+> b
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder Instance -> sep [keyword classS <+>
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder keyword (instanceS ++ if p then sS else ""), b]
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder GenVarItems l _ -> topSigKey (varS ++ pluralS l) <+> printGenVarDecls l
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder FreeDatatype l _ -> sep
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [ keyword freeS <+> keyword (typeS ++ pluralS l)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , semiAnnos pretty l]
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder GenItems l _ -> let gkw = keyword generatedS in
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder (if all (isDatatype . item) l then \ i -> gkw <+> rmTopKey i
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder else \ i -> sep [gkw, specBraces i])
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder $ vcat $ map (printAnnoted pretty) l
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder AxiomItems vs fs _ -> sep
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [ if null vs then empty else forallDoc <+> printGenVarDecls vs
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , case fs of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [] -> empty
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> let pp = addBullet . pretty in
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder vcat $ map (printAnnoted pp) (init fs)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ++ [printSemiAnno pp True $ last fs]]
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Internal l _ -> sep
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [ keyword internalS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , specBraces $ vcat $ map (printAnnoted pretty) l]
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederplClass :: [Annoted ClassItem] -> Bool
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederplClass l = case map item l of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ : _ : _ -> True
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [ClassItem (ClassDecl (_ : _ : _) _ _) _ _] -> True
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> False
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederpluralS :: [a] -> String
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederpluralS l = case l of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ : _ : _ -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> ""
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederisDatatype :: SigItems -> Bool
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederisDatatype si = case si of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder TypeItems _ l _ -> all
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ((\ t -> case t of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Datatype _ -> True
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> False) . item) l
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder _ -> False
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty OpBrand where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty b = keyword $ show b
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty SigItems where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty si = case si of
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder TypeItems i l _ -> let b = semiAnnos pretty l in case i of
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder Plain -> topSigKey ((if all (isSimpleTypeItem . item) l
62fb92b09f732b770317b46a793b60b960d5f481Christian Maeder then typeS else typeS) ++ plTypes l) <+> b
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder Instance ->
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder sep [keyword typeS <+> keyword (instanceS ++ plTypes l), b]
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder OpItems b l _ -> noNullPrint l $ topSigKey (show b ++ plOps l)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder <+> let po = (prettyOpItem $ isPred b) in
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder if case item $ last l of
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder OpDecl _ _ a@(_ : _) _ -> case last a of
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder UnitOpAttr {} -> True
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder _ -> False
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder OpDefn {} -> True
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder _ -> False
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder then vcat (map (printSemiAnno po True) l)
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder else semiAnnos po l
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederplTypes :: [Annoted TypeItem] -> String
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederplTypes l = case map item l of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ : _ : _ -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [TypeDecl (_ : _ : _) _ _] -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [SubtypeDecl (_ : _ : _) _ _] -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [IsoDecl (_ : _ : _) _] -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> ""
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederplOps :: [Annoted OpItem] -> String
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederplOps l = case map item l of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ : _ : _ -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [OpDecl (_ : _ : _) _ _ _] -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> ""
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederisSimpleTypeItem :: TypeItem -> Bool
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederisSimpleTypeItem ti = case ti of
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder TypeDecl l k _ -> k == universe && all isSimpleTypePat l
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder SubtypeDecl l (TypeName i _ _) _ ->
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder not (isMixfix i) && all isSimpleTypePat l
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder SubtypeDefn p (Var _) t _ _ ->
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder isSimpleTypePat p && isSimpleType t
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder _ -> False
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederisSimpleTypePat :: TypePattern -> Bool
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederisSimpleTypePat tp = case tp of
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder TypePattern i [] _ -> not $ isMixfix i
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder _ -> False
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaederisSimpleType :: Type -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaederisSimpleType t = case t of
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder TypeName i _ _ -> not $ isMixfix i
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder TypeToken _ -> True
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder MixfixType[TypeToken _, BracketType Squares (_ : _) _] -> True
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder _ -> False
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty ClassItem where
bf4263f9dab040818efc7a67172aab8f32218061Christian Maeder pretty (ClassItem d l _) = pretty d $+$ noNullPrint l
32a2f5f00ff72c095b39629101043db4407974f9Christian Maeder (specBraces $ vcat $ map (printAnnoted pretty) l)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty ClassDecl where
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder pretty (ClassDecl l k _) = let cs = ppWithCommas l in
749074bf849727439f584139415f6a985a8aa875Christian Maeder if k == universe then cs else fsep [cs, less, pretty k]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Vars where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty vd = case vd of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Var v -> pretty v
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder VarTuple vs _ -> parens $ ppWithCommas vs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeItem where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty ti = case ti of
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder TypeDecl l k _ -> sep [ppWithCommas l, printKind k]
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder SubtypeDecl l t _ ->
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder fsep [ppWithCommas l, less, pretty t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder IsoDecl l _ -> fsep $ punctuate (space <> equals) $ map pretty l
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder SubtypeDefn p v t f _ ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep [pretty p, equals,
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder specBraces $ fsep
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder [pretty v, colon <+> pretty t, bullet <+> pretty f]]
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder AliasType p _ (TypeScheme l t _) _ ->
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder fsep $ pretty p : map (pretty . varOfTypeArg) l
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder ++ [text assignS <+> pretty t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Datatype t -> pretty t
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederprettyTypeScheme :: Bool -> TypeScheme -> Doc
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederprettyTypeScheme b = pretty . (if b then unPredTypeScheme else id)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederprettyOpItem :: Bool -> OpItem -> Doc
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederprettyOpItem b oi = case oi of
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder OpDecl l t a _ -> fsep $ punctuate comma (map pretty l)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder ++ [colon <+>
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder (if null a then id else (<> comma))(prettyTypeScheme b t)]
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder ++ punctuate comma (map pretty a)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder OpDefn n ps s t _ -> fcat $
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ((if null ps then (<> space) else id) $ pretty n)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder : map ((<> space) . parens . semiDs) ps
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ++ (if b then [] else [colon <+> prettyTypeScheme b s <> space])
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ++ [(if b then equiv else equals) <> space, pretty t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty BinOpAttr where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty a = text $ case a of
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder Assoc -> assocS
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder Comm -> commS
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder Idem -> idemS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty OpAttr where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty oa = case oa of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder BinOpAttr a _ -> pretty a
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder UnitOpAttr t _ -> text unitS <+> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty DatatypeDecl where
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder pretty (DatatypeDecl p k alts d _) =
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder fsep [ pretty p, printKind k, defn
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder <+> cat (punctuate (space <> bar <> space)
54b698a84a1686b828c99d839fc671942b817534Christian Maeder $ map pretty alts)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder , case d of
54b698a84a1686b828c99d839fc671942b817534Christian Maeder [] -> empty
d92635f998347112e5d5803301c2abfe7832ab65Christian Maeder _ -> keyword derivingS <+> ppWithCommas d]
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Alternative where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty alt = case alt of
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder Constructor n cs p _ -> pretty n <+> fsep
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder (map ( \ l -> case (l, p) of
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder-- comment out the following line to output real CASL
bf4263f9dab040818efc7a67172aab8f32218061Christian Maeder ([NoSelector (TypeToken t)], Total) | isSimpleId n -> pretty t
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder _ -> parens $ semiDs l) cs) <> pretty p
62fb92b09f732b770317b46a793b60b960d5f481Christian Maeder Subtype l _ -> text (if all isSimpleType l then typeS else typeS)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder <+> ppWithCommas l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Component where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty sel = case sel of
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder Selector n _ t _ _ -> sep [pretty n, colon <+> pretty t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder NoSelector t -> pretty t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Symb where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (Symb i mt _) =
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder sep $ pretty i : case mt of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Nothing -> []
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Just (SymbType t) -> [colon <+> pretty t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty SymbItems where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (SymbItems k syms _ _) =
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder printSK k syms <> ppWithCommas syms
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty SymbOrMap where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (SymbOrMap s mt _) =
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder sep $ pretty s : case mt of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Nothing -> []
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Just t -> [mapsto <+> pretty t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty SymbMapItems where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (SymbMapItems k syms _ _) =
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder printSK k syms <> ppWithCommas syms
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- | print symbol kind
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederprintSK :: SymbKind -> [a] -> Doc
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederprintSK k l = case k of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Implicit -> empty
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> keyword (drop 3 (show k) ++ case l of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ : _ : _ -> sS
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder _ -> "") <> space