msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

Transfer: added beginnings of a type checking algorithm description.

Browse Source
This commit is contained in:
bringert
2006-03-03 10:37:59 +00:00
parent 61898554b5
commit dd0d26c022
3 changed files with 636 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

41
transfer/doc/Makefile Normal file
View File

@@ -0,0 +1,41 @@
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

390
transfer/doc/mathpartir.sty Normal file
View File

@@ -0,0 +1,390 @@
% 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

205
transfer/doc/typesystem.tex Normal file
View File

@@ -0,0 +1,205 @@
\documentclass[a4paper,11pt]{article}
\usepackage{mathpartir}
\begin{document}
\title{Transfer Type Checking}
\author{Bj\"orn Bringert \\ \texttt{bringert@cs.chalmers.se}}
\maketitle
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.
\begin{figure}
\begin{mathpar}
\inferrule[Type annotation]
{ \Gamma \vdash t \downarrow A }
{ \Gamma \vdash t : A \uparrow A }
\and
\inferrule[Variable]
{ x : A \in \Gamma }
{ \Gamma \vdash x \uparrow A }
\and
\inferrule[Function type]
{ \Gamma \vdash A \uparrow Type \\
\Gamma, x : A \vdash B \uparrow Type }
{ \Gamma \vdash (x : A) \rightarrow B \uparrow Type }
\and
\inferrule[Abstraction]
{ \Gamma, x : A \vdash s \uparrow B }
{ \Gamma \vdash \lambda x. s \downarrow (x : A) \rightarrow B }
\and
\inferrule[Application]
{ \Gamma \vdash s \uparrow (x : A) \rightarrow B \\
\Gamma \vdash t \downarrow A }
{ \Gamma \vdash s t \uparrow B [x / t] }
\and
\inferrule[Local definition]
{ \Gamma \vdash s \uparrow A \\
\Gamma, s : A \vdash t \uparrow B }
{ \Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t \uparrow B }
\and
\inferrule[Case analysis]
{ \Gamma \vdash t \uparrow A \\
\Gamma \vdash p_1 \downarrow A, \Gamma' \\
\Gamma, \Gamma' \vdash g_1 \downarrow Bool \\
\Gamma, \Gamma' \vdash t_1 \uparrow B \\
\ldots \\
p_n \textrm{match} A, \Gamma' \\
\Gamma, \Gamma' \vdash g_n \downarrow Bool \\
\Gamma, \Gamma' \vdash t_n \uparrow B \\
}
{ \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[Variable pattern]
{ }
{ x \ \textrm{match} \ A, \{ x : A \} }
\and
\inferrule[Wildcard pattern]
{ }
{ \_ \ \textrm{match} \ A, \{ \} }
\and
\inferrule[Constructor pattern]
{ C : (x_1 : T_1) \rightarrow \ldots \rightarrow T \in \Delta \\
p_1 \textrm{match} T_1, \Gamma_1 \\
\ldots \\
p_n \textrm{match} T_n, \Gamma_n \\
}
{ C p_1 \ldots p_n \ \textrm{match} \ T, \Gamma_1, \ldots, \Gamma_n }
\and
\inferrule[Record pattern]
{ p_1 \ \textrm{match} \ T_1, \Gamma_1 \\
\ldots \\
p_n \ \textrm{match} \ T_n, \Gamma_n \\
}
{ \textrm{rec} \ \{ l_1 = p_1; \ldots; l_n = p_n \} \ \textrm{match} \
\textrm{sig} \ \{ l_1 : T_1; \ldots; l_n : T_n \}, \Gamma_1, \ldots, \Gamma_n }
\and
\inferrule[Integer literal pattern]
{ }
{ integer \ \textrm{match} \ Integer, \{ \} }
\and
\inferrule[String literal pattern]
{ }
{ string \ \textrm{match} \ String, \{ \} }
\and
\end{mathpar}
\caption{Patterns.}
\label{fig:patterns}
\end{figure}
\begin{figure}
\begin{mathpar}
\inferrule[Record type]
{ \Gamma \vdash T_1 \uparrow Type \\
\ldots \\
\Gamma, l_1 : T_1, \ldots, l_{n-1} : T_{n-1} \vdash T_n \uparrow Type }
{ \Gamma \vdash \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} \uparrow Type }
\and
\inferrule[Record]
{ \Gamma \vdash t_1 \uparrow T_1 \\
\ldots \\
\Gamma \vdash t_n \uparrow T_n [l_{n-1} / t_{n-1}] \ldots [l_1 / t_1] }
{ \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]
{ \Gamma \vdash t \uparrow \textrm{sig} \{ l : T \} }
{ \Gamma \vdash t . l \uparrow T }
\end{mathpar}
\caption{Records.}
\label{fig:records}
\end{figure}
\begin{figure}
\begin{mathpar}
\inferrule[Integer type]
{ }
{ \Gamma \vdash Integer \uparrow Type }
\and
\inferrule[Integer literal]
{ }
{ \Gamma \vdash integer \uparrow Integer }
\and
\inferrule[Double type]
{ }
{ \Gamma \vdash Double \uparrow Type }
\and
\inferrule[Double literal]
{ }
{ \Gamma \vdash double \uparrow Double }
\and
\inferrule[String type]
{ }
{ \Gamma \vdash String \uparrow Type }
\and
\inferrule[String literal]
{ }
{ \Gamma \vdash string \uparrow String }
\end{mathpar}
\caption{Primitive types.}
\label{fig:primitive-types}
\end{figure}
\end{document}