abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder{- |

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : print the abstract syntax so that it can be re-parsed

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : Christian.Maeder@dfki.de

413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederStability : experimental

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederprinting data types of the abstract syntax

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedermodule HasCASL.PrintAs where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maederimport HasCASL.As

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport HasCASL.AsUtils

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport HasCASL.FoldTerm

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport HasCASL.Builtin

d48085f765fca838c1d972d2123601997174583dChristian Maederimport Common.Id

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederimport Common.Keywords

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.DocUtils

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Doc

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Common.AS_Annotation

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederimport Data.List (groupBy, mapAccumL)

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder-- | short cut for: if b then empty else d

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian MaedernoPrint :: Bool -> Doc -> Doc

413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedernoPrint b d = if b then empty else d

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder

413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedernoNullPrint :: [a] -> Doc -> Doc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedernoNullPrint = noPrint . null

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersemiDs :: Pretty a => [a] -> Doc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersemiDs = fsep . punctuate semi . map pretty

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedersemiAnnoted :: Pretty a => [Annoted a] -> Doc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Variance where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty = sidDoc . mkSimpleId . show

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty a => Pretty (AnyKind a) where

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder pretty knd = case knd of

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder ClassKind ci -> pretty ci

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder FunKind v k1 k2 _ -> fsep

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [ pretty v <> (case k1 of

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder FunKind _ _ _ _ -> parens

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder _ -> id) (pretty k1)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , funArrow, pretty k2]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedervarOfTypeArg :: TypeArg -> Id

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedervarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypePattern where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty tp = case tp of

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder TypePattern name@(Id ts cs _) args _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let ds = map (pretty . varOfTypeArg) args in

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder if placeCount name == length args then

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder let (ras, dts) = mapAccumL ( \ l t -> if isPlace t then

c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder case l of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder x : r -> (r, x)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> error "Pretty TypePattern"

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else (l, printTypeToken t)) ds ts

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in fsep $ dts ++ (if null cs then [] else

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [brackets $ sepByCommas $ map printTypeId cs])

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ++ ras

92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maeder else printTypeId name <+> fsep ds

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypePatternToken t -> printTypeToken t

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder MixfixTypePattern ts -> fsep $ map pretty ts

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder TypePatternArg t _ -> parens $ pretty t

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | put proper brackets around a document

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederbracket :: BracketKind -> Doc -> Doc

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederbracket b = case b of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Parens -> parens

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Squares -> brackets

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Braces -> specBraces

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder NoBrackets -> id

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | print a 'Kind' plus a preceding colon (or nothing)

d48085f765fca838c1d972d2123601997174583dChristian MaederprintKind :: Kind -> Doc

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | print the kind of a variable with its variance and a preceding colon

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederprintVarKind :: Variance -> VarKind -> Doc

413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederprintVarKind e vk = case vk of

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Downset t -> space <> less <+> pretty t

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder VarKind k -> space <> colon <+> pretty e <> pretty k

d48085f765fca838c1d972d2123601997174583dChristian Maeder MissingKind -> empty

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maederdata TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder deriving (Eq, Ord)

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

d48085f765fca838c1d972d2123601997174583dChristian Maeder

413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederprintTypeToken :: Token -> Doc

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederprintTypeToken t = let

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder l = ("*", cross) : map ( \ (a, d) -> (show a, d) )

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder [ (FunArr, funArrow)

d48085f765fca838c1d972d2123601997174583dChristian Maeder , (PFunArr, pfun)

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder , (ContFunArr, cfun)

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder , (PContFunArr, pcfun) ]

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder in case lookup (tokStr t) l of

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Just d -> d

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder _ -> pretty t

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder

d48085f765fca838c1d972d2123601997174583dChristian MaederprintTypeId :: Id -> Doc

413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederprintTypeId (Id ts cs _) = let (toks, pls) = splitMixToken ts in

d48085f765fca838c1d972d2123601997174583dChristian Maeder fcat $ map printTypeToken toks

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder ++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder ++ map printTypeToken pls

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedertoMixType :: Type -> (TypePrec, Doc)

d48085f765fca838c1d972d2123601997174583dChristian MaedertoMixType typ = case typ of

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder TypeName name _ _ -> (Outfix, printTypeId name)

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder TypeToken tt -> (Outfix, printTypeToken tt)

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder TypeAbs v t _ ->

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])

d48085f765fca838c1d972d2123601997174583dChristian Maeder ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder BracketType k l _ ->

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (Outfix, bracket k $ sepByCommas $ map (snd . toMixType) l)

d48085f765fca838c1d972d2123601997174583dChristian Maeder KindedType t kind _ ->

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (Lazyfix, fsep [parenPrec Lazyfix $ toMixType t, colon, pretty kind])

d48085f765fca838c1d972d2123601997174583dChristian Maeder MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder TypeAppl t1 t2 -> let

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (topTy, tyArgs) = getTypeApplAux False typ

d48085f765fca838c1d972d2123601997174583dChristian Maeder aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1

d48085f765fca838c1d972d2123601997174583dChristian Maeder , parenPrec Prefix $ toMixType t2 ])

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in case topTy of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypeName name@(Id ts cs _) _k _i ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case map toMixType tyArgs of

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder [dArg] -> case ts of

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder [e] | name == lazyTypeId ->

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (Lazyfix, pretty e <+> parenPrec Lazyfix dArg)

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder [e1, e2, e3] | not (isPlace e1) && isPlace e2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder && not (isPlace e3) && null cs ->

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (Outfix, fsep [pretty e1, snd dArg, pretty e3])

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> aArgs

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder [dArg1, dArg2] -> case ts of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [_, e2, _] | isInfix name && null cs ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder if tokStr e2 == prodS then

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (ProdInfix, fsep

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder [ parenPrec ProdInfix dArg1

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , cross, parenPrec ProdInfix dArg2])

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder else -- assume fun type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (FunInfix, fsep

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [ parenPrec FunInfix dArg1

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder , printTypeToken e2, snd dArg2])

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> aArgs

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder dArgs -> if isProductIdWithArgs name $ length tyArgs then

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (ProdInfix, fsep $ punctuate (space <> cross) $

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (parenPrec ProdInfix) dArgs) else aArgs

37354e3ed68875fb527338105a610df481f98cb0Christian Maeder _ -> aArgs

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance Pretty Type where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty = snd . toMixType

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- no curried notation for bound variables

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeScheme where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (TypeScheme vs t _) = let tdoc = pretty t in

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if null vs then tdoc else

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep [forallDoc, semiDs vs, bullet <+> tdoc]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Partiality where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty p = case p of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Partial -> quMarkD

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Total -> empty

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Quantifier where

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian 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

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty Term where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty = printTerm . rmSomeTypes

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederisSimpleTerm :: Term -> Bool

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederisSimpleTerm trm = case trm of

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder QualVar _ -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder QualOp _ _ _ _ _ -> True

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder ResolvedMixTerm _ _ _ _ -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ApplTerm _ _ _ -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TupleTerm _ _ -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TermToken _ -> True

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder BracketTerm _ _ _ -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> False

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | used only to produce CASL applications

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederisSimpleArgTerm :: Term -> Bool

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian MaederisSimpleArgTerm trm = case trm of

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder QualVar vd -> not (isPatVarDecl vd)

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder QualOp _ _ _ _ _ -> True

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder ResolvedMixTerm n _ l _ -> placeCount n /= 0 || not (null l)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TupleTerm _ _ -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder BracketTerm _ _ _ -> True

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder _ -> False

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian MaederhasRightQuant :: Term -> Bool

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederhasRightQuant t = case t of

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder QuantifiedTerm {} -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder LambdaTerm {} -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder CaseTerm {} -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder LetTerm Let _ _ _ -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> hasRightQuant (last ts)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case t2 of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder _ -> hasRightQuant t2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ApplTerm _ t2 _ -> hasRightQuant t2

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder _ -> False

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederzipArgs :: Id -> [Term] -> [Doc] -> [Doc]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederzipArgs n ts ds = case (ts, ds) of

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (t : r, d : s) -> let

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder p = parenTermDoc t d

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder e = if hasRightQuant t then parens d else p

966e627a1c06b302a06d59d08b8ab45905f3509cChristian Maeder in if null r && null s && endPlace n then

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [if hasRightQuant t then d else p]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else e : zipArgs n r s

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> []

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederisPatVarDecl :: VarDecl -> Bool

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederisPatVarDecl (VarDecl v ty _ _) = case ty of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypeName t _ _ -> isSimpleId v && take 2 (show t) == "_v"

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder _ -> False

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederparenTermDoc :: Term -> Doc -> Doc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederparenTermDoc trm = if isSimpleTerm trm then id else parens

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintTermRec :: FoldRec Doc (Doc, Doc)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintTermRec = FoldRec

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder { foldQualVar = \ _ vd@(VarDecl v _ _ _) ->

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder if isPatVarDecl vd then pretty v

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder else parens $ keyword varS <+> pretty vd

68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder , foldQualOp = \ _ br n t tys _ -> (if null tys then id else

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (<> brackets (ppWithCommas tys))) $

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder parens $ fsep [pretty br, pretty n, colon, pretty $

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if isPred br then unPredTypeScheme t else t]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldResolvedMixTerm =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder \ (ResolvedMixTerm _ _ os _) n@(Id toks cs ps) tys ts _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let pn = placeCount n in if pn == length ts || null ts then

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let ds = zipArgs n os ts in

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if null tys then idApplDoc n ds

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else let (ftoks, _) = splitMixToken toks

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fId = Id ftoks cs ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (fts, rts) = splitAt (placeCount fId) $ if null ts

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder then replicate pn $ pretty placeTok else ds

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder in fsep $ (idApplDoc fId fts <> brackets (ppWithCommas tys))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder : rts

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else idApplDoc applId [idDoc n, parens $ sepByCommas ts]

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , foldApplTerm = \ (ApplTerm o1 o2 _) t1 t2 _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case (o1, o2) of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- comment out the following two guards for CASL applications

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (ResolvedMixTerm n _ [] _, TupleTerm ts@(_ : _) _)

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder | placeCount n == length ts ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder idApplDoc n (zipArgs n ts $ map printTerm ts)

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (ResolvedMixTerm n _ [] _, _) | placeCount n == 1

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> idApplDoc n $ zipArgs n [o2] [t2]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldTypedTerm = \ (TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder LambdaTerm {} -> parens

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder LetTerm {} -> parens

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder CaseTerm {} -> parens

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder QuantifiedTerm {} -> parens

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder _ -> id) t, pretty q, pretty typ]

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder , foldQuantifiedTerm = \ _ q vs t _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep [pretty q, printGenVarDecls vs, bullet <+> t]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldLambdaTerm = \ _ ps q t _ ->

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder fsep [ lambda

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , case ps of

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder [p] -> if show p == "()" then empty else p

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder _ -> fcat $ map parens ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , (case q of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Partial -> bullet

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Total -> bullet <> text exMark) <+> t]

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , foldCaseTerm = \ _ t es _ ->

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder fsep [text caseS, t, text ofS,

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cat $ punctuate (space <> bar <> space) $

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (printEq0 funArrow) es]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldLetTerm = \ _ br es t _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let des = sep $ punctuate semi $ map (printEq0 equals) es

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian 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]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian 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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fsep [pretty v, text asP, p]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldProgEq = \ _ p t _ -> (p, t) }

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederprintTerm :: Term -> Doc

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederprintTerm = foldTerm printTermRec

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederrmTypeRec :: MapRec

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederrmTypeRec = mapRec

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder { foldQualOp = \ t _ i _ _ ps ->

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder if elem i $ map fst bList then

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder ResolvedMixTerm i [] [] ps else t

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldTypedTerm = \ _ nt q ty ps ->

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder case q of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Inferred -> nt

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder _ -> case nt of

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder QualVar (VarDecl _ oty _ _) | oty == ty -> nt

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> TypedTerm nt q ty ps }

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrmSomeTypes :: Term -> Term

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrmSomeTypes = foldTerm rmTypeRec

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | put parenthesis around applications

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederparenTermRec :: MapRec

eab576044505ba1fbc64610323053490fbd9e82cChristian MaederparenTermRec = let

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder addParAppl t = case t of

eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder ResolvedMixTerm _ _ [] _ -> t

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder QualVar _ -> t

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder QualOp _ _ _ _ _ -> t

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder TermToken _ -> t

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder BracketTerm _ _ _ -> t

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TupleTerm _ _ -> t

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder _ -> TupleTerm [t] nullRange

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in mapRec

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { foldApplTerm = \ _ t1 t2 ps ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ApplTerm (addParAppl t1) (addParAppl t2) ps

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder , foldResolvedMixTerm = \ _ n tys ts ps ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ResolvedMixTerm n tys (map addParAppl ts) ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldTypedTerm = \ _ t q typ ps ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypedTerm (addParAppl t) q typ ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldMixfixTerm = \ _ ts -> MixfixTerm $ map addParAppl ts

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder , foldAsPattern = \ _ v p ps -> AsPattern v (addParAppl p) ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder }

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederparenTerm :: Term -> Term

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederparenTerm = foldTerm parenTermRec

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | print an equation with different symbols between 'Pattern' and 'Term'

ce3928e71520030ad0275b72050a8f4377f9313cChristian MaederprintEq0 :: Doc -> (Doc, Doc) -> Doc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintEq0 s (p, t) = sep [p, hsep [s, t]]

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintGenVarDecls :: [GenVarDecl] -> Doc

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian MaederprintGenVarDecls = fsep . punctuate semi . map

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ( \ l -> case l of

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder [x] -> pretty x

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GenVarDecl (VarDecl _ t _ _) : _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ppWithCommas (map ( \ (GenVarDecl (VarDecl v _ _ _)) -> v) l)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <> printVarDeclType t

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GenTypeVarDecl (TypeArg _ e c _ _ _ _) : _ ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ppWithCommas (map ( \ (GenTypeVarDecl v) -> varOfTypeArg v) l)

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder <> printVarKind e c

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder _ -> error "printGenVarDecls") . groupBy sameType

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder

48c4688439e0aade4faeebf25ca8b16d661e47afChristian MaedersameType :: GenVarDecl -> GenVarDecl -> Bool

48c4688439e0aade4faeebf25ca8b16d661e47afChristian MaedersameType g1 g2 = case (g1, g2) of

aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder (GenVarDecl (VarDecl _ t1 Comma _), GenVarDecl (VarDecl _ t2 _ _))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | t1 == t2 -> True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (GenTypeVarDecl (TypeArg _ e1 c1 _ _ Comma _),

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GenTypeVarDecl (TypeArg _ e2 c2 _ _ _ _)) | e1 == e2 && c1 == c2 -> True

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder _ -> False

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder

ce3928e71520030ad0275b72050a8f4377f9313cChristian MaederprintVarDeclType :: Type -> Doc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintVarDeclType t = case t of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder MixfixType [] -> empty

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> space <> colon <+> pretty t

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty VarDecl where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (VarDecl v t _ _) = pretty v <> printVarDeclType t

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maederinstance Pretty GenVarDecl where

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder pretty gvd = case gvd of

aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder GenVarDecl v -> pretty v

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GenTypeVarDecl tv -> pretty tv

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty TypeArg where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (TypeArg v e c _ _ _ _) =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty v <> printVarKind e c

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | don't print an empty list and put parens around longer lists

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintList0 :: (Pretty a) => [a] -> Doc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprintList0 l = case l of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [] -> empty

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder [x] -> pretty x

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> parens $ ppWithCommas l

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder

aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance Pretty BasicSpec where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty (BasicSpec l) = if null l then specBraces empty else

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder changeGlobalAnnos addBuiltins . vcat $ map pretty l

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty ProgEq where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty = printEq0 equals . foldEq printTermRec

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Pretty BasicItem where

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pretty bi = case bi of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder SigItems s -> pretty s

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ProgItems l _ -> sep [keyword programS, semiAnnoted l]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ClassItems i l _ -> let

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder b = semiAnnos pretty l

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder p = plClass l

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in case i of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Plain -> topSigKey (classS ++ if p then "es" else "") <+> b

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Instance -> sep [keyword classS <+>

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder keyword (instanceS ++ if p then sS else ""), b]

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder GenVarItems l _ -> topSigKey (varS ++ pluralS l) <+> printGenVarDecls l

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder FreeDatatype l _ -> sep

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [ keyword freeS <+> keyword (typeS ++ pluralS l)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , semiAnnos pretty l]

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder GenItems l _ -> let gkw = keyword generatedS in

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (if all (isDatatype . item) l then \ i -> gkw <+> rmTopKey i

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else \ i -> sep [gkw, specBraces i])

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ vcat $ map (printAnnoted pretty) l

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder AxiomItems vs fs _ -> sep

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [ if null vs then empty else forallDoc <+> printGenVarDecls vs

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , case fs of

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder [] -> empty

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> let pp = addBullet . pretty in

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder vcat $ map (printAnnoted pp) (init fs)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ [printSemiAnno pp True $ last fs]]

f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder Internal l _ -> sep

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [ keyword internalS

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , specBraces $ vcat $ map (printAnnoted pretty) l]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederplClass :: [Annoted ClassItem] -> Bool

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederplClass l = case map item l of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ : _ : _ -> True

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder [ClassItem (ClassDecl (_ : _ : _) _ _) _ _] -> True

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder _ -> False

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederpluralS :: [a] -> String

413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederpluralS l = case l of

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder _ : _ : _ -> sS

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder _ -> ""

isDatatype :: SigItems -> Bool

isDatatype si = case si of

TypeItems _ l _ -> all

((\ t -> case t of

Datatype _ -> True

_ -> False) . item) l

_ -> False

instance Pretty OpBrand where

pretty b = keyword $ show b

instance Pretty SigItems where

pretty si = case si of

TypeItems i l _ -> let b = semiAnnos pretty l in case i of

Plain -> topSigKey ((if all (isSimpleTypeItem . item) l

then typeS else typeS) ++ plTypes l) <+> b

Instance ->

sep [keyword typeS <+> keyword (instanceS ++ plTypes l), b]

OpItems b l _ -> noNullPrint l $ topSigKey (show b ++ plOps l)

<+> let po = (prettyOpItem $ isPred b) in

if case item $ last l of

OpDecl _ _ a@(_ : _) _ -> case last a of

UnitOpAttr {} -> True

_ -> False

OpDefn {} -> True

_ -> False

then vcat (map (printSemiAnno po True) l)

else semiAnnos po l

plTypes :: [Annoted TypeItem] -> String

plTypes l = case map item l of

_ : _ : _ -> sS

[TypeDecl (_ : _ : _) _ _] -> sS

[SubtypeDecl (_ : _ : _) _ _] -> sS

[IsoDecl (_ : _ : _) _] -> sS

_ -> ""

plOps :: [Annoted OpItem] -> String

plOps l = case map item l of

_ : _ : _ -> sS

[OpDecl (_ : _ : _) _ _ _] -> sS

_ -> ""

isSimpleTypeItem :: TypeItem -> Bool

isSimpleTypeItem ti = case ti of

TypeDecl l k _ -> k == universe && all isSimpleTypePat l

SubtypeDecl l (TypeName i _ _) _ ->

not (isMixfix i) && all isSimpleTypePat l

SubtypeDefn p (Var _) t _ _ ->

isSimpleTypePat p && isSimpleType t

_ -> False

isSimpleTypePat :: TypePattern -> Bool

isSimpleTypePat tp = case tp of

TypePattern i [] _ -> not $ isMixfix i

_ -> False

isSimpleType :: Type -> Bool

isSimpleType t = case t of

TypeName i _ _ -> not $ isMixfix i

TypeToken _ -> True

MixfixType[TypeToken _, BracketType Squares (_ : _) _] -> True

_ -> False

instance Pretty ClassItem where

pretty (ClassItem d l _) = pretty d $+$ noNullPrint l

(specBraces $ vcat $ map (printAnnoted pretty) l)

instance Pretty ClassDecl where

pretty (ClassDecl l k _) = let cs = ppWithCommas l in

if k == universe then cs else fsep [cs, less, pretty k]

instance Pretty Vars where

pretty vd = case vd of

Var v -> pretty v

VarTuple vs _ -> parens $ ppWithCommas vs

instance Pretty TypeItem where

pretty ti = case ti of

TypeDecl l k _ -> ppWithCommas l <> printKind k

SubtypeDecl l t _ ->

fsep [ppWithCommas l, less, pretty t]

IsoDecl l _ -> fsep $ punctuate (space <> equals) $ map pretty l

SubtypeDefn p v t f _ ->

fsep [pretty p, equals,

specBraces $ fsep

[pretty v, colon <+> pretty t, bullet <+> pretty f]]

AliasType p _ (TypeScheme l t _) _ ->

fsep $ pretty p : map (pretty . varOfTypeArg) l

++ [text assignS <+> pretty t]

Datatype t -> pretty t

prettyTypeScheme :: Bool -> TypeScheme -> Doc

prettyTypeScheme b = pretty . (if b then unPredTypeScheme else id)

prettyOpItem :: Bool -> OpItem -> Doc

prettyOpItem b oi = case oi of

OpDecl l t a _ -> fsep $ punctuate comma (map pretty l)

++ [colon <+>

(if null a then id else (<> comma))(prettyTypeScheme b t)]

++ punctuate comma (map pretty a)

OpDefn n ps s t _ -> fcat $

((if null ps then (<> space) else id) $ pretty n)

: map ((<> space) . parens . semiDs) ps

++ (if b then [] else [colon <+> prettyTypeScheme b s <> space])

++ [(if b then equiv else equals) <> space, pretty t]

instance Pretty BinOpAttr where

pretty a = text $ case a of

Assoc -> assocS

Comm -> commS

Idem -> idemS

instance Pretty OpAttr where

pretty oa = case oa of

BinOpAttr a _ -> pretty a

UnitOpAttr t _ -> text unitS <+> pretty t

instance Pretty DatatypeDecl where

pretty (DatatypeDecl p k alts d _) =

fsep [ pretty p <> printKind k, defn

<+> cat (punctuate (space <> bar <> space)

$ map pretty alts)

, case d of

[] -> empty

_ -> keyword derivingS <+> ppWithCommas d]

instance Pretty Alternative where

pretty alt = case alt of

Constructor n cs p _ -> pretty n <+> fsep

(map ( \ l -> case (l, p) of

-- comment out the following line to output real CASL

([NoSelector (TypeToken t)], Total) | isSimpleId n -> pretty t

_ -> parens $ semiDs l) cs) <> pretty p

Subtype l _ -> text (if all isSimpleType l then typeS else typeS)

<+> ppWithCommas l

instance Pretty Component where

pretty sel = case sel of

Selector n _ t _ _ -> sep [pretty n, colon <+> pretty t]

NoSelector t -> pretty t

instance Pretty Symb where

pretty (Symb i mt _) =

sep $ pretty i : case mt of

Nothing -> []

Just (SymbType t) -> [colon <+> pretty t]

instance Pretty SymbItems where

pretty (SymbItems k syms _ _) =

printSK k syms <> ppWithCommas syms

instance Pretty SymbOrMap where

pretty (SymbOrMap s mt _) =

sep $ pretty s : case mt of

Nothing -> []

Just t -> [mapsto <+> pretty t]

instance Pretty SymbMapItems where

pretty (SymbMapItems k syms _ _) =

printSK k syms <> ppWithCommas syms

-- | print symbol kind

printSK :: SymbKind -> [a] -> Doc

printSK k l = case k of

Implicit -> empty

_ -> keyword (drop 3 (show k) ++ case l of

_ : _ : _ -> sS

_ -> "") <> space