LaTeX_HasCASL.hs revision 715ffaf874309df081d1e1cd8e05073fc1227729
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Christian Maeder and Uni Bremen 2004
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : maeder@tzi.de
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettStability : experimental
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach latex output of the abstract syntax
ae930b77ed60580110b52a09456d651f9b841883Andy Gimblettimport Common.GlobalAnnotations(GlobalAnnos)
ae930b77ed60580110b52a09456d651f9b841883Andy Gimblettimport qualified Common.Lib.Map as Map
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- | short cut for: if b then empty else d
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachnoPrint :: Bool -> Doc -> Doc
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaedernoPrint b d = if b then empty else d
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettinstance PrintLaTeX Variance where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach printLatex0 _ v = text $ show v
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblettinstance PrintLaTeX Kind where
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett printLatex0 ga knd = case knd of
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Universe _ -> text "Type"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett MissingKind -> space
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett ClassKind ci _ -> printLatex0 ga ci
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett Downset mt t _ _ ->
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett let tok = case mt of
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Nothing -> text "\\_"
a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly Just x -> (printLatex0 ga x) <+> hc_sty_axiom "\\bullet" <+> (printLatex0 ga x)
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder in braces_latex (tok <+>
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder hc_sty_axiom lessS <+> printLatex0 ga t)
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder Intersection ks _ -> printList0 ga ks
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder FunKind k1 k2 _ ->
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder ExtKind (FunKind _ _ _) InVar _ -> parens
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder FunKind _ _ _ -> parens
a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly _ -> id) (printLatex0 ga k1)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett <+> hc_sty_axiom "\\rightarrow"
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett <+> printLatex0 ga k2
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett ExtKind k v _ -> (case v of
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett _ -> case k of
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett FunKind _ _ _ -> parens
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett _ -> id) (printLatex0 ga k) <> printLatex0 ga v
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance PrintLaTeX TypePattern where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 ga tp = case tp of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett TypePattern name args _ -> printLatex0 ga name
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett <> fcat (map (parens . printLatex0 ga) args)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett TypePatternToken t -> printLatex0 ga t
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett MixfixTypePattern ts -> fsep_latex (map (printLatex0 ga) ts)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett BracketTypePattern k l _ -> bracket k $ commaT_latex ga l
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett TypePatternArg t _ -> parens $ printLatex0 ga t
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett-- | put proper brackets around a document
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettbracket :: BracketKind -> Doc -> Doc
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettbracket b t = let (o,c) = getBrackets b in ptext o <> t <> ptext c
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett-- | print a 'Kind' plus a preceding colon (or nothing for 'star')
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettprintKind :: GlobalAnnos -> Kind -> Doc
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettprintKind ga kind = case kind of
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Universe _ -> empty
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Downset Nothing t _ _ ->
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett space <> hc_sty_axiom lessS <+> printLatex0 ga t
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett _ -> space <> colon <+> printLatex0 ga kind
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettinstance PrintLaTeX Type where
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett printLatex0 ga ty = case ty of
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett TypeName name _k _i -> printLatex0 ga name
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett TypeAppl t1 t2 -> case t1 of
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett TypeName (Id [a, Token "__" _, b] [] []) _ _ ->
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett printLatex0 ga a <> printLatex0 ga t2 <> printLatex0 ga b
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett TypeAppl (TypeName (Id [Token "__" _, inTok, Token "__" _]
820947bd01ca952c3909eaa0366c6914c87cc1cbTill Mossakowski [] []) _ _) t0 -> printLatex0 ga t0
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett <+> printLatex0 ga inTok <+> printLatex0 ga t2
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett _ -> (case t1 of
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett TypeName _ _ _ -> id
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett TypeToken _ -> id
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett BracketType _ _ _ -> id
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett TypeAppl _ _ -> id
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett _ -> parens) (printLatex0 ga t1) <+>
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett TypeName _ _ _ -> id
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett TypeToken _ -> id
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett BracketType _ _ _ -> id
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett _ -> parens) (printLatex0 ga t2)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett TypeToken t -> printLatex0 ga t
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett BracketType k l _ -> bracket k $ commaT_latex ga l
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett KindedType t kind _ -> (case t of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett FunType _ _ _ _ -> parens
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ProductType [] _ -> id
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ProductType _ _ -> parens
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett LazyType _ _ -> parens
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett TypeAppl _ _ -> parens
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett _ -> id) (printLatex0 ga t)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett <+> colon <+> printLatex0 ga kind
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett MixfixType ts -> fsep_latex (map (printLatex0 ga) ts)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett LazyType t _ -> hc_sty_axiom quMark <+> (case t of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett FunType _ _ _ _ -> parens
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ProductType [] _ -> id
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ProductType _ _ -> parens
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett KindedType _ _ _ -> parens
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett _ -> id) (printLatex0 ga t)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ProductType ts _ -> if null ts then hc_sty_plain_keyword "Unit"
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- parens empty
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett else fsep_latex (punctuate (space <> char '*')
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (map ( \ t ->
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett FunType _ _ _ _ -> parens
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ProductType [] _ -> id
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ProductType _ _ -> parens
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett _ -> id) $ printLatex0 ga t) ts))
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett FunType t1 arr t2 _ -> (case t1 of
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett FunType _ _ _ _ -> parens
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett _ -> id) (printLatex0 ga t1)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett <+> printLatex0 ga arr
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett <+> printLatex0 ga t2
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettinstance PrintLaTeX Pred where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett printLatex0 ga (IsIn c ts) = if null ts then printLatex0 ga c
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett else if null $ tail ts then
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett printLatex0 ga (head ts) <+>
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett colon <+> printLatex0 ga c
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett else printLatex0 ga c <+>
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett fsep_latex (punctuate space
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett (map (printLatex0 ga) ts))
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance PrintLaTeX t => PrintLaTeX (Qual t) where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett printLatex0 ga (ps :=> t) = (if null ps then empty
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett else parens $ commaT_latex ga ps <+>
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett hc_sty_axiom implS <+> space) <>
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett printLatex0 ga t
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett-- no curried notation for bound variables
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance PrintLaTeX TypeScheme where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 ga (TypeScheme vs t _) = let tdoc = printLatex0 ga t in
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett if null vs then tdoc else
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett hang (hc_sty_axiom forallS <+> semiT_latex ga vs <+> hc_sty_axiom "\\bullet") 2 tdoc
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance PrintLaTeX Instance where
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett printLatex0 _ i = case i of
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett Instance -> space <> hc_sty_axiom instanceS
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Plain -> empty
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance PrintLaTeX Partiality where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett printLatex0 _ p = case p of
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Partial -> hc_sty_axiom quMark
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Total -> empty
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettinstance PrintLaTeX Arrow where
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett printLatex0 _ a = case a of
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett FunArr -> hc_sty_axiom "\\rightarrow"
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett PFunArr -> hc_sty_axiom ("\\rightarrow" ++ quMark)
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett ContFunArr -> hc_sty_axiom "\\stackrel{c}{\\rightarrow}"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett PContFunArr -> hc_sty_axiom ("\\stackrel{c}{\\rightarrow}" ++ quMark)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblettinstance PrintLaTeX Quantifier where
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett printLatex0 _ Universal = hc_sty_axiom "\\forall"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 _ Existential = hc_sty_axiom "\\exists"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 _ Unique = hc_sty_axiom "\\exists!"
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance PrintLaTeX TypeQual where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett printLatex0 _ q = text $ show q
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance PrintLaTeX Term where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett printLatex0 ga t = printTerm ga
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett QualVar _ _ _ -> True
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett QualOp _ _ _ _ -> True
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett _ -> False) t
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettunPredType :: Type -> Type
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettunPredType t = case t of
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett FunType ty PFunArr (ProductType [] _) _ -> ty
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettunPredTypeScheme :: TypeScheme -> TypeScheme
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettunPredTypeScheme = mapTypeOfScheme unPredType
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettsubstituteArgs :: GlobalAnnos -> [Token] -> [Doc] -> Doc
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettsubstituteArgs _ [] ds = cat ds
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettsubstituteArgs ga ts [] = cat (map (printLatex0 ga) ts)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettsubstituteArgs ga (t:ts) (d:ds) =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett then d <+> substituteArgs ga ts ds
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett else printLatex0 ga t <+> substituteArgs ga ts (d:ds)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettfindMixfixOp :: Term -> Maybe Id
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettfindMixfixOp (QualOp _ (InstOpId ident _ _) _ _) =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett if isMixfix ident then Just ident else Nothing
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettfindMixfixOp (ApplTerm t1 _ _) = findMixfixOp t1
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettfindMixfixOp _ = Nothing
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettprintTerm :: GlobalAnnos -> Bool -> Term -> Doc
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettprintTerm ga b trm =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let ppParen = if b then parens else id
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett commaT = fsep_latex . punctuate comma . map (printTerm ga False)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TupleTerm _ _ -> id
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett BracketTerm _ _ _ -> id
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TermToken _ -> id
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett MixTypeTerm _ _ _ -> id
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett _ -> ppParen)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett $ case trm of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett QualVar v _t _ -> printLatex0 ga v
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett {-sep [hc_sty_axiom varS <+> printLatex0 ga v,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett colon <+> printLatex0 ga t]-}
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett QualOp _br n _t _ -> printLatex0 ga n
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett {-sep [printLatex0 ga br <+> printLatex0 ga n,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett colon <+> printLatex0 ga
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (if isPred br then unPredTypeScheme t else t)]-}
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ResolvedMixTerm n ts _ ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett [] -> printLatex0 ga n
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett [t] -> printLatex0 ga n <> printTerm ga True t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett _ -> printLatex0 ga n <>
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett parens (commaT ts)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ApplTerm t1 t2 _ ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case (findMixfixOp t1,t2) of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (Just (Id toks [] _), TupleTerm ts _) ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett if length (filter isPlace toks) == length ts
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett then substituteArgs ga toks (map (printTerm ga True) ts)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett else cat [printLatex0 ga t1, nest 2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett $ printTerm ga True t2]
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett _ -> cat [printLatex0 ga t1, nest 2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett $ printTerm ga True t2]
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TupleTerm ts _ -> parens (commaT ts)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TypedTerm term q typ _ -> hang (printLatex0 ga term
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> printLatex0 ga q)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett 4 $ printLatex0 ga typ
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett QuantifiedTerm q vs t _ -> printLatex0 ga q
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> semiT_latex ga vs
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> hc_sty_axiom "\\bullet"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett LambdaTerm ps q t _ -> hang (hc_sty_axiom lamS
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> (case ps of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett [p] -> printLatex0 ga p
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett _ -> fcat $ map
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (parens . printTerm ga False) ps)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> (case q of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Partial -> hc_sty_axiom "\\bullet"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Total -> hc_sty_axiom $ "\\bullet" ++ exMark))
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett 2 $ printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett CaseTerm t es _ -> hang (hc_sty_axiom caseS
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> hc_sty_axiom ofS)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett 4 $ vcat (punctuate (hc_sty_axiom " | ")
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (map (printEq0 ga "\\rightarrow") es))
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett LetTerm br es t _ ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let dt = printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett des = vcat $ punctuate semi $
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett map (printEq0 ga equalS) es
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett in case br of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Let -> sep [hc_sty_axiom letS <+> des, hc_sty_axiom inS <+> dt]
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Where -> hang (sep [dt, hc_sty_axiom whereS]) 6 des
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TermToken t -> printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett MixTypeTerm q t _ -> printLatex0 ga q <+> printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett MixfixTerm ts -> fsep_latex $ map (printLatex0 ga) ts
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett BracketTerm k l _ -> bracket k $ commaT l
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett AsPattern v p _ -> printLatex0 ga v
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> hc_sty_axiom asP
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> printLatex0 ga p
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | print an equation with different symbols between 'Pattern' and 'Term'
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettprintEq0 :: GlobalAnnos -> String -> ProgEq -> Doc
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettprintEq0 ga s (ProgEq p t _) = hang (hang (printLatex0 ga p) 2 $ text s)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett 4 $ printLatex0 ga t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance PrintLaTeX VarDecl where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 ga (VarDecl v t _ _) = printLatex0 ga v <+> colon
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> printLatex0 ga t
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX GenVarDecl where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga gvd = case gvd of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett GenVarDecl v -> printLatex0 ga v
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett GenTypeVarDecl tv -> printLatex0 ga tv
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblettinstance PrintLaTeX TypeArg where
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett printLatex0 ga (TypeArg v c _ _) = printLatex0 ga v <+> colon
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett <+> printLatex0 ga c
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett-- | don't print an empty list and put parens around longer lists
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy GimblettprintList0 :: (PrintLaTeX a) => GlobalAnnos -> [a] -> Doc
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy GimblettprintList0 ga l = case l of
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett [x] -> printLatex0 ga x
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett _ -> parens $ commaT_latex ga l
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettinstance PrintLaTeX InstOpId where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga (InstOpId n l _) =
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (if n==mkId[mkSimpleId place,mkSimpleId "/\\",mkSimpleId place]
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett then hc_sty_axiom "\\wedge"
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett else printLatex0 ga n)
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett <> noPrint (null l)
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett (brackets $ semiT_latex ga l)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett------------------------------------------------------------------------
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett------------------------------------------------------------------------
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett-- | print a 'TypeScheme' as a pseudo type
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettprintPseudoType :: GlobalAnnos -> TypeScheme -> Doc
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettprintPseudoType ga (TypeScheme l t _) = noPrint (null l) (hc_sty_axiom lamS
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> (if null $ tail l then
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga $ head l
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett else fcat(map (parens . printLatex0 ga) l))
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> hc_sty_axiom "\\bullet" <> space) <> printLatex0 ga t
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettinstance PrintLaTeX BasicSpec where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 ga (BasicSpec l) = vcat (map (printLatex0 ga) l)
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblettinstance PrintLaTeX ProgEq where
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett printLatex0 ga = printEq0 ga equalS
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblettinstance PrintLaTeX BasicItem where
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett printLatex0 ga bi = case bi of
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett SigItems s -> printLatex0 ga s
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ProgItems l _ -> hc_sty_plain_keyword programS <+> semiT_latex ga l
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ClassItems i l _ -> hc_sty_plain_keyword classS <> printLatex0 ga i <+> semiT_latex ga l
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett GenVarItems l _ -> hc_sty_plain_keyword varS <+> semiT_latex ga l
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett FreeDatatype l _ -> hc_sty_plain_keyword freeS <+> hc_sty_plain_keyword typeS
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett <+> semiT_latex ga l
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett GenItems l _ -> hc_sty_plain_keyword generatedS <+> braces_latex (semiT_latex ga l)
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett AxiomItems vs fs _ -> (if null vs then empty
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett else hc_sty_plain_keyword forallS <+> semiT_latex ga vs)
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett (\x -> hc_sty_axiom "\\bullet" <+> printLatex0 ga x)
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett Internal l _ -> hc_sty_plain_keyword internalS <+> braces_latex (semiT_latex ga l)
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblettinstance PrintLaTeX OpBrand where
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett printLatex0 _ b = text $ show b
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstance PrintLaTeX SigItems where
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett printLatex0 ga si = case si of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett TypeItems i l _ -> hc_sty_plain_keyword typeS <> printLatex0 ga i <+> semiT_latex ga l
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett OpItems b l _ -> printLatex0 ga b <+> semiT_latex ga
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett (if isPred b then concat $
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett mapAnM ((:[]) . mapOpItem) l else l)
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblettinstance PrintLaTeX ClassItem where
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett printLatex0 ga (ClassItem d l _) = printLatex0 ga d $$
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett if null l then empty
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett else braces_latex (semiT_latex ga l)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettinstance PrintLaTeX ClassDecl where
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett printLatex0 ga (ClassDecl l k _) = commaT_latex ga l
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> hc_sty_axiom lessS <+> printLatex0 ga k
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettinstance PrintLaTeX Vars where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga vd = case vd of
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett Var v -> printLatex0 ga v
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett VarTuple vs _ -> parens $ commaT_latex ga vs
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblettinstance PrintLaTeX TypeItem where
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett printLatex0 ga ti = case ti of
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett TypeDecl l k _ -> commaT_latex ga l <>
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett printKind ga k
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett SubtypeDecl l t _ -> commaT_latex ga l <+> hc_sty_axiom lessS
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett <+> printLatex0 ga t
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett IsoDecl l _ -> cat(punctuate (hc_sty_axiom " = ")
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett (map (printLatex0 ga) l))
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett SubtypeDefn p v t f _ -> printLatex0 ga p
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> hc_sty_axiom equalS
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> braces_latex (printLatex0 ga v
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> printLatex0 ga t
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> hc_sty_axiom "\\bullet"
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> printLatex0 ga f)
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett AliasType p k t _ -> (printLatex0 ga p <>
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Nothing -> empty
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Just j -> space <> colon <+>
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga j)
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> hc_sty_axiom assignS
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> printPseudoType ga t
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Datatype t -> printLatex0 ga t
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettmapOpItem :: OpItem -> OpItem
a731366827a80af216ce6bfd4aa6388260577791Andy GimblettmapOpItem oi = case oi of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett OpDecl l t as ps -> OpDecl l (unPredTypeScheme t) as ps
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett OpDefn n ps s p t qs -> OpDefn n ps (unPredTypeScheme s) p t qs
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblettinstance PrintLaTeX OpItem where
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett printLatex0 ga oi = case oi of
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett OpDecl l t as _ -> commaT_latex ga l <+> colon
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett <+> (printLatex0 ga t
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett <> (if null as then empty
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett else comma <> space)
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett <> commaT_latex ga as)
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett OpDefn n ps s p t _ ->
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett printLatex0 ga n <> fcat (map (parens . semiT_latex ga) ps)
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett <+> colon <> printLatex0 ga p
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett <+> printLatex0 ga s
adce8375991a372444ab995895442dca6faf9677Andy Gimblett <+> hc_sty_axiom equalS
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett <+> printLatex0 ga t
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblettinstance PrintLaTeX BinOpAttr where
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett printLatex0 _ a = hc_sty_axiom $ case a of
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett Assoc -> assocS
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett Comm -> commS
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett Idem -> idemS
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettinstance PrintLaTeX OpAttr where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 ga oa = case oa of
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett BinOpAttr a _ -> printLatex0 ga a
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett UnitOpAttr t _ -> hc_sty_axiom unitS <+> printLatex0 ga t
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblettinstance PrintLaTeX DatatypeDecl where
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga (DatatypeDecl p k as d _) = (printLatex0 ga p <>
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printKind ga k)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <+> hc_sty_axiom defnS
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett <+> vcat(punctuate (hc_sty_axiom " | ")
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (map (printLatex0 ga) as))
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <+> case d of [] -> empty
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett _ -> hc_sty_plain_keyword derivingS
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett <+> commaT_latex ga d
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblettinstance PrintLaTeX Alternative where
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga alt = case alt of
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett Constructor n cs p _ ->
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga n <+> fsep_latex (map (parens . semiT_latex ga) cs)
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett <> printLatex0 ga p
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett Subtype l _ -> hc_sty_plain_keyword typeS <+> commaT_latex ga l
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblettinstance PrintLaTeX Component where
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga sel = case sel of
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett Selector n p t _ _ -> printLatex0 ga n
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <+> colon <> printLatex0 ga p
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <+> printLatex0 ga t
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett NoSelector t -> printLatex0 ga t
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstance PrintLaTeX OpId where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 ga (OpId n ts _) = printLatex0 ga n
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett <+> noPrint (null ts)
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (brackets $ commaT_latex ga ts)
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblettinstance PrintLaTeX Symb where
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga (Symb i mt _) =
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga i <> (case mt of Nothing -> empty
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett Just (SymbType t) ->
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett empty <+> colon <+>
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 ga t)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstance PrintLaTeX SymbItems where
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett printLatex0 ga (SymbItems k syms _ _) =
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printSK k <> commaT_latex ga syms
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblettinstance PrintLaTeX SymbOrMap where
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga (SymbOrMap s mt _) =
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga s <> (case mt of Nothing -> empty
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett empty <+> hc_sty_axiom "\\mapsto" <+>
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett printLatex0 ga t)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstance PrintLaTeX SymbMapItems where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett printLatex0 ga (SymbMapItems k syms _ _) =
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett printSK k <> commaT_latex ga syms
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett-- | print symbol kind
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettprintSK :: SymbKind -> Doc
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett case k of Implicit -> empty
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett _ -> ptext (drop 3 $ show k) <> space
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett------------------------------------- Le -----------------------------------
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettinstance PrintLaTeX ClassInfo where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (ClassInfo ks) =
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett space <> hc_sty_axiom lessS <+> printList0 ga ks
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettprintGenKind :: GenKind -> Doc
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettprintGenKind k = case k of
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Loose -> empty
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Free -> hc_sty_plain_keyword freeS <> space
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Generated -> hc_sty_plain_keyword generatedS <> space
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance PrintLaTeX TypeDefn where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 _ NoTypeDefn = empty
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 _ PreDatatype = space <> text "\\%(data type)\\%"
c909c215242232fe78ce335e677e6f22264a0ee9Christian Maeder printLatex0 _ TypeVarDefn = space <> text "\\%(var)\\%"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett printLatex0 ga (AliasTypeDefn s) = space <> hc_sty_axiom assignS
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> printPseudoType ga s
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (Supertype v t f) = space <> hc_sty_axiom equalS <+>
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett braces_latex (printLatex0 ga v
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> printLatex0 ga t
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> hc_sty_axiom "\\bullet"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> printLatex0 ga f)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (DatatypeDefn de) = text " \\%[" <>
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga de <> text "]\\%"
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettprintAltDefn :: GlobalAnnos -> Type -> AltDefn -> Doc
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettprintAltDefn ga dt (Construct mi ts p sels) = case mi of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Just i -> printLatex0 ga i <+> colon
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> printLatex0 ga (getConstrType dt p ts)
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <+> fcat (map (parens . semiT_latex ga) sels)
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Nothing -> hc_sty_plain_keyword (typeS ++ sS) <+> commaT_latex ga ts
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettinstance PrintLaTeX Selector where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga (Select mi t p) = (case mi of
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Just i -> printLatex0 ga i <+> (case p of
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Partial -> hc_sty_axiom ":?"
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Total -> colon) <> space
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Nothing -> empty) <> printLatex0 ga t
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettinstance PrintLaTeX TypeInfo where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett printLatex0 ga (TypeInfo _ ks sups defn) =
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett space <> colon <+> printList0 ga ks
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <> noPrint (null sups)
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (space <> hc_sty_axiom lessS <+> printList0 ga sups)
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett <> printLatex0 ga defn
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX ConstrInfo where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (ConstrInfo i t) =
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga i <+> colon <+> printLatex0 ga t
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX OpDefn where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 _ (NoOpDefn b) = space <> text ("\\%(" ++ show b ++ ")\\%")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 _ VarDefn = space <> text "\\%(var)\\%"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 _ (ConstructData i) = space <> text ("\\%(construct " ++
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett showId i ")\\%")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (SelectData c i) = space <> text ("\\%(select from " ++
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett showId i " constructed by")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ printList0 ga c <> text ")\\%"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (Definition b t) = printLatex0 ga (NoOpDefn b) <+>
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett hc_sty_axiom equalS <+> printLatex0 ga t
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX OpInfo where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga o = space <> colon <+> printLatex0 ga (opType o)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <> (case opAttrs o of
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett l -> comma <> commaT_latex ga l)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <> printLatex0 ga (opDefn o)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX OpInfos where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (OpInfos l) = vcat $ map (printLatex0 ga) l
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX DataEntry where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (DataEntry im i k args alts) =
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printGenKind k <> hc_sty_plain_keyword typeS <+> printLatex0 ga i
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <> hcat (map (parens . printLatex0 ga) args)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> (hc_sty_axiom defnS $$
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett vcat (map (printAltDefn ga $ typeIdToType i args star) alts))
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ nest 2 (noPrint (Map.isEmpty im)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (hc_sty_plain_keyword withS <+> hc_sty_plain_keyword (typeS ++ sS)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> printMap0 ga (hc_sty_axiom mapsTo) im))
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX Sentence where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga s = case s of
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Formula t -> printLatex0 ga t
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett DatatypeSen ls -> vcat (map (printLatex0 ga) ls)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ProgEqSen _ _ pe -> hc_sty_plain_keyword programS
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <+> printLatex0 ga pe
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrintLaTeX Env where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printLatex0 ga (Env{classMap=cm, typeMap=tm,
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett assumps=as, sentences=se, envDiags=_ds}) =
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett noPrint (Map.isEmpty cm) (header "Classes")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ printMap0 ga empty cm
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ noPrint (Map.isEmpty tm) (header "Type Constructors")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ printMap0 ga empty tm
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ noPrint (Map.isEmpty as) (header "Assumptions")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ printMap0 ga empty as
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ noPrint (null se) (header "Sentences")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $$ vcat (map (printLatex0 ga) se)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett-- $$ noPrint (null ds) (header "Diagnostics")
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett-- $$ vcat (map (printLatex0 ga) $ reverse ds)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett where header s = text "\\%\\%" <+> text s
=> GlobalAnnos -> Doc -> Map.Map a b -> Doc
printMap0 g d m =let l = Map.toList m in