macros.tex 8.03 KB
Newer Older
1 2 3 4
% EBNF syntax.

\let\nt\textit % Nonterminal.
\newcommand{\is}{& ${} ::= {}$ &}
POTTIER Francois's avatar
POTTIER Francois committed
5 6 7
\newcommand{\newprod}{\\\hspace{1cm}\barre\hspace{2mm}}
\newcommand{\phaprod}{\\\hspace{1cm}\phantom\barre\hspace{2mm}}
% Options and choices.
8 9 10 11
\newcommand{\optional}[1]{%
  \ifmmode [\,#1\,]%
  \else    $[\,\text{#1}\,]$%
  \fi
POTTIER Francois's avatar
POTTIER Francois committed
12 13 14
}
\newcommand{\metachoice}{$\,\mid\,$}
% Lists.
15 16 17
\newcommand{\seplist}[2]{#2#1${}\ldots{}$#1#2}
\newcommand{\sepspacelist}[1]{\seplist{\ }{#1}}
\newcommand{\sepcommalist}[1]{\seplist{,\ }{#1}}
POTTIER Francois's avatar
POTTIER Francois committed
18 19 20 21 22 23 24 25 26 27
\newcommand{\precseplist}[2]{%
  \optional{#1} \seplist{\ #1}{#2}%
}
% Optional parameters.
\newcommand{\tuple}[1]{\dlpar\sepcommalist{#1}\drpar}
\newcommand{\oparams}[1]{\optional{\tuple{#1}}}
% Some nonterminal symbols used in the grammar.
\newcommand{\expression}{\nt{expression}\xspace}
\newcommand{\expressionsub}[1]{\nt{expression}${}_{#1}$}
\newcommand{\pattern}{\nt{pattern}\xspace}
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46

% Concrete syntax.

\newcommand{\percentpercent}{\kw{\%\%}\xspace}
\newcommand{\deuxpoints}{\kw{:}\xspace}
\newcommand{\barre}{\kw{\textbar}\xspace}
\newcommand{\kangle}[1]{\kw{\textless} #1 \kw{\textgreater}}
\newcommand{\ocamltype}{\kangle{\textit{\ocaml type}}\xspace}
\newcommand{\ocamlparam}{\kangle{\nt{uid} \deuxpoints \textit{\ocaml module type}}\xspace}
\newcommand{\dheader}[1]{\kw{\%\{} #1 \kw{\%\}}}
\newcommand{\dtoken}{\kw{\%token}\xspace}
\newcommand{\dstart}{\kw{\%start}\xspace}
\newcommand{\dtype}{\kw{\%type}\xspace}
\newcommand{\dnonassoc}{\kw{\%nonassoc}\xspace}
\newcommand{\dleft}{\kw{\%left}\xspace}
\newcommand{\dright}{\kw{\%right}\xspace}
\newcommand{\dparameter}{\kw{\%parameter}\xspace}
\newcommand{\dpublic}{\kw{\%public}\xspace}
\newcommand{\dinline}{\kw{\%inline}\xspace}
47
\newcommand{\donerrorreduce}{\kw{\%on\_error\_reduce}\xspace}
48
\newcommand{\dattribute}{\kw{\%attribute}\xspace}
49 50
\newcommand{\dpaction}[1]{\kw{\{} #1 \kw{\}}\xspace}
\newcommand{\daction}{\dpaction{\textit{\ocaml code}}\xspace}
POTTIER Francois's avatar
POTTIER Francois committed
51 52
\newcommand{\dpfaction}[1]{\kw{<} #1 \kw{>}\xspace}
\newcommand{\dpfidentityaction}{\kw{<>}\xspace}
53
\newcommand{\dprec}{\kw{\%prec}\xspace}
POTTIER Francois's avatar
POTTIER Francois committed
54
\newcommand{\dequal}{\kw{\small =}\xspace}
55
\newcommand{\dquestion}{\kw{?}\xspace}
56
\newcommand{\dplus}{\raisebox{2pt}{\kw{\small +}}\xspace}
POTTIER Francois's avatar
POTTIER Francois committed
57 58
\newcommand{\dcolonequal}{\kw{\small :=}\xspace}
\newcommand{\dequalequal}{\kw{\small ==}\xspace}
59 60 61 62 63
\newcommand{\dstar}{\kw{*}\xspace}
\newcommand{\dlpar}{\kw{(}\,\xspace}
\newcommand{\drpar}{\,\kw{)}\xspace}
\newcommand{\eos}{\kw{\#}\xspace}
\newcommand{\dnewline}{\kw{\textbackslash n}\xspace}
POTTIER Francois's avatar
POTTIER Francois committed
64 65 66 67
\newcommand{\dlet}{\kw{let}\xspace}
\newcommand{\dsemi}{\kw{;}\xspace}
\newcommand{\dunderscore}{\kw{\_}\xspace}
\newcommand{\dtilde}{\raisebox{-4pt}{\kw{\textasciitilde}}\xspace}
68 69 70 71 72

% Stylistic conventions.

\newcommand{\kw}[1]{\text{\upshape\sf\bfseries #1}}
\newcommand{\inlinesidecomment}[1]{\textit{\textbf{\footnotesize // #1}}}
73
\newcommand{\sidecomment}[1]{\hspace{2cm}\inlinesidecomment{#1}}
74 75
\newcommand{\docskip}{\vspace{1mm plus 1mm}}
\newcommand{\docswitch}[1]{\docskip#1.\hspace{3mm}}
76 77
\newcommand{\error}{\kw{error}\xspace}

78 79 80 81 82
% Links to Menhir's repository.

\newcommand{\repo}[2]{\href{https://gitlab.inria.fr/fpottier/menhir/blob/master/#1}{#2}}
\newcommand{\menhirlibconvert}{\repo{src/Convert.mli}{\texttt{MenhirLib.Convert}}\xspace}
\newcommand{\menhirlibincrementalengine}{\repo{src/IncrementalEngine.ml}{\texttt{MenhirLib.IncrementalEngine}}\xspace}
83
\newcommand{\standardmly}{\repo{src/standard.mly}{\texttt{standard.mly}}\xspace}
POTTIER Francois's avatar
POTTIER Francois committed
84
\newcommand{\distrib}[1]{\repo{#1}{\texttt{#1}}}
85 86 87 88 89 90

% Links to CompCert's repository.

\newcommand{\compcertgithub}{https://github.com/AbsInt/CompCert/tree/master}
\newcommand{\compcertgithubfile}[1]{\href{\compcertgithub/#1}{\texttt{#1}}}

91 92 93 94
% Abbreviations.

\newcommand{\menhir}{Menhir\xspace}
\newcommand{\menhirlib}{\texttt{MenhirLib}\xspace}
95
\newcommand{\menhirsdk}{\texttt{MenhirSdk}\xspace}
96
\newcommand{\menhirinterpreter}{\texttt{MenhirInterpreter}\xspace}
97 98 99 100
\newcommand{\cmenhir}{\texttt{menhir}\xspace}
\newcommand{\ml}{\texttt{.ml}\xspace}
\newcommand{\mli}{\texttt{.mli}\xspace}
\newcommand{\mly}{\texttt{.mly}\xspace}
101 102
\newcommand{\cmly}{\texttt{.cmly}\xspace}
\newcommand{\vy}{\texttt{.vy}\xspace}
103
\newcommand{\ocaml}{OCaml\xspace}
104 105 106 107 108 109 110
\newcommand{\ocamlc}{\texttt{ocamlc}\xspace}
\newcommand{\ocamlopt}{\texttt{ocamlopt}\xspace}
\newcommand{\ocamldep}{\texttt{ocamldep}\xspace}
\newcommand{\ocamlfind}{\texttt{ocamlfind}\xspace}
\newcommand{\make}{\texttt{make}\xspace}
\newcommand{\omake}{\texttt{omake}\xspace}
\newcommand{\ocamlbuild}{\texttt{ocamlbuild}\xspace}
POTTIER Francois's avatar
POTTIER Francois committed
111
\newcommand{\dune}{\texttt{dune}\xspace}
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
\newcommand{\Makefile}{\texttt{Makefile}\xspace}
\newcommand{\yacc}{\texttt{yacc}\xspace}
\newcommand{\bison}{\texttt{bison}\xspace}
\newcommand{\ocamlyacc}{\texttt{ocamlyacc}\xspace}
\newcommand{\ocamllex}{\texttt{ocamllex}\xspace}
\newcommand{\token}{\texttt{token}\xspace}
\newcommand{\automaton}{\texttt{.automaton}\xspace}
\newcommand{\conflicts}{\texttt{.conflicts}\xspace}
\newcommand{\dott}{\texttt{.dot}\xspace}

% Environments.

\newcommand{\question}[1]{\vspace{3mm}$\diamond$ \textbf{#1}}

% Ocamlweb settings.

\newcommand{\basic}[1]{\textit{#1}}
\let\ocwkw\kw
\let\ocwbt\basic
\let\ocwupperid\basic
\let\ocwlowerid\basic
\let\ocwtv\basic
\newcommand{\ocwbar}{\vskip 2mm plus 2mm \hrule \vskip 2mm plus 2mm}
\newcommand{\tcup}{${}\cup{}$}
\newcommand{\tcap}{${}\cap{}$}
\newcommand{\tminus}{${}\setminus{}$}

% Command line options.

POTTIER Francois's avatar
POTTIER Francois committed
141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
\newcommand{\oo}[1]{\texttt{-{}-#1}\xspace}

\newcommand{\obase}{\oo{base}}
\newcommand{\ocanonical}{\oo{canonical}} % undocumented!
\newcommand{\ocomment}{\oo{comment}}
\newcommand{\ocmly}{\oo{cmly}}
\newcommand{\odepend}{\oo{depend}}
\newcommand{\orawdepend}{\oo{raw-depend}}
\newcommand{\odump}{\oo{dump}}
\newcommand{\oerrorrecovery}{\oo{error-recovery}}
\newcommand{\oexplain}{\oo{explain}}
\newcommand{\oexternaltokens}{\oo{external-tokens}}
\newcommand{\ofixedexc}{\oo{fixed-exception}}
\newcommand{\ograph}{\oo{graph}}
\newcommand{\oignoreone}{\oo{unused-token}}
\newcommand{\oignoreall}{\oo{unused-tokens}}
\newcommand{\oignoreprec}{\oo{unused-precedence-levels}}
\newcommand{\oinfer}{\oo{infer}}
159 160
\newcommand{\oinferwrite}{\oo{infer-write-query}}
\newcommand{\oinferread}{\oo{infer-read-reply}}
161
\newcommand{\oinferprotocolsupported}{\oo{infer-protocol-supported}}
POTTIER Francois's avatar
POTTIER Francois committed
162 163 164 165 166 167
\newcommand{\oinspection}{\oo{inspection}}
\newcommand{\ointerpret}{\oo{interpret}}
\newcommand{\ointerpretshowcst}{\oo{interpret-show-cst}}
\newcommand{\ologautomaton}{\oo{log-automaton}}
\newcommand{\ologcode}{\oo{log-code}}
\newcommand{\ologgrammar}{\oo{log-grammar}}
168
\newcommand{\onodollars}{\oo{no-dollars}}
POTTIER Francois's avatar
POTTIER Francois committed
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
\newcommand{\onoinline}{\oo{no-inline}}
\newcommand{\onostdlib}{\oo{no-stdlib}}
\newcommand{\oocamlc}{\oo{ocamlc}}
\newcommand{\oocamldep}{\oo{ocamldep}}
\newcommand{\oonlypreprocess}{\oo{only-preprocess}}
\newcommand{\oonlytokens}{\oo{only-tokens}}
\newcommand{\ostrict}{\oo{strict}}
\newcommand{\osuggestcomp}{\oo{suggest-comp-flags}}
\newcommand{\osuggestlinkb}{\oo{suggest-link-flags-byte}}
\newcommand{\osuggestlinko}{\oo{suggest-link-flags-opt}}
\newcommand{\osuggestmenhirlib}{\oo{suggest-menhirLib}}
\newcommand{\osuggestocamlfind}{\oo{suggest-ocamlfind}}
\newcommand{\otable}{\oo{table}}
\newcommand{\otimings}{\oo{timings}}
\newcommand{\otrace}{\oo{trace}}
\newcommand{\ostdlib}{\oo{stdlib}}
\newcommand{\oversion}{\oo{version}}
\newcommand{\ocoq}{\oo{coq}}
187 188
\newcommand{\ocoqlibpath}{\oo{coq-lib-path}}
\newcommand{\ocoqlibnopath}{\oo{coq-lib-no-path}}
POTTIER Francois's avatar
POTTIER Francois committed
189 190 191 192 193 194 195 196
\newcommand{\ocoqnocomplete}{\oo{coq-no-complete}}
\newcommand{\ocoqnoactions}{\oo{coq-no-actions}}
\newcommand{\olisterrors}{\oo{list-errors}}
\newcommand{\ointerpreterror}{\oo{interpret-error}}
\newcommand{\ocompileerrors}{\oo{compile-errors}}
\newcommand{\ocompareerrors}{\oo{compare-errors}}
\newcommand{\oupdateerrors}{\oo{update-errors}}
\newcommand{\oechoerrors}{\oo{echo-errors}}
197 198 199

% The .messages file format.
\newcommand{\messages}{\texttt{.messages}\xspace}
200 201 202 203 204 205 206 207

% Adding mathstruts to ensure a common baseline.
\newcommand{\mycommonbaseline}{
\let\oldnt\nt
\renewcommand{\nt}[1]{$\mathstrut$\oldnt{##1}}
\let\oldbasic\basic
\renewcommand{\basic}[1]{$\mathstrut$\oldbasic{##1}}
}
208

209 210
% Position keywords.
\newcommand{\ksymbolstartpos}{\texttt{\$symbolstartpos}\xspace}