9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett{- |

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettModule : $Header$

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettCopyright : (c) Klaus L�ttich, Christian Maeder and Uni Bremen 2002-2006

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettMaintainer : luettich@tzi.de

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettStability : experimental

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettPortability : portable

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettlatex printing data types of 'BASIC_SPEC'

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett-}

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettmodule CASL.LaTeX_AS_Basic

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett ( hc_sty_sig_item_keyword

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett , optLatexQuMark

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ) where

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblettimport CASL.AS_Basic_CASL

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport CASL.Print_AS_Basic

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.Id

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.AS_Annotation

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.Print_AS_Annotation

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.GlobalAnnotations

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.LaTeX_AS_Annotation

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.Keywords

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.Lib.Pretty

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.PrintLaTeX

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.LaTeX_utils

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport Common.PPUtils

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblettimport Data.Char (toUpper)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettinstance (PrintLaTeX b, PrintLaTeX s, PrintLaTeX f)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett => PrintLaTeX (BASIC_SPEC b s f) where

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett printLatex0 ga (Basic_spec l) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett if null l then braces_latex empty else vcat (map (printLatex0 ga) l)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettinstance (PrintLaTeX b, PrintLaTeX s, PrintLaTeX f) =>

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett PrintLaTeX (BASIC_ITEMS b s f) where

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett printLatex0 ga (Sig_items s) = printLatex0 ga s

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Free_datatype l _) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett fsep_latex [hc_sty_plain_keyword "free"

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett <~> setTab_latex

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett <> hc_sty_plain_keyword ("type"++ pluralS l)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ,tabbed_nest_latex $ semiAnno_latex ga l]

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett printLatex0 ga (Sort_gen l _) =

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett hang_latex (hc_sty_plain_keyword generatedS

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett <~> setTab_latex<> condTypeS) 9 $

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett tabbed_nest_latex $ condBraces

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (vcat (map (printLatex0 ga) l))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett where condTypeS =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett if isOnlyDatatype then

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett hc_sty_plain_keyword (typeS++pluralS l)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett else empty

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett condBraces d =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett if isOnlyDatatype then

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett case l of

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett [x] -> case x of

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Annoted (Datatype_items l' _) _ lans _ ->

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett vcat (map (printLatex0 ga) lans)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett $$ semiAnno_latex ga l'

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett _ -> error "wrong implementation of isOnlyDatatype"

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett _ -> error "wrong implementation of isOnlyDatatype"

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else braces_latex d

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett isOnlyDatatype =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett case l of

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett [x] -> case x of

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Annoted (Datatype_items _ _) _ _ _ -> True

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett _ -> False

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett _ -> False

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Var_items l _) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett hc_sty_plain_keyword (varS++pluralS l) <\+>

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett semiT_latex ga l

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Local_var_axioms l f _) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett hc_sty_axiom "\\forall" <\+> semiT_latex ga l

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett $$ printLatex0Axioms ga f

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Axiom_items f _) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0Axioms ga f

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Ext_BASIC_ITEMS b) = printLatex0 ga b

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettprintLatex0Axioms :: PrintLaTeX f =>

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett GlobalAnnos -> [Annoted (FORMULA f)] -> Doc

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy GimblettprintLatex0Axioms ga f =

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett vcat $ map (printAnnotedFormula_Latex0 ga) f

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettprintAnnotedFormula_Latex0 :: PrintLaTeX f =>

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett GlobalAnnos -> Annoted (FORMULA f) -> Doc

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettprintAnnotedFormula_Latex0 ga (Annoted i _ las ras) =

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett let i' = hc_sty_axiom "\\bullet"

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett <\+> set_tabbed_nest_latex (printLatex0 ga i)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett las' = if not $ null las then

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sp_text 0 "\n" <> printAnnotationList_Latex0 ga las

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett else

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett empty

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett (la,ras') =

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett splitAndPrintRAnnos printLatex0

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett printAnnotationList_Latex0

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett (<\+>) (latex_macro "\\`" <>)

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett empty ga ras

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett in {-trace (show i)-} (las' $+$ fsep_latex [i',la] $$ ras')

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettinstance (PrintLaTeX s, PrintLaTeX f) =>

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett PrintLaTeX (SIG_ITEMS s f) where

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett printLatex0 ga (Sort_items l _) =

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett hc_sty_sig_item_keyword ga (sortS++pluralS l) <\+>

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett set_tabbed_nest_latex (semiAnno_latex ga l)

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Op_items l _) =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett hc_sty_sig_item_keyword ga (opS++pluralS l) <\+>

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett set_tabbed_nest_latex (semiAnno_latex ga l)

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Pred_items l _) =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett hc_sty_sig_item_keyword ga (predS++pluralS l) <\+>

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett set_tabbed_nest_latex (semiAnno_latex ga l)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Datatype_items l _) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett hc_sty_sig_item_keyword ga (typeS++pluralS l) <\+>

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett set_tabbed_nest_latex (semiAnno_latex ga l)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Ext_SIG_ITEMS s) = printLatex0 ga s

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblettinstance PrintLaTeX f => PrintLaTeX (SORT_ITEM f) where

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Sort_decl l _) = commaT_latex ga l

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Subsort_decl l t _) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett hang_latex (commaT_latex ga l) 8 $

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett hc_sty_axiom lessS <\+> printLatex0 ga t

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Subsort_defn s v t f _) =

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga s <\+> equals_latex <\+>

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett braces_latex (set_tabbed_nest_latex $ fsep

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett [printLatex0 ga v

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett <> colon_latex

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett <\+> printLatex0 ga t,

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett hc_sty_axiom "\\bullet"

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett <\+> set_tabbed_nest_latex (printLatex0 ga f)])

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett printLatex0 ga (Iso_decl l _) =

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett fsep_latex $ punctuate (space_latex<>equals_latex) $

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett map (printLatex0 ga) l

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettinstance PrintLaTeX f => PrintLaTeX (OP_ITEM f) where

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Op_decl l t a _) =

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett {-cat [ cat [commaT_latex ga l

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett ,colon_latex <> printLatex0 ga t <> condComma]

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett , if na then empty

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett else commaT_latex ga a

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett ]-}

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett if na then ids_sig

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else setTabWithSpaces_latex 4

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <>

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett fsep [ids_sig,

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett tabbed_nest_latex $ commaT_latex ga a]

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett where ids_sig = -- setTabWithSpaces_latex 6 <>

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett fsep [commaT_latex ga l<\+>colon_latex,

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett tabbed_nest_latex (if na then sig

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett else sig <> comma_latex)]

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sig = printLatex0 ga t

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett na = null a

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Op_defn n h term _) =

b34e5090387d45b3a35f88eaa23477a83d2a2962Andy Gimblett setTabWithSpaces_latex 4 <>

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett tab_hang_latex (printLatex0 ga n

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett <> printLatex0 ga h

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett <\+> equals_latex)

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett 4 (printLatex0 ga term)

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblettinstance PrintLaTeX OP_TYPE where

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Op_type Total l s _) =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett let (arg_types,type_arr) = if null l then (empty,empty)

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else (space_latex <>

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett crossT_latex ga l,

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett hc_sty_axiom "\\rightarrow")

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett result_type = printLatex0 ga s

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett in if isEmpty arg_types then result_type

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else sep_latex [arg_types,type_arr <\+> result_type]

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Op_type Partial l s _) =

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett (if null l then hc_sty_axiom quMark

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else space_latex

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <> crossT_latex ga l

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <\+>hc_sty_axiom ("\\rightarrow" ++ quMark))

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <\+> printLatex0 ga s

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettoptLatexQuMark :: FunKind -> Doc

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettoptLatexQuMark Partial = hc_sty_axiom quMark

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy GimblettoptLatexQuMark Total = empty

fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblettinstance PrintLaTeX OP_HEAD where

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Op_head k l s _) =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (if null l then empty

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else parens_latex (semiT_latex ga l))

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett <> colon_latex <> optLatexQuMark k

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett <\+> printLatex0 ga s

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettinstance PrintLaTeX ARG_DECL where

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 ga (Arg_decl l s _) = commaT_latex ga l

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <> colon_latex

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <\+> printLatex0 ga s

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettinstance PrintLaTeX f => PrintLaTeX (OP_ATTR f) where

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 _ (Assoc_op_attr) = hc_sty_id assocS

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 _ (Comm_op_attr) = hc_sty_id commS

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 _ (Idem_op_attr) = hc_sty_id idemS

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Unit_op_attr t) = hc_sty_id unitS <\+> printLatex0 ga t

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblettinstance PrintLaTeX f => PrintLaTeX (PRED_ITEM f) where

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 ga (Pred_decl l t _) = commaT_latex ga l

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett <\+> colon_latex <\+> printLatex0 ga t

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 ga (Pred_defn n h f _) =

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett sep_latex [printLatex0 ga n

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett <> printLatex0 ga h

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett <\+> hc_sty_axiom "\\Leftrightarrow",

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga f]

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblettinstance PrintLaTeX PRED_TYPE where

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 _ (Pred_type [] _) = parens_latex empty

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 ga (Pred_type l _) = crossT_latex ga l

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblettinstance PrintLaTeX PRED_HEAD where

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Pred_head l _) =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett parens_latex (semiT_latex ga l)

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettinstance PrintLaTeX DATATYPE_DECL where

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Datatype_decl s a _) =

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 ga s <\+>

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sep_latex

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (defnS'<> setTab_latex<~>

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett (printLatex0 ga $ head a)<>casl_normal_latex "~":

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett (map (\x -> tabbed_nest_latex (latex_macro

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett "\\hspace*{-0.84mm}"<> ---}

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett casl_normal_latex "\\textbar")

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett <~> (printLatex0 ga x)<>casl_normal_latex "~") $

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett tail a))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett where defnS' = hc_sty_axiom defnS

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettinstance PrintLaTeX ALTERNATIVE where

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Alt_construct k n l _) = tabbed_nest_latex (

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga n <> (if null l then case k of

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett Partial -> parens_tab_latex empty

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett _ -> empty

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett else parens_tab_latex ( semiT_latex ga l))

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett <> optLatexQuMark k)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Subsorts l _) =

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett sp_text (axiom_width s') s'' <\+> commaT_latex ga l

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett where s' = sortS ++ pluralS l

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett s'' = '\\':map toUpper s' ++ "[ID]"

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettinstance PrintLaTeX COMPONENTS where

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Cons_select k l s _) =

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett commaT_latex ga l <> colon_latex <> optLatexQuMark k

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett <> printLatex0 ga s

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Sort s) = printLatex0 ga s

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettinstance PrintLaTeX VAR_DECL where

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Var_decl l s _) = commaT_latex ga l

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett <> colon_latex

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett <\+> printLatex0 ga s

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettinstance PrintLaTeX f => PrintLaTeX (FORMULA f) where

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Quantification q l f _) =

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett set_tabbed_nest_latex $ fsep_latex

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett [printLatex0 ga q <\+> semiT_latex ga l ,

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett hc_sty_axiom "\\bullet"

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett <\+> set_tabbed_nest_latex (printLatex0 ga f)]

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Conjunction fs _) =

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett sep_latex $ punctuate (space_latex <> hc_sty_axiom "\\wedge")

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett $ map (condParensXjunction printLatex0 parens_tab_latex ga) fs

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett{- (sep_latex $ prepand_head $

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett prepPunctuate (hc_sty_axiom "\\wedge" <> space_latex) $

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett map (condParensXjunction printLatex0 parens_tab_latex ga) fs)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett where prepand_head l = case l of

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett [] -> []

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett [x] -> l

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (x:xs) -> (hspace_latex "0.375cm"<>x) : xs-}

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett printLatex0 ga (Disjunction fs _) =

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett sep_latex $ punctuate (space_latex <> hc_sty_axiom "\\vee")

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett $ map (condParensXjunction printLatex0 parens_tab_latex ga) fs

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett{- (sep_latex $ prepand_head $

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett prepPunctuate (hc_sty_axiom "\\vee" <> space_latex) $

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett map (condParensXjunction printLatex0 parens_tab_latex ga) fs)

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett where prepand_head l = case l of

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett [] -> []

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett [x] -> l

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (x:xs) -> (hspace_latex "0.375cm"<>x): xs-}

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga i@(Implication f g b _) =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett {-trace pos $ -}

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett if not b

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett then (

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett hang_latex (condParensImplEquiv printLatex0 parens_tab_latex ga i g False

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <\+> hc_sty_id "if") 3 $

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett condParensImplEquiv printLatex0 parens_tab_latex ga i f True)

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else (

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett hang_latex (condParensImplEquiv printLatex0 parens_tab_latex ga i f False

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <\+> hc_sty_axiom "\\Rightarrow") 3 $

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett condParensImplEquiv printLatex0 parens_tab_latex ga i g True)

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett{- where pos = "Implication: \"=>\": "++show p

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett ++"; left_most_id_of_first_formula: "

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett ++(show $ left_most_pos f )-}

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga e@(Equivalence f g _) =

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sep_latex

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett [condParensImplEquiv printLatex0 parens_tab_latex ga e f False

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett <\+> hc_sty_axiom "\\Leftrightarrow",

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett condParensImplEquiv printLatex0 parens_tab_latex ga e g True]

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 ga (Negation f _) = hc_sty_axiom "\\neg" <\+> condParensNeg f parens_latex (printLatex0 ga f)

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 _ (True_atom _) = hc_sty_id trueS

b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett printLatex0 _ (False_atom _) = hc_sty_id falseS

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett printLatex0 ga (Predication p l _) =

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett let (p_id,isQual) =

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett case p of

9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett Pred_name i -> (i,False)

Qual_pred_name i _ _ -> (i,True)

p' = printLatex0 ga p

in if isQual then

print_prefix_appl_latex ga p' l

else condPrint_Mixfix_latex ga p_id l

printLatex0 ga (Definedness f _) = hc_sty_id defS <\+> printLatex0 ga f

printLatex0 ga (Existl_equation f g _) =

hang_latex (printLatex0 ga f

<\+> sp_text (axiom_width "=")

"\\Ax{\\stackrel{e}{=}}") 8

$ printLatex0 ga g

printLatex0 ga (Strong_equation f g _) =

hang_latex (printLatex0 ga f <\+> hc_sty_axiom "=") 8

$ printLatex0 ga g

printLatex0 ga (Membership f g _) =

printLatex0 ga f <\+> hc_sty_axiom "\\in" <\+> printLatex0 ga g

printLatex0 ga (Mixfix_formula t) = printLatex0 ga t

printLatex0 _ (Unparsed_formula s _) = text s

printLatex0 ga (Sort_gen_ax constrs _) =

hc_sty_id generatedS <>

braces_latex (hc_sty_id sortS <+> commaT_latex ga sorts

<> semi_latex <+> semiT_latex ga ops)

<+>(if null sortMap then empty

else hc_sty_id withS

<+> fsep_latex (punctuate comma_latex (map printSortMap sortMap)))

where

(sorts,ops,sortMap) = recover_Sort_gen_ax constrs

printSortMap (s1,s2) = printLatex0 ga s1 <+> hc_sty_axiom "\\mapsto"

<+> printLatex0 ga s2

printLatex0 ga (ExtFORMULA f) = printLatex0 ga f

instance PrintLaTeX QUANTIFIER where

printLatex0 _ (Universal) = hc_sty_axiom "\\forall"

printLatex0 _ (Existential) = hc_sty_axiom "\\exists"

printLatex0 _ (Unique_existential) = hc_sty_axiom "\\exists!"

instance PrintLaTeX PRED_SYMB where

printLatex0 ga (Pred_name n) = printLatex0 ga n

printLatex0 ga (Qual_pred_name n t _) =

parens_latex $ hc_sty_id predS

<\+> printLatex0 ga n

<\+> colon_latex <\+> printLatex0 ga t

instance PrintLaTeX f => PrintLaTeX (TERM f) where

printLatex0 ga (Simple_id i) = printLatex0 ga i

printLatex0 ga (Qual_var n t _) = -- HERE

parens_latex $ hc_sty_id varS

<\+> printLatex0 ga n

<\+> colon_latex <\+> printLatex0 ga t

printLatex0 ga (Application o l _) =

let (o_id,isQual) =

case o of

Op_name i -> (i,False)

Qual_op_name i _ _ -> (i,True)

o' = printLatex0 ga o

in if isQual then

print_prefix_appl_latex ga (parens_latex o') l

else

print_Literal_latex ga o_id l

printLatex0 ga (Sorted_term t s _) =

condParensSorted_term parens_latex t (printLatex0 ga t) <>

colon_latex <\+> printLatex0 ga s

printLatex0 ga (Cast t s _) =

printLatex0 ga t <\+> hc_sty_id asS <\+> printLatex0 ga s

printLatex0 ga(Conditional u f v _) =

hang_latex (printLatex0 ga u) 8 $

sep_latex ((hc_sty_id whenS <\+> printLatex0 ga f):

[hc_sty_id elseS <\+> printLatex0 ga v])

printLatex0 _ (Unparsed_term s _) = text s

printLatex0 ga (Mixfix_qual_pred p) = printLatex0 ga p

printLatex0 ga (Mixfix_term l) =

cat(punctuate space (map (printLatex0 ga) l))

printLatex0 ga (Mixfix_token t) = printLatex0 ga t

printLatex0 ga (Mixfix_sorted_term s _) = colon

<> printLatex0 ga s

printLatex0 ga (Mixfix_cast s _) = text asS

<\+> printLatex0 ga s

printLatex0 ga (Mixfix_parenthesized l _) =

parens_tab_latex (commaT_latex ga l)

printLatex0 ga (Mixfix_bracketed l _) =

brackets_latex (commaT_latex ga l)

printLatex0 ga (Mixfix_braced l _) =

braces_latex (commaT_latex ga l)

instance PrintLaTeX OP_SYMB where

printLatex0 ga (Op_name o) = printLatex0 ga o

printLatex0 ga (Qual_op_name o t _) =

hc_sty_id opS

<\+> printLatex0 ga o <\+> colon_latex <> printLatex0 ga t

instance PrintLaTeX SYMB_ITEMS where

printLatex0 ga (Symb_items k l _) =

print_kind_latex ga k l <\+> commaT_latex ga l

instance PrintLaTeX SYMB_MAP_ITEMS where

printLatex0 ga (Symb_map_items k l _) =

print_kind_latex ga k l <\+> commaT_latex ga l

instance PrintLaTeX SYMB_KIND where

printLatex0 _ Implicit = empty

printLatex0 _ Sorts_kind = casl_keyword_latex sortS

printLatex0 _ Ops_kind = casl_keyword_latex opS

printLatex0 _ Preds_kind = casl_keyword_latex predS

instance PrintLaTeX SYMB where

printLatex0 ga (Symb_id i) = printLatex0 ga i

printLatex0 ga (Qual_id i t _) =

printLatex0 ga i <\+> colon_latex <\+> printLatex0 ga t

instance PrintLaTeX TYPE where

printLatex0 ga (O_type t) = printLatex0 ga t

printLatex0 ga (P_type t) = printLatex0 ga t

printLatex0 ga (A_type t) = printLatex0 ga t

instance PrintLaTeX SYMB_OR_MAP where

printLatex0 ga (Symb s) = printLatex0 ga s

printLatex0 ga (Symb_map s t _) =

printLatex0 ga s <\+> hc_sty_axiom "\\mapsto" <\+> printLatex0 ga t

print_kind_latex :: GlobalAnnos -> SYMB_KIND -> [a] -> Doc

print_kind_latex ga k l =

case k of

Implicit -> empty

_ -> latex_macro "\\KW{"<>kw<>s<>latex_macro "}"

where kw = printLatex0 ga k

s = case pluralS_symb_list k l of

"" -> empty

s' -> casl_keyword_latex s'

condPrint_Mixfix_latex :: PrintLaTeX f => GlobalAnnos -> Id -> [TERM f] -> Doc

condPrint_Mixfix_latex ga =

condPrint_Mixfix (printLatex0 ga) (printLatex0 ga) (printLatex0 ga)

parens_tab_latex

(<\+>) fsep_latex comma_latex

(Just $ printDisplayToken_latex casl_axiom_latex)

(Just DF_LATEX) ga

print_prefix_appl_latex :: PrintLaTeX f => GlobalAnnos -> Doc -> [TERM f] -> Doc

print_prefix_appl_latex ga =

print_prefix_appl (printLatex0 ga) parens_tab_latex fsep_latex comma_latex

print_Literal_latex :: PrintLaTeX f => GlobalAnnos -> Id -> [TERM f] -> Doc

print_Literal_latex ga =

print_Literal (printLatex0 ga) (printLatex0 ga) (printLatex0 ga)

parens_tab_latex

(<\+>) fsep_latex comma_latex

(Just $ printDisplayToken_latex casl_axiom_latex)

(Just DF_LATEX) ga

hc_sty_sig_item_keyword :: GlobalAnnos -> String -> Doc

hc_sty_sig_item_keyword ga str =

(if is_inside_gen_arg ga then hc_sty_plain_keyword

else hc_sty_casl_keyword ) str