design/tpl: Remove glossary
This is an unnecessary feature to maintain right now. I will include symbols at the very beginning of the index, which is common in mathematics texts, and may will add a table of common symbols in the future.master
parent
cacb72b2bd
commit
c371d12a02
|
|
@ -11,12 +11,6 @@
|
|||
*.out
|
||||
*.toc
|
||||
|
||||
# Glossary
|
||||
*.glg
|
||||
*.glo
|
||||
*.gls
|
||||
*.ist
|
||||
|
||||
# Index
|
||||
*.idx
|
||||
*.ilg
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
|
||||
inputs := tpl.tex tpl.sty glossary.tex \
|
||||
inputs := tpl.tex tpl.sty \
|
||||
$(wildcard sec/*.tex)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,169 +0,0 @@
|
|||
% The TAME Programming Language glossary
|
||||
%
|
||||
% Copyright (C) 2021 Ryan Specialty Group, LLC.
|
||||
%
|
||||
% Licensed under the Creative Commons Attribution-ShareAlike 4.0
|
||||
% International License.
|
||||
%%
|
||||
|
||||
\makeglossaries
|
||||
|
||||
\newacronym{tamer}{\textsc{Tamer}}{\tame{} in Rust}
|
||||
|
||||
\newglossaryentry{classification}
|
||||
{
|
||||
name={classification},
|
||||
description={TODO}
|
||||
}
|
||||
|
||||
\newglossaryentry{free variable}
|
||||
{
|
||||
name={free variable},
|
||||
description={a variable that is not a \gls{bound variable}}
|
||||
}
|
||||
|
||||
\newglossaryentry{bound variable}
|
||||
{
|
||||
name={bound variable},
|
||||
description={}
|
||||
}
|
||||
|
||||
\newglossaryentry{predicate}
|
||||
{
|
||||
name={predicate},
|
||||
description={}
|
||||
}
|
||||
|
||||
\newglossaryentry{boolean}
|
||||
{
|
||||
name={boolean},
|
||||
description={a value of \gls{true} or \gls{false}},
|
||||
symbol={\Bool},
|
||||
}
|
||||
|
||||
\newglossaryentry{true}
|
||||
{
|
||||
name={true},
|
||||
description={boolean value representing ``true''},
|
||||
symbol={\true},
|
||||
}
|
||||
|
||||
\newglossaryentry{false}
|
||||
{
|
||||
name={false},
|
||||
description={boolean value representing ``false''},
|
||||
symbol={\false},
|
||||
}
|
||||
|
||||
\newglossaryentry{conjunction}
|
||||
{
|
||||
name={conjunction},
|
||||
description={logical conjunction (``and'')},
|
||||
symbol={\ensuremath{\logand}},
|
||||
}
|
||||
\newglossaryentry{disjunction}
|
||||
{
|
||||
name={disjunction},
|
||||
description={logical disjunction (``or'')},
|
||||
symbol={\ensuremath{\logor}},
|
||||
}
|
||||
|
||||
\newglossaryentry{cardinality}
|
||||
{
|
||||
name={cardinality},
|
||||
description={number of elements in some set~$S$},
|
||||
symbol={\ensuremath{|S|}}
|
||||
}
|
||||
|
||||
\newglossaryentry{family}
|
||||
{
|
||||
name={family},
|
||||
description={a set sharing the same \gls{index set}},
|
||||
symbol={\ensuremath{\{A_j\}_{j\in J}}}
|
||||
}
|
||||
|
||||
\newglossaryentry{index set}
|
||||
{
|
||||
name={index set},
|
||||
description={a set whose members index members of another set; see also
|
||||
\gls{family}},
|
||||
}
|
||||
|
||||
\newglossaryentry{castable}
|
||||
{
|
||||
name={castable},
|
||||
description={type $A$ is castable to type $B$ if there exists some
|
||||
\gls{surjective} function $A\rightarrow B$}
|
||||
}
|
||||
|
||||
\newglossaryentry{surjective}
|
||||
{
|
||||
name={surjective},
|
||||
description={$\forall y\in Y : \exists x\in X : f(x) = y$},
|
||||
}
|
||||
|
||||
\newglossaryentry{equivalent}
|
||||
{
|
||||
name={equivalent},
|
||||
description={an equivalence relation is a reflexive, symmetric, and
|
||||
transitive binary operation},
|
||||
}
|
||||
|
||||
\newglossaryentry{logical equivalence}
|
||||
{
|
||||
name={logical equivalence},
|
||||
description={$p$ and $q$ are logically equivalent ($p\equiv q$) \gls{iff}
|
||||
both $q$ and~$p$ are~\true or both are~\false},
|
||||
symbol={\ensuremath{\equiv}},
|
||||
}
|
||||
|
||||
\newglossaryentry{logical implication}
|
||||
{
|
||||
name={logical implication},
|
||||
description={},
|
||||
symbol={\ensuremath{\implies}},
|
||||
}
|
||||
|
||||
\newglossaryentry{iff}
|
||||
{
|
||||
name={iff},
|
||||
description={if and only if},
|
||||
symbol={\ensuremath{\iff}},
|
||||
}
|
||||
|
||||
\newglossaryentry{forall}
|
||||
{
|
||||
name={universal quantification},
|
||||
description={expresses a predicate that must be satisfied for every
|
||||
element in a \gls{domain}},
|
||||
symbol={\ensuremath{\forall}},
|
||||
}
|
||||
|
||||
\newglossaryentry{exists}
|
||||
{
|
||||
name={existential quantification},
|
||||
description={expresses a predicate that must be satisfied for some
|
||||
element in a \gls{domain}},
|
||||
symbol={\ensuremath{\exists}},
|
||||
}
|
||||
|
||||
\newglossaryentry{domain}
|
||||
{
|
||||
name={domain of discourse},
|
||||
description={set of elements over which variables of interest may range},
|
||||
symbol={\ensuremath{\mathbb{D}}},
|
||||
}
|
||||
|
||||
\newglossaryentry{integer}
|
||||
{
|
||||
name={integer},
|
||||
description={set of all integers},
|
||||
symbol={\ensuremath{\mathbb{Z}}},
|
||||
}
|
||||
|
||||
\newglossaryentry{empty set}
|
||||
{
|
||||
name={empty set},
|
||||
description={set of zero elements},
|
||||
symbol={\ensuremath{\emptyset}}
|
||||
}
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
|
||||
\section{Classification System}\seclabel{class}
|
||||
\index{classification}
|
||||
A \gls{classification} is a user-defined abstraction that describes
|
||||
A \emph{classification} is a user-defined abstraction that describes
|
||||
(``classifies'') arbitrary data.
|
||||
Classifications can be used as predicates, generating functions, and can be
|
||||
composed into more complex classifications.
|
||||
|
|
@ -11,7 +11,7 @@ Nearly all conditions in \tame{} are specified using classifications.
|
|||
\index{classification!coupling}
|
||||
All classifications represent \emph{first-order sentences}---%
|
||||
that is,
|
||||
they contain no \glspl{free variable}.
|
||||
they contain no \emph{free variables}.
|
||||
Intuitively,
|
||||
this means that all variables within a~classification are
|
||||
\emph{tightly coupled} to the classification itself.
|
||||
|
|
@ -36,7 +36,7 @@ is then equivalent to the proposition
|
|||
\end{equation*}
|
||||
|
||||
\index{classification!domain}
|
||||
A classification is either \glssymbol{true} or~\glssymbol{false}.
|
||||
A classification is either \true or~\false.
|
||||
Let $\tameparam{cost}=150.00$.
|
||||
Then,
|
||||
|
||||
|
|
@ -46,8 +46,8 @@ Then,
|
|||
& \equiv \true.
|
||||
\end{align*}
|
||||
|
||||
Each \xmlnode{match} of a classification is a~\gls{predicate}.
|
||||
Multiple predicates are by default joined by \gls{conjunction}:
|
||||
Each \xmlnode{match} of a classification is a~\emph{predicate}.
|
||||
Multiple predicates are by default joined by conjunction:
|
||||
|
||||
\begin{lstlisting}
|
||||
<classify as="pool-hazard" desc="Hazardous pool">
|
||||
|
|
@ -66,7 +66,7 @@ is equivalent to the proposition
|
|||
|
||||
\index{classification!universal}
|
||||
\begin{definition}[Universal Classification]\dfnlabel{classu}
|
||||
A classification~$c$ by default performs \gls{conjunction} on its match
|
||||
A classification~$c$ by default performs conjunction on its match
|
||||
expressions $M_0\ldots M_n$.
|
||||
|
||||
\begin{alignat*}{2}
|
||||
|
|
@ -83,7 +83,7 @@ is equivalent to the proposition
|
|||
\index{classification!existential}
|
||||
\begin{definition}[Existential Classification]\dfnlabel{classe}
|
||||
A classification~$c$ with the attribute \xpath{@any="true"} performs
|
||||
\gls{disjunction} on its match expressions $M_0\ldots M_n$.
|
||||
disjunction on its match expressions $M_0\ldots M_n$.
|
||||
|
||||
\begin{alignat*}{2}
|
||||
&\xml{<classify as="} &&c\xml{" any="true" desc="$\ldots$">} \\
|
||||
|
|
|
|||
|
|
@ -89,7 +89,7 @@ We assume that the axioms of ZFC~set theory hold,
|
|||
\index{first-order logic!quantification (\ensuremath{\forall, \exists})}
|
||||
$\forall$ denotes first-order universal quantification (``for all''),
|
||||
and $\exists$ first-order existential quantification (``there exists''),
|
||||
over some \gls{domain}.
|
||||
over some domain.
|
||||
|
||||
\index{disjunction|see {first-order logic}}
|
||||
\index{first-order logic!disjunction (\ensuremath{\logor})}
|
||||
|
|
@ -117,9 +117,9 @@ $\forall$ denotes first-order universal quantification (``for all''),
|
|||
\end{definition}
|
||||
|
||||
\tamefalse{} and~\tametrue{} are constants in \tame{} mapping to the
|
||||
\gls{integer} values $\{0,1\}\in\Int$.
|
||||
integer values $\{0,1\}\in\Int$.
|
||||
\dfnref{bool-int} relates these constants to their
|
||||
\gls{boolean} counterparts so that they may be used in numeric contexts
|
||||
boolean counterparts so that they may be used in numeric contexts
|
||||
and vice-versa.
|
||||
|
||||
|
||||
|
|
@ -240,7 +240,7 @@ Unfortunately,
|
|||
its implementation history leaves those concepts a bit tortured.
|
||||
|
||||
A vector is a sequence of values, defined as a function of
|
||||
an~\gls{index set}.
|
||||
an index~set.
|
||||
|
||||
\begin{definition}[Vector]\dfnlabel{vec}
|
||||
Let $J\subset\Int$ represent an index set.
|
||||
|
|
|
|||
|
|
@ -10,7 +10,6 @@
|
|||
\usepackage[amsfonts,amssymb]{concmath}
|
||||
|
||||
\usepackage{makeidx}
|
||||
\usepackage[toc]{glossaries}
|
||||
|
||||
% Note that we force draft=false so hyperlinks always appear
|
||||
\usepackage[colorlinks=true,linkcolor=href,draft=false]{hyperref}
|
||||
|
|
@ -19,6 +18,7 @@
|
|||
\usepackage{listings}
|
||||
|
||||
% Definitions, theorems, proofs, etc
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amsthm}
|
||||
|
||||
% Line spacing instead of indentation for paragraphs
|
||||
|
|
@ -38,7 +38,7 @@
|
|||
|
||||
% TAME is typeset in smallcaps
|
||||
\newcommand{\tame}{\textsc{Tame}}
|
||||
\newcommand{\tamer}{\gls{tamer}}
|
||||
\newcommand{\tamer}{\textsc{tamer}}
|
||||
|
||||
% TODO: highlighting
|
||||
\lstset{
|
||||
|
|
|
|||
|
|
@ -26,7 +26,6 @@
|
|||
\setcounter{section}{-1}
|
||||
|
||||
\makeindex
|
||||
\input{glossary.tex}
|
||||
|
||||
\begin{document}
|
||||
|
||||
|
|
@ -58,7 +57,6 @@
|
|||
\input{sec/class.tex}
|
||||
|
||||
\clearpage
|
||||
\printglossary[style=altlong4col]
|
||||
\printindex
|
||||
|
||||
\end{document}
|
||||
|
|
|
|||
Loading…
Reference in New Issue