38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- HetCATS/HasCASL/PrintAs.hs

46c318705d1532d90572abf9ee869016583d985bTill Mossakowski $Id$

2cff1f0e5a572a33bc692c96ce2a1590f160eed7cmaeder Authors: Christian Maeder

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Year: 2002

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

34bff097c14521b5e57ce37279a34256e1f78aa5Klaus Luettich printing As data types

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-}

2cff1f0e5a572a33bc692c96ce2a1590f160eed7cmaeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maedermodule PrintAs where

46c318705d1532d90572abf9ee869016583d985bTill Mossakowski

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederimport As

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Keywords

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport HToken

66771c3723200a54eceaf0d82de861ca4b917b05Christian Maederimport Pretty

66771c3723200a54eceaf0d82de861ca4b917b05Christian Maederimport PrettyPrint

66771c3723200a54eceaf0d82de861ca4b917b05Christian Maederimport GlobalAnnotations(GlobalAnnos)

66771c3723200a54eceaf0d82de861ca4b917b05Christian Maederimport GlobalAnnotationsFunctions(emptyGlobalAnnos)

66771c3723200a54eceaf0d82de861ca4b917b05Christian Maederimport Print_AS_Annotation

be110dccc9f7bd9e987b35943b16ccb22922248fChristian Maeder

66771c3723200a54eceaf0d82de861ca4b917b05Christian MaedernoPrint :: Bool -> Doc -> Doc

66771c3723200a54eceaf0d82de861ca4b917b05Christian MaedernoPrint b d = if b then empty else d

66771c3723200a54eceaf0d82de861ca4b917b05Christian Maeder

d0c8d69c1a35ed2972ae093ecf7abb12dfbafb4dChristian MaedershowPretty :: PrettyPrint a => a -> ShowS

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian MaedershowPretty = showString . render . printText0 emptyGlobalAnnos

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder where _just_avoid_unused_import_warning = smallSpace_latex

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder

66771c3723200a54eceaf0d82de861ca4b917b05Christian Maedercommas, semis :: PrettyPrint a => GlobalAnnos -> [a] -> Doc

b53688bfed888214b485cf76439d57262d80e0a7Christian Maedercommas ga l = fcat $ punctuate comma (map (printText0 ga) l)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maedersemis ga l = sep $ punctuate semi (map (printText0 ga) l)

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maederinstance PrettyPrint TypePattern where

bbcb456803d40f9b48dd43b1c84bdf8932d2672bChristian Maeder printText0 ga (TypePattern name args _) = printText0 ga name

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder <> fcat (map (parens . printText0 ga) args)

60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa printText0 ga (TypePatternToken t) = printText0 ga t

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder printText0 ga (MixfixTypePattern ts) = fsep (map (printText0 ga) ts)

b0b5ce95f738d35e520c20d1b0bd253f152a677fChristian Maeder printText0 ga (BracketTypePattern k l _) = bracket k $ commas ga l

ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder printText0 ga (TypePatternArgs l) = semis ga l

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder

ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maederbracket :: BracketKind -> Doc -> Doc

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maederbracket Parens t = parens t

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederbracket Squares t = Pretty.brackets t

ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maederbracket Braces t = braces t

db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederprintKind :: GlobalAnnos -> Kind -> Doc

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian MaederprintKind ga kind = case kind of

91a356d176c7e9b4eef6e8734559bfb858d5e630Christian Maeder PlainClass (Intersection [] _) -> empty

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder _ -> space <> colon <> printText0 ga kind

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint Type where

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder printText0 ga (TypeName name i) = printText0 ga name

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder <> if i == 0 then empty

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder else parens (int i)

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (TypeAppl t1 t2) = parens (printText0 ga t1)

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder <> parens (printText0 ga t2)

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder printText0 ga (TypeToken t) = printText0 ga t

af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz printText0 ga (BracketType k l _) = bracket k $ commas ga l

593ac6474255679d77ce1961474355822176ba43Christian Maeder printText0 ga (KindedType t kind _) = printText0 ga t

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa <> printKind ga kind

bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder printText0 ga (MixfixType ts) = fsep (map (printText0 ga) ts)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder printText0 ga (LazyType t _) = text quMark <+> printText0 ga (t)

3753288339ad80053053d92409bd37b335a96197Christian Maeder printText0 ga (ProductType ts _) = fsep (punctuate (space <> text timesS)

3753288339ad80053053d92409bd37b335a96197Christian Maeder (map (printText0 ga) ts))

3753288339ad80053053d92409bd37b335a96197Christian Maeder printText0 ga (FunType t1 arr t2 _) = printText0 ga t1

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder <+> printText0 ga arr

3753288339ad80053053d92409bd37b335a96197Christian Maeder <+> printText0 ga t2

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder

3753288339ad80053053d92409bd37b335a96197Christian Maederinstance PrettyPrint Pred where

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder printText0 ga (IsIn c ts) = if null ts then printText0 ga c

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder else if null $ tail ts then

3753288339ad80053053d92409bd37b335a96197Christian Maeder printText0 ga (head ts) <+>

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder colon <+> printText0 ga c

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder else printText0 ga c <+>

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder fsep (punctuate space

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder (map (printText0 ga) ts))

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder

897a04683fb30873e84dc3360dea770a4435971cChristian Maederinstance PrettyPrint t => PrettyPrint (Qual t) where

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder printText0 ga (ps :=> t) = (if null ps then empty

9a7f7c6399a1014e51abc7049a5fbd265461e1a7Christian Maeder else parens $ commas ga ps <+>

9a7f7c6399a1014e51abc7049a5fbd265461e1a7Christian Maeder ptext implS <+> space) <>

593ac6474255679d77ce1961474355822176ba43Christian Maeder printText0 ga t

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder

dab742f3b90c81f4a926ef2cdb096d358fb72c12Christian Maeder-- no curried notation for bound variables

dab742f3b90c81f4a926ef2cdb096d358fb72c12Christian Maederinstance PrettyPrint TypeScheme where

c3d02da98e2806333eacf170309abff7a1377e14notanartist printText0 ga (TypeScheme vs t _) = noPrint (null vs) (text forallS

c3d02da98e2806333eacf170309abff7a1377e14notanartist <+> semis ga vs

c3d02da98e2806333eacf170309abff7a1377e14notanartist <+> text dotS <+> space)

dab742f3b90c81f4a926ef2cdb096d358fb72c12Christian Maeder <> printText0 ga t

dab742f3b90c81f4a926ef2cdb096d358fb72c12Christian Maeder

9a7f7c6399a1014e51abc7049a5fbd265461e1a7Christian Maederinstance PrettyPrint Partiality where

9a7f7c6399a1014e51abc7049a5fbd265461e1a7Christian Maeder printText0 _ Partial = text quMark

593ac6474255679d77ce1961474355822176ba43Christian Maeder printText0 _ Total = text exMark

897a04683fb30873e84dc3360dea770a4435971cChristian Maeder

06b97c160c9160682f18591409cadc9e97873020Christian Maederinstance PrettyPrint Arrow where

06b97c160c9160682f18591409cadc9e97873020Christian Maeder printText0 _ FunArr = text funS

9a7f7c6399a1014e51abc7049a5fbd265461e1a7Christian Maeder printText0 _ PFunArr = text pFun

06b97c160c9160682f18591409cadc9e97873020Christian Maeder printText0 _ ContFunArr = text contFun

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder printText0 _ PContFunArr = text pContFun

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder

8869b0b47d4ebc275098d1777301b652648b3c45Christian Maeder

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maederinstance PrettyPrint Quantifier where

38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder printText0 _ Universal = text forallS

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder printText0 _ Existential = text existsS

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder printText0 _ Unique = text $ existsS ++ exMark

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

60e6795dd310e10194e12bb660575aadf941328bEugen Kuksainstance PrettyPrint TypeQual where

60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa printText0 _ OfType = colon

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder printText0 _ AsType = text asS

38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder printText0 _ InType = text inS

38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder

8869b0b47d4ebc275098d1777301b652648b3c45Christian Maederinstance PrettyPrint LogOp where

94c729aeac99df6d844da014f46d584c035a91a6Christian Maeder printText0 _ NotOp = text notS

38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder printText0 _ AndOp = text lAnd

8869b0b47d4ebc275098d1777301b652648b3c45Christian Maeder printText0 _ OrOp = text lOr

8869b0b47d4ebc275098d1777301b652648b3c45Christian Maeder printText0 _ ImplOp = text implS

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder printText0 _ EquivOp = text equivS

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder

38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maederinstance PrettyPrint EqOp where

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder printText0 _ EqualOp = text equalS

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder printText0 _ ExEqualOp = text exEqual

2a9702a373738717c83824512bd9389b5870fc92Christian Maeder

2a9702a373738717c83824512bd9389b5870fc92Christian Maederinstance PrettyPrint Formula where

2a9702a373738717c83824512bd9389b5870fc92Christian Maeder printText0 ga (TermFormula t) = printText0 ga t

e90b8ee3fac5c932d83af2061579c6b57d528885Christian Maeder printText0 ga (ConnectFormula o fs _) = parens $

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder fsep (punctuate (space <> printText0 ga o) (map (printText0 ga) fs))

7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder printText0 ga (EqFormula o t1 t2 _) = printText0 ga t1

a081d56252673c9e4a017e6282f59766f0cbcd42Christian Maeder <+> printText0 ga o

a081d56252673c9e4a017e6282f59766f0cbcd42Christian Maeder <+> printText0 ga t2

2a9702a373738717c83824512bd9389b5870fc92Christian Maeder printText0 ga (DefFormula t _) = text defS <+> printText0 ga t

2a9702a373738717c83824512bd9389b5870fc92Christian Maeder printText0 ga (QuantifiedFormula q vs f _) =

2a9702a373738717c83824512bd9389b5870fc92Christian Maeder printText0 ga q <+> semis ga vs <+> text dotS <+> printText0 ga f

91a356d176c7e9b4eef6e8734559bfb858d5e630Christian Maeder printText0 ga (PolyFormula ts f _) =

91a356d176c7e9b4eef6e8734559bfb858d5e630Christian Maeder text forallS <+> semis ga ts <+> text dotS <+> printText0 ga f

2a9702a373738717c83824512bd9389b5870fc92Christian Maeder

2a9702a373738717c83824512bd9389b5870fc92Christian Maederinstance PrettyPrint Term where

7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder printText0 ga (CondTerm t1 f t2 _) = printText0 ga t1

7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder <+> text whenS

f39c70229e74147a02d15bd45c05a0b1b325532dChristian Maeder <+> printText0 ga f

11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder <+> text elseS

db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder <+> printText0 ga t2

bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder printText0 ga (QualVar v t _) = parens $ text varS

f997c50e79d277ae8d7d3bc536a276d67b75f953Simon Ulbricht <+> printText0 ga v

f997c50e79d277ae8d7d3bc536a276d67b75f953Simon Ulbricht <+> colon

be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder <+> printText0 ga t

f997c50e79d277ae8d7d3bc536a276d67b75f953Simon Ulbricht printText0 ga (QualOp n t _) = parens $

f39c70229e74147a02d15bd45c05a0b1b325532dChristian Maeder text opS

f39c70229e74147a02d15bd45c05a0b1b325532dChristian Maeder <+> printText0 ga n

f39c70229e74147a02d15bd45c05a0b1b325532dChristian Maeder <+> colon

7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder <+> printText0 ga t

333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder printText0 ga (ApplTerm t1 t2 _) = printText0 ga t1

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder <+> parens (printText0 ga t2)

8a2f18f56cc083acea15615185e5e9366bc9eceeChristian Maeder printText0 ga (TupleTerm ts _) = parens $ commas ga ts

cb2044812811d66efe038d914966e04290be93faChristian Maeder printText0 ga (TypedTerm term q typ _) = printText0 ga term

333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder <+> printText0 ga q

cb2044812811d66efe038d914966e04290be93faChristian Maeder <+> printText0 ga typ

94c729aeac99df6d844da014f46d584c035a91a6Christian Maeder printText0 ga (QuantifiedTerm q vs t _) = printText0 ga q

94c729aeac99df6d844da014f46d584c035a91a6Christian Maeder <+> semis ga vs

94c729aeac99df6d844da014f46d584c035a91a6Christian Maeder <+> text dotS

94c729aeac99df6d844da014f46d584c035a91a6Christian Maeder <+> printText0 ga t

cb2044812811d66efe038d914966e04290be93faChristian Maeder printText0 ga (LambdaTerm ps q t _) = text lamS

ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder <+> (if length ps == 1 then

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder printText0 ga $ head ps

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder else fcat $ map

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder (parens.printText0 ga) ps)

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder <+> (case q of

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder Partial -> text dotS

93603bd881e43d4ff5a57d7ca4e2b9fa619f25b4cmaeder Total -> text $ dotS ++ exMark)

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder <+> printText0 ga t

55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa printText0 ga (CaseTerm t es _ ) = text caseS

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder <+> printText0 ga t

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> text ofS

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> vcat (punctuate (text " | ")

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder (map (printEq0 ga funS) es))

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (LetTerm es t _) = text letS

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> vcat (punctuate semi

0130083f314580170af1195037be3325f125fbceChristian Maeder (map (printEq0 ga equalS) es))

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> text inS

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> printText0 ga t

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (TermToken t) = printText0 ga t

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (MixfixTerm ts) = fsep $ map (printText0 ga) ts

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (BracketTerm k l _) = bracket k $ commas ga l

0130083f314580170af1195037be3325f125fbceChristian Maeder

ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maederinstance PrettyPrint Pattern where

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa printText0 ga (PatternVars vs _) = semis ga vs

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printText0 ga (PatternConstr n t args _) = printText0 ga n

ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder <+> colon

23b1f89c05c67d7778e2736bd24fdec33212f323cmaeder <+> printText0 ga t

23b1f89c05c67d7778e2736bd24fdec33212f323cmaeder <+> fcat (map (parens.printText0 ga) args)

23b1f89c05c67d7778e2736bd24fdec33212f323cmaeder printText0 ga (PatternToken t) = printText0 ga t

23b1f89c05c67d7778e2736bd24fdec33212f323cmaeder printText0 ga (BracketPattern k l _) =

23b1f89c05c67d7778e2736bd24fdec33212f323cmaeder case l of

23b1f89c05c67d7778e2736bd24fdec33212f323cmaeder [TuplePattern _ _] -> printText0 ga $ head l

0130083f314580170af1195037be3325f125fbceChristian Maeder _ -> bracket k $ commas ga l

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (TuplePattern ps _) = parens $ commas ga ps

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (MixfixPattern ps) = fsep (map (printText0 ga) ps)

0130083f314580170af1195037be3325f125fbceChristian Maeder printText0 ga (TypedPattern p t _) = printText0 ga p

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> colon

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> printText0 ga t

c4b508b43eb5e3a92e464b5f85b5a2b5ecd7d3c3cmaeder printText0 ga (AsPattern v p _) = printText0 ga v

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> text asP

0130083f314580170af1195037be3325f125fbceChristian Maeder <+> printText0 ga p

0130083f314580170af1195037be3325f125fbceChristian Maeder

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa

0130083f314580170af1195037be3325f125fbceChristian MaederprintEq0 :: GlobalAnnos -> String -> ProgEq -> Doc

0130083f314580170af1195037be3325f125fbceChristian MaederprintEq0 ga s (ProgEq p t _) = fsep [printText0 ga p

0130083f314580170af1195037be3325f125fbceChristian Maeder , text s

0130083f314580170af1195037be3325f125fbceChristian Maeder , printText0 ga t]

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder

2cff1f0e5a572a33bc692c96ce2a1590f160eed7cmaederinstance PrettyPrint VarDecl where

2cff1f0e5a572a33bc692c96ce2a1590f160eed7cmaeder printText0 ga (VarDecl v t _ _) = printText0 ga v <+> colon

2cff1f0e5a572a33bc692c96ce2a1590f160eed7cmaeder <+> printText0 ga t

fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder

2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaederinstance PrettyPrint GenVarDecl where

fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder printText0 ga (GenVarDecl v) = printText0 ga v

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder printText0 ga (GenTypeVarDecl tv) = printText0 ga tv

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maederinstance PrettyPrint TypeArg where

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder printText0 ga (TypeArg v c _ _) = printText0 ga v <> colon

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder <> printText0 ga c

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder

fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaederinstance PrettyPrint Variance where

2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder printText0 _ CoVar = text plusS

2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder printText0 _ ContraVar = text minusS

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder printText0 _ InVar = empty

2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maederinstance PrettyPrint Kind where

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder printText0 ga (PlainClass c) = printText0 ga c

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder printText0 ga (ExtClass k v _) = (case k of

fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder PlainClass _ -> id

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder _ -> parens) (printText0 ga k)

1c4dfa148603d4fcf4cdd2ed66c8b6e1de0dd696Till Mossakowski <> printText0 ga v

2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder printText0 ga (ProdClass l _) = fcat $ punctuate (space <> text timesS)

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder (map (\ k ->

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder (case k of KindAppl _ _ _ -> parens

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder ProdClass _ _ -> parens

ea2dff2ba7790f5c9f8f5454181f86f45d2674d2Christian Maeder _ -> id)

1c4dfa148603d4fcf4cdd2ed66c8b6e1de0dd696Till Mossakowski (printText0 ga k)) l)

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder printText0 ga (KindAppl k1 k2 _) =

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder (case k1 of

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder KindAppl _ _ _ -> parens

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder _ -> id) (printText0 ga k1)

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder <+> text funS

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder <> printText0 ga k2

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder

f448ac6b7846addfe6041275edf1fb90962e76eacmaederinstance PrettyPrint Class where

f448ac6b7846addfe6041275edf1fb90962e76eacmaeder printText0 ga (Downset t) = braces $

text "_" <+> text lessS <+> printText0 ga t

printText0 ga (Intersection c _) = if null c then ptext "Type"

else if null $ tail c then printText0 ga $ head c

else parens $ commas ga c

instance PrettyPrint Types where

printText0 ga (Types l _) = Pretty.brackets $ commas ga l

instance PrettyPrint InstOpId where

printText0 ga (InstOpId n l) = printText0 ga n

<> fcat(map (printText0 ga) l)

------------------------------------------------------------------------

-- item stuff

------------------------------------------------------------------------

instance PrettyPrint PseudoType where

printText0 ga (PseudoType l t _) = noPrint (null l) (text lamS

<+> fcat(map (printText0 ga) l)

<+> text dotS <+> space) <> printText0 ga t

instance PrettyPrint TypeArgs where

printText0 ga (TypeArgs l _) = semis ga l

instance PrettyPrint TypeVarDecls where

printText0 ga (TypeVarDecls l _) = Pretty.brackets $ semis ga l

instance PrettyPrint BasicSpec where

printText0 ga (BasicSpec l) = vcat (map (printText0 ga) l)

instance PrettyPrint ProgEq where

printText0 ga = printEq0 ga equalS

instance PrettyPrint BasicItem where

printText0 ga (SigItems s) = printText0 ga s

printText0 ga (ProgItems l _) = text programS <+> semis ga l

printText0 ga (ClassItems i l _) = text classS <+> printText0 ga i

<+> semis ga l

printText0 ga (GenVarItems l _) = text varS <+> semis ga l

printText0 ga (FreeDatatype l _) = text freeS <+> text typeS

<+> semis ga l

printText0 ga (GenItems l _) = text generatedS <+> braces (semis ga l)

printText0 ga (AxiomItems vs fs _) = (if null vs then empty

else text forallS <+> semis ga vs)

$$ vcat (map

(\x -> text dotS <+> printText0 ga x)

fs)

instance PrettyPrint SigItems where

printText0 ga (TypeItems i l _) = text typeS <+> printText0 ga i

<+> semis ga l

printText0 ga (OpItems l _) = text opS <+> semis ga l

printText0 ga (PredItems l _) = text predS <+> semis ga l

instance PrettyPrint Instance where

printText0 _ Instance = text instanceS

printText0 _ _ = empty

instance PrettyPrint ClassItem where

printText0 ga (ClassItem d l _) = printText0 ga d $$

if null l then empty

else braces (semis ga l)

instance PrettyPrint ClassDecl where

printText0 ga (ClassDecl l _) = commas ga l

printText0 ga (SubclassDecl l s _) = commas ga l <> text lessS

<> printText0 ga s

printText0 ga (ClassDefn n c _) = printText0 ga n

<> text equalS

<> printText0 ga c

printText0 ga (DownsetDefn c v t _) =

let pv = printText0 ga v in

printText0 ga c

<> text equalS

<> braces (pv <> text dotS <> pv

<> text lessS

<+> printText0 ga t)

instance PrettyPrint TypeItem where

printText0 ga (TypeDecl l k _) = commas ga l <>

printKind ga k

printText0 ga (SubtypeDecl l t _) = commas ga l <+> text lessS

<+> printText0 ga t

printText0 ga (IsoDecl l _) = cat(punctuate (text " = ")

(map (printText0 ga) l))

printText0 ga (SubtypeDefn p v t f _) = printText0 ga p

<+> text equalS

<+> braces (printText0 ga v

<+> colon

<+> printText0 ga t

<+> text dotS

<+> printText0 ga f)

printText0 ga (AliasType p k t _) = (printText0 ga p <>

printKind ga k)

<+> text assignS

<+> printText0 ga t

printText0 ga (Datatype t) = printText0 ga t

instance PrettyPrint OpItem where

printText0 ga (OpDecl l t as _) = commas ga l <+> colon

<+> (printText0 ga t

<> (if null as then empty else comma)

<> commas ga as)

printText0 ga (OpDefn n ps s p t _) = (printText0 ga n

<> fcat (map (printText0 ga) ps))

<+> (colon <> if p == Partial

then text quMark else empty)

<+> printText0 ga s

<+> text equalS

<+> printText0 ga t

instance PrettyPrint PredItem where

printText0 ga (PredDecl l t _) = commas ga l <+> colon <+> printText0 ga t

printText0 ga (PredDefn n ps f _) = (printText0 ga n

<> fcat (map (printText0 ga) ps))

<+> text equivS

<+> printText0 ga f

instance PrettyPrint BinOpAttr where

printText0 _ Assoc = text assocS

printText0 _ Comm = text commS

printText0 _ Idem = text idemS

instance PrettyPrint OpAttr where

printText0 ga (BinOpAttr a _) = printText0 ga a

printText0 ga (UnitOpAttr t _) = text unitS <+> printText0 ga t

instance PrettyPrint DatatypeDecl where

printText0 ga (DatatypeDecl p k as d _) = (printText0 ga p <>

printKind ga k)

<+> text defnS

<+> vcat(punctuate (text " | ")

(map (printText0 ga) as))

<+> case d of { Nothing -> empty

; Just c -> text derivingS

<+> printText0 ga c

}

instance PrettyPrint Alternative where

printText0 ga (Constructor n cs p _) = printText0 ga n

<> fcat (map (printText0 ga) cs)

<> (case p of {Partial -> text quMark;

_ -> empty})

printText0 ga (Subtype l _) = text typeS <+> commas ga l

instance PrettyPrint Components where

printText0 ga (Selector n p t _ _) = printText0 ga n

<> colon <> (case p of { Partial ->text quMark;

_ -> empty }

<+> printText0 ga t)

printText0 ga (NoSelector t) = printText0 ga t

printText0 ga (NestedComponents l _) = parens $ semis ga l

instance PrettyPrint OpId where

printText0 ga (OpId n ts) = printText0 ga n

<+> fcat(map (printText0 ga) ts)