LaTeX_AS_Architecture.hs revision b4fbc96e05117839ca409f5f20f97b3ac872d1ed
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj{-|
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjModule : $Header$
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjCopyright : (c) Klaus L�ttich, Uni Bremen 2002-2004
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjMaintainer : luettich@tzi.de
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjStability : provisional
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjPortability : non-portable(Grothendieck)
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignac LaTeX Printing the Architechture stuff of HetCASL.
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignac-}
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjmodule Syntax.LaTeX_AS_Architecture where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjimport Common.Lib.Pretty
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignacimport Common.PrintLaTeX
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignacimport Common.LaTeX_utils
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignacimport Common.Keywords
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignacimport Syntax.AS_Architecture
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjimport Syntax.LaTeX_AS_Structured
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjimport Syntax.Print_AS_Structured
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjimport Syntax.Print_AS_Architecture
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX ARCH_SPEC where
43cf232e238dd2e98c8b2badc91071b6ada52956gary.williams printLatex0 ga (Basic_arch_spec aa ab _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = semiT_latex ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in (hang_latex (hc_sty_plain_keyword (unitS ++ sS)) 4 aa')
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj $$ (hc_sty_plain_keyword resultS <\+> ab')
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Arch_spec_name aa) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Group_arch_spec aa _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj braces_latex $ printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX UNIT_REF where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_ref aa ab _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = simple_id_latex aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in aa' <\+> hc_sty_plain_keyword toS <\+> ab'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX UNIT_DECL_DEFN where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_decl aa ab ac _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = simple_id_latex aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ac' = if null ac then empty
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj else hc_sty_plain_keyword givenS <\+>
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj (commaT_latex ga ac)
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in hang_latex (aa' <> colon_latex <\+> ab') 4 ac'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_defn aa ab _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = simple_id_latex aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in hang_latex (aa' <\+> equals_latex) 4 ab'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX UNIT_SPEC where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_type aa ab _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = fsep_latex $ punctuate
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj (space_latex <> hc_sty_axiom "\\times"<> space_latex)
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj $ map (condBracesGroupSpec printLatex0
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj braces_latex Nothing ga) aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = condBracesGroupSpec printLatex0 braces_latex Nothing ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in if null aa then ab' else
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj aa' <\+> hc_sty_axiom "\\rightarrow" <\+> ab'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Spec_name aa) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in aa'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Closed_unit_spec aa _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in hang_latex (hc_sty_plain_keyword closedS) 4 aa'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX REF_SPEC where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_spec u) = printLatex0 ga u
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Refinement b u m r _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj (if b then empty else
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj hc_sty_plain_keyword behaviourallyS <> space_latex)
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj <> hc_sty_plain_keyword refinedS <\+> printLatex0 ga u <\+>
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj (if null m then empty else hc_sty_plain_keyword viaS <\+>
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj commaT_latex ga m <> space_latex) <> printLatex0 ga r
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Arch_unit_spec aa _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in hang_latex (hc_sty_plain_keyword archS
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj <\+> hc_sty_plain_keyword specS) 4 aa'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Compose_ref aa _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj listSep_latex (space_latex <> hc_sty_plain_keyword thenS) ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Component_ref aa _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj braces_latex $ commaT_latex ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX UNIT_EXPRESSION where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_expression aa ab _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = semiT_latex ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in if null aa then ab'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj else hang_latex (hc_sty_plain_keyword lambdaS) 4
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj (hang_latex aa' (-2)
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ( hc_sty_axiom "\\bullet" <\+> ab'))
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX UNIT_BINDING where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_binding aa ab _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in aa' <\+> colon_latex <\+> ab'
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX UNIT_TERM where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_reduction aa ab) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in fsep_latex [aa', ab']
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_translation aa ab) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in fsep [aa', ab']
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Amalgamation aa _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj listSep_latex (space_latex <> hc_sty_plain_keyword andS) ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Local_unit aa ab _) =
43cf232e238dd2e98c8b2badc91071b6ada52956gary.williams let aa' = semiT_latex ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = printLatex0 ga ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in (hang_latex (hc_sty_plain_keyword localS) 4 aa') $$
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj (hang_latex (hc_sty_plain_keyword withinS) 4 ab')
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Unit_appl aa ab _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj let aa' = simple_id_latex aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj ab' = fsep_latex $ map (printLatex0 ga) ab
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj in aa' <> (if null ab then empty else space_latex <> ab')
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Group_unit_term aa _) =
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj sp_between_latex (latex_macro "\\{") (latex_macro "\\}")
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj $ printLatex0 ga aa
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudjinstance PrintLaTeX FIT_ARG_UNIT where
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga (Fit_arg_unit aa ab _) = brackets_latex $
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj printLatex0 ga aa <>
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj (if null ab then empty else space_latex <>
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj hc_sty_plain_keyword fitS <\+>
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj set_tabbed_nest_latex (fsep_latex (map (printLatex0 ga) ab)))
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj
5ca6c5dacac07297bb0b2162fa8f58f5b073d8d7maudj