summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 14:38:53 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 14:38:53 -0500
commit61bd40e1af8c3f7ace2a09068557ac7c05662b69 (patch)
tree3f180b88f47fe8cfb1f6dda748baf30d41363b56 /doc
parentdf08dfc3be26b2cf829a1ea31b63f4aaecf1f3bf (diff)
Start of manual
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile23
-rw-r--r--doc/manual.tex85
2 files changed, 108 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
index 00000000..777c5bf7
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,23 @@
+PAPERS=manual
+
+FIGURES=
+
+all: $(PAPERS:%=%.dvi) $(PAPERS:%=%.ps) $(PAPERS:%=%.pdf)
+
+%.dvi: %.tex $(FIGURES:%=%.eps)
+ latex $<
+ latex $<
+
+%.ps: %.dvi
+ dvips $< -o $@
+
+%.pdf: %.dvi $(FIGURES:%=%.pdf)
+ pdflatex $(<:%.dvi=%)
+
+%.pdf: %.eps
+ epstopdf $<
+
+clean:
+ rm -f *.aux *.bbl *.blg *.dvi *.log *.pdf *.ps
+
+.PHONY: all clean
diff --git a/doc/manual.tex b/doc/manual.tex
new file mode 100644
index 00000000..8517206a
--- /dev/null
+++ b/doc/manual.tex
@@ -0,0 +1,85 @@
+\documentclass{article}
+\usepackage{fullpage,amsmath,amssymb,proof}
+
+\newcommand{\cd}[1]{\texttt{#1}}
+\newcommand{\mt}[1]{\mathsf{#1}}
+
+\newcommand{\rc}{+ \hspace{-.075in} + \;}
+
+\begin{document}
+
+\title{The Ur/Web Manual}
+\author{Adam Chlipala}
+
+\maketitle
+
+\section{Syntax}
+
+\subsection{Lexical Conventions}
+
+We give the Ur language definition in \LaTeX $\;$ math mode, since that is prettier than monospaced ASCII. The corresponding ASCII syntax can be read off directly. Here is the key for mapping math symbols to ASCII character sequences.
+
+\begin{center}
+ \begin{tabular}{rl}
+ \textbf{\LaTeX} & \textbf{ASCII} \\
+ $\to$ & \cd{->} \\
+ $\times$ & \cd{*} \\
+ $\lambda$ & \cd{fn} \\
+ $\Rightarrow$ & \cd{=>} \\
+ $\rc$ & \cd{++} \\
+ \\
+ $x$ & Normal textual identifier, not beginning with an uppercase letter \\
+ $\alpha$ & Normal textual identifier, not beginning with an uppercase letter \\
+ $f$ & Normal textual identifier, beginning with an uppercase letter \\
+ \end{tabular}
+\end{center}
+
+We often write syntax like $N, \cdots, N$ to stand for the non-terminal $N$ repeated 0 or more times. That is, the $\cdots$ symbol is not translated literally to ASCII.
+
+\subsection{Core Syntax}
+
+\emph{Kinds} classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies.
+$$\begin{array}{rrcll}
+ \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
+ &&& \mid \mt{Unit} & \textrm{the trivial constructor} \\
+ &&& \mid \mt{Name} & \textrm{field names} \\
+ &&& \mid \kappa \to \kappa & \textrm{type-level functions} \\
+ &&& \mid \{\kappa\} & \textrm{type-level records} \\
+ &&& \mid (\kappa \times \cdots \times \kappa) & \textrm{type-level tuples} \\
+ &&& \mid (\kappa) & \textrm{explicit precedence} \\
+\end{array}$$
+
+Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
+$$\begin{array}{rrcll}
+ \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
+ &&& \mid \; ::: & \textrm{implicit}
+\end{array}$$
+
+\emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
+$$\begin{array}{rrcll}
+ \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
+ &&& \mid \alpha & \textrm{constructor variable} \\
+ \\
+ &&& \mid \tau \to \tau & \textrm{function type} \\
+ &&& \mid \alpha \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
+ &&& \mid \$ c & \textrm{record type} \\
+ \\
+ &&& \mid c \; c & \textrm{type-level function application} \\
+ &&& \mid \lambda \alpha \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
+ \\
+ &&& \mid () & \textrm{type-level unit} \\
+ &&& \mid \#f & \textrm{field name} \\
+ \\
+ &&& \mid [c = c, \cdots, c = c] & \textrm{known-length type-level record} \\
+ &&& \mid c \rc c & \textrm{type-level record concatenation} \\
+ &&& \mid \mt{fold} & \textrm{type-level record fold} \\
+ \\
+ &&& \mid (c, \cdots, c) & \textrm{type-level tuple} \\
+ &&& \mid c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
+ \\
+ &&& \mid \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
+ \\
+ &&& \mid (c) & \textrm{explicit precedence} \\
+\end{array}$$
+
+\end{document} \ No newline at end of file