removed transfer from gf3

3 files changed, 0 insertions, 910 deletions

diff --git a/transfer/doc/Makefile b/transfer/doc/Makefile
deleted file mode 100644
index 02f0bec10..000000000
--- a/transfer/doc/Makefile
+++ /dev/null
@@ -1,41 +0,0 @@
-FIGURES=
-
-NAME=typesystem
-
-default: pdf
-
-ps: $(NAME).ps
-
-pdf: $(NAME).pdf
-
-%.ps: %.dvi
-	dvips -f $^ > $@
-
-#%.pdf: %.ps
-#	ps2pdf $^
-
-%.pdf: %.dvi
-	dvipdfm $^
-
-%.dvi: %.tex # %.bib
-	latex $*
-#	bibtex $*
-#	latex $*
-#	latex $*
-
-%.ps: %.dot
-	dot -Tps -o $@ $^
-
-%.eps: %.ps
-	ps2epsi $^ $@
-
-$(NAME).dvi: $(FIGURES)
-
-clean:
-	-rm -f *.aux *.dvi *.log *.blg *.bbl *.toc
-
-psclean: clean
-	-rm -f *.pdf *.ps
-
-show: $(NAME).dvi
-	xdvi $(NAME).dvi
diff --git a/transfer/doc/mathpartir.sty b/transfer/doc/mathpartir.sty
deleted file mode 100644
index 549596797..000000000
--- a/transfer/doc/mathpartir.sty
+++ /dev/null
@@ -1,390 +0,0 @@
-%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
-%
-%  Copyright (C) 2001, 2002, 2003 Didier Rémy
-%
-%  Author         : Didier Remy 
-%  Version        : 1.1.1
-%  Bug Reports    : to author
-%  Web Site       : http://pauillac.inria.fr/~remy/latex/
-% 
-%  WhizzyTeX is free software; you can redistribute it and/or modify
-%  it under the terms of the GNU General Public License as published by
-%  the Free Software Foundation; either version 2, or (at your option)
-%  any later version.
-%  
-%  Mathpartir is distributed in the hope that it will be useful,
-%  but WITHOUT ANY WARRANTY; without even the implied warranty of
-%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-%  GNU General Public License for more details 
-%  (http://pauillac.inria.fr/~remy/license/GPL).
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%  File mathpartir.sty (LaTeX macros)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
-    [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-\newdimen \mpr@tmpdim
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing 
-% in mathpar or in inferrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
-  \edef \MathparNormalpar
-     {\noexpand \lineskiplimit \the\lineskiplimit
-      \noexpand \lineskip \the\lineskip}%
-  }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
-   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
-  \let \and \mpr@andcr
-  \let \par \mpr@andcr
-  \let \\\mpr@cr
-  \let \eqno \mpr@eqno
-  \let \hva \mpr@hva
-  } 
-\let \MathparBindings \mpr@bindings
-
-% \@ifundefined {ignorespacesafterend}
-%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
-
-\newenvironment{mathpar}[1][]
-  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
-     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
-     \noindent $\displaystyle\fi
-     \MathparBindings}
-  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
-  \vbox \bgroup \tabskip 0em \let \\ \cr
-  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
-  \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
-      \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
-   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
-   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
-   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
-     \mpr@flatten \mpr@all \mpr@to \mpr@one
-     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
-     \mpr@all \mpr@stripend  
-     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
-     \ifx 1\mpr@isempty
-   \repeat
-}
-
-%% Part III -- Type inference rules
-
-\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
-   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@htovlist {%
-   \setbox \mpr@hlist
-      \hbox {\strut
-             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
-             \unhbox \mpr@hlist}%
-   \setbox \mpr@vlist
-      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-             \else \unvbox \mpr@vlist \box \mpr@hlist
-             \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-%    \setbox \mpr@hlist
-%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-%    \setbox \mpr@vlist
-%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
-%              \else \unvbox \mpr@vlist \box \mpr@hlist
-%              \fi}%
-% }
-
-\def \mpr@sep{2em}
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
-  \bgroup
-  \ifx #1T\@premissetrue
-  \else \ifx #1B\@premissefalse
-  \else
-     \PackageError{mathpartir}
-       {Premisse orientation should either be P or B}
-       {Fatal error in Package}%
-  \fi \fi
-  \def \@test {#2}\ifx \@test \mpr@blank\else
-  \setbox \mpr@hlist \hbox {}%
-  \setbox \mpr@vlist \vbox {}%
-  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
-  \let \@hvlist \empty \let \@rev \empty
-  \mpr@tmpdim 0em
-  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
-  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
-  \def \\##1{%
-     \def \@test {##1}\ifx \@test \empty
-        \mpr@htovlist
-        \mpr@tmpdim 0em %%% last bug fix not extensively checked
-     \else
-      \setbox0 \hbox{$\displaystyle {##1}$}\relax
-      \advance \mpr@tmpdim by \wd0
-      %\mpr@tmpdim 1.02\mpr@tmpdim
-      \ifnum \mpr@tmpdim < \hsize
-         \ifnum \wd\mpr@hlist > 0
-           \if@premisse
-             \setbox \mpr@hlist 
-                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
-           \else
-             \setbox \mpr@hlist
-                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
-           \fi
-         \else 
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-         \fi
-      \else
-         \ifnum \wd \mpr@hlist > 0
-            \mpr@htovlist 
-            \mpr@tmpdim \wd0
-         \fi
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-      \fi
-      \advance \mpr@tmpdim by \mpr@sep
-   \fi
-   }%
-   \@rev
-   \mpr@htovlist
-   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
-   \fi
-   \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
-    \let\@@over\over % fallback if amsmath is not loaded
-    \let\@@overwithdelims\overwithdelims
-    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
-    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
-  }{}
-
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
-    $\displaystyle {#1\@@over #2}$}}
-\let \mpr@fraction \mpr@@fraction
-\def \mpr@@reduce #1#2{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@@rewrite #1#2#3{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
-  {\bgroup
-     \ifnum \linewidth<\hsize \hsize \linewidth\fi
-     \mpr@rulelineskip
-     \let \and \qquad
-     \let \hva \mpr@hva
-     \let \@rulename \mpr@empty
-     \let \@rule@options \mpr@empty
-     \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
-  {\everymath={\displaystyle}%       
-   \def \@test {#2}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
-   \else 
-   \def \@test {#3}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
-   \else
-   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
-   \fi \fi
-   \def \@test {#1}\ifx \@test\empty \box0
-   \else \vbox 
-%%% Suggestion de Francois pour les etiquettes longues
-%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
-      {\hbox {\RefTirName {#1}}\box0}\fi
-   \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \inferrule [label]{[premisses}{conclusions}
-% or
-% \inferrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible, 
-% and  vertical breaks if needed. 
-% 
-% An empty element obtained by \\\\ produces a vertical break in all cases. 
-%
-% The former rule is aligned on the fraction bar. 
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-% 
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%       
-%  width                set the width of the rule to val
-%  narrower             set the width of the rule to val\hsize
-%  before               execute val at the beginning/left
-%  lab                  put a label [Val] on top of the rule
-%  lskip                add negative skip on the right
-%  left                 put a left label [Val]
-%  Left                 put a left label [Val],  ignoring its width 
-%  right                put a right label [Val]
-%  Right                put a right label [Val], ignoring its width
-%  leftskip             skip negative space on the left-hand side
-%  rightskip            skip negative space on the right-hand side
-%  vdots                lift the rule by val and fill vertical space with dots
-%  after                execute val at the end/right
-%  
-%  Note that most options must come in this order to avoid strange
-%  typesetting (in particular  leftskip must preceed left and Left and
-%  rightskip must follow Right or right; vdots must come last 
-%  or be only followed by rightskip. 
-%  
-
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\def \mprset #1{\setkeys{mprset}{#1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{sep}{\def\mpr@sep{#1}}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
-\define@key {mpr}{right}
-  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{RIGHT}
-  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-
-\newdimen \rule@dimen
-\newcommand \mpr@inferstar@ [3][]{\setbox0
-  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
-         \setbox \mpr@right \hbox{}%
-         $\setkeys{mpr}{#1}%
-          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
-          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
-          \box \mpr@right \mpr@vdots$}
-  \setbox1 \hbox {\strut}
-  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
-  \raise \rule@dimen \box0}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode 
-    \let \@do \mpr@inferstar@
-  \else 
-    \let \@do \mpr@err@skipargs
-    \PackageError {mathpartir}
-      {\string\inferrule* can only be used in math mode}{}%
-  \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \TirNameStyle #1{\small \textsc{#1}}
-\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
-\let \TirName \tir@name
-\let \DefTirName \TirName
-\let \RefTirName \TirName
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-
-
-\endinput
diff --git a/transfer/doc/typesystem.tex b/transfer/doc/typesystem.tex
deleted file mode 100644
index fb26b064c..000000000
--- a/transfer/doc/typesystem.tex
+++ /dev/null
@@ -1,479 +0,0 @@
-\documentclass[a4paper,11pt]{article}
-\usepackage{mathpartir}
-\usepackage{amssymb}
-
-\begin{document}
-
-\title{Transfer Type Checking}
-\author{Bj\"orn Bringert \\ \texttt{bringert@cs.chalmers.se}}
-\maketitle
-
-\section{Type Checking Algorithm}
-
-This is the beginnings of a type checking algorithm for the 
-Transfer Core language. It is far from complete,
-and some of the rules make no sense at all at the moment.
-
-\subsection{Notation}
-
-$\overline{a}$ is a list of $a$s. 
-
-$x$ stands for variables.
-
-$A$,$B$,$C$ are terms which we use for types.
-
-$s$,$t$ are any terms.
-
-$l$ refers to record labels.
-
-$p$ refers to patterns.
-
-$c$ refers to constructors.
-
-$\Delta$ is a set of constructor typings.
-
-$\Gamma$ is a set of variable typings.
-
-$\Delta;\Gamma \vdash t \uparrow A$ means that in the
-variable typing context $\Gamma$ and the constructor
-typing context $\Delta$, the type of $t$ can be inferred 
-to be $A$.
-
-$\Delta;\Gamma \vdash t \downarrow A$ means that in the
-variable typing context $\Gamma$ and the constructor
-typing context $\Delta$, the type of $t$ can be 
-checked to be $A$.
-
-$\Delta \vdash_p p \downarrow A; \Gamma$ means that
-in the constructor typing context $\Delta$,
-the pattern $p$ can matched against a value of type
-$A$, and if the match succeeds, it will create
-variable bindings with the typings $\Gamma$.
-
-$A \leq B$ means that $A$ is a subtype of of $B$.
-
-$A \lesssim B$ means that $A$ is convertible
-to a subtype of $B$.
-
-\subsection{Language}
-
-\begin{eqnarray*}
-s,t,u & ::= & \textrm{let} \ x = s \ \textrm{in} \ t  \\
-& & | \ \textrm{case} \ s \ \textrm{of} \{ \overline{p \mid t \rightarrow u} \} \\
-& & | \ \lambda x . t \\
-& & | \ (x : s) \rightarrow t \\
-& & | \ s \ t \\
-& & | \ s.l \\
-& & | \ \textrm{sig} \ \{ \overline{l : t} \} \\
-& & | \ \textrm{rec} \ \{ \overline{l = t} \} \\
-& & | \ x \\
-& & | \ Type \\
-& & | \ string \\
-& & | \ integer \\
-& & | \ double \\
-p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ | \ string \ | \ integer 
-\end{eqnarray*}
-
-
-
-\subsection{Rules}
-
-\begin{figure}
-\begin{mathpar}
-
-\inferrule[Type annotation]
-{ \Delta;\Gamma \vdash t \downarrow A }
-{ \Delta;\Gamma \vdash t : A \uparrow A }
-
-\and
-
-\inferrule[Check by inferring]
-{ \Delta;\Gamma \vdash t \uparrow A' \\
-  A' \lesssim A}
-{ \Delta;\Gamma \vdash t \downarrow A }
-
-\and
-
-\inferrule[Variable]
-{ x : A \in \Gamma }
-{ \Delta;\Gamma \vdash x \uparrow A }
-
-\and 
-
-\inferrule[Constructor]
-{ c : A \in \Delta }
-{ \Delta;\Gamma \vdash c \uparrow A }
-
-\and 
-
-\inferrule[Function type]
-{ \Delta;\Gamma \vdash A \downarrow Type \\
-  \Delta;\Gamma, x : A \vdash B \downarrow Type }
-{ \Delta;\Gamma \vdash (x : A) \rightarrow B \downarrow Type }
-
-\and
-
-\inferrule[Abstraction]
-{ \Delta;\Gamma, x : A \vdash s \downarrow B }
-{ \Delta;\Gamma \vdash \lambda x. s \downarrow (x : A) \rightarrow B }
-
-\and 
-
-\inferrule[Application]
-{ \Delta;\Gamma \vdash s \uparrow (x : A) \rightarrow B \\ 
-  \Delta;\Gamma \vdash t \downarrow A
-}
-{ \Delta;\Gamma \vdash s \ t \uparrow B [x / t] }
-
-\and 
-
-\inferrule[Local definition]
-{ \Delta;\Gamma \vdash s \uparrow A \\ 
-  \Delta;\Gamma, x : A \vdash t \uparrow B }
-{ \Delta;\Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t \uparrow B }
-
-\and 
-
-\inferrule[Case analysis]
-{ \Delta;\Gamma \vdash s \uparrow A \\
-  B = B_1 \vee \ldots \vee B_n \\
-  \Delta \vdash_p p_1 \downarrow A; \Gamma_1 \\
-  \Delta;\Gamma,\Gamma_1 \vdash g_1 \downarrow Bool \\
-  \Delta;\Gamma,\Gamma_1 \vdash t_1 \uparrow B_1 \\
-  \ldots \\
-  \Delta p_n \vdash_p A; \Gamma_n \\
-  \Delta;\Gamma, \Gamma_n \vdash g_n \downarrow Bool \\
-  \Delta;\Gamma, \Gamma_n \vdash t_n \uparrow B_n
-}
-{ \Delta;\Gamma \vdash \textrm{case} \ s \ \textrm{of} \ \{ 
-    p_1 \mid g_1 \rightarrow t_1;
-    \ldots;
-    p_n \mid g_n \rightarrow t_n
-  \} \uparrow B }
-
-\end{mathpar}
-\caption{Basics.}
-\label{fig:basics}
-\end{figure}
-
-\begin{figure}
-\begin{mathpar}
-
-\inferrule[Record type]
-{ \Delta;\Gamma \vdash T_1 \uparrow Type \\ 
-  \ldots \\
-  \Delta;\Gamma, l_1 : T_1, \ldots, l_{n-1} : T_{n-1} \vdash T_n \uparrow Type \\
-  l_1 \ldots l_n \ \textrm{different}
-}
-{ \Delta;\Gamma \vdash \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} \uparrow Type }
-
-\and
-
-\inferrule[Record]
-{ \Delta;\Gamma \vdash t_1 \uparrow T_1 \\ 
-  \ldots \\
-  \Delta;\Gamma \vdash t_n \uparrow T_n [l_{n-1} / t_{n-1}] \ldots [l_1 / t_1] \\
-  l_1 \ldots l_n \ \textrm{different} }
-{ \Delta;\Gamma \vdash \textrm{rec} \{ l_1 = t_1, \ldots, l_n = t_n \} 
-  \uparrow \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} }
-
-\and 
-
-\inferrule[Record projection]
-{ \Delta;\Gamma \vdash t \downarrow \textrm{sig} \{ l : T \} }
-{ \Delta;\Gamma \vdash t . l \uparrow T }
-
-\end{mathpar}
-\caption{Records.}
-\label{fig:records}
-\end{figure}
-
-
-\begin{figure}
-\begin{mathpar}
-
-\inferrule[Variable pattern]
-{  }
-{ \Delta \vdash_p x \downarrow \ A; \{ x : A \} }
-
-\and 
-
-\inferrule[Wildcard pattern]
-{  }
-{ \Delta \vdash_p \_ \ \downarrow \ A; \{ \} }
-
-\and 
-
-\inferrule[Constructor pattern]
-{ c : (x_1 : T_1) \rightarrow \ldots \rightarrow (x_n : T_n) \rightarrow T' \in \Delta \\
-  T' = T \\
-  \Delta \vdash_p p_1 \downarrow T_1; \Gamma_1 \\
-  \ldots \\
-  \Delta \vdash_p p_n \downarrow T_n; \Gamma_n \\
-  \Gamma_1 \ldots \Gamma_n \ \textrm{disjoint} \\
-  \textrm{FIXME: $x_k$ can occur in $T_{k+1}$}
-  }
-{ \Delta \vdash_p c \ p_1 \ldots p_n \ \downarrow \ T; \Gamma_1, \ldots, \Gamma_n }
-
-\and 
-
-\inferrule[Record pattern]
-{ \textrm{FIXME: allow more fields in type, ignore order} \\
-  \textrm{FIXME: types can depend on field values} \\
-\Delta \vdash_p p_1 \ \downarrow \ T_1; \Gamma_1 \\
-  \ldots \\
-  \Delta \vdash_p p_n \ \downarrow \ T_n; \Gamma_n \\
-  \Gamma_1 \ldots \Gamma_n \ \textrm{disjoint} \\
-  l_1 \ldots l_n \ \textrm{different}
-  }
-{ \Delta \vdash_p \textrm{rec} \ \{ l_1 = p_1; \ldots; l_n = p_n \} \ \downarrow \ 
-  \textrm{sig} \ \{ l_1 : T_1; \ldots; l_n : T_n \}; \Gamma_1, \ldots, \Gamma_n }
-
-\and 
-
-\inferrule[Integer literal pattern]
-{  }
-{ \Delta \vdash_p integer \ \downarrow \ Integer; \{ \} }
-
-\and 
-
-\inferrule[String literal pattern]
-{  }
-{ \Delta \vdash_p string \ \downarrow \ String; \{ \} }
-
-\and 
-
-\end{mathpar}
-\caption{Type-checking patterns.}
-\label{fig:typing-patterns}
-\end{figure}
-
-
-
-
-
-\begin{figure}
-\begin{mathpar}
-
-\inferrule[Integer type]
-{ }
-{ \Delta;\Gamma \vdash Integer \uparrow Type }
-
-\and 
-
-\inferrule[Integer literal]
-{ }
-{ \Delta;\Gamma \vdash integer \uparrow Integer }
-
-\and 
-
-\inferrule[Double type]
-{ }
-{ \Delta;\Gamma \vdash Double \uparrow Type }
-
-\and 
-
-\inferrule[Double literal]
-{ }
-{ \Delta;\Gamma \vdash double \uparrow Double }
-
-\and 
-
-\inferrule[String type]
-{ }
-{ \Delta;\Gamma \vdash String \uparrow Type }
-
-\and 
-
-\inferrule[String literal]
-{ }
-{ \Delta;\Gamma \vdash string \uparrow String }
-
-\end{mathpar}
-\caption{Primitive types.}
-\label{fig:primitive-types}
-\end{figure}
-
-\begin{figure}
-\begin{mathpar}
-
-\inferrule[Subtype conversion]
-{ \vdash s \Downarrow_{wh} s' \\
-  \vdash t \Downarrow_{wh} t' \\
-  s' \leq t' }
-{ s \lesssim t }
-
-\and 
-
-\inferrule[Function type conversion]
-{ A_2 \lesssim A_1 \\
-  B_1 [x_1/z] \lesssim B_2 [x_2/z] }
-{ (x_1 : A_1) \rightarrow B_1 
-  \leq (x_2 : A_2) \rightarrow B_2 }
-
-\and 
-
-\inferrule[Constructor conversion]
-{ s_1 \lesssim t_1 \\ 
-  \ldots \\ 
-  s_n \lesssim t_n \\ 
-}
-{ c \ s_1 \ldots s_n \leq c \ t_1 \ldots t_n }
-
-\and 
-
-\inferrule[Record type conversion]
-{ A_1 \lesssim B_1 \ldots A_n \lesssim B_n \\ 
-  \textrm{FIXME: types can depend on fields} \\
-  \textrm{FIXME: allow more fields on the left, ignore order} }
-{ \textrm{sig} \ \{ l_1 : A_1 \ldots l_n : A_n \} 
-  \leq 
-  \textrm{sig} \ \{ k_1 : B_1 \ldots k_m : B_m \}  }
-
-\and 
-
-\inferrule[Record conversion]
-{ 
-  \textrm{FIXME: allow more fields on the left, ignore order} \\
-  s_1 \lesssim t_1 \ldots s_n \lesssim s_n
-}
-{ \textrm{rec} \ \{ l_1 = s_1 \ldots l_n = s_n \} 
-  \leq 
-  \textrm{rec} \ \{ k_1 = t_1 \ldots k_m = t_m \}  }
-
-\and 
-
-\inferrule[Integer conversion]
-{ i_1 \ \textrm{integer} \\
-  i_2 \ \textrm{integer} \\
-  i_1 =_{integer} i_2}
-{ i_1 \leq i_2 }
-
-\and 
-
-\inferrule[String conversion]
-{ i_1 \ \textrm{string} \\
-  i_2 \ \textrm{string} \\
-  i_1 =_{string} i_2}
-{ i_1 \leq i_2 }
-
-\and 
-
-\inferrule[Double conversion]
-{ i_1 \ \textrm{double} \\
-  i_2 \ \textrm{double} \\
-  i_1 =_{double} i_2}
-{ i_1 \leq i_2 }
-
-\end{mathpar}
-\caption{Conversion and subtyping.}
-\label{fig:conversion}
-\end{figure}
-
-\begin{figure}
-\begin{mathpar}
-
-\inferrule[WHNF-Let]
-{ s \Downarrow_{wh} s' \\ 
-  \textrm{This is a weird way to evaluate a let} }
-{ \Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t 
-                \Downarrow_{wh} t [x/s']
-}
-
-\and
-
-\inferrule[WHNF-Case]
-{ \textrm{FIXME: find the right case arm} \\
-  \textrm{FIXME: bind / substitute variables in RHS} }
-{ \Gamma \vdash \textrm{case} \ s \ \textrm{of} \{ \overline{p \mid t \rightarrow u} \}
-  \Downarrow_{wh}
-}
-
-\and
-
-\inferrule[WHNF-Beta]
-{ \Gamma \vdash s \Downarrow_{wh} \lambda x . s' \\
-  \Gamma \vdash t \Downarrow_{wh} t' }
-{ \Gamma \vdash s \ t \Downarrow_{wh} s' [x/t'] \}
-}
-
-\and
-
-\inferrule[WHNF-Proj]
-{ \Gamma \vdash s \Downarrow_{wh} \textrm{rec} \ \{ \ldots, l = t, \ldots \} }
-{ \Gamma \vdash s.l \Downarrow_{wh} t }
-
-\and
-
-\inferrule[WHNF-Var]
-{ x = t \in \Gamma \\
-  \textrm{FIXME: there shouldn't be any free variables (but there can be functions and constructors)} }
-{ \Gamma \vdash x \Downarrow_{wh} t }
-
-
-% unchanged:
-
-\and
-
-\inferrule[WHNF-Lambda]
-{ }
-{ \Gamma \vdash \lambda x . t \Downarrow_{wh} \lambda x . t }
-
-\and
-
-\inferrule[WHNF-Pi]
-{ }
-{ \Gamma \vdash (x : s) \rightarrow t \Downarrow_{wh} (x : s) \rightarrow t
-}
-
-\and
-
-\inferrule[WHNF-Sig]
-{ }
-{ \Gamma \vdash \textrm{sig} \ \{ l_1 : A_1, \ldots, l_n : A_n \} 
-   \Downarrow_{wh} \textrm{sig} \ \{ l_1 : A_1, \ldots, l_n : A_n \} }
-
-\and
-
-\inferrule[WHNF-Rec]
-{ }
-{ \Gamma \vdash \textrm{rec} \ \{ l_1 = t_1, \ldots, l_n = t_n \} 
-   \Downarrow_{wh} \textrm{rec} \ \{ l_1 = t_1, \ldots, l_n = t_n \} }
-
-\and
-
-\inferrule[WHNF-Type]
-{ }
-{ \Gamma \vdash Type \Downarrow_{wh} Type }
-
-\and
-
-\inferrule[WHNF-String]
-{ }
-{ \Gamma \vdash string \Downarrow_{wh} string }
-
-\and
-
-\inferrule[WHNF-Integer]
-{ }
-{ \Gamma \vdash integer \Downarrow_{wh} integer }
-
-\and
-
-\inferrule[WHNF-Double]
-{ }
-{ \Gamma \vdash double \Downarrow_{wh} double }
-
-% FIXME: applications which are not beta redexes?
-
-
-
-
-\end{mathpar}
-\caption{Weak head normal form evaluation.}
-\label{fig:whnf-evaluation}
-\end{figure}
-
-
-
-\end{document}