start a glossary

Makefile.in

@@ -819,6 +819,9 @@ doc: $(DOC)
 
 doc/manual.pdf: doc/apidoc.tex doc/manual.tex doc/version.tex
 	cd doc; pdflatex manual
+	cd doc; makeglossaries manual
+	cd doc; pdflatex manual
+	cd doc; makeglossaries manual
 	cd doc; pdflatex manual
 
 doc/manual.html: doc/manual.tex doc/version.tex

doc/glossary.tex

+\newcommand{\why}{\textsc{Why}}
+
+\newglossaryentry{ident}{
+  name={identifier},
+  description={
+    (type \texttt{Ident.ident}) --- a common type to represent
+    a name of an object. Every \gls{tysymbol}, \gls{lsymbol},
+    \gls{prsymbol}, \gls{tvsymbol}, \gls{vsymbol}, and
+    \gls{theory} has a unique identifier that can be used
+    to distinguish it from any other object of the same type.
+\glspar
+    Every identifier has an associated, possibly non-unique,
+    string. To avoid collisions in \gls{prettyprinting} and
+    to make the output conform to a given format, various
+    \glspl{printer} may \glslink{sanitization}{sanitize}
+    identifiers. Identifiers may also bear a \gls{location}
+    of their origin and a list of \glspl{label}.
+\glspar
+    An identifier is \gls{unigen} from a \gls{preid} and
+    is suitable for \gls{weakmemo}.
+\nopostdesc}
+}
+
+\newglossaryentry{label}{
+  name={label},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{location}{
+  name={location},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{decl}{
+  name={declaration},
+  description={(type \texttt{Decl.decl})
+\nopostdesc}
+}
+
+\newglossaryentry{algtype}{
+  name={algebraic type},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{constructor}{
+  name={constructor},
+  description={--- a \gls{lsymbol} introduced in
+  an \gls{algtype} \gls{decl}. Can be used in \glspl{pattern}
+  and as a usual function symbol.
+\nopostdesc}
+}
+
+\newglossaryentry{lsymbol}{
+  name={logical symbol},
+  description={(type \texttt{Term.lsymbol}) --- a type representing
+  function and predicate symbols. A logical symbol bears a unique
+  \gls{ident} and a type signature, describing what types a symbol
+  admits in its arguments.
+\glspar
+  A logical symbol is \gls{unigen} from a \gls{preid} and
+  is suitable for \gls{weakmemo}.
+\nopostdesc}
+}
+
+\newglossaryentry{preid}{
+  name={pre-identifier},
+  description={(type \texttt{Ident.preid}) --- a preliminary
+  non-unique object used to produce unique \glspl{ident}.
+\nopostdesc}
+}
+
+\newglossaryentry{prettyprinting}{
+  name={pretty-printing},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{printer}{
+  name={printer},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{proposition}{
+  name={printer},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{prsymbol}{
+  name={proposition symbol},
+  description={(type \texttt{Decl.prsymbol}) --- a type representing
+  \gls{proposition} names. A proposition symbol bears a unique \gls{ident},
+  is \gls{unigen} from a \gls{preid}, and is suitable for \gls{weakmemo}.
+\nopostdesc}
+}
+
+\newglossaryentry{sanitization}{
+  name={sanitization},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{theory}{
+  name={theory},
+  description={
+\nopostdesc}
+}
+
+\newglossaryentry{tvsymbol}{
+  name={type variable},
+  description={
+    (type \texttt{Ty.tvsymbol}) --- a type representing symbols of
+    type variables. A type variable bears a unique \gls{ident}
+    and is \gls{unigen} from a \gls{preid}.
+\nopostdesc}
+}
+
+\newglossaryentry{hashcons}{
+  name={hash-consed},
+  description={
+    Objects of a given type are hash-consed whenever (a) every
+    two semantically equal objects are also physically equal;
+    and (b) contrary to \gls{unigen} objects, one can construct
+    an hash-consed object equal to an existing one.
+\glspar
+    Hash-consed objects provide efficient comparison and hash
+    operations and are suitable for \gls{weakmemo}.
+\nopostdesc}
+}
+
+\newglossaryentry{pattern}{
+  name={pattern},
+  description={(type \texttt{Term.pattern}) --- objects used
+  in pattern-matching expressions. A pattern is built of
+  \glspl{constructor} and \glspl{vsymbol} with the help of
+  smart constructors guaranteeing that every pattern is well-typed.
+\glspar
+  Patterns are \gls{hashcons}.
+\nopostdesc}
+}
+
+\newglossaryentry{type}{
+  name={type},
+  description={(type \texttt{Ty.ty}) --- a type representing, well,
+  types in {\why}. Types are built with the help of smart constructors
+  guaranteeing that every type is well-formed.
+\glspar
+  Types are \gls{hashcons} and suitable for \gls{weakmemo}.
+\nopostdesc}
+}
+
+\newglossaryentry{term}{
+  name={term},
+  description={(type \texttt{Term.term}) --- a type of logical terms.
+  Every term has a \gls{type}. Terms are built with the help of
+  smart constructors guaranteeing that every term is well-typed.
+  A term can bear a list of \glspl{label}.
+\glspar
+  In addition to usual first-order terms, {\why} terms can contain
+  if-then-else expressions, let-expressions, and \gls{pattern} matching.
+\glspar
+  Terms are \gls{hashcons}.
+\nopostdesc}
+}
+
+\newglossaryentry{formula}{
+  name={formula},
+  description={(type \texttt{Term.fmla}) --- a type of logical formulas.
+  Formulas are built with the help of smart constructors guaranteeing
+  that every formula is well-typed. A formula can bear a list of
+  \glspl{label}.
+\glspar
+  In addition to usual first-order formulas, {\why} formulas can contain
+  if-then-else expressions, let-expressions, and \gls{pattern} matching.
+\glspar
+  Formulas are \gls{hashcons}.
+\nopostdesc}
+}
+
+\newglossaryentry{tysymbol}{
+  name={type symbol},
+  description={(type \texttt{Ty.tysymbol}) --- a type representing
+  \gls{type} constructors. A type symbol bears a unique \gls{ident}
+  and an arity, is \gls{unigen} from a \gls{preid}, and
+  is suitable for \gls{weakmemo}.
+\nopostdesc}
+}
+
+\newglossaryentry{unigen}{
+  name={uniquely generated},
+  description={
+    Objects of a given type are uniquely generated whenever every
+    newly constructed object is physically and semantically distinct
+    from any other value of the same type. For example, \glspl{ident}
+    are uniquely generated, while \glspl{preid} or \glspl{term} are not.
+\glspar
+    Uniquely generated objects usually provide efficient comparison
+    and hash operations. Thus, they can be used in \gls{hashcons}
+    objects and are suitable for \gls{weakmemo}.
+\nopostdesc}
+}
+
+\newglossaryentry{vsymbol}{
+  name={variable},
+  description={(type \texttt{Ty.vsymbol}) --- a type representing
+  variable symbols. A variable symbol bears a unique \gls{ident}
+  and has an associated \gls{type}.
+\glspar
+  A variable is \gls{unigen} from a \gls{preid}.
+\nopostdesc}
+}
+
+\newglossaryentry{weakmemo}{
+  name={forgetful memoization},
+  description={(module \texttt{Hashweak}) --- memoization technique
+  that does not create an additional reference to a key, allowing it
+  (and its associated value) to be garbage-collected even while
+  the memoization table is still accessible. Forgetful memoization
+  is used, in particular, to implement \gls{task} \glspl{trans}:
+  the transformation results are memoized, but as soon as the
+  original task is garbage-collected, these results can be
+  dropped, too.
+\glspar
+  \Glspl{tysymbol}, \glspl{lsymbol}, \glspl{prsymbol},
+  \glspl{type}, \glspl{decl}, \glspl{task}, and \glspl{env}
+  can be used as keys in forgetful memoization.
+\nopostdesc}
+}
+
+\newglossaryentry{trans}{
+  name={transformation},
+  description={(type \texttt{Trans.trans})
+\nopostdesc}
+}
+
+\newglossaryentry{task}{
+  name={task},
+  description={(type \texttt{Task.task})
+\nopostdesc}
+}
+
+\newglossaryentry{env}{
+  name={environment},
+  description={(type \texttt{Env.env})
+\nopostdesc}
+}
+
+
+\printglossary
+
+\gls{type} \gls{term} \gls{formula} \gls{ident} \gls{weakmemo}
+\gls{vsymbol} \gls{unigen} \gls{tysymbol} \gls{pattern}

doc/manual.tex

@@ -4,6 +4,9 @@
 %\usepackage{url}
 \usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
 
+\usepackage[toc,nonumberlist]{glossaries}
+\makeglossaries
+
 % for ocamldoc generated pages
 \usepackage{ocamldoc}
 \let\tt\ttfamily
@@ -26,9 +29,9 @@
 
 \vfill
 
-{\Large F. Bobot$^{1,2}$ \\ 
-J.-C. Filli\^atre$^{2,1}$  \\ 
-C. March\'e$^{3,1}$ \\ 
+{\Large F. Bobot$^{1,2}$ \\
+J.-C. Filli\^atre$^{2,1}$  \\
+C. March\'e$^{3,1}$ \\
 A. Paskevich$^{1,2}$}
 
 \vfill
@@ -36,7 +39,7 @@ A. Paskevich$^{1,2}$}
 \begin{tabular}{l}
 $^1$ Univ Paris-Sud, Orsay, F-91405 \\
 $^2$ LRI, CNRS, Orsay, F-91405 \\
-$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893 
+$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
 \end{tabular}
 
 \vfill
@@ -83,6 +86,8 @@ We gratefully thank all the people who contributed to this document:
 
 \input{api.tex}
 
+\input{glossary.tex}
+
 \input{manpages.tex}
 
 \chapter{Complete API documentation}