LaTeX_HasCASL.hs revision 2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Christian Maeder and Uni Bremen 2004
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : maeder@tzi.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : experimental
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach latex output of the abstract syntax
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Common.GlobalAnnotations(GlobalAnnos)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.Lib.Map as Map
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- | short cut for: if b then empty else d
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaedernoPrint :: Bool -> Doc -> Doc
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedernoPrint b d = if b then empty else d
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettinstance PrintLaTeX Variance where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett printLatex0 _ v = text $ show v
9f93b2a8b552789cd939d599504d39732672dc84Christian Maederinstance PrintLaTeX Kind where
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett printLatex0 ga knd = case knd of
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder Intersection [] _ -> text "Type"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly MissingKind -> space
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ClassKind ci _ -> printLatex0 ga ci
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Downset mt t _ _ ->
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let tok = case mt of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> text "\\_"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just x -> (printLatex0 ga x) <+> hc_sty_axiom "\\bullet" <+> (printLatex0 ga x)
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett in braces_latex (tok <+>
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder hc_sty_axiom lessS <+> printLatex0 ga t)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder Intersection ks _ -> printList0 ga ks
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder FunKind k1 k2 _ ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder FunKind _ _ _ -> parens
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> id) (printLatex0 ga k1)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> hc_sty_axiom "\\rightarrow"
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett <+> printLatex0 ga k2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ExtKind k v _ -> (case k of
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder FunKind _ _ _ -> parens
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder _ -> id) (printLatex0 ga k) <> printLatex0 ga v
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maederinstance PrintLaTeX TypePattern where
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder printLatex0 ga tp = case tp of
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder TypePattern name args _ -> printLatex0 ga name
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder <> fcat (map (parens . printLatex0 ga) args)
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder TypePatternToken t -> printLatex0 ga t
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder MixfixTypePattern ts -> fsep_latex (map (printLatex0 ga) ts)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder BracketTypePattern k l _ -> bracket k $ commaT_latex ga l
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder TypePatternArg t _ -> parens $ printLatex0 ga t
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder-- | put proper brackets around a document
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederbracket :: BracketKind -> Doc -> Doc
bcd914850de931848b86d7728192a149f9c0108bChristian Maederbracket b = case b of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Parens -> parens_latex
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Squares -> brackets_latex
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Braces -> braces_latex
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder-- | print a 'Kind' plus a preceding colon (or nothing for 'star')
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederprintKind :: GlobalAnnos -> Kind -> Doc
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederprintKind ga kind = case kind of
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Intersection [] _ -> empty
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Downset Nothing t _ _ ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett space <> hc_sty_axiom lessS <+> printLatex0 ga t
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett _ -> space <> colon <+> printLatex0 ga kind
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblettinstance PrintLaTeX Type where
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett printLatex0 ga ty = case ty of
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett TypeName name _k _i -> printLatex0 ga name
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett TypeAppl t1 t2 -> case t1 of
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett TypeName (Id [a, Token "__" _, b] [] []) _ _ ->
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder printLatex0 ga a <> printLatex0 ga t2 <> printLatex0 ga b
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder TypeAppl (TypeName (Id [Token "__" _, inTok, Token "__" _]
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder [] []) _ _) t0 -> printLatex0 ga t0
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett <+> printLatex0 ga inTok <+> printLatex0 ga t2
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett _ -> (case t1 of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder TypeName _ _ _ -> id
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder TypeToken _ -> id
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett BracketType _ _ _ -> id
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett TypeAppl _ _ -> id
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder _ -> parens) (printLatex0 ga t1) <+>
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder TypeName _ _ _ -> id
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder TypeToken _ -> id
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder BracketType _ _ _ -> id
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> parens) (printLatex0 ga t2)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ExpandedType t1 _ -> printLatex0 ga t1
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder TypeToken t -> printLatex0 ga t
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder BracketType k l _ -> bracket k $ commaT_latex ga l
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett KindedType t kind _ -> (case t of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett FunType _ _ _ _ -> parens
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ProductType [] _ -> id
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ProductType _ _ -> parens
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder LazyType _ _ -> parens
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder TypeAppl _ _ -> parens
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> id) (printLatex0 ga t)
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder <+> colon <+> printLatex0 ga kind
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder MixfixType ts -> fsep_latex (map (printLatex0 ga) ts)
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly LazyType t _ -> hc_sty_axiom quMark <+> (case t of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly FunType _ _ _ _ -> parens
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly ProductType [] _ -> id
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly ProductType _ _ -> parens
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly KindedType _ _ _ -> parens
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly _ -> id) (printLatex0 ga t)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder ProductType ts _ -> if null ts then hc_sty_plain_keyword "Unit"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- parens empty
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder else fsep_latex (punctuate (space <> char '*')
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (map ( \ t ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett FunType _ _ _ _ -> parens
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ProductType [] _ -> id
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder ProductType _ _ -> parens
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett _ -> id) $ printLatex0 ga t) ts))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly FunType t1 arr t2 _ -> (case t1 of
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett FunType _ _ _ _ -> parens
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett _ -> id) (printLatex0 ga t1)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett <+> printLatex0 ga arr
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <+> printLatex0 ga t2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrintLaTeX Pred where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (IsIn c ts) = if null ts then printLatex0 ga c
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else if null $ tail ts then
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (head ts) <+>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly colon <+> printLatex0 ga c
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else printLatex0 ga c <+>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly fsep_latex (punctuate space
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (map (printLatex0 ga) ts))
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX t => PrintLaTeX (Qual t) where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (ps :=> t) = (if null ps then empty
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else parens $ commaT_latex ga ps <+>
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder hc_sty_axiom implS <+> space) <>
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder printLatex0 ga t
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- no curried notation for bound variables
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance PrintLaTeX TypeScheme where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (TypeScheme vs t _) = let tdoc = printLatex0 ga t in
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder if null vs then tdoc else
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder hang (hc_sty_axiom forallS <+> semiT_latex ga vs <+> hc_sty_axiom "\\bullet") 2 tdoc
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX Instance where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 _ i = case i of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Instance -> space <> hc_sty_axiom instanceS
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Plain -> empty
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maederinstance PrintLaTeX Partiality where
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maeder printLatex0 _ p = case p of
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Partial -> hc_sty_axiom quMark
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly Total -> empty
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrintLaTeX Arrow where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 _ a = case a of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly FunArr -> hc_sty_axiom "\\rightarrow"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly PFunArr -> hc_sty_axiom ("\\rightarrow" ++ quMark)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ContFunArr -> hc_sty_axiom "\\stackrel{c}{\\rightarrow}"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly PContFunArr -> hc_sty_axiom ("\\stackrel{c}{\\rightarrow}" ++ quMark)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrintLaTeX Quantifier where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 _ Universal = hc_sty_axiom "\\forall"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 _ Existential = hc_sty_axiom "\\exists"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 _ Unique = hc_sty_axiom "\\exists!"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX TypeQual where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 _ q = text $ show q
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX Term where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga t = printTerm ga
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly QualVar _ -> True
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly QualOp _ _ _ _ -> True
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> False) t
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyunPredType :: Type -> Type
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyunPredType t = case t of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly FunType ty PFunArr (ProductType [] _) _ -> ty
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyunPredTypeScheme :: TypeScheme -> TypeScheme
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettunPredTypeScheme = mapTypeOfScheme unPredType
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedersubstituteArgs :: GlobalAnnos -> [Token] -> [Doc] -> Doc
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedersubstituteArgs _ [] ds = cat ds
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedersubstituteArgs ga ts [] = cat (map (printLatex0 ga) ts)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedersubstituteArgs ga (t:ts) (d:ds) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then d <+> substituteArgs ga ts ds
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else printLatex0 ga t <+> substituteArgs ga ts (d:ds)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyfindMixfixOp :: Term -> Maybe Id
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyfindMixfixOp (QualOp _ (InstOpId ident _ _) _ _) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly if isMixfix ident then Just ident else Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyfindMixfixOp (ApplTerm t1 _ _) = findMixfixOp t1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyfindMixfixOp _ = Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyprintTerm :: GlobalAnnos -> Bool -> Term -> Doc
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyprintTerm ga b trm =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let ppParen = if b then parens else id
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder commaT = fsep_latex . punctuate comma . map (printTerm ga False)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder TupleTerm _ _ -> id
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder BracketTerm _ _ _ -> id
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly TermToken _ -> id
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder MixTypeTerm _ _ _ -> id
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly _ -> ppParen)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $ case trm of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder QualVar (VarDecl v _ _t _) -> printLatex0 ga v
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {-sep [hc_sty_axiom varS <+> printLatex0 ga v,
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder colon <+> printLatex0 ga t]-}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder QualOp _br n _t _ -> printLatex0 ga n
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {-sep [printLatex0 ga br <+> printLatex0 ga n,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder colon <+> printLatex0 ga
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (if isPred br then unPredTypeScheme t else t)]-}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ResolvedMixTerm n ts _ ->
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly [] -> printLatex0 ga n
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett [t] -> printLatex0 ga n <> printTerm ga True t
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> printLatex0 ga n <>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parens (commaT ts)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ApplTerm t1 t2 _ ->
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly case (findMixfixOp t1,t2) of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (Just (Id toks [] _), TupleTerm ts _) ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder if length (filter isPlace toks) == length ts
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder then substituteArgs ga toks (map (printTerm ga True) ts)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else cat [printLatex0 ga t1, nest 2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $ printTerm ga True t2]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> cat [printLatex0 ga t1, nest 2
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett $ printTerm ga True t2]
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett TupleTerm ts _ -> parens (commaT ts)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly TypedTerm term q typ _ -> hang (printLatex0 ga term
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> printLatex0 ga q)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder 4 $ printLatex0 ga typ
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder QuantifiedTerm q vs t _ -> printLatex0 ga q
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> semiT_latex ga vs
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> hc_sty_axiom "\\bullet"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> printLatex0 ga t
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett LambdaTerm ps q t _ -> hang (hc_sty_axiom lamS
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <+> (case ps of
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett [p] -> printLatex0 ga p
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> fcat $ map
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (parens . printTerm ga False) ps)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> (case q of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Partial -> hc_sty_axiom "\\bullet"
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Total -> hc_sty_axiom $ "\\bullet" ++ exMark))
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder 2 $ printLatex0 ga t
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder CaseTerm t es _ -> hang (hc_sty_axiom caseS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> hc_sty_axiom ofS)
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly 4 $ vcat (punctuate (hc_sty_axiom " | ")
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (map (printEq0 ga "\\rightarrow") es))
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly LetTerm br es t _ ->
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly let dt = printLatex0 ga t
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly des = vcat $ punctuate semi $
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett map (printEq0 ga equalS) es
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder in case br of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Let -> sep [hc_sty_axiom letS <+> des, hc_sty_axiom inS <+> dt]
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Where -> hang (sep [dt, hc_sty_axiom whereS]) 6 des
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TermToken t -> printLatex0 ga t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder MixTypeTerm q t _ -> printLatex0 ga q <+> printLatex0 ga t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder MixfixTerm ts -> fsep_latex $ map (printLatex0 ga) ts
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly BracketTerm k l _ -> bracket k $ commaT l
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett AsPattern v p _ -> printLatex0 ga v
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <+> hc_sty_axiom asP
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <+> printLatex0 ga p
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | print an equation with different symbols between 'Pattern' and 'Term'
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyprintEq0 :: GlobalAnnos -> String -> ProgEq -> Doc
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyprintEq0 ga s (ProgEq p t _) = hang (hang (printLatex0 ga p) 2 $ text s)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly 4 $ printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance PrintLaTeX VarDecl where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly printLatex0 ga (VarDecl v t _ _) = printLatex0 ga v <+> colon
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> printLatex0 ga t
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance PrintLaTeX GenVarDecl where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 ga gvd = case gvd of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GenVarDecl v -> printLatex0 ga v
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GenTypeVarDecl tv -> printLatex0 ga tv
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederinstance PrintLaTeX TypeArg where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder printLatex0 ga (TypeArg v c _ _) = printLatex0 ga v <+> colon
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> printLatex0 ga c
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | don't print an empty list and put parens around longer lists
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettprintList0 :: (PrintLaTeX a) => GlobalAnnos -> [a] -> Doc
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederprintList0 ga l = case l of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [x] -> printLatex0 ga x
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> parens $ commaT_latex ga l
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance PrintLaTeX InstOpId where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 ga (InstOpId n l _) =
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (if n==mkId[mkSimpleId place,mkSimpleId "/\\",mkSimpleId place]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder then hc_sty_axiom "\\wedge"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder else printLatex0 ga n)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <> noPrint (null l)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (brackets $ semiT_latex ga l)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett------------------------------------------------------------------------
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder------------------------------------------------------------------------
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | print a 'TypeScheme' as a pseudo type
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederprintPseudoType :: GlobalAnnos -> TypeScheme -> Doc
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintPseudoType ga (TypeScheme l t _) = noPrint (null l) (hc_sty_axiom lamS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> (if null $ tail l then
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 ga $ head l
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder else fcat(map (parens . printLatex0 ga) l))
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder <+> hc_sty_axiom "\\bullet" <> space) <> printLatex0 ga t
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX BasicSpec where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly printLatex0 ga (BasicSpec l) = vcat (map (printLatex0 ga) l)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance PrintLaTeX ProgEq where
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printLatex0 ga = printEq0 ga equalS
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance PrintLaTeX BasicItem where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga bi = case bi of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly SigItems s -> printLatex0 ga s
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly ProgItems l _ -> hc_sty_plain_keyword programS <+> semiT_latex ga l
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ClassItems i l _ -> hc_sty_plain_keyword classS <> printLatex0 ga i <+> semiT_latex ga l
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett GenVarItems l _ -> hc_sty_plain_keyword varS <+> semiT_latex ga l
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder FreeDatatype l _ -> hc_sty_plain_keyword freeS <+> hc_sty_plain_keyword typeS
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly <+> semiT_latex ga l
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GenItems l _ -> hc_sty_plain_keyword generatedS <+> braces_latex (semiT_latex ga l)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder AxiomItems vs fs _ -> (if null vs then empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else hc_sty_plain_keyword forallS <+> semiT_latex ga vs)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (\x -> hc_sty_axiom "\\bullet" <+> printLatex0 ga x)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Internal l _ -> hc_sty_plain_keyword internalS <+> braces_latex (semiT_latex ga l)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance PrintLaTeX OpBrand where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly printLatex0 _ b = text $ show b
5858e6262048894b0e933b547852f04aed009b58Andy Gimblettinstance PrintLaTeX SigItems where
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett printLatex0 ga si = case si of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder TypeItems i l _ -> hc_sty_plain_keyword typeS <> printLatex0 ga i <+> semiT_latex ga l
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder OpItems b l _ -> printLatex0 ga b <+> semiT_latex ga
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (if isPred b then concat $
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly mapAnM ((:[]) . mapOpItem) l else l)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance PrintLaTeX ClassItem where
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printLatex0 ga (ClassItem d l _) = printLatex0 ga d $$
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly if null l then empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else braces_latex (semiT_latex ga l)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX ClassDecl where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly printLatex0 ga (ClassDecl l k _) = commaT_latex ga l
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> hc_sty_axiom lessS <+> printLatex0 ga k
5a859092c242b0e37183a44c3c79479125b2920aChristian Maederinstance PrintLaTeX Vars where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder printLatex0 ga vd = case vd of
5a859092c242b0e37183a44c3c79479125b2920aChristian Maeder Var v -> printLatex0 ga v
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder VarTuple vs _ -> parens $ commaT_latex ga vs
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance PrintLaTeX TypeItem where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 ga ti = case ti of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder TypeDecl l k _ -> commaT_latex ga l <>
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printKind ga k
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly SubtypeDecl l t _ -> commaT_latex ga l <+> hc_sty_axiom lessS
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder <+> printLatex0 ga t
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder IsoDecl l _ -> cat(punctuate (hc_sty_axiom " = ")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (map (printLatex0 ga) l))
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder SubtypeDefn p v t f _ -> printLatex0 ga p
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> hc_sty_axiom equalS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> braces_latex (printLatex0 ga v
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> printLatex0 ga t
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> hc_sty_axiom "\\bullet"
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett <+> printLatex0 ga f)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder AliasType p k t _ -> (printLatex0 ga p <>
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just j -> space <> colon <+>
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printLatex0 ga j)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder <+> hc_sty_axiom assignS
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder <+> printPseudoType ga t
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Datatype t -> printLatex0 ga t
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapOpItem :: OpItem -> OpItem
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedermapOpItem oi = case oi of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder OpDecl l t as ps -> OpDecl l (unPredTypeScheme t) as ps
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly OpDefn n ps s p t qs -> OpDefn n ps (unPredTypeScheme s) p t qs
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrintLaTeX OpItem where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 ga oi = case oi of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly OpDecl l t as _ -> commaT_latex ga l <+> colon
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly <+> (printLatex0 ga t
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly <> (if null as then empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else comma <> space)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <> commaT_latex ga as)
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly OpDefn n ps s p t _ ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga n <> fcat (map (parens . semiT_latex ga) ps)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> colon <> printLatex0 ga p
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly <+> printLatex0 ga s
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> hc_sty_axiom equalS
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> printLatex0 ga t
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX BinOpAttr where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 _ a = hc_sty_axiom $ case a of
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly Assoc -> assocS
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Comm -> commS
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Idem -> idemS
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederinstance PrintLaTeX OpAttr where
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printLatex0 ga oa = case oa of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder BinOpAttr a _ -> printLatex0 ga a
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder UnitOpAttr t _ -> hc_sty_axiom unitS <+> printLatex0 ga t
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettinstance PrintLaTeX DatatypeDecl where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (DatatypeDecl p k as d _) = (printLatex0 ga p <>
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printKind ga k)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> hc_sty_axiom defnS
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <+> vcat(punctuate (hc_sty_axiom " | ")
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (map (printLatex0 ga) as))
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <+> case d of [] -> empty
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> hc_sty_plain_keyword derivingS
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> commaT_latex ga d
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX Alternative where
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly printLatex0 ga alt = case alt of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Constructor n cs p _ ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga n <+> fsep_latex (map (parens . semiT_latex ga) cs)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <> printLatex0 ga p
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Subtype l _ -> hc_sty_plain_keyword typeS <+> commaT_latex ga l
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstance PrintLaTeX Component where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga sel = case sel of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Selector n p t _ _ -> printLatex0 ga n
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> colon <> printLatex0 ga p
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly <+> printLatex0 ga t
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly NoSelector t -> printLatex0 ga t
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance PrintLaTeX OpId where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly printLatex0 ga (OpId n ts _) = printLatex0 ga n
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly <+> noPrint (null ts)
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder (brackets $ commaT_latex ga ts)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance PrintLaTeX Symb where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly printLatex0 ga (Symb i mt _) =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly printLatex0 ga i <> (case mt of Nothing -> empty
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Just (SymbType t) ->
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly empty <+> colon <+>
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly printLatex0 ga t)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrintLaTeX SymbItems where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (SymbItems k syms _ _) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printSK k <> commaT_latex ga syms
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrintLaTeX SymbOrMap where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 ga (SymbOrMap s mt _) =
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder printLatex0 ga s <> (case mt of Nothing -> empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder empty <+> hc_sty_axiom "\\mapsto" <+>
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga t)
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance PrintLaTeX SymbMapItems where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printLatex0 ga (SymbMapItems k syms _ _) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printSK k <> commaT_latex ga syms
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | print symbol kind
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederprintSK :: SymbKind -> Doc
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder case k of Implicit -> empty
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder _ -> ptext (drop 3 $ show k) <> space
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder------------------------------------- Le -----------------------------------
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maederinstance PrintLaTeX ClassInfo where
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder printLatex0 ga (ClassInfo ks) =
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder space <> hc_sty_axiom lessS <+> printList0 ga ks
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian MaederprintGenKind :: GenKind -> Doc
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian MaederprintGenKind k = case k of
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder Loose -> empty
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder Free -> hc_sty_plain_keyword freeS <> space
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder Generated -> hc_sty_plain_keyword generatedS <> space
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maederinstance PrintLaTeX TypeDefn where
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder printLatex0 _ NoTypeDefn = empty
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder printLatex0 _ PreDatatype = space <> text "\\%(data type)\\%"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder printLatex0 _ (TypeVarDefn i) =
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder space <> text ("\\%(var_{" ++ show i ++ "})\\%")
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder printLatex0 ga (AliasTypeDefn s) = space <> hc_sty_axiom assignS
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder <+> printPseudoType ga s
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder printLatex0 ga (Supertype v t f) = space <> hc_sty_axiom equalS <+>
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder braces_latex (printLatex0 ga v
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder <+> printLatex0 ga t
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder <+> hc_sty_axiom "\\bullet"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder <+> printLatex0 ga f)
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder printLatex0 ga (DatatypeDefn de) = text " \\%[" <>
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder printLatex0 ga de <> text "]\\%"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederprintAltDefn :: GlobalAnnos -> DataPat -> AltDefn -> Doc
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederprintAltDefn ga dt (Construct mi ts p sels) = case mi of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Just i -> printLatex0 ga i <+> colon
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <+> printLatex0 ga (getConstrType dt p ts)
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett <+> fcat (map (parens . semiT_latex ga) sels)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> hc_sty_plain_keyword (typeS ++ sS) <+> commaT_latex ga ts
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX Selector where
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printLatex0 ga (Select mi t p) = (case mi of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Just i -> printLatex0 ga i <+> (case p of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Partial -> hc_sty_axiom ":?"
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Total -> colon) <> space
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Nothing -> empty) <> printLatex0 ga t
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederinstance PrintLaTeX TypeInfo where
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 ga (TypeInfo _ ks sups defn) =
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly space <> colon <+> printList0 ga ks
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly <> noPrint (null sups)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (space <> hc_sty_axiom lessS <+> printList0 ga sups)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly <> printLatex0 ga defn
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillyinstance PrintLaTeX ConstrInfo where
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 ga (ConstrInfo i t) =
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 ga i <+> colon <+> printLatex0 ga t
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillyinstance PrintLaTeX OpDefn where
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly printLatex0 _ (NoOpDefn b) = space <> text ("\\%(" ++ show b ++ ")\\%")
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 _ VarDefn = space <> text "\\%(var)\\%"
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 _ (ConstructData i) = space <> text ("\\%(construct " ++
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder showId i ")\\%")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (SelectData c i) = space <> text ("\\%(select from " ++
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder showId i " constructed by")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $$ printList0 ga c <> text ")\\%"
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printLatex0 ga (Definition b t) = printLatex0 ga (NoOpDefn b) <+>
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly hc_sty_axiom equalS <+> printLatex0 ga t
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillyinstance PrintLaTeX OpInfo where
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 ga o = space <> colon <+> printLatex0 ga (opType o)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <> (case opAttrs o of
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly l -> comma <> commaT_latex ga l)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly <> printLatex0 ga (opDefn o)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillyinstance PrintLaTeX OpInfos where
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 ga (OpInfos l) = vcat $ map (printLatex0 ga) l
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX DataEntry where
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printLatex0 ga (DataEntry im i k args alts) =
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printGenKind k <> hc_sty_plain_keyword typeS <+> printLatex0 ga i
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly <> hcat (map (parens . printLatex0 ga) args)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly <+> (hc_sty_axiom defnS $$
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly vcat (map (printAltDefn ga (i, args, star))
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $$ nest 2 (noPrint (Map.isEmpty im)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (hc_sty_plain_keyword withS <+> hc_sty_plain_keyword (typeS ++ sS)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> printMap0 ga (hc_sty_axiom mapsTo) im))
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederinstance PrintLaTeX Sentence where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga s = case s of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Formula t -> printLatex0 ga t
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder DatatypeSen ls -> vcat (map (printLatex0 ga) ls)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly ProgEqSen _ _ pe -> hc_sty_plain_keyword programS
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly <+> printLatex0 ga pe
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reillyinstance PrintLaTeX Env where
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly printLatex0 ga (Env{classMap=cm, typeMap=tm,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder assumps=as, sentences=se, envDiags=_ds}) =
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly noPrint (Map.isEmpty cm) (header "Classes")
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly $$ printMap0 ga empty cm
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $$ noPrint (Map.isEmpty tm) (header "Type Constructors")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $$ printMap0 ga empty tm
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $$ noPrint (Map.isEmpty as) (header "Assumptions")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $$ printMap0 ga empty as
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly $$ noPrint (null se) (header "Sentences")
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly $$ vcat (map (printLatex0 ga) se)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- $$ noPrint (null ds) (header "Diagnostics")
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- $$ vcat (map (printLatex0 ga) $ reverse ds)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder where header s = text "\\%\\%" <+> text s
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly <+> text (replicate (70 - length s) '-')
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyprintMap0 :: (PrintLaTeX a, Ord a, PrintLaTeX b)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly => GlobalAnnos -> Doc -> Map.Map a b -> Doc
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederprintMap0 g d m =let l = Map.toList m in
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder vcat(map (\ (a, b) -> printLatex0 g a <> d <> printLatex0 g b) l)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance PrintLaTeX SymbolType where
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder printLatex0 ga t = case t of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder OpAsItemType sc -> printLatex0 ga sc
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder TypeAsItemType k -> printLatex0 ga k
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder ClassAsItemType k -> printLatex0 ga k
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblettinstance PrintLaTeX Symbol where
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder printLatex0 ga s = hc_sty_plain_keyword (case symType s of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder OpAsItemType _ -> opS
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett TypeAsItemType _ -> typeS
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ClassAsItemType _ -> classS) <+>
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder printLatex0 ga (symName s) <+> hc_sty_axiom colonS <+>
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder printLatex0 ga (symType s)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederinstance PrintLaTeX RawSymbol where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga rs = case rs of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder AnID i -> printLatex0 ga i
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder AKindedId k i -> printSK k <> printLatex0 ga i
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder AQualId i t -> printSK (symbTypeToKind t) <> printLatex0 ga i <+> colon
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> printLatex0 ga t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder------------------------------- Morphism ------------------------------------
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance PrintLaTeX Morphism where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder printLatex0 ga m = braces_latex (printLatex0 ga (msource m))
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $$ hc_sty_axiom "\\mapsto"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <+> braces_latex (printLatex0 ga (mtarget m))