diff options
| -rw-r--r-- | .hgignore | 7 | ||||
| -rw-r--r-- | CHANGELOG | 1 | ||||
| -rw-r--r-- | doc/Makefile | 23 | ||||
| -rw-r--r-- | doc/manual.tex | 85 |
4 files changed, 115 insertions, 1 deletions
@@ -13,7 +13,7 @@ src/urweb.mlb *.grm.* *.o -Makefile +./Makefile src/config.sml *.exe @@ -27,3 +27,8 @@ demo/demo.* *.sql *mlmon.out + +*.aux +*.dvi +*.pdf +*.ps @@ -3,6 +3,7 @@ - Optimization: Fusing page writes with calls to recursive functions - Optimization of bottleneck compiler phases +- Start of manual ======== 20081120 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 |