1\makeatletter
2
3\typeout{``page''}
4
5% cedric: removed for llncs
6
7%page layout
8%\oddsidemargin 0cm
9%\evensidemargin 0cm
10%\topmargin 10pt
11
12%\headheight 0pt
13%\headsep 0pt
14%\footheight 0pt
15%\footskip 24pt
16%\textheight 24cm
17%\textwidth 15.5cm
18%\footnotesep 1cm
19
20%\baselineskip = 24pt plus 4pt minus 3pt
21%\voffset=-0.5cm
22%\hoffset=0.5cm
23
24\makeatother
25
26\makeatletter
27
28% on  active  et  desactive  le  mode  frtypo  par \frtypotrue et frtypofalse
29% quelquesoit le mode les caract\`eres :  ; ?   !   sont actifs.
30% En  particulier  ces  caract\`eres  ne  peuvent  plus \^etre  mis  dans des
31% \'etiquettes.
32
33\def\halfspace{\kern .166em}
34
35\def\space@pv{\ifmmode ;\else \halfspace;\fi}
36\def\space@dc{\ifmmode :\else \halfspace:\fi}
37\def\space@pi{\ifmmode ?\else \halfspace?\fi}
38\def\space@pe{\ifmmode !\else \halfspace!\fi}
39
40\let\nospace@pv=;
41\let\nospace@dc=:
42\let\nospace@pi=?
43\let\nospace@pe=!
44
45\catcode`;=\active \catcode`:=\active \catcode`?=\active \catcode`!=\active
46
47\def \frtypo
48    {\let;=\space@pv\let:=\space@dc\let!=\space@pe\let?=\space@pi}
49\def \entypo
50    {\let;=\nospace@pv\let:=\nospace@dc\let!=\nospace@pe\let?=\nospace@pi}
51
52\frtypo
53
54\def\@sanitize
55 {\@makeother\ \@makeother\\\@makeother\$\@makeother\&%
56\@makeother\#\@makeother\^\@makeother\^^K\@makeother\_\@makeother\^^A%
57\@makeother\%\@makeother\~\@makeother\;\@makeother\?\@makeother%
58\:\@makeother\!}
59
60\let \oldspecials \dospecials
61\def \dospecials {\oldspecials \do\:\do\!\do \?\do\;}
62
63%\scrollmode
64
65\makeatletter
66%===========================================================================
67% Personals macros (They might have strange latex side effects
68%-----------------
69
70\def\noparindent{\everypar={\hskip -\parindent\everypar={}}}
71\def \para {\medskip\noparindent}
72\def \pari {\medskip\noparindent}
73\def \parii {\smallskip\noparindent}
74\let\paro=\noparindent
75
76
77%===========================================================================
78% Definitions Theorems
79%---------------------
80
81\newif \iffrench
82\if \csname french\endcsname \relax  \frenchfalse \else  \frenchtrue\fi
83
84\if \csname definition\endcsname\relax
85\newtheorem{definition}{D\iffrench \'e\else e\fi  finition}\fi
86\def\bdf{\begin{definition}\begin{em}}
87\def\edf{\ifvmode\vskip-\lastskip\nopagebreak\else
88         \penalty 100\fi\end{em}\end{definition}}
89
90\if \csname theorem\endcsname\relax
91\newtheorem{theorem}{\iffrench Th�or�me\else Theorem\fi}\fi
92\def\bthm{\begin{theorem}}
93\def\ethm{\end{theorem}}
94
95\newtheorem{algorithm}{Algorithm\if\french e\else\fi}
96\def\balgo{\begin{algorithm}}
97\def\ealgo{\end{algorithm}}
98
99\if \csname proposition\endcsname\relax
100\newtheorem{proposition}{Proposition}\fi
101\def\bprop{\begin{proposition}}
102\def\eprop{\end{proposition}}
103
104\if \csname lemma\endcsname\relax
105\newtheorem{lemma}[proposition]{Lemm\iffrench e\else a\fi}\fi
106\def\blem{\begin{lemma}}
107\def\elem{\end{lemma}}
108
109\if \csname corollary\endcsname\relax
110\newtheorem{corollary}[proposition]{Corollary}\fi
111\def\bcor{\begin{corollary}}
112\def\ecor{\end{corollary}}
113
114\def\brmk{\trivlist \item[\hskip \labelsep {\bf {Note}}]}
115\def\ermk{\endtrivlist}
116
117\newtheorem{Note}{Note}
118\def\bnote{\begin{note}\begin{em}}
119\def\enote{\end{em}\end{note}}
120
121\if \csname example\endcsname\relax
122%\newtheorem{example}[remark]{Ex\iffrench a\else e\fi mple}\fi
123\newtheorem{example}{Ex\iffrench a\else e\fi mple}\fi
124\def\bxple{\trivlist \item[\hskip \labelsep {\bf {Example}}]}
125%{\begin{example}\begin{em}}
126\def\exple{\endtrivlist}
127%{\end{em}\end{example}}
128
129\def\@begintheorem#1#2{\it \trivlist \item[\hskip \labelsep{\bf #1\ #2}]}
130\def\@opargbegintheorem#1#2#3{\it \trivlist
131      \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]}
132\def\@endtheorem{\endtrivlist}
133
134\newcount \indemo
135\def \makeno #1{\global \advance \indemo by 1\global
136      \expandafter \edef \csname demo/\the\cdemo/#1\endcsname{\the\indemo}}
137\def \refno #1{\if \relax\csname demo/\the\cdemo/#1\endcsname \relax
138  \write0 {Demo counter #1 undefined}??\else
139   \csname demo/\the\cdemo/#1\endcsname\fi}
140\def \labno #1{\makeno {#1}\refno {#1}}
141
142\newif \ifdemo \demotrue
143\newcount \cdemo
144\newenvironment{demo}{\bdemo}{\edemo}
145\def\bdemotrue{\trivlist \item[\hskip \labelsep
146  {\underline
147        {\iffrench Preuve\else Proof\fi}:}]\advance\cdemo by 1\indemo 0}
148\def\edemo{\penalty 100\hfill\rule{2mm}{2mm} \endtrivlist\@doendpe}
149\long \def \bdemofalse #1\edemo{\relax}
150\outer \def \bdemo
151  {\ifdemo \bdemotrue \else \expandafter \bdemofalse \fi\indent}
152
153\newif \ifhint \hintfalse
154\newtheorem{hint}{\rm \underline {Hint}}
155\def\bhintiftrue{\trivlist \item[\hskip \labelsep {\underline {Hint}:}]}
156\def\ehint{\penalty 100\hfill\noindent\rule{2mm}{2mm}\endtrivlist}
157\long \def \bhintiffalse #1\ehint{\relax}
158\outer \def \bhint
159  {\ifhint \bhintiftrue \else \expandafter \bhintiffalse \fi}
160
161\newif \ifexpert \expertfalse
162\newtheorem{expert}{Remark}
163\def\bexpertiftrue{\trivlist \item[\hskip \labelsep {\underline {Hint}:}]}
164\def\eexpert{\penalty 100\hfill\noindent\rule{2mm}{2mm}\endtrivlist}
165\long \def \bexpertiffalse #1\eexpert{\relax}
166\outer \def \bexpert
167  {\ifexpert \bexpertiftrue \else  \expandafter \bexpertiffalse \fi}
168
169
170
171\def\notitle{\hskip\hsize minus\hsize\nobreak\hbox{}}
172
173\def\notation{\paragraph*{Notation}}
174\def\hypothesis{\paragraph*{Assumption}}
175
176
177\def \caseparagraph{\@startsection
178 {case}{6}{\z@}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}}
179\def \subcaseparagraph{\@startsection
180% {subcase}{7}{\parindent}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}}
181 {subcase}{7}{\z@}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}}
182
183
184\if \csname datefrench\endcsname\relax
185\def \langcase {Case}
186\def \langsubcase {Subcase}
187\else
188\def \langcase {Cas}
189\def \langsubcase {Sous-cas}
190\fi
191
192\def\case#1{\caseparagraph*{\langcase\space #1:}}
193\def\othercase#1{\caseparagraph*{#1:}}
194\def\mathcase#1{\caseparagraph*{\langcase\space $#1$:}}
195\def\subcase#1{\subcaseparagraph*{\langsubcase\space #1:}}
196
197% Send a warning when running latex
198\def\warning#1{\immediate\write0{Warning: #1}}
199
200\newenvironment{care}{\bwarning}{\ewarning}
201\def\bcare{\trivlist \item[\hskip \labelsep {\bf Warning!}]}
202\def\ecare{\endtrivlist}
203
204\def\subst#1#2{^{#1} \!/\! _{#2}}
205
206\def \comment #1{{\em #1}}
207%\def \comment #1{}
208\makeatother
209
210
211\makeatletter
212%%% To change size in math mode
213
214\let\Ts=\textstyle
215\let\Ds=\displaystyle
216\let\Ss=\scriptstyle
217
218%%% Abrevs
219
220\let \comp \circ
221\let \wild \_
222
223
224%%% To put text between two formulas on the same line
225
226\def\text#1{\qquad\hbox{#1}\qquad}
227
228%%%  Macros for mathematics
229
230%% Special symbols
231
232\def \nat {{\mathord{I\kern -.33em N}}}
233\def \natb {{\mathord{I\kern -.33em\overline{N}}}}
234
235\def\Vdash {\mathrel{\hbox{\vrule\kern .1ex$\vdash$}}}
236\def\VVdash {\mathrel{\hbox{\vrule\kern .2ex\vrule\kern .1ex $\vdash$}}}
237
238% An open box to end demonstrations with
239
240\def\Box{\hbox
241  {\vbox
242    {\hrule height .033em
243     \hbox to .5em
244       {\vrule width .033em
245        \hbox{\vbox to .5em{\vss}\hss}
246        \vrule width .033em}
247     \hrule height .033em
248    }}}
249
250
251%% Balanced symbols
252
253\def\absolute#1{\mathopen\mid#1\mathclose\mid}
254
255%% Operators
256
257\def \domain {\dv}
258%\def \domain {\dvmathop{\sl dom\,}}
259\def \image {\mathop{\sl im\,}}
260\def \modulo {\mathbin{\rm modulo}}
261\def \inverse{{}^{-1}}
262\def \cardinal {{\sl Card\,}}
263%\def \restrict #1{\mathbin{\mid}_{#1}}
264\def \restrict
265   {\mathbin{\hbox{$\mid$\kern-.24em\lower.09em\hbox{\rm\char'22}$\!$}}}
266\let \arity = \varrho
267
268
269%% Quantifiers
270
271\def \fall #1,{\forall #1,\;}
272\def \exist #1,{\exists #1,\;}
273\def \qt #1.{\forall\,#1.\,}
274\def \ex #1.{\exists\,#1.\,}
275
276%% Arrows
277
278\let\ar=\rightarrow
279\let\dar=\Rightarrow
280\def\imply{\Longrightarrow}
281
282
283\def \rewrite {\mathrel{-}\joinrel\leadsto}
284
285
286%% Equalities
287
288%\def \axiom {\mathrel {\mathop =^!}}
289\def \axiom {=}
290\def \eqdef {\mathrel {\mathop {=\joinrel=}\limits^{def}}}
291
292%% Sizes
293
294\def\({\left(}
295\def\){\right)}
296
297\def\Mid{\mathrel{\Big|}}
298
299%% Indices  see also indices.def
300
301\def \ind #1#2{_{#1\in[1,#2]}}
302
303%%
304
305%% names
306
307\let \th \vdash
308\let \tth \Vdash
309\let \ttth \VVdash
310\let \thh \models
311
312\def\Cal#1{{\cal #1}}
313
314\let \eset = \emptyset
315
316
317
318%% Aligned constructions in math mode
319
320% For internal use only
321
322\def\noskip{\lineskiplimit=\the\lineskiplimit
323                \lineskip=\the\lineskip}
324\def\moreskip{\lineskiplimit=0.4em\lineskip=0.4em plus 0.2em}
325\def\moremoreskip{\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
326
327\def\vatrix#1{\null\,\vcenter{\normalbaselines\moreskip\m@th
328    \let \and \cr
329    \ialign{$\displaystyle##$\hfil
330      &\quad$\displaystyle##$\hfil&\quad##\hfil\crcr
331      \mathstrut\crcr\noalign{\kern-\baselineskip}
332      #1\crcr\mathstrut\crcr\noalign{\kern-\baselineskip}}}\,}
333
334% A sequence of expressions is writen on separate lines to form one expression
335
336\def \band #1{\left\{\vatrix{#1}\right.}          % brace and
337\def \wand #1{\wedge\band{#1}}                    % wedge  and
338\def \vand #1{\vee\band{#1}}                      % vee  and
339\def \vor  #1{\vee\left[\vatrix{#1}\right.}       % vee and or
340\def \Wand #1{\bigwedge\band{#1}}                 % big wedge and
341\def \Vand #1{\bigvee\band{#1}}                   % big vee and
342\def \Wor  #1{\bigvee\left[\vatrix{#1}\right.}    % big vee and
343
344
345
346% A general usage tabulation in math mode.
347%     Indentation is alternatively left and right, so that good place for
348%     tabs will produce many different
349
350% \dalign { & blabla :& blabla    \cr
351%           &    bla :& blablabla \cr
352%         }
353
354% \dalign {  blabla :&& blabla    \cr
355%            bla :   && blablabla \cr
356%         }
357
358% \dalign { & blabla :&    blabla \cr
359%           &    bla :& blablabla \cr
360%         }
361
362% Internal and personal use
363\def\Dalign#1#2{\vcenter
364 \bgroup
365   \let\>=\qquad
366   \def\title##1{\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}}
367%   \halign{$##$\hfil\qquad&&\hfil$##{}$&${}##$\hfil\qquad\cr#2\crcr}
368%   \halign{$##$\hfil&&\qquad\hfil$##{}$&${}##$\hfil\cr#2\crcr}
369   \halign{&${}##$\hfil&\hfil$##{}$\cr#2\crcr}
370 \egroup}
371% End internal use
372
373\def\align#1{\vcenter
374 \bgroup
375   \let\>=\qquad
376   \halign{#1\crcr}
377 \egroup}
378
379%\def\aligndef#1#2{\expandafter\def\csname aligndef#1\endcsname{#2}}
380%\aligndef ]{\argalign}
381%\aligndef l{&\hfil$##{}$}
382%\aligndef r{&${}##$\hfil}
383%\aligndef c{&\hfil$##$\hfil}
384%\aligndef -{\qquad}
385%\aligndef L{&\hfil##$}
386%\aligndef R{&##\hfil}
387%\aligndef C{&\hfil##\hfil}
388%\def\argalign#1{\relax}
389%\def\prealign#1{\csname aligndef#1\endcsname\prealign}
390%\def\doalign#1]{\dohalign{\prealign#1]}}
391%\def\dohalign#1#2{\expandafter\halign{#1\cr#2\crcr}}
392
393
394
395%\def\dalign#1{\ifx#1[\doalign\else\Dalign3{#1}\fi}
396\def\dalign{\Dalign3}
397
398
399\def\Strut{\raise .4em\hbox{\strut}\raise -.4em\hbox{\strut}}
400
401\def \deftitle #1
402   {\def \title ##1
403      {\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}}}
404
405
406
407\bgroup
408 \catcode `\^^M \active
409 \gdef \obeycr {\catcode `\^^M\active \let ^^M\crcr}
410\egroup
411
412
413\ifx \csname linewidth\endcsname \hsize
414 \let  \realwidth \hsize
415\else
416 \let \realwidth \linewidth
417\fi
418
419\def \oris {\crcr \mid&}
420\def \syntaxtable #1
421  {\def\is {::=&}
422   \def \\{\cr\noalign{\medskip}}\def\cont{\cr&}\vbox
423   \bgroup
424   \tabskip=100pt plus 1000pt minus 1000pt
425   \halign to \realwidth
426       {\hfil$##{}$\tabskip=0pt&
427        ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt&
428        &##\hfil \cr#1\crcr}
429   \egroup}
430
431
432\def \assertions #1
433  {\deftitle2 \vbox
434   \bgroup
435     \halign {\hfil$##{}$&$##$\hfil&&\quad##\hfil\cr#1\crcr}
436   \egroup}
437
438
439%%% old version
440
441\def\malign#1{\vcenter\bgroup
442   \deftitle #1
443   \def \lign ##1\cr {\noalign {##1}}
444   \def \textlign##1{\noalign {\medskip \vbox {\noindent ##1}\medskip}}
445   \tabskip=100pt plus 1000pt minus 1000pt
446   \halign to \realwidth
447       {\hfil$##{}$\tabskip=0pt&
448        ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt&
449        &##\hfil&$##$\hfil&  \cr#1\crcr\egroup}}
450
451\newif \ifhsize \hsizefalse
452
453\newskip \nullskip \nullskip 0pt
454\newskip \fullskip \fullskip 100pt plus 1000pt minus 1000pt
455\def \maligntrue {\tabskip \fullskip
456                   \halign to \realwidth \bgroup}
457\def \malignfalse {\halign \bgroup}
458\def \malign {\vcenter \bgroup \ifhsize \expandafter \maligntrue \else \expandafter \malignfalse \fi}
459\def \endmalign {\crcr \egroup \egroup}
460
461\def \makeword #1#2#3{\expandafter
462   \def \noexpand#3{#2 {#1\expandafter \let \expandafter \dummy\string #3}}}
463
464\let \vect \overrightarrow
465
466\def \uad {\hskip 0.5em}
467
468
469\newskip \mathandskip
470\newskip\mathmargin \mathmargin  0em
471
472\mathandskip 2em plus 0.5fil minus 0.5em
473\def \mathand {\hskip \mathandskip}
474\def \mathleftright {\hfill{}\hskip 0em plus -2fill\penalty 50{}\hfill}
475\def \mathandcr {\penalty 50\mathand}
476\def \mathcr {\penalty -10000\mathand}
477\def \mathcrleft {\hfill{}\hskip 0em plus -2fill\penalty -10000{}\hskip
478     \mathmargin}
479\def \mathbreak {\penalty 50}
480
481\def \incrmargin #1{\advance\mathmargin by #1em\advance\mathmargin by #1em}
482\def \mathslash#1{\let \do \mathcrleft
483   \ifx #1[\let\do\mathdoskip\fi\do#1}
484\def \mathdoskip#1#2]{\incrmargin {#2}\mathcrleft}
485
486% Type inference rules
487
488\let \mathmoreskip=\moremoreskip
489\def \nomoreskip {\let \mathmoreskip \relax}
490
491\def \bmaths {\let \and \mathandcr  \hsize \realwidth
492    \centering \vbox \bgroup \mathmoreskip  \noindent
493    $\displaystyle \let \\ \mathslash}
494\def \emaths {\unskip$\egroup}
495\def \mathflushleft {\def \emaths {\hfill$\egroup}\nomoreskip}
496\newenvironment {maths}{\bmaths}{\emaths}
497
498\def \maths #1{\bmaths #1\emaths}
499
500\def \whereis {\leftarrow}
501\def \where #1{[{\let \is \whereis #1}]}
502\def \dowhere #1\is#2\is{[\ifx#2\empty #1\else #2/#1\fi]}
503\def \where #1{\let \is \relax\dowhere #1\is\empty\is}
504
505\let \closeplus\relax
506\let \Empty \relax
507\let \is \relax
508\def \plus #1{\PLUS #1\is\is\END}
509\def \PLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1\plustoken#2)\else #1\fi}
510\let \plustoken \mapsto
511
512\let \diverge \uparrow
513
514\def \set #1{\{#1\}}
515\def \sem #1{\lbrack\!\lbrack#1\rbrack\!\rbrack}
516
517
518\def\mathrm #1{\mathrel {\rm #1}}
519\let \coerce \leq
520\makeatother
521
522\makeatletter
523
524
525%% see infer.doc for a documentation
526
527% Judgements
528
529\let\th=\vdash
530
531% naming
532
533\expandafter \ifx \csname name\endcsname\relax
534   \def\name#1{\hbox{\sc #1}}\else \relax \fi
535
536\def \labname #1{{\rm(\name{#1})}}
537\let \lab = \labname
538\def \clab #1{\hbox {$\smash {\lab{#1}}$}}
539\newskip \beforelabskip \beforelabskip = 0.5em
540\def \eqlab {\eqno \lab}
541
542%% inside rules
543
544\def \nmir #1[#2]{\crcr \hrulefill \cr}
545\def \rmir #1[#2]{\crcr \hrulefill & \clab {#2} \cr}
546\def \lmir #1[#2]{\relax}
547\def \Lmir #1[#2]{\crcr \Llabo {#2}\hrulefill \cr}
548\def \Rmir #1[#2]{\crcr \hrulefill \Rlabo {#2}\cr}
549\def \imir {\crcr \hrulefill\cr}
550
551% outside rules
552
553\def \rlabo #1{\hskip \beforelabskip \clab {#1}}
554\def \llabo #1{\clab {#1}\hskip \beforelabskip}
555\def \Rlabo #1{\rlap {\rlabo {#1}}}
556\def \Llabo #1{\llap {\llabo {#1}}}
557\let \labr \rlabo \let \labl \llabo \let \labR \Rlabo \let \labL \Llabo
558
559
560\def \rlab #1 {\rlap {\lab {#1}}}
561\def \llab #1 {\llap {\lab {#1}}}
562
563
564% A good separator for multiple hypothesis
565
566\let \and \qquad
567\let \andcr \cr
568
569
570% Single rules
571
572\def \lessskip  {\lineskiplimit=.3em\lineskip= .2em plus .1em}
573
574\makeatletter
575\def \mathrulename {\scriptsize \labname}
576\def \ignoredash #1{\let\next\ignoredash
577         \ifx #1-\relax\else\let\next#1\fi\next}
578\def \mathrule {\@ifnextchar [{\mathrulelab}{\@mathrule}}
579\def \mathrulelab[#1]#2{\hbox
580   {\vbox {\hbox {\mathrulename {#1}}\nointerlineskip\smallskip
581           \hbox {$\@mathrule{#2}$}}}}
582\def \@mathrule #1{{\let \and \qquad \let \rlab \rl \let \llab \ll
583     \def \mir {MiR}\def\endrule {EnDrUlE}
584     \displaystyle \offinterlineskip \lessskip  \bgroup \openrule
585     \beginrule #1\mir \mir \endrule}}
586\def \beginrule #1\mir#2{#1\ifx #2\mir \let \next \finishrule
587     \else \def \next {\middlerule\openrule \beginrule\ignoredash#2}\fi\next}
588\def\finishrule#1\endrule{\closerule\egroup}
589
590\def \openrule {\hbox \bgroup \vbox \bgroup
591     \halign \bgroup \hfil $##$\hfil &\hskip \beforelabskip$##$\hfil \cr}
592\def \closerule {\crcr\egroup\egroup\egroup}
593%\def \endrule {\closerule \egroup}
594
595\def \singleRule {\crcr\noalign {\vskip -0.1em}\closerule \over}
596\let \middlerule \singleRule
597
598
599% Double and Tripple rules see infer-more.def
600
601% Logic and rewriterules
602
603\def \logicrule #1{\let \mir \Longrightarrow #1}
604
605
606\def \longleadsto {\mathrel{-}\joinrel\leadsto}
607
608\def \rewriterule #1{\displaystyle \offinterlineskip \lessskip
609     \bgroup\let \mir \longleadsto \openrule#1\endrule}
610
611\def \suspend #1{\vbox to #1 {\leaders \hbox {$\cdot$}\vfill}}
612
613
614\if \relax \csname keywordstyle\endcsname  \let \keywordstyle \tt \fi
615
616%\def \keyword #1{{\hbox {\keywordstyle #1}}}
617\def \keyword #1{{\keywordstyle #1}}
618\def \mathtoken #1{\ifmmode
619   \mathopen{}\keyword {#1}\mathclose{}\else \keyword{#1}\fi}
620\def \mathpostfix #1{\mathrel{\keyword {#1}}\mathclose{}}
621\def \mathprefix #1{\mathopen{}\mathrel{\keyword {#1}}}
622\def \mathinfix #1{\mathrel{\keyword {#1}}}
623
624\def\ignorefirst #1{}
625\def \lwt #1{\expandafter \lowercase \expandafter \bgroup
626  \expandafter \ignorefirst \string #1\egroup}
627
628
629\def \makeprefix #1#2{\expandafter\def \noexpand #1{\mathprefix  {#2}}}
630\def \makepostfix #1#2{\expandafter\def \noexpand #1{\mathpostfix  {#2}}}
631\def \maketoken #1#2{\expandafter\def \noexpand #1{\mathtoken {#2}}}
632\def \makeinfix #1#2{\expandafter\def \noexpand #1{\mathinfix {#2}}}
633
634\def \makein #1{\expandafter\def
635  \noexpand #1##1in{\keyword {\lwt #1}\,\,##1\,\,\keyword {in}\,\,}}
636
637\let \@ \;
638\def \Let #1=#2in{\keyword {let}\@ {#1 = #2} \@\keyword {in}\@}
639\def \fun (#1){\keyword {fun}\@ #1 \rightarrow}
640\def \type #1=#2in{\keyword {type}\@ #1 = #2 \@\keyword {in}\@}
641
642\makeatother
643
644\let \cont \kappa
645\let \t \tau
646\let \l \ell
647\let \s \sigma
648\let \tv \alpha
649\let \vect \bar
650
651\def \Gen {{\rm Gen}}
652
653\def \tplus #1{\TPLUS #1\is\is\END}
654\def \TPLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1:#2)\else #1\fi}
655
656%%%%%%%%%%%%%%% light programs
657
658\makeatletter
659\def \progstyle {\tt}
660\newskip \programindent \programindent 4em
661\def \program {\par \begingroup
662    \medskip \parindent \programindent \@tempswafalse
663    \frenchspacing \@vobeyspaces \let \par \programpar
664    \obeylines \progstyle
665    \catcode``=13 \@noligs \let \do \@makeother \dospecials
666    \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2
667    \prog@specials \prog@initspecials \obeyspaces}
668
669\def \programpar {\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
670
671\bgroup
672\gdef \less@specials {\relax
673 \catcode `| \active
674 \catcode `< \active
675 \catcode `> \active
676 \catcode `- \active
677 \catcode `\' \active
678}
679\gdef \more@specials {\relax
680 \catcode `( \active
681 \catcode `) \active
682}
683\gdef \prog@specials {\less@specials\more@specials}
684\prog@specials
685\gdef \prog@initspecials {\def
686    -{\minus@program}\def
687    '{\acurate@program}\def
688    |{\bar@program}\def
689    <{\less@program}\def
690    >{\greater@program}\def
691    ({\less@program}\def
692    ){\greater@program}}
693 \gdef \bar@@program {\let\do \eattoken
694  \ifx \token >$\droite$\else ${}\mid{}$\let \do \relax\fi \do}
695 \gdef \minus@@program {\let\do \eattoken
696  \ifx \token >$\ar$\else -\let \do \relax\fi \do}
697\egroup
698
699\def \acurate@program {\futurelet \token \acurate@@program}
700\def \acurate@@program {\let \do \eattoken
701  \ifx \token a$\alpha$\else
702   \ifx \token b$\beta$\else
703    \char `\' \let \do \relax\fi\fi \do}
704\def \less@program {\hbox{$<$}}
705\def \greater@program {\hbox{$>$}}
706\def \bar@program {\futurelet \token \bar@@program}
707\def \minus@program {\futurelet \token \minus@@program}
708
709
710\def \endprogram {\ifdim\lastskip >\z@ \@tempskipa\lastskip
711       \vskip -\lastskip\fi\medskip \endgroup
712     \@endpetrue}
713
714\def\prog {\begingroup \hbox \bgroup
715  \catcode ``=13 \@noligs
716  \let \do \@makeother \dospecials \progstyle
717   \prog@specials \prog@initspecials
718    \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2
719  \@prog}
720\def\@prog#1{\obeyspaces \frenchspacing \catcode `\  10
721            \def\@tempa ##1#1{##1\egroup\endgroup}\@tempa}
722\makeatother
723
724%%%%%%%%%%%%%%%%%%%  "quotations"
725
726\makeatletter
727% on  active  le cararectere " et on s'en sert pour le mode \prog
728% s'il est d�fini ou \verb autrement
729
730\bgroup
731\@makeother \"
732\gdef \progquote {\prog"}
733\catcode `\" \active
734\gdef "{\progquote}
735\egroup
736
737\def \quoteon {
738\let \quote@sanitize \@sanitize
739\def \@sanitize {\quote@sanitize \@makeother\"}
740\let \quote@specials \dospecials
741\def \dospecials {\quote@specials \do\"}
742\def \quoteon {\catcode `\" \active}\quoteon}
743
744\def \quoteoff {\@makeother \"}
745\makeatother
746
747
748
749%%%%%%%%%%%%%%%%
750\def \lift #1{\;{}^{#1}}
751\def \inu #1{\lift {i \in 1..#1}}
752\def \jnu #1{\lift {j \in 1..#1}}
753
754%% typo
755
756\mathchardef \le "313C
757\mathchardef \ge "313E
758
759\mathcode `< "4268
760\mathcode `> "5269
761
762
763\catcode `\| \active
764\let \olspecials \dospecials \def \dospecials {\olspecials \do \|}
765
766%\def \droite {\mathrel {\,\hbox {\large$\triangleright$}\,}}
767\def \droite {\mathrel{\tt =}}
768
769\makeatletter
770\def |{\baractive}
771\def \baractive {\futurelet\token \next@baractive}
772\def \eattoken #1{}
773\def \next@baractive{\let\do\eattoken
774    \ifx \token>\droite\else \mid \let \do \relax \fi \do}
775
776
777\def \Def #1in{\mathprefix {let}#1\mathinfix{in}}
778\def \Let#1in{\mathprefix {let}#1\mathinfix{in}}
779\def \Reply#1to{\mathprefix {reply}#1\mathinfix{to}}
780\def \>{\droite}
781\def \And {\mathrel{\tt and}}
782\def \tuple #1{{\tt (}#1{\tt )}}
783\def \<#1> {\tuple {#1}}
784
785\let \bcup \cup
786\let \thd \th
787\def \fv {fv}
788\def \defines {::}
789\def \produces #1{\Ds\mathop{\Longrightarrow}^{#1}}
790\def \reduces {\longrightarrow}
791\let \red \reduces
792\let \redcham \mapsto
793
794\let \plus \tplus
795
796\makeatother
797
798
799\def \dd {{\cal D}}
800\def \pp {{\cal P}}
801
802\def \dv {dv}
803
804\def \redsoupe {\mathrel {\mathop {\red} \limits^s}}
805\let \redstruct \rightleftharpoons
806\let \redchaud \rightharpoonup
807\let \redfroid \leftharpoondown
808\let \cool \leftharpoondown
809\let \heat \rightharpoonup
810
811\def\redstep{\mathrel{\mathpalette\redstepaux{}}}
812\def\redstepaux#1{\vcenter{\hbox{\ooalign{\hfil
813      \raise2pt \hbox{$\rightharpoonup$}\hfil\cr\hfil
814      \lower2pt\hbox {$\leftharpoondown$}\hfil\crcr
815      $\longrightarrow$}}}}
816
817
818\let \redsoupe \red
819\let \redx \red
820
821
822\def \Comment #1{}
823\let \agree \approx
824\quoteon
825
826\maketoken \int {int}
827
828
829