final version of the ESOP paper; used set+ instead of res as requested by one reviewer
--- 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)) ==> (\<And>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)
--- 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}
--- 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)
--- 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 ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
- alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
abs_set2 ("_ \<approx>\<^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 "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. x \<rightarrow> y"}\hspace{10mm}
+ @{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
\end{equation}
%
@@ -138,7 +138,7 @@
\eqref{one} as $\alpha$-equivalent with
%
\begin{center}
- @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
+ @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}
\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 \<rightarrow> y)"} and
@{text "({y, x}, y \<rightarrow> 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 \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> 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 \<rightarrow> 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 \<noteq> 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 \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> 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 "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
+ new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}
representing $\alpha$-equivalence classes of pairs of type
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
(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\<AL>"}$_{i..n}$. The conclusion of the induction principle is
+ for the types @{text "ty\<AL>"}$_{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\<AL>"}$_{1..n}$.
%%in \eqref{weakinduct}.
Having these equivariant properties established, we can
show that the support of term-constructors @{text "C\<^sup>\<alpha>"} 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
--- 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'.
--- 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,
--- 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}
--- 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} <then-clause> \else <else-clause> \fi
-
-% A predicate can be used with \@setflag as follows:
-%
-% \@setflag \flag = {<predicate>}
-
-% 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 <then-clause> \else <else-clause> \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.