LaTeX_HasCASL.hs revision 699511266869036921be9c7ae6ac83d1b66ba51d
c343be283b7152554bac0c02493a4e1759c163f7Kay SieversModule : $Header$
b3ae710c251d0ce5cf2cef63208e325497b5e323Zbigniew Jędrzejewski-SzmekCopyright : (c) Christian Maeder and Uni Bremen 2004
b3ae710c251d0ce5cf2cef63208e325497b5e323Zbigniew Jędrzejewski-SzmekLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
f957632b960a0a42999b38ded7089fa602b41745Kay SieversMaintainer : maeder@tzi.de
f957632b960a0a42999b38ded7089fa602b41745Kay SieversStability : experimental
f957632b960a0a42999b38ded7089fa602b41745Kay SieversPortability : portable
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sieverslatex output of the abstract syntax
d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmekmodule HasCASL.LaTeX_HasCASL where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringimport Common.GlobalAnnotations(GlobalAnnos)
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poetteringimport qualified Common.Lib.Map as Map
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poetteringimport qualified Common.Lib.Set as Set
83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmekinstance PrintLaTeX Variance where
83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmek printLatex0 _ = hc_sty_axiom . show
83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmekinstance PrintLaTeX a => PrintLaTeX (AnyKind a) where
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers printLatex0 ga knd = case knd of
fbe1a1a94f19112d7e5d60c40d87487ad24e2ce4Lennart Poettering ClassKind ci -> printLatex0 ga ci
f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering FunKind v k1 k2 _ -> printLatex0 ga v <>
f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering FunKind _ _ _ _ -> parens
f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering _ -> id) (printLatex0 ga k1)
f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering <\+> hc_sty_axiom "\\rightarrow"
f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering <\+> printLatex0 ga k2
d48b7bd271b1e70924c8485d2f95c2f5a1ae77cbLennart Poetteringinstance PrintLaTeX TypePattern where
4e143738bf170be9f957c47605deea8c54b75fdfLennart Poettering printLatex0 ga tp = case tp of
4e143738bf170be9f957c47605deea8c54b75fdfLennart Poettering TypePattern name args _ -> printLatex0 ga name
d48b7bd271b1e70924c8485d2f95c2f5a1ae77cbLennart Poettering <> fcat (map (parens . printLatex0 ga) args)
d48b7bd271b1e70924c8485d2f95c2f5a1ae77cbLennart Poettering TypePatternToken t -> printLatex0 ga t
25e14499c4c5b02229d05a5bc26c3693ade5f987Lennart Poettering MixfixTypePattern ts -> fsep_latex $ map (printLatex0 ga) ts
25e14499c4c5b02229d05a5bc26c3693ade5f987Lennart Poettering BracketTypePattern k l _ -> latexBracket k $ commaT_latex ga l
57f2a947270faf65e1876797b930e3f6d60ebd06Lennart Poettering TypePatternArg t _ -> parens $ printLatex0 ga t
f85857df75cfedbc0d10b8ca2400188dc8f4c22eLennart Poettering-- | put proper brackets around a document
f85857df75cfedbc0d10b8ca2400188dc8f4c22eLennart PoetteringlatexBracket :: BracketKind -> Doc -> Doc
758c4d7a391c0e024737053c815bf3924653b8c5Lennart PoetteringlatexBracket b = case b of
758c4d7a391c0e024737053c815bf3924653b8c5Lennart Poettering Parens -> parens_latex
758c4d7a391c0e024737053c815bf3924653b8c5Lennart Poettering Squares -> brackets_latex
758c4d7a391c0e024737053c815bf3924653b8c5Lennart Poettering Braces -> braces_latex
821cc13ddae40fb7608458b44aaa7a3fd33d56d9Lennart Poettering NoBrackets -> id
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering-- | print a 'Kind' plus a preceding colon (or nothing for 'star')
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringlatexKind :: GlobalAnnos -> Kind -> Doc
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringlatexKind ga k = if k == universe then empty else latexVarKind ga InVar $ VarKind k
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringlatexVarKind :: GlobalAnnos -> Variance -> VarKind -> Doc
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringlatexVarKind ga vv vk = case vk of
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering VarKind k -> space <> colon_latex <\+>
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering printLatex0 ga vv <>
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering printLatex0 ga k
b857e042d621ffb98a652f33850b431fafbece43Lennart Poettering space <> hc_sty_axiom lessS <\+> printLatex0 ga t
8a25e11e6c4b74b7e5299792601e352ee96b8207Lennart PoetteringlatexType :: GlobalAnnos -> Type -> Doc
8a25e11e6c4b74b7e5299792601e352ee96b8207Lennart PoetteringlatexType ga ty = case ty of
384a4be2b00cb95ce215dd343cc9aa77adc9b1ecLennart Poettering TypeName name _k _i -> printLatex0 ga name
384a4be2b00cb95ce215dd343cc9aa77adc9b1ecLennart Poettering TypeAppl t1 t2 -> parens (latexType ga t1) <>
706d97503df83d141d241b645d2c920d691b3d62Lennart Poettering parens (latexType ga t2)
706d97503df83d141d241b645d2c920d691b3d62Lennart Poettering ExpandedType t1 _ -> latexType ga t1
402696d787d252d6317e36c5be340d47578bb27bLennart Poettering TypeToken t -> printLatex0 ga t
402696d787d252d6317e36c5be340d47578bb27bLennart Poettering BracketType k l _ -> latexBracket k $ fsep_latex $
402696d787d252d6317e36c5be340d47578bb27bLennart Poettering punctuate comma_latex $ map (latexType ga) l
402696d787d252d6317e36c5be340d47578bb27bLennart Poettering KindedType t kind _ -> latexType ga t
402696d787d252d6317e36c5be340d47578bb27bLennart Poettering <\+> colon_latex <\+> printLatex0 ga kind
3bcde97e8502c48b53f7420e2433ca68e601662dLennart Poettering MixfixType ts -> fsep_latex $ map (latexType ga) ts
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poetteringinstance PrintLaTeX Type where
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering printLatex0 ga = latexType ga . snd . toMixType
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering-- no curried notation for bound variables
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poetteringinstance PrintLaTeX TypeScheme where
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering printLatex0 ga (TypeScheme vs t _) = let tdoc = printLatex0 ga t in
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering if null vs then tdoc else
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering hang (hc_sty_plain_keyword forallS <\+> semiT_latex ga vs
202aea456dfb279cd34da7bfd1880f6ac0fd849fLennart Poettering <\+> hc_sty_axiom "\\bullet") 2 tdoc
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poetteringinstance PrintLaTeX Instance where
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poettering printLatex0 _ i = case i of
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poettering Instance -> space <> hc_sty_plain_keyword instanceS
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poettering Plain -> empty
8a0dec98a3d18666da739c984f8952865d6e0ce3Lennart Poetteringinstance PrintLaTeX Partiality where
8a0dec98a3d18666da739c984f8952865d6e0ce3Lennart Poettering printLatex0 _ p = case p of
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poettering Partial -> hc_sty_axiom quMark
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poettering Total -> empty
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poetteringinstance PrintLaTeX Arrow where
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poettering printLatex0 _ a = case a of
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poettering FunArr -> hc_sty_axiom "\\rightarrow"
9da465df2a7d5d87e4af61364fb1475b1c8cbc6fLennart Poettering PFunArr -> hc_sty_axiom ("\\rightarrow" ++ quMark)
9da465df2a7d5d87e4af61364fb1475b1c8cbc6fLennart Poettering ContFunArr -> hc_sty_axiom "\\stackrel{c}{\\rightarrow}"
9da465df2a7d5d87e4af61364fb1475b1c8cbc6fLennart Poettering PContFunArr -> hc_sty_axiom ("\\stackrel{c}{\\rightarrow}" ++ quMark)
9da465df2a7d5d87e4af61364fb1475b1c8cbc6fLennart Poetteringinstance PrintLaTeX Quantifier where
563b1bdc09efe0cf94dd3f514f30376ca854c1ceLennart Poettering printLatex0 _ Universal = hc_sty_axiom "\\forall"
563b1bdc09efe0cf94dd3f514f30376ca854c1ceLennart Poettering printLatex0 _ Existential = hc_sty_axiom "\\exists"
ca70bec9261977336c94f44d5fcf37e1c495326aLennart Poettering printLatex0 _ Unique = hc_sty_axiom "\\exists!"
5dcf983854c2e8314dbee239180255490ec8ae1cLennart Poetteringinstance PrintLaTeX TypeQual where
5dcf983854c2e8314dbee239180255490ec8ae1cLennart Poettering printLatex0 _ q = case q of
5dcf983854c2e8314dbee239180255490ec8ae1cLennart Poettering OfType -> colon_latex
b873d33ec9583c92a0c2bc6807d010720fa31595Lennart Poettering Inferred -> colon_latex
d61bb44a89fde3042c7c15ea4975239f7dcb0cb0Lennart Poettering _ -> hc_sty_plain_keyword $ show q
ed220efd6657822332b9563ec53c5ab9f3c33220Lennart Poetteringinstance PrintLaTeX Term where
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering printLatex0 ga t = latexTerm ga
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering QualVar _ -> True
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering QualOp _ _ _ _ -> True
41488fe9024a8955d19811620fd55dcc56a5b2baLennart PoetteringsubstituteArgs :: GlobalAnnos -> [Token] -> [Doc] -> Doc
41488fe9024a8955d19811620fd55dcc56a5b2baLennart PoetteringsubstituteArgs _ [] ds = cat ds
ca70bec9261977336c94f44d5fcf37e1c495326aLennart PoetteringsubstituteArgs ga ts [] = cat (map (printLatex0 ga) ts)
ca70bec9261977336c94f44d5fcf37e1c495326aLennart PoetteringsubstituteArgs ga (t:ts) (d:ds) =
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering then d <\+> substituteArgs ga ts ds
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering else printLatex0 ga t <\+> substituteArgs ga ts (d:ds)
b873d33ec9583c92a0c2bc6807d010720fa31595Lennart PoetteringfindMixfixOp :: Term -> Maybe Id
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart PoetteringfindMixfixOp (QualOp _ (InstOpId ident _ _) _ _) =
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering if isMixfix ident then Just ident else Nothing
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart PoetteringfindMixfixOp (ApplTerm t1 _ _) = findMixfixOp t1
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart PoetteringfindMixfixOp _ = Nothing
ff3d6560bead6879a2fed1bf99bfe8273b3723f1Zbigniew Jędrzejewski-SzmeklatexTerm :: GlobalAnnos -> Bool -> Term -> Doc
151226ab4bf276d60d51864330a99f886b923697Zbigniew Jędrzejewski-SzmeklatexTerm ga b trm =
23c4091dc2b85d117512e89233fdeb47d1ff3d92Lennart Poettering let ppParen = if b then parens else id
23c4091dc2b85d117512e89233fdeb47d1ff3d92Lennart Poettering commaT = fsep_latex . punctuate comma . map (latexTerm ga False)
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poettering TupleTerm _ _ -> id
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart Poettering BracketTerm _ _ _ -> id
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart Poettering TermToken _ -> id
b6b63571ae3eca1741d54172922961af972b8f20Lennart Poettering MixTypeTerm _ _ _ -> id
3f77a1b19f5a8ce33566f7f6e28e94c08ea30841Kay Sievers $ case trm of
3f77a1b19f5a8ce33566f7f6e28e94c08ea30841Kay Sievers QualVar (VarDecl v _ _t _) -> printLatex0 ga v
3f77a1b19f5a8ce33566f7f6e28e94c08ea30841Kay Sievers QualOp _br n _t _ -> printLatex0 ga n
3f77a1b19f5a8ce33566f7f6e28e94c08ea30841Kay Sievers ResolvedMixTerm n ts _ ->
e2a69298819b58f008be61d314f8ab95ccaec427Lennart Poettering [] -> printLatex0 ga n
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering [t] -> printLatex0 ga n <> latexTerm ga True t
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering _ -> printLatex0 ga n <>
fed515f0a845a2ce387cb2d1fcac1ca36b5bac46Lennart Poettering parens (commaT ts)
229811628584b370e3fa7e8524d66be46c5a4661Lennart Poettering ApplTerm t1 t2 _ ->
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering case (findMixfixOp t1,t2) of
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering (Just (Id toks [] _), TupleTerm ts _) ->
a01647e53727107d82382bc5c9d98c894e8f386cLennart Poettering if length (filter isPlace toks) == length ts
3c779fa59d1825d7db2a9516669d34ded7916913Lennart Poettering then substituteArgs ga toks (map (latexTerm ga True) ts)
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering else cat [printLatex0 ga t1, nest 2
a01647e53727107d82382bc5c9d98c894e8f386cLennart Poettering $ latexTerm ga True t2]
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering _ -> cat [printLatex0 ga t1, nest 2
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering $ latexTerm ga True t2]
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering TupleTerm ts _ -> parens (commaT ts)
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering TypedTerm term q typ _ -> hang (printLatex0 ga term
2b1c3767515672dfd0f5e0a9c9d7ac3a16a6a361Lennart Poettering <\+> printLatex0 ga q)
2b1c3767515672dfd0f5e0a9c9d7ac3a16a6a361Lennart Poettering 4 $ printLatex0 ga typ
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart Poettering QuantifiedTerm q vs t _ -> printLatex0 ga q
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart Poettering <\+> semiT_latex ga vs
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering <\+> hc_sty_axiom "\\bullet"
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering <\+> printLatex0 ga t
f55b9bdfae46e3683c74c30f1d063642a41368a5Lennart Poettering LambdaTerm ps q t _ -> hang (hc_sty_axiom lamS
f55b9bdfae46e3683c74c30f1d063642a41368a5Lennart Poettering <\+> (case ps of
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering [p] -> printLatex0 ga p
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering _ -> fcat $ map
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers (parens . latexTerm ga False) ps)
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers <\+> (case q of
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering Partial -> hc_sty_axiom "\\bullet"
f598ac3e28b729dd0b1d0a881df3e16465687a2bLennart Poettering Total -> hc_sty_axiom $ "\\bullet"
01083ad094664e5c685060f4fb35a05ea2f212edLennart Poettering 2 $ printLatex0 ga t
01083ad094664e5c685060f4fb35a05ea2f212edLennart Poettering CaseTerm t es _ -> hang (hc_sty_plain_keyword caseS
b107b705cc97d3033e37c44229deb37b5aa31df5Lennart Poettering <\+> printLatex0 ga t
b107b705cc97d3033e37c44229deb37b5aa31df5Lennart Poettering <\+> hc_sty_plain_keyword ofS)
edb2935c5c5b95c42b8679086f60da5eafad74cbLennart Poettering 4 $ vcat (punctuate (hc_sty_axiom " | ")
edb2935c5c5b95c42b8679086f60da5eafad74cbLennart Poettering (map (latexEq0 ga "\\rightarrow") es))
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering LetTerm br es t _ ->
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering let dt = printLatex0 ga t
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering des = vcat $ punctuate semi $
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering map (latexEq0 ga equalS) es
2a781fc9bd33982c81e5ff75974a442a33d4f167Lennart Poettering Let -> sep [hc_sty_plain_keyword letS <\+> des, hc_sty_plain_keyword inS <\+> dt]
2a781fc9bd33982c81e5ff75974a442a33d4f167Lennart Poettering Where -> hang (sep [dt, hc_sty_plain_keyword whereS]) 6 des
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poettering Program -> des
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poettering TermToken t -> printLatex0 ga t
efc141b8ffbfa1e449da40ce27fccaa81428f779Lennart Poettering MixTypeTerm q t _ -> printLatex0 ga q <\+> printLatex0 ga t
efc141b8ffbfa1e449da40ce27fccaa81428f779Lennart Poettering MixfixTerm ts -> fsep_latex $ map (printLatex0 ga) ts
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt BracketTerm k l _ -> latexBracket k $ commaT l
efc141b8ffbfa1e449da40ce27fccaa81428f779Lennart Poettering AsPattern v p _ -> printLatex0 ga v
efc141b8ffbfa1e449da40ce27fccaa81428f779Lennart Poettering <\+> hc_sty_axiom asP
650264033f2f98f6319513958d94d59078654af8Lennart Poettering <\+> printLatex0 ga p
650264033f2f98f6319513958d94d59078654af8Lennart Poettering-- | print an equation with different symbols between 'Pattern' and 'Term'
f8901862b2b030921b3d5aba4157044ceab16451Lennart PoetteringlatexEq0 :: GlobalAnnos -> String -> ProgEq -> Doc
eda8f06755bd98c4639293c26b856c225f0d1fe1Lennart PoetteringlatexEq0 ga s (ProgEq p t _) = hang (hang (printLatex0 ga p) 2
eda8f06755bd98c4639293c26b856c225f0d1fe1Lennart Poettering $ hc_sty_axiom s) 4 $ printLatex0 ga t
d4fdc205a4610965cee46408dbd046c922e7620cLennart Poetteringinstance PrintLaTeX VarDecl where
d4fdc205a4610965cee46408dbd046c922e7620cLennart Poettering printLatex0 ga (VarDecl v t _ _) = printLatex0 ga v <\+> colon_latex
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart Poettering <\+> printLatex0 ga t
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart Poetteringinstance PrintLaTeX GenVarDecl where
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart Poettering printLatex0 ga gvd = case gvd of
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering GenVarDecl v -> printLatex0 ga v
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering GenTypeVarDecl tv -> printLatex0 ga tv
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poetteringinstance PrintLaTeX TypeArg where
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering printLatex0 ga (TypeArg v vv c _ _ _ _) =
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering printLatex0 ga v <> latexVarKind ga vv c
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart Poettering-- | don't print an empty list and put parens around longer lists
09ecd746c9d6581664873674c2188f8c93ed7780Lennart PoetteringlatexList0 :: (PrintLaTeX a) => GlobalAnnos -> [a] -> Doc
09ecd746c9d6581664873674c2188f8c93ed7780Lennart PoetteringlatexList0 ga l = case l of
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poettering [x] -> printLatex0 ga x
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poettering _ -> parens $ commaT_latex ga l
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poetteringinstance PrintLaTeX InstOpId where
ef417cfd2211ae017a38b9796c6db29130133e63Zbigniew Jędrzejewski-Szmek printLatex0 ga (InstOpId n l _) =
ef417cfd2211ae017a38b9796c6db29130133e63Zbigniew Jędrzejewski-Szmek (if n==mkId[mkSimpleId place,mkSimpleId "/\\",mkSimpleId place]
3333d748facc15f49935b6b793490ba0824976e6Zbigniew Jędrzejewski-Szmek then hc_sty_axiom "\\wedge"
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering else printLatex0 ga n)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering <> noPrint (null l)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering (brackets_latex $ semiT_latex ga l)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering------------------------------------------------------------------------
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering------------------------------------------------------------------------
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering-- | print a 'TypeScheme' as a pseudo type
0bee65f0622c4faa8ac8ae771cc0c8a936dfa284Lennart PoetteringlatexPseudoType :: GlobalAnnos -> TypeScheme -> Doc
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringlatexPseudoType ga (TypeScheme l t _) = noPrint (null l)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering (hc_sty_axiom lamS <\+>
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering (if null $ tail l then printLatex0 ga $ head l
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering else fcat(map (parens . printLatex0 ga) l))
ebcf1f97de4f6b1580ae55eb56b1a3939fe6b602Lennart Poettering <\+> hc_sty_axiom "\\bullet" <> space) <> printLatex0 ga t
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart Poetteringinstance PrintLaTeX BasicSpec where
718db96199eb307751264e4163555662c9a389faLennart Poettering printLatex0 ga (BasicSpec l) = vcat (map (printLatex0 ga) l)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance PrintLaTeX ProgEq where
718db96199eb307751264e4163555662c9a389faLennart Poettering printLatex0 ga = latexEq0 ga equalS
718db96199eb307751264e4163555662c9a389faLennart Poetteringinstance PrintLaTeX BasicItem where
966204e010ed432a1d7a0481d41a326d8ec7b0c8Lennart Poettering printLatex0 ga bi = case bi of
966204e010ed432a1d7a0481d41a326d8ec7b0c8Lennart Poettering SigItems s -> printLatex0 ga s
94676f3e9352cbf1f72e0a512ee0d2ed83ff676dLennart Poettering ProgItems l _ -> hc_sty_plain_keyword programS <\+> semiT_latex ga l
6fd4d0209827e5c3e52fa8c7144852f550f8f95cLennart Poettering ClassItems i l _ -> hc_sty_plain_keyword classS <> printLatex0 ga i
416446221d905b6815175dc4d525d27f8ae43d1bLennart Poettering <\+> semiT_latex ga l
416446221d905b6815175dc4d525d27f8ae43d1bLennart Poettering GenVarItems l _ -> hc_sty_plain_keyword varS <\+> semiT_latex ga l
7f79cd7109a60810140a045cc725291fc5515264Lennart Poettering FreeDatatype l _ -> hc_sty_plain_keyword freeS
0aafd43d235982510d1c40564079f7bcec0c7c19Lennart Poettering <\+> hc_sty_plain_keyword typeS <\+> semiT_latex ga l
19aadacf92ad86967ffb678e37b2ff9e83cb9480Jan Engelhardt GenItems l _ -> hc_sty_plain_keyword generatedS
19aadacf92ad86967ffb678e37b2ff9e83cb9480Jan Engelhardt <\+> braces_latex (semiT_latex ga l)
df5f6971e6e15b4632884916c71daa076c8bae96Lennart Poettering AxiomItems vs fs _ ->
df5f6971e6e15b4632884916c71daa076c8bae96Lennart Poettering (if null vs then empty
fcba531ed4c6e6f8f21d8ca4e3a56e3162b1c578Lennart Poettering else hc_sty_plain_keyword forallS <\+> semiT_latex ga vs)
fcba531ed4c6e6f8f21d8ca4e3a56e3162b1c578Lennart Poettering $$ vcat (map (\x -> hc_sty_axiom "\\bullet" <\+> printLatex0 ga x)
8b8f259170e35b93e6c6d1757cb8b835bbdaa40cZbigniew Jędrzejewski-Szmek Internal l _ -> hc_sty_plain_keyword internalS
e10e429f2dcbb586215e65f62847f40c7d8b5956David Herrmann <\+> braces_latex (semiT_latex ga l)
c3bb87dbab8b79bb9253407cb5b7f3e6fe8db395Lennart Poetteringinstance PrintLaTeX OpBrand where
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt printLatex0 _ b = hc_sty_plain_keyword $ show b
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart Poetteringinstance PrintLaTeX SigItems where
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart Poettering printLatex0 ga si = case si of
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart Poettering TypeItems i l _ -> hc_sty_plain_keyword typeS <> printLatex0 ga i
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart Poettering <\+> semiT_latex ga l
4e09014daf8f98584b3f15e64e93bed232e70a6bLennart Poettering OpItems b l _ -> printLatex0 ga b <\+> semiT_latex ga
4e09014daf8f98584b3f15e64e93bed232e70a6bLennart Poettering (if isPred b then concat $
4e09014daf8f98584b3f15e64e93bed232e70a6bLennart Poettering mapAnM ((:[]) . mapOpItem) l else l)
57f2a947270faf65e1876797b930e3f6d60ebd06Lennart Poetteringinstance PrintLaTeX ClassItem where
57f2a947270faf65e1876797b930e3f6d60ebd06Lennart Poettering printLatex0 ga (ClassItem d l _) = printLatex0 ga d $$
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt if null l then empty
7973ca1927e1f3bac9438f3529458c9ff868905dLennart Poettering else braces_latex (semiT_latex ga l)
7973ca1927e1f3bac9438f3529458c9ff868905dLennart Poetteringinstance PrintLaTeX ClassDecl where
7973ca1927e1f3bac9438f3529458c9ff868905dLennart Poettering printLatex0 ga (ClassDecl l k _) = commaT_latex ga l
dc17bcef197a0d5ee798cce59c40e4f5e85c24f6Lennart Poettering <\+> hc_sty_axiom lessS <\+> printLatex0 ga k
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance PrintLaTeX Vars where
dc17bcef197a0d5ee798cce59c40e4f5e85c24f6Lennart Poettering printLatex0 ga vd = case vd of
80caea6cc72ebd311a311b1527cc6b87201c13bfLennart Poettering Var v -> printLatex0 ga v
ab9716c2489f9141ed13ec22dbb216b3e6fbd6b5Lennart Poettering VarTuple vs _ -> parens $ commaT_latex ga vs
df98a87ba389bdfc0359beedf47557411f3af434Lennart Poetteringinstance PrintLaTeX TypeItem where
df98a87ba389bdfc0359beedf47557411f3af434Lennart Poettering printLatex0 ga ti = case ti of
df98a87ba389bdfc0359beedf47557411f3af434Lennart Poettering TypeDecl l k _ -> commaT_latex ga l <>
2ecfc64e59b5e4e96bed6f68bd36b612ef77a146Lennart Poettering latexKind ga k
6a8b5fa4635ed858788fb10099ec9b62b3359a0aLennart Poettering SubtypeDecl l t _ -> commaT_latex ga l <\+> hc_sty_axiom lessS
69727e6dc69ae5d9b5ae3681723778a3faa354e9Lennart Poettering <\+> printLatex0 ga t
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering IsoDecl l _ -> cat(punctuate (hc_sty_axiom " = ")
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering (map (printLatex0 ga) l))
12179984a38fe74581333fbcdc11c822d81f505fLennart Poettering SubtypeDefn p v t f _ -> printLatex0 ga p
0536ce5d0ceaf87f3e81faaff41d69ffeed2186fZbigniew Jędrzejewski-Szmek <\+> equals_latex
eb01ba5de14859d7a94835ab9299de40132d549aLennart Poettering <\+> braces_latex (printLatex0 ga v
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering <\+> colon_latex
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering <\+> printLatex0 ga t
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering <\+> hc_sty_axiom "\\bullet"
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering <\+> printLatex0 ga f)
69af45035913e7119cffd94c542bd3039600e45dZbigniew Jędrzejewski-Szmek AliasType p k t _ -> (printLatex0 ga p <>
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poettering Nothing -> empty
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poettering Just j -> space <> colon_latex <\+>
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poettering printLatex0 ga j)
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poettering <\+> hc_sty_axiom assignS
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poettering <\+> latexPseudoType ga t
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poettering Datatype t -> printLatex0 ga t
b454b11220e87add6d0f011695c7912b009c853dLennart Poetteringinstance PrintLaTeX OpItem where
b454b11220e87add6d0f011695c7912b009c853dLennart Poettering printLatex0 ga oi = case oi of
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering OpDecl l t as _ -> commaT_latex ga l <\+> colon_latex
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering <\+> (printLatex0 ga t
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-Szmek <> (if null as then empty
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-Szmek else comma <> space)
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-Szmek <> commaT_latex ga as)
b8b4d3dddc7611dce3bf28004b0375d661120c62Lennart Poettering OpDefn n ps s p t _ ->
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering printLatex0 ga n <> fcat (map (parens . semiT_latex ga) ps)
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt <\+> colon_latex <> printLatex0 ga p
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering <\+> printLatex0 ga s
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering <\+> equals_latex
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering <\+> printLatex0 ga t
eece8c6fb5f4d354dcef6fd369e876c4f3a3f163Lennart Poetteringinstance PrintLaTeX BinOpAttr where
eece8c6fb5f4d354dcef6fd369e876c4f3a3f163Lennart Poettering printLatex0 _ a = hc_sty_plain_keyword $ case a of
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering Assoc -> assocS
09f727eebd87661f263d3c2c1e0de7b7771acd40Lennart Poetteringinstance PrintLaTeX OpAttr where
c144692179098c1861f2aeafc67689a74439cf4cLennart Poettering printLatex0 ga oa = case oa of
c144692179098c1861f2aeafc67689a74439cf4cLennart Poettering BinOpAttr a _ -> printLatex0 ga a
c144692179098c1861f2aeafc67689a74439cf4cLennart Poettering UnitOpAttr t _ -> hc_sty_plain_keyword unitS <\+> printLatex0 ga t
795607b22308f5b92073b012e43be1892fdd97c0Lennart Poetteringinstance PrintLaTeX DatatypeDecl where
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering printLatex0 ga (DatatypeDecl p k args d _) =
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering (printLatex0 ga p <> latexKind ga k)
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering <\+> hc_sty_axiom defnS
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering <\+> vcat(punctuate (hc_sty_axiom " | ") (map (printLatex0 ga) args))
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering <\+> case d of
54c31a79f72ff57ac8eba089acacc4ab482b745dLennart Poettering _ -> hc_sty_plain_keyword derivingS <\+> commaT_latex ga d
826872b61e4857dfffe63ba84e2b005623baecd6Lennart Poetteringinstance PrintLaTeX Alternative where
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt printLatex0 ga alt = case alt of
826872b61e4857dfffe63ba84e2b005623baecd6Lennart Poettering Constructor n cs p _ ->
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering printLatex0 ga n <\+> fsep_latex (map (parens . semiT_latex ga) cs)
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering <> printLatex0 ga p
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering Subtype l _ -> hc_sty_plain_keyword typeS <\+> commaT_latex ga l
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poetteringinstance PrintLaTeX Component where
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering printLatex0 ga sel = case sel of
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering Selector n p t _ _ -> printLatex0 ga n
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering <\+> colon_latex <> printLatex0 ga p
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering <\+> printLatex0 ga t
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering NoSelector t -> printLatex0 ga t
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX OpId where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (OpId n ts _) = printLatex0 ga n
466784c8710e5cb0e0b86a16506d992d7ec5b619Kay Sievers <\+> noPrint (null ts)
e41814846c19a48f4490169d82e359e005c4db45Lennart Poettering (brackets_latex $ commaT_latex ga ts)
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poetteringinstance PrintLaTeX Symb where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (Symb i mt _) =
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering printLatex0 ga i <> (case mt of Nothing -> empty
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Just (SymbType t) ->
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering empty <\+> colon_latex <\+>
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poettering printLatex0 ga t)
8ed206517c2be381324ac5832bf34cc14024270eLennart Poetteringinstance PrintLaTeX SymbItems where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (SymbItems k syms _ _) =
e6c6e7afffa80ad74efdb1ddfa815294624f1608Lennart Poettering latexSK k <> commaT_latex ga syms
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX SymbOrMap where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (SymbOrMap s mt _) =
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga s <> (case mt of Nothing -> empty
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering empty <\+> hc_sty_axiom "\\mapsto" <\+>
e5ec62c56963d997edaffa904af5dc45dac23988Lennart Poettering printLatex0 ga t)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance PrintLaTeX SymbMapItems where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (SymbMapItems k syms _ _) =
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering latexSK k <> commaT_latex ga syms
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering-- | print symbol kind
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart PoetteringlatexSK :: SymbKind -> Doc
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering case k of Implicit -> empty
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering _ -> hc_sty_plain_keyword (drop 3 $ show k) <> space
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering------------------------------------- Le -----------------------------------
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX ClassInfo where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (ClassInfo _ ks) =
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt space <> hc_sty_axiom lessS <\+> latexList0 ga ks
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringlatexGenKind :: GenKind -> Doc
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringlatexGenKind k = case k of
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Loose -> empty
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Free -> hc_sty_plain_keyword freeS <> space
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Generated -> hc_sty_plain_keyword generatedS <> space
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX TypeDefn where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 _ NoTypeDefn = empty
f47ec8ebb3858553dec870e1c596e39525f46360Lennart Poettering printLatex0 _ PreDatatype =
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering space <> hc_sty_comment (hc_sty_plain_keyword dataS)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (AliasTypeDefn s) = space <> hc_sty_axiom assignS
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <\+> latexPseudoType ga s
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (DatatypeDefn de) =
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering space <> hc_sty_comment (printLatex0 ga de)
f47ec8ebb3858553dec870e1c596e39525f46360Lennart PoetteringlatexAltDefn :: GlobalAnnos -> Id -> [TypeArg] -> RawKind -> AltDefn -> Doc
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringlatexAltDefn ga dt args rk (Construct mi ts p sels) = case mi of
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Just i -> printLatex0 ga i <\+> colon_latex
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <\+> printLatex0 ga (createConstrType dt args rk p ts)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <\+> fcat (map (parens . semiT_latex ga) sels)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Nothing -> hc_sty_plain_keyword (typeS ++ sS) <\+> commaT_latex ga ts
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance PrintLaTeX Selector where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (Select mi t p) = (case mi of
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering Just i -> printLatex0 ga i <\+> (case p of
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering Partial -> hc_sty_axiom ":?"
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering Total -> colon_latex) <> space
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering Nothing -> empty) <> printLatex0 ga t
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance PrintLaTeX TypeInfo where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (TypeInfo _ ks sups defn) =
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt space <> colon_latex <\+> latexList0 ga ks
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering <> noPrint (Set.null sups)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering (space <> hc_sty_axiom lessS <\+> latexList0 ga (Set.toList sups))
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <> printLatex0 ga defn
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX ConstrInfo where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (ConstrInfo i t) =
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga i <\+> colon_latex <\+> printLatex0 ga t
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poetteringinstance PrintLaTeX OpDefn where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (NoOpDefn b) =
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering space <> hc_sty_comment (printLatex0 ga b)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (ConstructData i) =
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering space <> hc_sty_comment (hc_sty_plain_keyword "construct"
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering <\+> printLatex0 ga i)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (SelectData c i) =
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering space <> hc_sty_comment
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering (hc_sty_plain_keyword "selected from"
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <\+> printLatex0 ga i <\+> hc_sty_plain_keyword "constructed by"
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering $$ latexList0 ga c)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga (Definition b t) = printLatex0 ga (NoOpDefn b) <\+>
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering equals_latex <\+> printLatex0 ga t
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX OpInfo where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga o = space <> colon_latex <\+> printLatex0 ga (opType o)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <> (case opAttrs o of
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt l -> comma <> commaT_latex ga l)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <> printLatex0 ga (opDefn o)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX OpInfos where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (OpInfos l) = vcat $ map (printLatex0 ga) l
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance PrintLaTeX DataEntry where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga (DataEntry im i k args rk alts) =
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering latexGenKind k <> hc_sty_plain_keyword typeS <\+> printLatex0 ga i
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering <> hcat (map (parens . printLatex0 ga) args)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering <\+> (hc_sty_axiom defnS $$
8b04b925e587ff56568c62ff5ad3f2ea2b34ca7aLennart Poettering vcat (map (latexAltDefn ga i args rk) alts))
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering $$ nest 2 (noPrint (Map.null im)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering (hc_sty_plain_keyword withS <\+> hc_sty_plain_keyword (typeS ++ sS)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering <\+> printMap0 ga (hc_sty_axiom mapsTo) im))
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poetteringinstance PrintLaTeX Sentence where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering printLatex0 ga s = case s of
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt Formula t -> printLatex0 ga t
90e071d1d59be05fcba66561439c3ca67c80ee20Lennart Poettering DatatypeSen ls -> vcat (map (printLatex0 ga) ls)
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers ProgEqSen _ _ pe -> hc_sty_plain_keyword programS
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering <\+> printLatex0 ga pe
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poetteringinstance PrintLaTeX Env where
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering printLatex0 ga (Env{classMap=cm, typeMap=tm,
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering assumps=as, sentences=se, envDiags=_ds}) =
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt noPrint (Map.null cm) (header "Classes")
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering $$ printMap0 ga empty cm
603cd8fe07cb03e8b11722d1a732e569e5a46347Lennart Poettering $$ noPrint (Map.null tm) (header "Type Constructors")
a7a3f28be404875eff20443a0fa8088bcc4c18dfLennart Poettering $$ printMap0 ga empty tm
a7a3f28be404875eff20443a0fa8088bcc4c18dfLennart Poettering $$ noPrint (Map.null as) (header "Assumptions")
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering $$ printMap0 ga empty as
08f9588885c5d65694b324846b0ed19211d2c178Lennart Poettering $$ noPrint (null se) (header "Sentences")
9ee58bddeb6eb044753167e0047fe836479ca5dbKay Sievers $$ vcat (map (printLatex0 ga) se)
9ee58bddeb6eb044753167e0047fe836479ca5dbKay Sievers where header s = hc_sty_comment $ hc_sty_plain_keyword s
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart PoetteringprintMap0 :: (PrintLaTeX a, Ord a, PrintLaTeX b)
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poettering => GlobalAnnos -> Doc -> Map.Map a b -> Doc
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan EngelhardtprintMap0 g d m =let l = Map.toList m in
1b89884ba31cbe98f159ce2c7d6fac5f6a57698fLennart Poettering vcat(map (\ (a, b) -> printLatex0 g a <> d <> printLatex0 g b) l)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX a => PrintLaTeX (SymbolType a) where
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-Szmek printLatex0 ga t = case t of
a56b63f41dc779a86573ae77814c14c1db156398Lennart Poettering OpAsItemType sc -> printLatex0 ga sc
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering TypeAsItemType k -> printLatex0 ga k
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering ClassAsItemType k -> printLatex0 ga k
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance PrintLaTeX Symbol where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering printLatex0 ga s = hc_sty_plain_keyword (case symType s of
5f1dac6bf605871615b35891a3966fa474db5b20Lennart Poettering OpAsItemType _ -> opS
f801968466fed39d50d410b30ac828c26722cc95Lennart Poettering TypeAsItemType _ -> typeS
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poettering ClassAsItemType _ -> classS) <\+>
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poettering printLatex0 ga (symName s) <\+> colon_latex <\+>
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poettering printLatex0 ga (symType s)
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poetteringinstance PrintLaTeX RawSymbol where
a1cccad1fe88ddd6943e18af97cf7f466296970fLennart Poettering printLatex0 ga rs = case rs of
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poettering AnID i -> printLatex0 ga i
4a30847b9d71e0381948d68279c8f775b9de7850Lennart Poettering AKindedId k i -> latexSK k <> printLatex0 ga i
4a30847b9d71e0381948d68279c8f775b9de7850Lennart Poettering AQualId i t -> latexSK (symbTypeToKind t) <> printLatex0 ga i
5e8b28838e493b59628322b69580097ef7dd9384Lennart Poettering <\+> colon_latex <\+> printLatex0 ga t
5e8b28838e493b59628322b69580097ef7dd9384Lennart Poettering ASymbol s -> printLatex0 ga s
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering------------------------------- Morphism ------------------------------------
0790b9fed42eefc4e22dbbe2337cba9713b7848cLennart Poetteringinstance PrintLaTeX Morphism where
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering printLatex0 ga m = braces_latex (printLatex0 ga (msource m))
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering $$ hc_sty_axiom "\\mapsto"
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt <\+> braces_latex (printLatex0 ga (mtarget m))