# HG changeset patch # User Christian Urban # Date 1294148858 0 # Node ID 3890483c674fe3a9b2ddcc04b50885695cb693ec # Parent 0865caafbfe6072e420261b7da9ae8da39e9b0cd final version of the ESOP paper; used set+ instead of res as requested by one reviewer diff -r 0865caafbfe6 -r 3890483c674f Nominal/Ex/Typing.thy --- a/Nominal/Ex/Typing.thy Mon Jan 03 16:21:12 2011 +0000 +++ b/Nominal/Ex/Typing.thy Tue Jan 04 13:47:38 2011 +0000 @@ -40,15 +40,16 @@ *} ML {* -fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = +fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = let - fun aux arg = arg + val vc_goal = concl_args + |> HOLogic.mk_tuple |> mk_fresh_star avoid_trm |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> (curry list_all_free) params in - if null avoid then [] else map aux concl_args + if null avoid then [] else [vc_goal] end *} @@ -192,16 +193,38 @@ end) ctxt *} + ML {* -fun binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trms ctxt = +fun fresh_thm ctxt fresh_thms p c prms avoid_trm = + let + val conj1 = + mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c + val conj2 = + mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) prms))) (Bound 0) + val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2)) + |> HOLogic.mk_Trueprop + + val _ = tracing ("fresh goal: " ^ Syntax.string_of_term ctxt fresh_goal) + in + Goal.prove ctxt [] [] fresh_goal + (K (HEADGOAL (rtac @{thm at_set_avoiding2}))) + end +*} + +ML {* +fun binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt = Subgoal.FOCUS (fn {context, params, ...} => let val thy = ProofContext.theory_of context - val (prms, p, _) = split_last2 (map snd params) - val prm_tys = map (fastype_of o term_of) prms + val (prms, p, c) = split_last2 (map snd params) + val prm_trms = map term_of prms + val prm_tys = map fastype_of prm_trms val cperms = map (cterm_of thy o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem + val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm + + val fthm = fresh_thm context fresh_thms (term_of p) (term_of c) (map term_of prms) avoid_trm' in Skip_Proof.cheat_tac thy (* EVERY1 [rtac prem'] *) @@ -209,10 +232,10 @@ *} ML {* -fun case_tac ctxt fresh_thms Ps avoid avoid_trm intr_cvars prem = +fun case_tac ctxt fresh_thms Ps (avoid, avoid_trm) intr_cvars param_trms prem = let val tac1 = non_binder_tac prem intr_cvars Ps ctxt - val tac2 = binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trm ctxt + val tac2 = binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt in EVERY' [ rtac @{thm allI}, rtac @{thm allI}, eqvt_stac ctxt, if null avoid then tac1 else tac2 ] @@ -220,16 +243,16 @@ *} ML {* -fun tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars {prems, context} = +fun prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms {prems, context} = let - val cases_tac = map4 (case_tac context fresh_thms Ps) avoids avoid_trms intr_cvars prems + val cases_tac = map4 (case_tac context fresh_thms Ps) (avoids ~~avoid_trms) intr_cvars param_trms prems in EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ] end *} ML {* -val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (\c. Q ==> P (0::perm) c)" by simp} +val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp} *} ML {* @@ -248,7 +271,7 @@ val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs val intr_vars = (map o map) fst intr_vars_tys val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms - val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys + val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys val (intr_prems, intr_concls) = intrs |> map prop_of @@ -291,7 +314,7 @@ fun after_qed ctxt_outside fresh_thms ctxt = let val thms = Goal.prove ctxt [] ind_prems' ind_concl' - (tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars) + (prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms) |> singleton (ProofContext.export ctxt ctxt_outside) |> Datatype_Aux.split_conj_thm |> map (fn thm => thm RS normalise) @@ -439,6 +462,7 @@ nominal_inductive typing avoids t_Lam: "x" + (* | t_Var: "x" *) apply - apply(simp_all add: fresh_star_def ty_fresh lam.fresh)? done @@ -506,6 +530,7 @@ apply(simp only: permute_plus) apply(rule supp_perm_eq) apply(simp add: supp_Pair fresh_star_Un) + (* apply(perm_simp) *) apply(simp (no_asm) only: eqvts) apply(rule a3) apply(simp only: eqvts permute_plus) @@ -517,6 +542,7 @@ apply(assumption) apply(perm_strict_simp) apply(simp only:) + thm at_set_avoiding2 apply(rule at_set_avoiding2) apply(simp add: finite_supp) apply(simp add: finite_supp) diff -r 0865caafbfe6 -r 3890483c674f Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Mon Jan 03 16:21:12 2011 +0000 +++ b/Nominal/nominal_dt_quot.ML Tue Jan 04 13:47:38 2011 +0000 @@ -466,7 +466,7 @@ |> mk_perm (Bound 0) val goal = mk_fresh_star lhs rhs - |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) + |> mk_exists ("p", @{typ perm}) |> HOLogic.mk_Trueprop val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} diff -r 0865caafbfe6 -r 3890483c674f Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Mon Jan 03 16:21:12 2011 +0000 +++ b/Nominal/nominal_library.ML Tue Jan 04 13:47:38 2011 +0000 @@ -23,6 +23,7 @@ val mk_id: term -> term val mk_all: (string * typ) -> term -> term val mk_All: (string * typ) -> term -> term + val mk_exists: (string * typ) -> term -> term val sum_case_const: typ -> typ -> typ -> term val mk_sum_case: term -> term -> term @@ -204,6 +205,8 @@ fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) +fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) + fun sum_case_const ty1 ty2 ty3 = Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) diff -r 0865caafbfe6 -r 3890483c674f Paper/Paper.thy --- a/Paper/Paper.thy Mon Jan 03 16:21:12 2011 +0000 +++ b/Paper/Paper.thy Tue Jan 04 13:47:38 2011 +0000 @@ -23,7 +23,7 @@ If ("if _ then _ else _" 10) and alpha_set ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and alpha_lst ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and - alpha_res ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and + alpha_res ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and abs_set2 ("_ \\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and fv ("fa'(_')" [100] 100) and @@ -32,7 +32,7 @@ Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and Abs_lst ("[_]\<^bsub>list\<^esub>._") and Abs_dist ("[_]\<^bsub>#list\<^esub>._") and - Abs_res ("[_]\<^bsub>res\<^esub>._") and + Abs_res ("[_]\<^bsub>set+\<^esub>._") and Abs_print ("_\<^bsub>set\<^esub>._") and Cons ("_::_" [78,77] 73) and supp_set ("aux _" [1000] 10) and @@ -104,7 +104,7 @@ the second pair should \emph{not} be $\alpha$-equivalent: % \begin{equation}\label{ex1} - @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. x \ y"}\hspace{10mm} + @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. y \ x"}\hspace{10mm} @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} \end{equation} % @@ -138,7 +138,7 @@ \eqref{one} as $\alpha$-equivalent with % \begin{center} - @{text "\ x = 3 \ y = 2 \ z = loop \ x - y \"} + @{text "\ x = 3 \ y = 2 \ z = foo \ x - y \"} \end{center} % \noindent @@ -318,7 +318,7 @@ The problem with introducing a new type in Isabelle/HOL is that in order to be useful, a reasoning infrastructure needs to be ``lifted'' from the underlying subset to the new type. This is usually a tricky and arduous - task. To ease it, we re-implemented in Isabelle/HOL the quotient package + task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package described by Homeier \cite{Homeier05} for the HOL4 system. This package allows us to lift definitions and theorems involving raw terms to definitions and theorems involving $\alpha$-equated terms. For example if we @@ -729,12 +729,12 @@ Now recall the examples shown in \eqref{ex1} and \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \ y)"} and @{text "({y, x}, y \ x)"} are $\alpha$-equivalent according to - $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to + $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then @{text "([x, y], x \ y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \ y)"} since there is no permutation that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \ y"}} - unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$ + unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$ @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity permutation. However, if @{text "x \ y"}, then @{text "({x}, x)"} $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no @@ -751,13 +751,13 @@ \end{equation} \noindent - (similarly for $\approx_{\,\textit{abs\_res}}$ + (similarly for $\approx_{\,\textit{abs\_set+}}$ and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence relations. %% and equivariant. \begin{lemma}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ - and $\approx_{\,\textit{abs\_res}}$ are equivalence relations. %, and if + and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if %@{term "abs_set (as, x) (bs, y)"} then also %@{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} (similarly for the other two relations). \end{lemma} @@ -772,7 +772,7 @@ \noindent This lemma allows us to use our quotient package for introducing - new types @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} + new types @{text "\ abs_set"}, @{text "\ abs_set+"} and @{text "\ abs_list"} representing $\alpha$-equivalence classes of pairs of type @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} (in the third case). @@ -797,8 +797,8 @@ \begin{tabular}{l} @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$ @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\ - @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} $\;\;=\;\;$ - @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]} + @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$ + @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]} \end{tabular} \end{center} \end{theorem} @@ -950,9 +950,9 @@ % \begin{center} \begin{tabular}{@ {}l@ {}} - \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\; - \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\; - \isacommand{bind (res)} {\it binders} \isacommand{in} {\it bodies} + \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, + \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, + \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies} \end{tabular} \end{center} % @@ -981,7 +981,7 @@ \noindent %Similarly for the other binding modes. %Interestingly, in case of \isacommand{bind (set)} - %and \isacommand{bind (res)} the binding clauses above will make a difference to the semantics + %and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics %of the specifications (the corresponding $\alpha$-equivalence will differ). We will %show this later with an example. @@ -998,7 +998,7 @@ For binders we distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders are just labels. The restriction we need to impose on them is that in case of - \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either + \isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either refer to atom types or to sets of atom types; in case of \isacommand{bind} the labels must refer to atom types or lists of atom types. Two examples for the use of shallow binders are the specification of lambda-terms, where a @@ -1018,7 +1018,7 @@ \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\ \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\ \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~% - \isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\ + \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\ \end{tabular} \end{tabular} \end{center} @@ -1037,7 +1037,7 @@ other arguments and also in the same argument (we will call such binders \emph{recursive}, see below). The binding functions are expected to return either a set of atoms (for \isacommand{bind (set)} and - \isacommand{bind (res)}) or a list of atoms (for \isacommand{bind}). They can + \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can be defined by recursion over the corresponding type; the equations must be given in the binding function part of the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with @@ -1487,7 +1487,7 @@ \noindent In this case we define a premise @{text P} using the relation $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly - $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other + $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other binding modes). This premise defines $\alpha$-equivalence of two abstractions involving multiple binders. As above, we first build the tuples @{text "D"} and @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding @@ -1641,7 +1641,7 @@ \begin{proof} The proof is by mutual induction over the definitions. The non-trivial cases involve premises built up by $\approx_{\textit{set}}$, - $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They + $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They can be dealt with as in Lemma~\ref{alphaeq}. \end{proof} @@ -1761,7 +1761,7 @@ Finally we can add to our infrastructure a cases lemma (explained in the next section) and a structural induction principle - for the types @{text "ty\"}$_{i..n}$. The conclusion of the induction principle is + for the types @{text "ty\"}$_{1..n}$. The conclusion of the induction principle is of the form % %\begin{equation}\label{weakinduct} @@ -1794,7 +1794,7 @@ \end{center} % \noindent - These properties can be established using the induction principle. + These properties can be established using the induction principle for the types @{text "ty\"}$_{1..n}$. %%in \eqref{weakinduct}. Having these equivariant properties established, we can show that the support of term-constructors @{text "C\<^sup>\"} is included in @@ -1954,7 +1954,7 @@ %in every induction step. What is left to show is that we covered all cases. To do so, we use - a cases lemma derived for each type. For the terms in \eqref{letpat} + a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} this lemma is of the form % \begin{equation}\label{weakcases} @@ -1974,7 +1974,7 @@ principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and \emph{all} @{text Let}-terms. - What we need instead is a cases rule where we only have to consider terms that have + What we need instead is a cases lemma where we only have to consider terms that have binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications % \begin{center} @@ -2257,7 +2257,7 @@ binding clauses. In Ott you specify binding clauses with a single body; we allow more than one. We have to do this, because this makes a difference for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and - \isacommand{bind (res)}. + \isacommand{bind (set+)}. % %Consider the examples % @@ -2312,7 +2312,7 @@ In a slightly different domain (programming with dependent types), the paper \cite{Altenkirch10} presents a calculus with a notion of - $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}. + $\alpha$-equivalence related to our binding mode \isacommand{bind (set+)}. The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it has a more operational flavour and calculates a partial (renaming) map. In this way, the definition can deal with vacuous binders. However, to our @@ -2330,7 +2330,7 @@ To specify general binders we used the specifications from Ott, but extended them in some places and restricted them in others so that they make sense in the context of $\alpha$-equated terms. - We also introduced two binding modes (set and res) that do not + We also introduced two binding modes (set and set+) that do not exist in Ott. We have tried out the extension with calculi such as Core-Haskell, type-schemes and approximately a dozen of other typical examples from programming diff -r 0865caafbfe6 -r 3890483c674f Paper/document/acmconf.cls --- a/Paper/document/acmconf.cls Mon Jan 03 16:21:12 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,442 +0,0 @@ -% ACMCONF DOCUMENT CLASS -% adapted from ARTICLE document style by Ken Traub -% Hacked for [preprint] option by Olin Shivers 4/91 -% Fixed up for LaTeX version 2e [compatibility mode] by Peter Lee 10/9 -% (with help from Simon Peyton Jones) -% Converted to a LaTeX2e document class by David A. Berson 11/94 -% -% ARTICLE DOCUMENT STYLE -- Released 16 March 1988 -% for LaTeX version 2.09 -% Copyright (C) 1988 by Leslie Lamport - -% To do: -% - Possibly move the commands related to 9pt size to a file size9.clo -% and write the stuff to unpack both acmconf.cls and size9.clo files -% from a single distribution file. - -%%% ACMCONF is a document class for producing two-column camera-ready pages for -%%% ACM conferences, according to ACM specifications. The main features of -%%% this class are: -%%% -%%% 1) Two columns. -%%% 2) Side and top margins of 4.5pc, bottom margin of 7.5pc, column gutter of -%%% 2pc, hence columns are 20pc wide and 54pc tall. (6pc = 1in, approx) -%%% 3) First page has title information, and an extra 4.5pc of space at the -%%% bottom of the first column for the ACM copyright notice. (You must -%%% use one of the commands \copyrightspace or \toappear{} to obtain this -%%% space.) -%%% 4) Text is 9pt on 10pt baselines; titles are 9pt bold sans-serif. -%%% (The acmconf.sty from which acmconf.cls was derived actually uses -%%% 9pt bold roman for section titles. Functionally, I have left this -%%% as is. I have added a commented out alternate defination of -%%% \acmtitlestyle that uses sans-serif) --DAB -%%% -%%% This document class supports a [preprint] class option that allows you -%%% to run off a copy for a preprint -- with page numbers, "to appear" -%%% information, and so forth. This is documented below. - -%%% There are a few restrictions you must observe: -%%% -%%% 1) You cannot change the font size; ACM wants you to use 9pt. -%%% 3) You must start your paper with the \maketitle command. Prior to the -%%% \maketitle you must have \title and \author commands. If you have a -%%% \date command it will be ignored; no date appears on the paper, since -%%% the proceedings will have a date on the front cover. -%%% Optionally, you may have an \affiliation command with text, such -%%% as company or university name and address, that will be centered -%%% just below the author(s). -%%% 4) Marginal paragraphs, tables of contents, lists of figures and tables, -%%% and page headings are all forbidden. -%%% 5) The `figure' environment will produce a figure one column wide; if you -%%% want one that is two columns wide, use `figure*'. Ditto for the -%%% `table' and `table*' environments. -%%% -%%% Page Headings: -%%% Normally, \pagestyle commands are ignored --- pages have no headings or -%%% numbers. ACM will number the pages for you when they are inserted into the -%%% proceedings (you should put page numbers on the BACK of each page, though, -%%% in case someone drops your paper on the floor). -%%% -%%% If the [preprint] option is present, then \pagestyle commands are obeyed, -%%% and the default is \pagestyle{plain}. The [twoside] option is also -%%% useful when using headers. -%%% -%%% The [draft] and [final] options as used in the article class are also -%%% supported. -%%% -%%% -%%% Copyright Space: -%%% You leave space at the bottom of page 1/column 1 one with the -%%% \copyrightspace command. Alternatively, you can use the -%%% \toappear{...} command. Normally, this turns into an unnumbered -%%% footnote 4.5pc high. If [preprint] is on, then this space is -%%% filled with the {...} text; otherwise, it's blank. You must put -%%% one of these commands in the text of page 1/column 1 *after* all the -%%% other footnotes that go on page1/column 1, of course. -%%% -%%% A typical usage looks like this: -%%% \toappear{To appear in the Ninth AES Conference on Midevil Lithuanian -%%% Embalming Technique, June 1991, Alfaretta, Georgia. -%%% Also available as Technical Report CMU-CS-91-119, -%%% Cranberry Melon School of Cucumber Science.} -%%% This will be included in the preprint, and left out of the conference -%%% version. -%%% -%%% Acmconf defines two useful conditionals. -%%% - \ifacmconf{true-stuff}{false-stuff} -%%% expands to true-stuff. -%%% - \ifpreprint true-stuff \else else-stuff \fi -%%% expands to true-stuff if the [preprint] option is being used, -%%% otherwise it expands to else-stuff. -%%% \ifacmconf is a latex command; \ifpreprint is a real latex conditional. -%%% -%%% WARNING: -%%% Some dvi-ps converters heuristically allow chars to drift from their -%%% true positions a few pixels. This loses noticeably with the 9pt sans-serif -%%% bold font used for section headers. You turn this hackery off in our -%%% dvi-ps converters with the -e option: -%%% dvips -e 0 foo.dvi >foo.ps - -\NeedsTeXFormat{LaTeX2e} -\ProvidesClass{acmconf}[1994/11/27 Alternative LaTeX document class] -\typeout{Bugs to berson@cs.pitt.edu} - -% -% Define the conditionals and command for the options. -% -\newif\if@acmconf\@acmconftrue -\long\def\ifacmconf#1#2{\if@acmconf#1\else#2\fi} -\newif\ifpreprint - -% -% Declare and process the options -% -\DeclareOption{draft}{\PassOptionsToClass{draft}{article}} -\DeclareOption{final}{\PassOptionsToClass{final}{article}} -\DeclareOption{twocolumn}{\PassOptionsToClass{twocolumn}{article}} -\DeclareOption{twoside}{\PassOptionsToClass{twoside}{article}} -\DeclareOption{preprint}{\preprintfalse} -%\DeclareOption{preprint}{\preprinttrue} -% -% Let them off with just a warning for any other option -% -\DeclareOption*{\ClassWarningNoLine{acmconf}{Unknown option `\CurrentOption'}} -%\DeclareOption*{\ClassError{acmconf} -% {The `\CurrentOption' option is not supported} -% {Remove the `\CurrentOption' option from the -% \protect\documentclass\space line.}} - -\ExecuteOptions{twocolumn} -\ProcessOptions - -% -% This class simply modifies a few behaviors of the article class, -% so load it now -% -\LoadClass{article} - - -%********************************************************************** -% -% The following commands would normally be in a file such as -% size9.clo for the article class. Since the size isn't really an -% option, I include them here. I have followed the order of the commands -% as found in size10.clo. -% -% I could test for the presence of % the file size9.clo and load it when -% availale, instead of executing these commands. -% - -% -% Set the font sizes and spacing -% -\renewcommand\baselinestretch{1} - -\renewcommand\normalsize{% - \@setfontsize\normalsize\@ixpt\@xpt - \abovedisplayskip 9\p@ \@plus2\p@ \@minus4.5\p@% - \abovedisplayshortskip \z@ \@plus3\p@% - \belowdisplayshortskip 5.4\p@ \@plus3\p@ \@minus3\p@% - \belowdisplayskip \abovedisplayskip - \let\@listi\@listI} -\normalsize -\renewcommand\small{% - \@setfontsize\small\@viiipt{9}% - \abovedisplayskip 7.6\p@ \@plus 3\p@ \@minus 4\p@% - \abovedisplayshortskip \z@ \@plus2\p@% - \belowdisplayshortskip 3.6\p@ \@plus2\p@ \@minus 2\p@ - \def\@listi{\leftmargin\leftmargini - \topsep 4\p@ \@plus 2\p@ \@minus 2\p@ - \parsep 2\p@ \@plus 1\p@ \@minus 1\p@ - \itemsep \parsep} - \belowdisplayskip \abovedisplayskip -} -\renewcommand\footnotesize{% - \@setfontsize\footnotesize\@viipt{8} - \abovedisplayskip 6.4\p@ \@plus 2\p@ \@minus 4\p@% - \abovedisplayshortskip \z@ \@plus 1\p@% - \belowdisplayshortskip 2.7\p@ \@plus 1\p@ \@minus 2\p@ - \def\@listi{\leftmargin\leftmargini - \topsep 3\p@ \@plus 1\p@ \@minus 1\p@ - \parsep 2\p@ \@plus 1\p@ \@minus 1\p@ - \itemsep \parsep}% - \belowdisplayskip \abovedisplayskip -} -\renewcommand\scriptsize{\@setfontsize\scriptsize\@viipt{8pt}} -\renewcommand\tiny{\@setfontsize\tiny\@vpt{6pt}} -\renewcommand\large{\@setfontsize\large\@xipt{13.6\p@}} -\renewcommand\Large{\@setfontsize\Large\@xiipt{14\p@}} -\renewcommand\LARGE{\@setfontsize\LARGE\@xivpt{18\p@}} -\renewcommand\huge{\@setfontsize\huge\@xviipt{22\p@}} -\renewcommand\Huge{\@setfontsize\Huge\@xxpt{25\p@}} - -\setlength\parindent{13.5\p@} % This is what normally used for one - % column. Should it be 1em for us? -\setlength\headheight{0\p@} -\setlength\headsep{0\p@} -\setlength\headheight{0\p@} -\setlength\headsep{0\p@} -\setlength\footskip{30\p@} -% -% There was no \topskip or \@maxdepth in the original acmconf.sty. -% Thus, we inherit -%\topskip 10pt -%\maxdepth .5\topskip -% from size10.clo loaded via article.cls -% -\setlength\textwidth{42pc} -\setlength\textheight{650\p@} -\setlength\oddsidemargin{4.5pc} -\addtolength\oddsidemargin{-1in} % Correct for LaTeX gratuittousness -\setlength\evensidemargin{4.5pc} -\addtolength\evensidemargin{-1in} % Correct for LaTeX gratuittousness -\setlength\marginparwidth{0\p@} % Margin pars are not allowed. -\setlength\marginparsep{11\p@} -\setlength\marginparpush{5\p@} -\setlength\topmargin{4.5pc} -\addtolength\topmargin{-1in} % Correct for LaTeX gratuitousness -% -% I wonder if these next three lines should only be executed if -% the preprint option is in effect? -- DAB -% -%% Must redefine the top margin so there's room for headers and -%% page numbers if you are using the preprint option. Footers -%% are OK as is. Olin. -\addtolength\topmargin{-37\p@} % Leave 37pt above text for headers -\setlength\headheight{12\p@} -\setlength\headsep{25\p@} - -\setlength\footnotesep{5.6\p@} -\setlength{\skip\footins}{8.1\p@ \@plus 4\p@ \@minus 2\p@} -\setlength\floatsep{11\p@ \@plus 2\p@ \@minus 2\p@} -\setlength\textfloatsep{18\p@ \@plus 2\p@ \@minus 4\p@} -\setlength\intextsep{11\p@ \@plus 2\p@ \@minus 2\p@} -\setlength\dblfloatsep{11\p@ \@plus 2\p@ \@minus 2\p@} -\setlength\dbltextfloatsep{18\p@ \@plus 2\p@ \@minus 4\p@} -% -% These values will be inherited from the default size10.clo file -% included when we load the base article class. I include them -% here for completeness in case we split out the size9.clo file someday. -% --DAB -\setlength\@fptop{0\p@ \@plus 1fil} -\setlength\@fpsep{8\p@ \@plus 2fil} -\setlength\@fpbot{0\p@ \@plus 1fil} -\setlength\@dblfptop{0\p@ \@plus 1fil} -\setlength\@dblfpsep{8\p@ \@plus 2fil} -\setlength\@dblfpbot{0\p@ \@plus 1fil} -\setlength\partopsep{2\p@ \@plus 1\p@ \@minus 1\p@} -% -% I think that all of these should be renewcommands. I also think -% that \setlength should be used. But, they are not in the size10.clo -% file that I am following. --DAB -% -\renewcommand\@listI{\leftmargin\leftmargini - \parsep 3.6\p@ \@plus 2\p@ \@minus 1\p@% - \topsep 7.2\p@ \@plus 2\p@ \@minus 4\p@% - \itemsep 3.6\p@ \@plus 2\p@ \@minus 1\p@} -\let\@listi\@listI -\@listi -\def\@listii {\leftmargin\leftmarginii - \labelwidth\leftmarginii - \advance\labelwidth-\labelsep - \topsep 3.6\p@ \@plus 2\p@ \@minus 1\p@ - \parsep 1.8\p@ \@plus 0.9\p@ \@minus 0.9\p@ - \itemsep \parsep} -\def\@listiii{\leftmargin\leftmarginiii - \labelwidth\leftmarginiii - \advance\labelwidth-\labelsep - \topsep 1.8\p@ plus 0.9\p@ minus 0.9\p@ - \parsep \z@ - \partopsep 1\p@ plus 0\p@ minus 1\p@ - \itemsep \topsep} -\def\@listiv {\leftmargin\leftmarginiv - \labelwidth\leftmarginiv - \advance\labelwidth-\labelsep} -\def\@listv {\leftmargin\leftmarginv - \labelwidth\leftmarginv - \advance\labelwidth-\labelsep} -\def\@listvi {\leftmargin\leftmarginvi - \labelwidth\leftmarginvi - \advance\labelwidth-\labelsep} -% -% End of the "size9.clo" commands -%********************************************************************** - -% -% here's a few things that I didn't find in either article.cls or -% size10.clo, so I left them here. --DAB -% -\setlength\columnsep{2pc} % Space between columns -\setlength\columnseprule{0\p@} % Width of rule between columns. -\hfuzz 1pt % Allow some variation in column width, otherwise it's - % too hard to typeset in narrow columns. - - -%********************************************************************** -% -% Now we get on with overriding things found in article.cls -% -\setlength\parindent{13.5\p@} - -% -% This command is used to format section headings. The format is the only -% thing that differs between these section commands and the ones in -% article.cls. -% -% Although the original documentation says that sans-serif is supposed to be -% used for section titles, the file as I received uses roman. The -% commented out line implements sans-serif. Be sure to comment out the -% \bfseries line if you switch. -% --DAB -% -\newcommand\@acmtitlestyle{\normalsize\bfseries} -%\newcommand\@acmtitlestyle{\normalsize\sffamily} - -\renewcommand\section{\@startsection {section}{1}{\z@}% - {-3.5ex \@plus -1ex \@minus -.2ex}% - {2.3ex \@plus .2ex}% - {\@acmtitlestyle}} -\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% - {-3.25ex \@plus -1ex \@minus -.2ex}% - {1.5ex \@plus .2ex}% - {\@acmtitlestyle}} -\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% - {-3.25ex \@plus -1ex \@minus -.2ex}% - {1.5ex \@plus .2ex}% - {\@acmtitlestyle}} -\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}% - {3.25ex \@plus 1ex \@minus .2ex}% - {-1em}% - {\@acmtitlestyle}} -\renewcommand\subparagraph{\@startsection{subparagraph}{4}{\parindent}% - {3.25ex \@plus 1ex \@minus .2ex}% - {-1em}% - {\@acmtitlestyle}} - -\setcounter{secnumdepth}{3} - -\setlength\arraycolsep{4.5\p@} -\setlength\tabcolsep{5.4\p@} -\setlength\doublerulesep{1.8\p@} - -\setlength\fboxsep{2.7\p@} -\setlength\fboxrule{.4\p@} - -\def\tableofcontents{\ClassError{acmconf}% - {\protect\tableofcontents: Tables of contents are not allowed in the `acmconf' document class}% - {Remove the \protect\tableofcontents\space command from the file}} - -\def\listoffigures{\ClassError{acmconf}% - {\protect\listoffigures: Lists of figures are not allowed in the `acmconf' document class}% - {Remove the \protect\listoffigures\space command from the file}} - -\def\listoftables{\ClassError{acmconf}% - {\protect\listoftables: Lists of tables are not allowed in the `acmconf' document class}% - {Remove the \protect\listoftables\space command from the file}} -\let\l@table\l@figure - -% -% Added \@makefntext definition so that the mark would not over print -% the beginning of the \thanks text. --DAB -% -\def\maketitle{\par - \begingroup - \def\thefootnote{\fnsymbol{footnote}}% - \def\@makefnmark{\hbox to 0pt{$\m@th^{\@thefnmark}$\hss}}% - \long\def\@makefntext##1{\parindent 1em\noindent - \hbox to1.8em{\hss$\m@th^{\@thefnmark}$}##1}% - \if@twocolumn - \twocolumn[\@maketitle] - \else \newpage - \global\@topnum\z@ % Prevents figures from going at top of page. - \@maketitle \fi - \thispagestyle{plain}\@thanks % UE: Changed {empty} to {plain} - \endgroup - \setcounter{footnote}{0} - \let\maketitle\relax - \let\@maketitle\relax - \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\gdef\@affili{}\let\thanks\relax} - -% -% extra declarations needed for our version of @maketitle -% -\newbox\@acmtitlebox -\gdef\affili{} -\def\affiliation#1{\gdef\affili{#1}} - -% -% The modified @maketitle -% -\def\@maketitle{\newpage - \null - \setbox\@acmtitlebox\vbox{% - \vskip 2em % Vertical space above title. - \begin{center} - {\LARGE \@title \par} % Title set in \LARGE size. - \vskip 1.5em % Vertical space after title. - {\large % each author set in \large, in a - \lineskip .5em % tabular environment - \begin{tabular}[t]{c}\@author - \end{tabular}\par} - \vskip 1em - \begin{center} - {\large \affili} - \end{center} - \vskip 1.5em % Vertical space after author. - \end{center}} - \dimen0=\ht\@acmtitlebox - \advance\dimen0 by -13.5pc\relax - \unvbox\@acmtitlebox - \ifdim\dimen0<0.0pt\relax\vskip-\dimen0\fi} - -\long\def\unmarkedfootnote#1{{\long\def\@makefntext##1{##1}\footnotetext{#1}}} - -%% Use one of \copyrightspace or \toappear{To appear in the ACM ...} -\def\copyrightspace{\unmarkedfootnote{\vrule height 4.5pc - width 0in depth 0in}} - -%% \small is bigger than \footnotesize. -\def\toappear#1% - {\ifpreprint \unmarkedfootnote{\vrule height 2.25pc% - depth 2.25pc width 0in% - \parbox{2.8in}{\small #1}}% - \else \copyrightspace \fi} - -%\def\marginpar{\ClassError{acmconf}% -% {The \protect\marginpar command is not allowed in the `acmconf' document class}% -% {Remove the \protect\marginpar\space command from the file}} - -\mark{{}{}} % Initializes TeX's marks - -%% Headings are ignored unless the [preprint] option is in force. -\ifpreprint\else % preprint off -- all \pagestyle commands ==> \pagestyle{empty}. -% \let\ps@plain\ps@empty % UE: Commented this line out - \let\ps@headings\ps@empty - \let\ps@myheadings\ps@empty -\fi - -\raggedbottom % Ragged bottom - -\endinput -%% -%% End of file `acmconf.cls'. diff -r 0865caafbfe6 -r 3890483c674f Paper/document/root.bib --- a/Paper/document/root.bib Mon Jan 03 16:21:12 2011 +0000 +++ b/Paper/document/root.bib Tue Jan 04 13:47:38 2011 +0000 @@ -1,3 +1,10 @@ + +@Unpublished{KaliszykUrban11, + author = {C.~Kaliszyk and C.~Urban}, + title = {{Q}uotients {R}evisited for {I}sabelle/{HOL}}, + note = {To appear in the Proc.~of the 26th ACM Symposium On Applied Computing}, + year = {2011} +} @InProceedings{cheney05a, author = {J.~Cheney}, @@ -188,10 +195,13 @@ year = 1999 } -@Unpublished{SatoPollack10, +@article{SatoPollack10, author = {M.~Sato and R.~Pollack}, title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, - note = {To appear in {\it J.~of Symbolic Computation}} + journal = {J.~of Symbolic Computation}, + volume = 45, + pages = {598--616}, + year = 2010 } @article{GabbayPitts02, diff -r 0865caafbfe6 -r 3890483c674f Paper/document/root.tex --- a/Paper/document/root.tex Mon Jan 03 16:21:12 2011 +0000 +++ b/Paper/document/root.tex Tue Jan 04 13:47:38 2011 +0000 @@ -101,8 +101,8 @@ \bibliography{root} \end{spacing} -\pagebreak -\input{Appendix} +%\pagebreak +%\input{Appendix} \end{document} diff -r 0865caafbfe6 -r 3890483c674f Paper/document/sigplanconf.cls --- a/Paper/document/sigplanconf.cls Mon Jan 03 16:21:12 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1251 +0,0 @@ -%----------------------------------------------------------------------------- -% -% LaTeX Class/Style File -% -% Name: sigplanconf.cls -% Purpose: A LaTeX 2e class file for SIGPLAN conference proceedings. -% This class file supercedes acm_proc_article-sp, -% sig-alternate, and sigplan-proc. -% -% Author: Paul C. Anagnostopoulos -% Windfall Software -% 978 371-2316 -% sigplan-style [atsign] acm.org -% -% Created: 12 September 2004 -% -% Revisions: See end of file. -% -%----------------------------------------------------------------------------- - - -\NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesClass{sigplanconf}[2010/05/24 v2.4 ACM SIGPLAN Proceedings] - -% The following few pages contain LaTeX programming extensions adapted -% from the ZzTeX macro package. - -% Token Hackery -% ----- ------- - - -\def \@expandaftertwice {\expandafter\expandafter\expandafter} -\def \@expandafterthrice {\expandafter\expandafter\expandafter\expandafter - \expandafter\expandafter\expandafter} - -% This macro discards the next token. - -\def \@discardtok #1{}% token - -% This macro removes the `pt' following a dimension. - -{\catcode `\p = 12 \catcode `\t = 12 - -\gdef \@remover #1pt{#1} - -} % \catcode - -% This macro extracts the contents of a macro and returns it as plain text. -% Usage: \expandafter\@defof \meaning\macro\@mark - -\def \@defof #1:->#2\@mark{#2} - -% Control Sequence Names -% ------- -------- ----- - - -\def \@name #1{% {\tokens} - \csname \expandafter\@discardtok \string#1\endcsname} - -\def \@withname #1#2{% {\command}{\tokens} - \expandafter#1\csname \expandafter\@discardtok \string#2\endcsname} - -% Flags (Booleans) -% ----- ---------- - -% The boolean literals \@true and \@false are appropriate for use with -% the \if command, which tests the codes of the next two characters. - -\def \@true {TT} -\def \@false {FL} - -\def \@setflag #1=#2{\edef #1{#2}}% \flag = boolean - -% IF and Predicates -% -- --- ---------- - -% A "predicate" is a macro that returns \@true or \@false as its value. -% Such values are suitable for use with the \if conditional. For example: -% -% \if \@oddp{\x} \else \fi - -% A predicate can be used with \@setflag as follows: -% -% \@setflag \flag = {} - -% Here are the predicates for TeX's repertoire of conditional -% commands. These might be more appropriately interspersed with -% other definitions in this module, but what the heck. -% Some additional "obvious" predicates are defined. - -\def \@eqlp #1#2{\ifnum #1 = #2\@true \else \@false \fi} -\def \@neqlp #1#2{\ifnum #1 = #2\@false \else \@true \fi} -\def \@lssp #1#2{\ifnum #1 < #2\@true \else \@false \fi} -\def \@gtrp #1#2{\ifnum #1 > #2\@true \else \@false \fi} -\def \@zerop #1{\ifnum #1 = 0\@true \else \@false \fi} -\def \@onep #1{\ifnum #1 = 1\@true \else \@false \fi} -\def \@posp #1{\ifnum #1 > 0\@true \else \@false \fi} -\def \@negp #1{\ifnum #1 < 0\@true \else \@false \fi} -\def \@oddp #1{\ifodd #1\@true \else \@false \fi} -\def \@evenp #1{\ifodd #1\@false \else \@true \fi} -\def \@rangep #1#2#3{\if \@orp{\@lssp{#1}{#2}}{\@gtrp{#1}{#3}}\@false \else - \@true \fi} -\def \@tensp #1{\@rangep{#1}{10}{19}} - -\def \@dimeqlp #1#2{\ifdim #1 = #2\@true \else \@false \fi} -\def \@dimneqlp #1#2{\ifdim #1 = #2\@false \else \@true \fi} -\def \@dimlssp #1#2{\ifdim #1 < #2\@true \else \@false \fi} -\def \@dimgtrp #1#2{\ifdim #1 > #2\@true \else \@false \fi} -\def \@dimzerop #1{\ifdim #1 = 0pt\@true \else \@false \fi} -\def \@dimposp #1{\ifdim #1 > 0pt\@true \else \@false \fi} -\def \@dimnegp #1{\ifdim #1 < 0pt\@true \else \@false \fi} - -\def \@vmodep {\ifvmode \@true \else \@false \fi} -\def \@hmodep {\ifhmode \@true \else \@false \fi} -\def \@mathmodep {\ifmmode \@true \else \@false \fi} -\def \@textmodep {\ifmmode \@false \else \@true \fi} -\def \@innermodep {\ifinner \@true \else \@false \fi} - -\long\def \@codeeqlp #1#2{\if #1#2\@true \else \@false \fi} - -\long\def \@cateqlp #1#2{\ifcat #1#2\@true \else \@false \fi} - -\long\def \@tokeqlp #1#2{\ifx #1#2\@true \else \@false \fi} -\long\def \@xtokeqlp #1#2{\expandafter\ifx #1#2\@true \else \@false \fi} - -\long\def \@definedp #1{% - \expandafter\ifx \csname \expandafter\@discardtok \string#1\endcsname - \relax \@false \else \@true \fi} - -\long\def \@undefinedp #1{% - \expandafter\ifx \csname \expandafter\@discardtok \string#1\endcsname - \relax \@true \else \@false \fi} - -\def \@emptydefp #1{\ifx #1\@empty \@true \else \@false \fi}% {\name} - -\let \@emptylistp = \@emptydefp - -\long\def \@emptyargp #1{% {#n} - \@empargp #1\@empargq\@mark} -\long\def \@empargp #1#2\@mark{% - \ifx #1\@empargq \@true \else \@false \fi} -\def \@empargq {\@empargq} - -\def \@emptytoksp #1{% {\tokenreg} - \expandafter\@emptoksp \the#1\@mark} - -\long\def \@emptoksp #1\@mark{\@emptyargp{#1}} - -\def \@voidboxp #1{\ifvoid #1\@true \else \@false \fi} -\def \@hboxp #1{\ifhbox #1\@true \else \@false \fi} -\def \@vboxp #1{\ifvbox #1\@true \else \@false \fi} - -\def \@eofp #1{\ifeof #1\@true \else \@false \fi} - - -% Flags can also be used as predicates, as in: -% -% \if \flaga \else \fi - - -% Now here we have predicates for the common logical operators. - -\def \@notp #1{\if #1\@false \else \@true \fi} - -\def \@andp #1#2{\if #1% - \if #2\@true \else \@false \fi - \else - \@false - \fi} - -\def \@orp #1#2{\if #1% - \@true - \else - \if #2\@true \else \@false \fi - \fi} - -\def \@xorp #1#2{\if #1% - \if #2\@false \else \@true \fi - \else - \if #2\@true \else \@false \fi - \fi} - -% Arithmetic -% ---------- - -\def \@increment #1{\advance #1 by 1\relax}% {\count} - -\def \@decrement #1{\advance #1 by -1\relax}% {\count} - -% Options -% ------- - - -\@setflag \@authoryear = \@false -\@setflag \@blockstyle = \@false -\@setflag \@copyrightwanted = \@true -\@setflag \@explicitsize = \@false -\@setflag \@mathtime = \@false -\@setflag \@natbib = \@true -\@setflag \@ninepoint = \@true -\newcount{\@numheaddepth} \@numheaddepth = 3 -\@setflag \@onecolumn = \@false -\@setflag \@preprint = \@false -\@setflag \@reprint = \@false -\@setflag \@tenpoint = \@false -\@setflag \@times = \@false - -% Note that all the dangerous article class options are trapped. - -\DeclareOption{9pt}{\@setflag \@ninepoint = \@true - \@setflag \@explicitsize = \@true} - -\DeclareOption{10pt}{\PassOptionsToClass{10pt}{article}% - \@setflag \@ninepoint = \@false - \@setflag \@tenpoint = \@true - \@setflag \@explicitsize = \@true} - -\DeclareOption{11pt}{\PassOptionsToClass{11pt}{article}% - \@setflag \@ninepoint = \@false - \@setflag \@explicitsize = \@true} - -\DeclareOption{12pt}{\@unsupportedoption{12pt}} - -\DeclareOption{a4paper}{\@unsupportedoption{a4paper}} - -\DeclareOption{a5paper}{\@unsupportedoption{a5paper}} - -\DeclareOption{authoryear}{\@setflag \@authoryear = \@true} - -\DeclareOption{b5paper}{\@unsupportedoption{b5paper}} - -\DeclareOption{blockstyle}{\@setflag \@blockstyle = \@true} - -\DeclareOption{cm}{\@setflag \@times = \@false} - -\DeclareOption{computermodern}{\@setflag \@times = \@false} - -\DeclareOption{executivepaper}{\@unsupportedoption{executivepaper}} - -\DeclareOption{indentedstyle}{\@setflag \@blockstyle = \@false} - -\DeclareOption{landscape}{\@unsupportedoption{landscape}} - -\DeclareOption{legalpaper}{\@unsupportedoption{legalpaper}} - -\DeclareOption{letterpaper}{\@unsupportedoption{letterpaper}} - -\DeclareOption{mathtime}{\@setflag \@mathtime = \@true} - -\DeclareOption{natbib}{\@setflag \@natbib = \@true} - -\DeclareOption{nonatbib}{\@setflag \@natbib = \@false} - -\DeclareOption{nocopyrightspace}{\@setflag \@copyrightwanted = \@false} - -\DeclareOption{notitlepage}{\@unsupportedoption{notitlepage}} - -\DeclareOption{numberedpars}{\@numheaddepth = 4} - -\DeclareOption{numbers}{\@setflag \@authoryear = \@false} - -%%%\DeclareOption{onecolumn}{\@setflag \@onecolumn = \@true} - -\DeclareOption{preprint}{\@setflag \@preprint = \@true} - -\DeclareOption{reprint}{\@setflag \@reprint = \@true} - -\DeclareOption{times}{\@setflag \@times = \@true} - -\DeclareOption{titlepage}{\@unsupportedoption{titlepage}} - -\DeclareOption{twocolumn}{\@setflag \@onecolumn = \@false} - -\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} - -\ExecuteOptions{9pt,indentedstyle,times} -\@setflag \@explicitsize = \@false -\ProcessOptions - -\if \@onecolumn - \if \@notp{\@explicitsize}% - \@setflag \@ninepoint = \@false - \PassOptionsToClass{11pt}{article}% - \fi - \PassOptionsToClass{twoside,onecolumn}{article} -\else - \PassOptionsToClass{twoside,twocolumn}{article} -\fi -\LoadClass{article} - -\def \@unsupportedoption #1{% - \ClassError{proc}{The standard '#1' option is not supported.}} - -% This can be used with the 'reprint' option to get the final folios. - -\def \setpagenumber #1{% - \setcounter{page}{#1}} - -\AtEndDocument{\label{sigplanconf@finalpage}} - -% Utilities -% --------- - - -\newcommand{\setvspace}[2]{% - #1 = #2 - \advance #1 by -1\parskip} - -% Document Parameters -% -------- ---------- - - -% Page: - -\setlength{\hoffset}{-1in} -\setlength{\voffset}{-1in} - -\setlength{\topmargin}{1in} -\setlength{\headheight}{0pt} -\setlength{\headsep}{0pt} - -\if \@onecolumn - \setlength{\evensidemargin}{.75in} - \setlength{\oddsidemargin}{.75in} -\else - \setlength{\evensidemargin}{.75in} - \setlength{\oddsidemargin}{.75in} -\fi - -% Text area: - -\newdimen{\standardtextwidth} -\setlength{\standardtextwidth}{42pc} - -\if \@onecolumn - \setlength{\textwidth}{40.5pc} -\else - \setlength{\textwidth}{\standardtextwidth} -\fi - -\setlength{\topskip}{8pt} -\setlength{\columnsep}{2pc} -\setlength{\textheight}{54.5pc} - -% Running foot: - -\setlength{\footskip}{30pt} - -% Paragraphs: - -\if \@blockstyle - \setlength{\parskip}{5pt plus .1pt minus .5pt} - \setlength{\parindent}{0pt} -\else - \setlength{\parskip}{0pt} - \setlength{\parindent}{12pt} -\fi - -\setlength{\lineskip}{.5pt} -\setlength{\lineskiplimit}{\lineskip} - -\frenchspacing -\pretolerance = 400 -\tolerance = \pretolerance -\setlength{\emergencystretch}{5pt} -\clubpenalty = 10000 -\widowpenalty = 10000 -\setlength{\hfuzz}{.5pt} - -% Standard vertical spaces: - -\newskip{\standardvspace} -\setvspace{\standardvspace}{5pt plus 1pt minus .5pt} - -% Margin paragraphs: - -\setlength{\marginparwidth}{36pt} -\setlength{\marginparsep}{2pt} -\setlength{\marginparpush}{8pt} - - -\setlength{\skip\footins}{8pt plus 3pt minus 1pt} -\setlength{\footnotesep}{9pt} - -\renewcommand{\footnoterule}{% - \hrule width .5\columnwidth height .33pt depth 0pt} - -\renewcommand{\@makefntext}[1]{% - \noindent \@makefnmark \hspace{1pt}#1} - -% Floats: - -\setcounter{topnumber}{4} -\setcounter{bottomnumber}{1} -\setcounter{totalnumber}{4} - -\renewcommand{\fps@figure}{tp} -\renewcommand{\fps@table}{tp} -\renewcommand{\topfraction}{0.90} -\renewcommand{\bottomfraction}{0.30} -\renewcommand{\textfraction}{0.10} -\renewcommand{\floatpagefraction}{0.75} - -\setcounter{dbltopnumber}{4} - -\renewcommand{\dbltopfraction}{\topfraction} -\renewcommand{\dblfloatpagefraction}{\floatpagefraction} - -\setlength{\floatsep}{18pt plus 4pt minus 2pt} -\setlength{\textfloatsep}{18pt plus 4pt minus 3pt} -\setlength{\intextsep}{10pt plus 4pt minus 3pt} - -\setlength{\dblfloatsep}{18pt plus 4pt minus 2pt} -\setlength{\dbltextfloatsep}{20pt plus 4pt minus 3pt} - -% Miscellaneous: - -\errorcontextlines = 5 - -% Fonts -% ----- - - -\if \@times - \renewcommand{\rmdefault}{ptm}% - \if \@mathtime - \usepackage[mtbold,noTS1]{mathtime}% - \else -%%% \usepackage{mathptm}% - \fi -\else - \relax -\fi - -\if \@ninepoint - -\renewcommand{\normalsize}{% - \@setfontsize{\normalsize}{9pt}{10pt}% - \setlength{\abovedisplayskip}{5pt plus 1pt minus .5pt}% - \setlength{\belowdisplayskip}{\abovedisplayskip}% - \setlength{\abovedisplayshortskip}{3pt plus 1pt minus 2pt}% - \setlength{\belowdisplayshortskip}{\abovedisplayshortskip}} - -\renewcommand{\tiny}{\@setfontsize{\tiny}{5pt}{6pt}} - -\renewcommand{\scriptsize}{\@setfontsize{\scriptsize}{7pt}{8pt}} - -\renewcommand{\small}{% - \@setfontsize{\small}{8pt}{9pt}% - \setlength{\abovedisplayskip}{4pt plus 1pt minus 1pt}% - \setlength{\belowdisplayskip}{\abovedisplayskip}% - \setlength{\abovedisplayshortskip}{2pt plus 1pt}% - \setlength{\belowdisplayshortskip}{\abovedisplayshortskip}} - -\renewcommand{\footnotesize}{% - \@setfontsize{\footnotesize}{8pt}{9pt}% - \setlength{\abovedisplayskip}{4pt plus 1pt minus .5pt}% - \setlength{\belowdisplayskip}{\abovedisplayskip}% - \setlength{\abovedisplayshortskip}{2pt plus 1pt}% - \setlength{\belowdisplayshortskip}{\abovedisplayshortskip}} - -\renewcommand{\large}{\@setfontsize{\large}{11pt}{13pt}} - -\renewcommand{\Large}{\@setfontsize{\Large}{14pt}{18pt}} - -\renewcommand{\LARGE}{\@setfontsize{\LARGE}{18pt}{20pt}} - -\renewcommand{\huge}{\@setfontsize{\huge}{20pt}{25pt}} - -\renewcommand{\Huge}{\@setfontsize{\Huge}{25pt}{30pt}} - -\else\if \@tenpoint - -\relax - -\else - -\relax - -\fi\fi - -% Abstract -% -------- - - -\renewenvironment{abstract}{% - \section*{Abstract}% - \normalsize}{% - } - -% Bibliography -% ------------ - - -\renewenvironment{thebibliography}[1] - {\section*{\refname - \@mkboth{\MakeUppercase\refname}{\MakeUppercase\refname}}% - \list{\@biblabel{\@arabic\c@enumiv}}% - {\settowidth\labelwidth{\@biblabel{#1}}% - \leftmargin\labelwidth - \advance\leftmargin\labelsep - \@openbib@code - \usecounter{enumiv}% - \let\p@enumiv\@empty - \renewcommand\theenumiv{\@arabic\c@enumiv}}% - \bibfont - \clubpenalty4000 - \@clubpenalty \clubpenalty - \widowpenalty4000% - \sfcode`\.\@m} - {\def\@noitemerr - {\@latex@warning{Empty `thebibliography' environment}}% - \endlist} - -\if \@natbib - -\if \@authoryear - \typeout{Using natbib package with 'authoryear' citation style.} - \usepackage[authoryear,sort,square]{natbib} - \bibpunct{[}{]}{;}{a}{}{,} % Change citation separator to semicolon, - % eliminate comma between author and year. - \let \cite = \citep -\else - \typeout{Using natbib package with 'numbers' citation style.} - \usepackage[numbers,sort&compress,square]{natbib} -\fi -\setlength{\bibsep}{3pt plus .5pt minus .25pt} - -\fi - -\def \bibfont {\small} - -% Categories -% ---------- - - -\@setflag \@firstcategory = \@true - -\newcommand{\category}[3]{% - \if \@firstcategory - \paragraph*{Categories and Subject Descriptors}% - \@setflag \@firstcategory = \@false - \else - \unskip ;\hspace{.75em}% - \fi - \@ifnextchar [{\@category{#1}{#2}{#3}}{\@category{#1}{#2}{#3}[]}} - -\def \@category #1#2#3[#4]{% - {\let \and = \relax - #1 [\textit{#2}]% - \if \@emptyargp{#4}% - \if \@notp{\@emptyargp{#3}}: #3\fi - \else - :\space - \if \@notp{\@emptyargp{#3}}#3---\fi - \textrm{#4}% - \fi}} - -% Copyright Notice -% --------- ------ - - -\def \ftype@copyrightbox {8} -\def \@toappear {} -\def \@permission {} -\def \@reprintprice {} - -\def \@copyrightspace {% - \@float{copyrightbox}[b]% - \vbox to 1in{% - \vfill - \parbox[b]{20pc}{% - \scriptsize - \if \@preprint - [Copyright notice will appear here - once 'preprint' option is removed.]\par - \else - \@toappear - \fi - \if \@reprint - \noindent Reprinted from \@conferencename, - \@proceedings, - \@conferenceinfo, - pp.~\number\thepage--\pageref{sigplanconf@finalpage}.\par - \fi}}% - \end@float} - -\long\def \toappear #1{% - \def \@toappear {#1}} - -\toappear{% - \noindent \@permission \par - \vspace{2pt} - \noindent \textsl{\@conferencename}\quad \@conferenceinfo \par - \noindent Copyright \copyright\ \@copyrightyear\ ACM \@copyrightdata - \dots \@reprintprice\par} - -\newcommand{\permission}[1]{% - \gdef \@permission {#1}} - -\permission{% - Permission to make digital or hard copies of all or - part of this work for personal or classroom use is granted without - fee provided that copies are not made or distributed for profit or - commercial advantage and that copies bear this notice and the full - citation on the first page. To copy otherwise, to republish, to - post on servers or to redistribute to lists, requires prior specific - permission and/or a fee.} - -% Here we have some alternate permission statements and copyright lines: - -\newcommand{\ACMCanadapermission}{% - \permission{% - Copyright \@copyrightyear\ Association for Computing Machinery. - ACM acknowledges that - this contribution was authored or co-authored by an affiliate of the - National Research Council of Canada (NRC). - As such, the Crown in Right of - Canada retains an equal interest in the copyright, however granting - nonexclusive, royalty-free right to publish or reproduce this article, - or to allow others to do so, provided that clear attribution - is also given to the authors and the NRC.}} - -\newcommand{\ACMUSpermission}{% - \permission{% - Copyright \@copyrightyear\ Association for - Computing Machinery. ACM acknowledges that - this contribution was authored or co-authored - by a contractor or affiliate - of the U.S. Government. As such, the Government retains a nonexclusive, - royalty-free right to publish or reproduce this article, - or to allow others to do so, for Government purposes only.}} - -\newcommand{\authorpermission}{% - \permission{% - Copyright is held by the author/owner(s).} - \toappear{% - \noindent \@permission \par - \vspace{2pt} - \noindent \textsl{\@conferencename}\quad \@conferenceinfo \par - ACM \@copyrightdata.}} - -\newcommand{\Sunpermission}{% - \permission{% - Copyright is held by Sun Microsystems, Inc.}% - \toappear{% - \noindent \@permission \par - \vspace{2pt} - \noindent \textsl{\@conferencename}\quad \@conferenceinfo \par - ACM \@copyrightdata.}} - -\newcommand{\USpublicpermission}{% - \permission{% - This paper is authored by an employee(s) of the United States - Government and is in the public domain.}% - \toappear{% - \noindent \@permission \par - \vspace{2pt} - \noindent \textsl{\@conferencename}\quad \@conferenceinfo \par - ACM \@copyrightdata.}} - -\newcommand{\reprintprice}[1]{% - \gdef \@reprintprice {#1}} - -\reprintprice{\$10.00} - -% Enunciations -% ------------ - - -\def \@begintheorem #1#2{% {name}{number} - \trivlist - \item[\hskip \labelsep \textsc{#1 #2.}]% - \itshape\selectfont - \ignorespaces} - -\def \@opargbegintheorem #1#2#3{% {name}{number}{title} - \trivlist - \item[% - \hskip\labelsep \textsc{#1\ #2}% - \if \@notp{\@emptyargp{#3}}\nut (#3).\fi]% - \itshape\selectfont - \ignorespaces} - -% Figures -% ------- - - -\@setflag \@caprule = \@true - -\long\def \@makecaption #1#2{% - \addvspace{4pt} - \if \@caprule - \hrule width \hsize height .33pt - \vspace{4pt} - \fi - \setbox \@tempboxa = \hbox{\@setfigurenumber{#1.}\nut #2}% - \if \@dimgtrp{\wd\@tempboxa}{\hsize}% - \noindent \@setfigurenumber{#1.}\nut #2\par - \else - \centerline{\box\@tempboxa}% - \fi} - -\newcommand{\nocaptionrule}{% - \@setflag \@caprule = \@false} - -\def \@setfigurenumber #1{% - {\rmfamily \bfseries \selectfont #1}} - -% Hierarchy -% --------- - - -\setcounter{secnumdepth}{\@numheaddepth} - -\newskip{\@sectionaboveskip} -\setvspace{\@sectionaboveskip}{10pt plus 3pt minus 2pt} - -\newskip{\@sectionbelowskip} -\if \@blockstyle - \setlength{\@sectionbelowskip}{0.1pt}% -\else - \setlength{\@sectionbelowskip}{4pt}% -\fi - -\renewcommand{\section}{% - \@startsection - {section}% - {1}% - {0pt}% - {-\@sectionaboveskip}% - {\@sectionbelowskip}% - {\large \bfseries \raggedright}} - -\newskip{\@subsectionaboveskip} -\setvspace{\@subsectionaboveskip}{8pt plus 2pt minus 2pt} - -\newskip{\@subsectionbelowskip} -\if \@blockstyle - \setlength{\@subsectionbelowskip}{0.1pt}% -\else - \setlength{\@subsectionbelowskip}{4pt}% -\fi - -\renewcommand{\subsection}{% - \@startsection% - {subsection}% - {2}% - {0pt}% - {-\@subsectionaboveskip}% - {\@subsectionbelowskip}% - {\normalsize \bfseries \raggedright}} - -\renewcommand{\subsubsection}{% - \@startsection% - {subsubsection}% - {3}% - {0pt}% - {-\@subsectionaboveskip} - {\@subsectionbelowskip}% - {\normalsize \bfseries \raggedright}} - -\newskip{\@paragraphaboveskip} -\setvspace{\@paragraphaboveskip}{6pt plus 2pt minus 2pt} - -\renewcommand{\paragraph}{% - \@startsection% - {paragraph}% - {4}% - {0pt}% - {\@paragraphaboveskip} - {-1em}% - {\normalsize \bfseries \if \@times \itshape \fi}} - -\renewcommand{\subparagraph}{% - \@startsection% - {subparagraph}% - {4}% - {0pt}% - {\@paragraphaboveskip} - {-1em}% - {\normalsize \itshape}} - -% Standard headings: - -\newcommand{\acks}{\section*{Acknowledgments}} - -\newcommand{\keywords}{\paragraph*{Keywords}} - -\newcommand{\terms}{\paragraph*{General Terms}} - -% Identification -% -------------- - - -\def \@conferencename {} -\def \@conferenceinfo {} -\def \@copyrightyear {} -\def \@copyrightdata {[to be supplied]} -\def \@proceedings {[Unknown Proceedings]} - - -\newcommand{\conferenceinfo}[2]{% - \gdef \@conferencename {#1}% - \gdef \@conferenceinfo {#2}} - -\newcommand{\copyrightyear}[1]{% - \gdef \@copyrightyear {#1}} - -\let \CopyrightYear = \copyrightyear - -\newcommand{\copyrightdata}[1]{% - \gdef \@copyrightdata {#1}} - -\let \crdata = \copyrightdata - -\newcommand{\proceedings}[1]{% - \gdef \@proceedings {#1}} - -% Lists -% ----- - - -\setlength{\leftmargini}{13pt} -\setlength\leftmarginii{13pt} -\setlength\leftmarginiii{13pt} -\setlength\leftmarginiv{13pt} -\setlength{\labelsep}{3.5pt} - -\setlength{\topsep}{\standardvspace} -\if \@blockstyle - \setlength{\itemsep}{1pt} - \setlength{\parsep}{3pt} -\else - \setlength{\itemsep}{1pt} - \setlength{\parsep}{3pt} -\fi - -\renewcommand{\labelitemi}{{\small \centeroncapheight{\textbullet}}} -\renewcommand{\labelitemii}{\centeroncapheight{\rule{2.5pt}{2.5pt}}} -\renewcommand{\labelitemiii}{$-$} -\renewcommand{\labelitemiv}{{\Large \textperiodcentered}} - -\renewcommand{\@listi}{% - \leftmargin = \leftmargini - \listparindent = 0pt} -%%% \itemsep = 1pt -%%% \parsep = 3pt} -%%% \listparindent = \parindent} - -\let \@listI = \@listi - -\renewcommand{\@listii}{% - \leftmargin = \leftmarginii - \topsep = 1pt - \labelwidth = \leftmarginii - \advance \labelwidth by -\labelsep - \listparindent = \parindent} - -\renewcommand{\@listiii}{% - \leftmargin = \leftmarginiii - \labelwidth = \leftmarginiii - \advance \labelwidth by -\labelsep - \listparindent = \parindent} - -\renewcommand{\@listiv}{% - \leftmargin = \leftmarginiv - \labelwidth = \leftmarginiv - \advance \labelwidth by -\labelsep - \listparindent = \parindent} - -% Mathematics -% ----------- - - -\def \theequation {\arabic{equation}} - -% Miscellaneous -% ------------- - - -\newcommand{\balancecolumns}{% - \vfill\eject - \global\@colht = \textheight - \global\ht\@cclv = \textheight} - -\newcommand{\nut}{\hspace{.5em}} - -\newcommand{\softraggedright}{% - \let \\ = \@centercr - \leftskip = 0pt - \rightskip = 0pt plus 10pt} - -% Program Code -% ------- ---- - - -\newcommand{\mono}[1]{% - {\@tempdima = \fontdimen2\font - \texttt{\spaceskip = 1.1\@tempdima #1}}} - -% Running Heads and Feet -% ------- ----- --- ---- - - -\def \@preprintfooter {} - -\newcommand{\preprintfooter}[1]{% - \gdef \@preprintfooter {#1}} - -\if \@preprint - -\def \ps@plain {% - \let \@mkboth = \@gobbletwo - \let \@evenhead = \@empty - \def \@evenfoot {\scriptsize \textit{\@preprintfooter}\hfil \thepage \hfil - \textit{\@formatyear}}% - \let \@oddhead = \@empty - \let \@oddfoot = \@evenfoot} - -\else\if \@reprint - -\def \ps@plain {% - \let \@mkboth = \@gobbletwo - \let \@evenhead = \@empty - \def \@evenfoot {\scriptsize \hfil \thepage \hfil}% - \let \@oddhead = \@empty - \let \@oddfoot = \@evenfoot} - -\else - -\let \ps@plain = \ps@empty -\let \ps@headings = \ps@empty -\let \ps@myheadings = \ps@empty - -\fi\fi - -\def \@formatyear {% - \number\year/\number\month/\number\day} - -% Special Characters -% ------- ---------- - - -\DeclareRobustCommand{\euro}{% - \protect{\rlap{=}}{\sf \kern .1em C}} - -% Title Page -% ----- ---- - - -\@setflag \@addauthorsdone = \@false - -\def \@titletext {\@latex@error{No title was provided}{}} -\def \@subtitletext {} - -\newcount{\@authorcount} - -\newcount{\@titlenotecount} -\newtoks{\@titlenotetext} - -\def \@titlebanner {} - -\renewcommand{\title}[1]{% - \gdef \@titletext {#1}} - -\newcommand{\subtitle}[1]{% - \gdef \@subtitletext {#1}} - -\newcommand{\authorinfo}[3]{% {names}{affiliation}{email/URL} - \global\@increment \@authorcount - \@withname\gdef {\@authorname\romannumeral\@authorcount}{#1}% - \@withname\gdef {\@authoraffil\romannumeral\@authorcount}{#2}% - \@withname\gdef {\@authoremail\romannumeral\@authorcount}{#3}} - -\renewcommand{\author}[1]{% - \@latex@error{The \string\author\space command is obsolete; - use \string\authorinfo}{}} - -\newcommand{\titlebanner}[1]{% - \gdef \@titlebanner {#1}} - -\renewcommand{\maketitle}{% - \pagestyle{plain}% - \if \@onecolumn - {\hsize = \standardtextwidth - \@maketitle}% - \else - \twocolumn[\@maketitle]% - \fi - \@placetitlenotes - \if \@copyrightwanted \@copyrightspace \fi} - -\def \@maketitle {% - \begin{center} - \@settitlebanner - \let \thanks = \titlenote - {\leftskip = 0pt plus 0.25\linewidth - \rightskip = 0pt plus 0.25 \linewidth - \parfillskip = 0pt - \spaceskip = .7em - \noindent \LARGE \bfseries \@titletext \par} - \vskip 6pt - \noindent \Large \@subtitletext \par - \vskip 12pt - \ifcase \@authorcount - \@latex@error{No authors were specified for this paper}{}\or - \@titleauthors{i}{}{}\or - \@titleauthors{i}{ii}{}\or - \@titleauthors{i}{ii}{iii}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{}{}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}% - \@titleauthors{vii}{}{}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}% - \@titleauthors{vii}{viii}{}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}% - \@titleauthors{vii}{viii}{ix}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}% - \@titleauthors{vii}{viii}{ix}\@titleauthors{x}{}{}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}% - \@titleauthors{vii}{viii}{ix}\@titleauthors{x}{xi}{}\or - \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}% - \@titleauthors{vii}{viii}{ix}\@titleauthors{x}{xi}{xii}% - \else - \@latex@error{Cannot handle more than 12 authors}{}% - \fi - \vspace{1.75pc} - \end{center}} - -\def \@settitlebanner {% - \if \@andp{\@preprint}{\@notp{\@emptydefp{\@titlebanner}}}% - \vbox to 0pt{% - \vskip -32pt - \noindent \textbf{\@titlebanner}\par - \vss}% - \nointerlineskip - \fi} - -\def \@titleauthors #1#2#3{% - \if \@andp{\@emptyargp{#2}}{\@emptyargp{#3}}% - \noindent \@setauthor{40pc}{#1}{\@false}\par - \else\if \@emptyargp{#3}% - \noindent \@setauthor{17pc}{#1}{\@false}\hspace{3pc}% - \@setauthor{17pc}{#2}{\@false}\par - \else - \noindent \@setauthor{12.5pc}{#1}{\@false}\hspace{2pc}% - \@setauthor{12.5pc}{#2}{\@false}\hspace{2pc}% - \@setauthor{12.5pc}{#3}{\@true}\par - \relax - \fi\fi - \vspace{20pt}} - -\def \@setauthor #1#2#3{% {width}{text}{unused} - \vtop{% - \def \and {% - \hspace{16pt}} - \hsize = #1 - \normalfont - \centering - \large \@name{\@authorname#2}\par - \vspace{5pt} - \normalsize \@name{\@authoraffil#2}\par - \vspace{2pt} - \textsf{\@name{\@authoremail#2}}\par}} - -\def \@maybetitlenote #1{% - \if \@andp{#1}{\@gtrp{\@authorcount}{3}}% - \titlenote{See page~\pageref{@addauthors} for additional authors.}% - \fi} - -\newtoks{\@fnmark} - -\newcommand{\titlenote}[1]{% - \global\@increment \@titlenotecount - \ifcase \@titlenotecount \relax \or - \@fnmark = {\ast}\or - \@fnmark = {\dagger}\or - \@fnmark = {\ddagger}\or - \@fnmark = {\S}\or - \@fnmark = {\P}\or - \@fnmark = {\ast\ast}% - \fi - \,$^{\the\@fnmark}$% - \edef \reserved@a {\noexpand\@appendtotext{% - \noexpand\@titlefootnote{\the\@fnmark}}}% - \reserved@a{#1}} - -\def \@appendtotext #1#2{% - \global\@titlenotetext = \expandafter{\the\@titlenotetext #1{#2}}} - -\newcount{\@authori} - -\iffalse -\def \additionalauthors {% - \if \@gtrp{\@authorcount}{3}% - \section{Additional Authors}% - \label{@addauthors}% - \noindent - \@authori = 4 - {\let \\ = ,% - \loop - \textbf{\@name{\@authorname\romannumeral\@authori}}, - \@name{\@authoraffil\romannumeral\@authori}, - email: \@name{\@authoremail\romannumeral\@authori}.% - \@increment \@authori - \if \@notp{\@gtrp{\@authori}{\@authorcount}} \repeat}% - \par - \fi - \global\@setflag \@addauthorsdone = \@true} -\fi - -\let \addauthorsection = \additionalauthors - -\def \@placetitlenotes { - \the\@titlenotetext} - -% Utilities -% --------- - - -\newcommand{\centeroncapheight}[1]{% - {\setbox\@tempboxa = \hbox{#1}% - \@measurecapheight{\@tempdima}% % Calculate ht(CAP) - ht(text) - \advance \@tempdima by -\ht\@tempboxa % ------------------ - \divide \@tempdima by 2 % 2 - \raise \@tempdima \box\@tempboxa}} - -\newbox{\@measbox} - -\def \@measurecapheight #1{% {\dimen} - \setbox\@measbox = \hbox{ABCDEFGHIJKLMNOPQRSTUVWXYZ}% - #1 = \ht\@measbox} - -\long\def \@titlefootnote #1#2{% - \insert\footins{% - \reset@font\footnotesize - \interlinepenalty\interfootnotelinepenalty - \splittopskip\footnotesep - \splitmaxdepth \dp\strutbox \floatingpenalty \@MM - \hsize\columnwidth \@parboxrestore -%%% \protected@edef\@currentlabel{% -%%% \csname p@footnote\endcsname\@thefnmark}% - \color@begingroup - \def \@makefnmark {$^{#1}$}% - \@makefntext{% - \rule\z@\footnotesep\ignorespaces#2\@finalstrut\strutbox}% - \color@endgroup}} - -% LaTeX Modifications -% ----- ------------- - -\def \@seccntformat #1{% - \@name{\the#1}% - \@expandaftertwice\@seccntformata \csname the#1\endcsname.\@mark - \quad} - -\def \@seccntformata #1.#2\@mark{% - \if \@emptyargp{#2}.\fi} - -% Revision History -% -------- ------- - - -% Date Person Ver. Change -% ---- ------ ---- ------ - -% 2004.09.12 PCA 0.1--5 Preliminary development. - -% 2004.11.18 PCA 0.5 Start beta testing. - -% 2004.11.19 PCA 0.6 Obsolete \author and replace with -% \authorinfo. -% Add 'nocopyrightspace' option. -% Compress article opener spacing. -% Add 'mathtime' option. -% Increase text height by 6 points. - -% 2004.11.28 PCA 0.7 Add 'cm/computermodern' options. -% Change default to Times text. - -% 2004.12.14 PCA 0.8 Remove use of mathptm.sty; it cannot -% coexist with latexsym or amssymb. - -% 2005.01.20 PCA 0.9 Rename class file to sigplanconf.cls. - -% 2005.03.05 PCA 0.91 Change default copyright data. - -% 2005.03.06 PCA 0.92 Add at-signs to some macro names. - -% 2005.03.07 PCA 0.93 The 'onecolumn' option defaults to '11pt', -% and it uses the full type width. - -% 2005.03.15 PCA 0.94 Add at-signs to more macro names. -% Allow margin paragraphs during review. - -% 2005.03.22 PCA 0.95 Implement \euro. -% Remove proof and newdef environments. - -% 2005.05.06 PCA 1.0 Eliminate 'onecolumn' option. -% Change footer to small italic and eliminate -% left portion if no \preprintfooter. -% Eliminate copyright notice if preprint. -% Clean up and shrink copyright box. - -% 2005.05.30 PCA 1.1 Add alternate permission statements. - -% 2005.06.29 PCA 1.1 Publish final first edition of guide. - -% 2005.07.14 PCA 1.2 Add \subparagraph. -% Use block paragraphs in lists, and adjust -% spacing between items and paragraphs. - -% 2006.06.22 PCA 1.3 Add 'reprint' option and associated -% commands. - -% 2006.08.24 PCA 1.4 Fix bug in \maketitle case command. - -% 2007.03.13 PCA 1.5 The title banner only displays with the -% 'preprint' option. - -% 2007.06.06 PCA 1.6 Use \bibfont in \thebibliography. -% Add 'natbib' option to load and configure -% the natbib package. - -% 2007.11.20 PCA 1.7 Balance line lengths in centered article -% title (thanks to Norman Ramsey). - -% 2009.01.26 PCA 1.8 Change natbib \bibpunct values. - -% 2009.03.24 PCA 1.9 Change natbib to use the 'numbers' option. -% Change templates to use 'natbib' option. - -% 2009.09.01 PCA 2.0 Add \reprintprice command (suggested by -% Stephen Chong). - -% 2009.09.08 PCA 2.1 Make 'natbib' the default; add 'nonatbib'. -% SB Add 'authoryear' and 'numbers' (default) to -% control citation style when using natbib. -% Add \bibpunct to change punctuation for -% 'authoryear' style. - -% 2009.09.21 PCA 2.2 Add \softraggedright to the thebibliography -% environment. Also add to template so it will -% happen with natbib. - -% 2009.09.30 PCA 2.3 Remove \softraggedright from thebibliography. -% Just include in the template. - -% 2010.05.24 PCA 2.4 Obfuscate author's email address.