%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[a4paper,10pt]{article}

\usepackage[utf8x]{inputenc}
\usepackage[frenchb]{babel}
\usepackage{listings}
\usepackage{mathpartir}
\usepackage{amsmath}
\usepackage{amssymb}

\lstset{basicstyle=\ttfamily}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\astProgram}[2]{#1 \; #2}
\newcommand{\astClass}[3]{\mathtt{class~} #1 \; \triangleleft \; #2 \; \{ \, #3 \, \}}
\newcommand{\astNone}{\mathtt{none}}
\newcommand{\astField}[3]{\mathtt{field~} #1 : #2 \; = \; #3}
\newcommand{\astMethod}[5]{\mathtt{method~} #1 \; \mathtt{(} \, #2 : #3 \, \mathtt{)} : #4 \; = \; #5}
\newcommand{\astInt}{\mathtt{Int}}
\newcommand{\astNothing}{\mathtt{Null}}
\newcommand{\astNew}[1]{\mathtt{new~} #1}
\newcommand{\astNull}{\mathtt{null}}
\newcommand{\astThis}{\mathtt{this}}
\newcommand{\astRead}[2]{#1.#2}
\newcommand{\astCall}[3]{#1.#2(#3)}
\newcommand{\astWrite}[3]{#1.#2 \; = \; #3}
\newcommand{\astIf}[3]{\mathtt{if~} #1 \mathtt{~then~} #2 \mathtt{~else~} #3}
\newcommand{\astEq}[2]{#1 \, = \, #2}
\newcommand{\astBinop}[3]{#1 \, #2 \, #3}
\newcommand{\astReadInt}{\mathtt{readInt}}
\newcommand{\astReadChar}{\mathtt{readChar}}
\newcommand{\astPrintInt}[1]{\mathtt{printInt}(#1)}
\newcommand{\astPrintChar}[1]{\mathtt{printChar}(#1)}
\newcommand{\astBlock}[2]{\{ \; #1 \mathtt{~return~} #2 \; \}}

\newcommand{\sClass}[3]{(#1\,|\,#2\,|\,#3)_c}
\newcommand{\sField}[1]{(#1)_f}
\newcommand{\sMethod}[2]{(#1\,|\,#2)_m}
\newcommand{\sParam}[1]{(#1)_p}
\newcommand{\sBind}[2]{#1 \mapsto #2}

\newcommand{\rProg}[2]{#1 \; #2 \; \diamond}
\newcommand{\rClassDef}[3]{#1 \, \vdash \, #2 \; \Rightarrow \; #3}
\newcommand{\rMemberDef}[3]{#1 \, \vdash \, #2 \; \Rrightarrow \; #3}
\newcommand{\rClass}[1]{\Gamma_c \, \vdash \, #1 \; \diamond}
\newcommand{\rMember}[2]{\Gamma_c \, ; \, #1 \, \vdash \, #2 \; \diamond}
\newcommand{\rType}[1]{\Gamma_c \, \vdash \, #1 \; \diamond}
\newcommand{\rSub}[2]{\Gamma_c \, \vdash \, #1 \triangleleft #2}
\newcommand{\rLub}[3]{\Gamma_c \, \vdash \, #1 \triangleleft #3 \triangleright #2}
\newcommand{\rTerm}[3]{\Gamma_c \, ; \, #1 \, \vdash \, #2 : #3}

\newcommand{\rfFieldEnv}[1]{fields(#1)}
\newcommand{\rfMethodEnv}[1]{methods(#1)}
\newcommand{\rfParamEnv}[2]{params(#1 : #2)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Le langage \emph{Vier}}
\author{pour le cours de construction de compilateurs de 2007}
\date{révision $\gamma_7$}

\begin{document}
\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section*{Grammaire lexicale}
\begin{tabular}{rrl}
input      & $::=$ & \{ whitespace $|$ comment $|$ token \} \\
token      & $::=$ & \emph{ident} \\
             & $|$ & \emph{number} \\
             & $|$ & \emph{string} \\
             & $|$ & ``\lstinline@true@'' $\;\;|\;\;$ ``\lstinline@false@'' \\
             & $|$ & `\lstinline@(@' $\;\;|\;\;$ `\lstinline@)@' $\;\;|\;\;$ `\lstinline@{@' $\;\;|\;\;$ `\lstinline@}@' \\
             & $|$ & `\lstinline@=@' $\;\;|\;\;$ `\lstinline@:@' $\;\;|\;\;$ `\lstinline@;@' $\;\;|\;\;$ `\lstinline@.@' \\
             & $|$ & ``\lstinline@class@'' $\;\;|\;\;$ ``\lstinline@extends@'' \\
             & $|$ & ``\lstinline@field@'' $\;\;|\;\;$ ``\lstinline@method@'' \\
             & $|$ & ``\lstinline@Int@'' $\;\;|\;\;$ ``\lstinline@Null@'' \\
             & $|$ & ``\lstinline@new@'' $\;\;|\;\;$ ``\lstinline@null@'' $\;\;|\;\;$ ``\lstinline@this@'' \\
             & $|$ & ``\lstinline@if@'' $\;\;|\;\;$ ``\lstinline@then@'' $\;\;|\;\;$ ``\lstinline@else@'' \\
             & $|$ & ``\lstinline@readInt@'' $\;\;|\;\;$ ``\lstinline@readChar@'' \\
             & $|$ & ``\lstinline@printInt@'' $\;\;|\;\;$ ``\lstinline@printChar@'' \\
             & $|$ & ``\lstinline@return@'' \\
             & $|$ & `\lstinline@+@' $\;\;|\;\;$ `\lstinline@-@' $\;\;|\;\;$ `\lstinline@*@' $\;\;|\;\;$ `\lstinline@/@' $\;\;|\;\;$ `\lstinline@%@' \\
             & $|$ & ``\lstinline@==@'' $\;\;|\;\;$ `\lstinline@<@' $\;\;|\;\;$ `\lstinline@>@' $\;\;|\;\;$ ``\lstinline@&&@'' $\;\;|\;\;$ ``\lstinline@||@'' \\
comment    & $::=$ & ``\lstinline@//@'' \{ cchar \} \\
\emph{ident}      & $::=$ & letter \{ letter $|$ digit $|$ `\lstinline@_@' \} \\
\emph{number}     & $::=$ & `\lstinline@0@' $\;\;|\;\;$ digit1 \{ digit \} \\
\emph{string}     & $::=$ & `\lstinline@"@' \{ schar \} `\lstinline@"@' \\
letter     & $::=$ & `\lstinline@a@' $|$ $\cdots$ $|$ `\lstinline@z@' $|$ `\lstinline@A@' $|$ $\cdots$ $|$  `\lstinline@Z@' \\
digit      & $::=$ & `\lstinline@0@' $|$ digit1 \\
digit1     & $::=$ & `\lstinline@1@' $|$ $\cdots$ $|$ `\lstinline@9@' \\
\end{tabular}

\medskip
\noindent Un caractère est ``whitespace'' si la méthode ``\lstinline@Character.isWhitespace@'' de la librairie Java l'accepte. Un caractère est ``cchar'' s'il ne définit pas de nouvelle ligne. Un caractère est ``schar'' s'il est ``cchar'' et pas `\lstinline@"@'.

\medskip
\noindent Dans la grammaire lexicale, ``abc'' doit être lu comme `a' `b' `c'.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section*{Grammaire syntaxique}
\begin{tabular}{rrl}
Program       & $::=$ & \{ ClassDef \} Expr \\
ClassDef      & $::=$ & ``\lstinline@class@'' \emph{ident} [ ``\lstinline@extends@'' \emph{ident} ] `\lstinline@{@' \{ Member \} `\lstinline@}@' \\
Member        & $::=$ & FieldDef \\
                & $|$ & MethDef \\
Type          & $::=$ & \emph{ident} $\;\;|\;\;$ ``\lstinline@Int@'' $\;\;|\;\;$ ``\lstinline@Null@'' \\
Formal        & $::=$ & \emph{ident} `\lstinline@:@' Type \\
Formals       & $::=$ & [ Formal \{ `\lstinline@;@' Formal \} ] \\
FieldDef      & $::=$ & ``\lstinline@field@'' Formal `\lstinline@=@' Expr \\
MethDef       & $::=$ & ``\lstinline@method@'' \emph{ident} `\lstinline@(@' Formals `\lstinline@)@' `\lstinline@:@' Type `\lstinline@=@' Expr \\
Expr          & $::=$ & ``\lstinline@if@'' Expr ``\lstinline@then@'' Expr ``\lstinline@else@'' Expr \\
                & $|$ & CmpExpr \\
CmpOp         & $::=$ & ``\lstinline@==@'' $\;\;|\;\;$ `\lstinline@<@' $\;\;|\;\;$ `\lstinline@>@' \\
CmpExpr       & $::=$ & [ SumExpr CompOp ] SumExpr \\
SumOp         & $::=$ & `\lstinline@+@' $\;\;|\;\;$ `\lstinline@-@' $\;\;|\;\;$ ``\lstinline@||@'' \\
SumExpr       & $::=$ & [ SumExpr SumOp ] Term \\
ProdOp        & $::=$ & `\lstinline@*@' $\;\;|\;\;$ `\lstinline@/@' $\;\;|\;\;$ `\lstinline@%@' $\;\;|\;\;$ ``\lstinline@&&@'' \\
Term          & $::=$ & [ Term ProdOp ] Factor \\
Factor        & $::=$ & \emph{ident} \\
                & $|$ & \emph{number} \\
                & $|$ & \emph{string} \\
                & $|$ & ``\lstinline@true@'' $\;\;|\;\;$ ``\lstinline@false@'' \\
                & $|$ & ``\lstinline@null@'' $\;\;|\;\;$ ``\lstinline@this@'' \\
                & $|$ & ``\lstinline@new@'' Type \\
                & $|$ & Factor `\lstinline@.@' \emph{ident} \\
                & $|$ & Factor `\lstinline@.@' `\lstinline@{@' Assigns `\lstinline@}@' \\
                & $|$ & Factor `\lstinline@.@' \emph{ident} `\lstinline@(@' Exprs `\lstinline@)@' \\
                & $|$ & `\lstinline@(@' Expr `\lstinline@)@' \\
                & $|$ & `\lstinline@{@' Exprs ``\lstinline@return@'' Expr `\lstinline@}@' \\
                & $|$ & ``\lstinline@readInt@'' $\;\;|\;\;$ ``\lstinline@readChar@'' \\
                & $|$ & ``\lstinline@printInt@'' `\lstinline@(@' Expr `\lstinline@)@' \\
                & $|$ & ``\lstinline@printChar@'' `\lstinline@(@' Expr `\lstinline@)@' \\
Exprs         & $::=$ & [ Expr \{ `\lstinline@;@' Expr \} ] \\
Assigns       & $::=$ & \emph{ident} `\lstinline@=@' Expr \{ `\lstinline@;@' \emph{ident} `\lstinline@=@' Expr \} \\
\end{tabular}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection*{Sucre syntaxique}
\begin{tabular}{r|l}
\text{Syntaxe concrète} & \text{Syntaxe abstraite} \\
\hline
\lstinline@true@ & $1$ \\
\lstinline@false@ & $0$ \\
$e$ \lstinline@||@ $f$ & $\neg(\astBinop{\neg e}{\land}{\neg e'})$ \\
$\neg e$ & $\astIf{\astEq{e}{0}}{1}{0}$ \\
$e$ \lstinline@.{@ $a$ \lstinline@=@ $f$ \lstinline@}@ & $\astWrite{e}{a}{f}$ \\
$e$ \lstinline@.{@ $a$ \lstinline@=@ $f$ \lstinline@; ... }@ &
	$(\astWrite{e}{a}{f})$ \lstinline@.{@ ... \lstinline@}@ \\
\lstinline@""@ & \lstinline@new Nil@ \\
\lstinline@"a..."@ & \lstinline@(new Cons).{ head = a; tail = "..." }@ \\
\end{tabular}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section*{Grammaire abstraite}
$$\begin{array}{lrrll}
\multicolumn{3}{l}{\text{nom référençable}} & a, b \\
\multicolumn{3}{l}{\text{nom de classe}} & t, u \\
\text{nombre}      &    n &&& \\
\text{programme}   &    P & ::= & \astProgram{\overline{D}}{e} & \\
\text{classe}      &    D & ::= & \astClass{t}{s}{\overline{d}} & \\
                   &    s & ::= & t & \\
                           && | & \astNone & \\
\text{membre}      &    d & ::= & \astField{a}{T}{e} & \\
                           && | & \astMethod{a}{\overline{a}}{\overline{T}}{T}{e} & \\
\text{type}        & T, U & ::= & t & \\
                           && | & \astInt & \\
                           && | & \astNothing & \\
\text{expression}  & e, f & ::= & a & \text{paramètre} \\
                           && | & n & \text{nombre} \\
                           && | & \astNew{t} & \text{nouvelle instance} \\
                           && | & \astNull & \text{valeur ``\lstinline@null@''} \\
                           && | & \astRead{e}{a} & \text{sélection de champ} \\
                           && | & \astCall{e}{a}{\overline{e}} & \text{appel de méthode} \\
                           && | & \astWrite{e}{a}{e} & \text{assignation de champ} \\
                           && | & \astIf{e}{e}{e} & \text{condition ``\lstinline@if@''} \\
                           && | & \astEq{e}{e} & \text{comparaison binaire} \\
                           && | & \astBinop{e}{p}{e} & \text{op. binaire} \\
                           && | & \astReadInt & \text{op. ``\lstinline@readInt@''} \\
                           && | & \astReadChar & \text{op. ``\lstinline@readChar@''} \\
                           && | & \astPrintInt{e} & \text{op. ``\lstinline@printInt@''} \\
                           && | & \astPrintChar{e} & \text{op. ``\lstinline@printChar@''} \\
                           && | & \astBlock{\overline{e}}{e} & \text{block} \\
\text{opérateur}   &    p & ::= & \multicolumn{2}{l}{+|-|\ast|\div|\%|<|>|\land} \\
\end{array}$$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section*{Validité du typage}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection*{Symboles et portées}
$$
\begin{array}{lrcl}
\text{symbole de classe}     & \sigma_c & ::= & \sClass{\overline{t}}{\Gamma_f}{\Gamma_m} \\
\text{symbole de champ}      & \sigma_f & ::= & \sField{T} \\
\text{symbole de méthode}    & \sigma_m & ::= & \sMethod{\overline{T}}{T} \\
\text{symbole de paramètre}  & \sigma_p & ::= & \sParam{T} \\
&&& \\
\text{portée des classes}    & \Gamma_c & ::= & \sBind{\overline{t}}{\overline{\sigma_c}} \\
\text{portée des champs}     & \Gamma_f & ::= & \sBind{\overline{a}}{\overline{\sigma_f}} \\
\text{portée des méthodes}   & \Gamma_m & ::= & \sBind{\overline{a}}{\overline{\sigma_m}} \\
\text{portée des paramètres} & \Gamma_p & ::= & \sBind{\overline{a}}{\overline{\sigma_p}} \\
\end{array}
$$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection*{Règles de typage}

%%%%%%%%%%%%%

\paragraph{Validité d'un programme} $\rProg{\overline{D}}{e}$
\begin{mathpar}
\inferrule
	{
		\rClassDef{\sBind{\astNone}{\sClass{\epsilon}{\epsilon}{\epsilon}}}{\overline{D}}{\Gamma_c'} \\
		\rMemberDef{\Gamma_c'}{\overline{D}}{\Gamma_c} \\
		\rClass{\overline{D}} \\
		\rTerm{\epsilon}{e}{T}
	}
	{\rProg{\overline{D}}{e}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Validité de l'héritage entre classes} $\rClassDef{\Gamma_c}{D}{\Gamma_c'}$
\begin{mathpar}
\inferrule
	{
		\sBind{s}{\sClass{\overline{s}}{\epsilon}{\epsilon}} \in \Gamma_c \\
		\Gamma_c' = \Gamma_c \uplus \sBind{t}{\sClass{s,\overline{s}}{\epsilon}{\epsilon}}
	}
	{\rClassDef{\Gamma_c}{\astClass{t}{s}{\overline{d}}}{\Gamma_c'}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Validité de la déclaration des membres} $\rMemberDef{\Gamma_c}{D}{\Gamma_c'}$
\begin{mathpar}
\inferrule
	{
		\sBind{s}{\sClass{\overline{s}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \\
		\Gamma_f' = \Gamma_f + \rfFieldEnv{\overline{d}} \\
		\Gamma_m' = \Gamma_m + \rfMethodEnv{\overline{d}} \\
		\Gamma_c' = \Gamma_c + \sBind{t}{\sClass{s,\overline{s}}{\Gamma_f'}{\Gamma_m'}}
	}
	{\rMemberDef{\Gamma_c}{\astClass{t}{s}{\overline{d}}}{\Gamma_c'}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Validité d'une classe} $\rClass{D}$
\begin{mathpar}
\inferrule
	{
		\rMember{\sBind{\astThis}{\sParam{t}}}{\overline{d}}
	}
	{\rClass{\astClass{t}{s}{\overline{d}}}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Validité d'un membre} $\rMember{\Gamma_p}{d}$
\begin{mathpar}
\inferrule
	{
		\sBind{\astThis}{\sParam{t}} \in \Gamma_p \\\\
			\left.\begin{array}{r}
				\sBind{t}{\sClass{s,\overline{s}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \endline
				\sBind{s}{\sClass{\overline{s}}{\Gamma_f'}{\Gamma_m'}} \in \Gamma_c \endline
				\sBind{a}{\sField{T'}} \in \Gamma_f' \endline
			\end{array}\right\}
		\Rightarrow T = T' \\
		\rType{T} \\
		\rTerm{\Gamma_p}{e}{U} \\
		\rSub{U}{T}
	}
	{\rMember{\Gamma_p}{\astField{a}{T}{e}}}
\and
\inferrule
	{
		\sBind{\astThis}{\sParam{t}} \in \Gamma_p \\\\
			\left.\begin{array}{r}
				\sBind{t}{\sClass{s,\overline{s}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \endline
				\sBind{s}{\sClass{\overline{s}}{\Gamma_f'}{\Gamma_m'}} \in \Gamma_c \endline
				\sBind{a}{\sMethod{\overline{T'}}{T'}} \in \Gamma_m' \endline
			\end{array}\right\}
		\Rightarrow \rSub{T}{T'} \land \rSub{\overline{T'}}{\overline{T}} \\
		\rType{T} \\
		\rType{\overline{T}} \\
		\rTerm{\Gamma_p + \rfParamEnv{\overline{a}}{\overline{T}}}{e}{U} \\
		\rSub{U}{T}
	}
	{\rMember{\Gamma_p}{\astMethod{a}{\overline{a}}{\overline{T}}{T}{e}}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Validité d'une expression} $\rTerm{\Gamma_p}{e}{T}$
\begin{mathpar}
\inferrule
	{
		\sBind{a}{\sParam{T}} \in \Gamma_p
	}
	{\rTerm{\Gamma_p}{a}{T}}
\and
\inferrule
	{}
	{\rTerm{\Gamma_p}{n}{\astInt}}
\and
\inferrule
	{
		\sBind{t}{\sClass{\overline{t}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \\
	}
	{\rTerm{\Gamma_p}{\astNew{t}}{t}}
\and
\inferrule
	{}
	{\rTerm{\Gamma_p}{\astNull}{\astNothing}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{t} \\
		\sBind{t}{\sClass{\overline{t}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \\
		\sBind{a}{\sField{U}} \in \Gamma_f \\
	}
	{\rTerm{\Gamma_p}{\astRead{e}{a}}{U}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{t} \\
		\sBind{t}{\sClass{\overline{t}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \\\\
		\sBind{a}{\sMethod{\overline{U}}{U}} \in \Gamma_m \\
		\rTerm{\Gamma_p}{\overline{e}}{\overline{T}} \\
		\rSub{\overline{T}}{\overline{U}}
	}
	{\rTerm{\Gamma_p}{\astCall{e}{a}{\overline{e}}}{U}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{t} \\
		\sBind{t}{\sClass{\overline{t}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \\\\
		\sBind{a}{\sField{U}} \in \Gamma_f \\
		\rTerm{\Gamma_p}{f}{T} \\
		\rSub{T}{U}
	}
	{\rTerm{\Gamma_p}{\astWrite{e}{a}{f}}{t}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{\astInt} \\
		\rTerm{\Gamma_p}{f}{U} \\
		\rTerm{\Gamma_p}{f'}{U'} \\
		\rLub{U}{U'}{T}
	}
	{\rTerm{\Gamma_p}{\astIf{e}{f}{f'}}{T}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{T} \\
		\rTerm{\Gamma_p}{e'}{T'} \\
		\rSub{T}{T'} \lor \rSub{T'}{T}
	}
	{\rTerm{\Gamma_p}{\astEq{e}{e'}}{\astInt}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{\astInt} \\
		\rTerm{\Gamma_p}{e'}{\astInt} \\
	}
	{\rTerm{\Gamma_p}{\astBinop{e}{p}{e'}}{\astInt}}
\and
\inferrule
	{}
	{\rTerm{\Gamma_p}{\astReadInt}{\astInt}}
\and
\inferrule
	{}
	{\rTerm{\Gamma_p}{\astReadChar}{\astInt}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{\astInt}
	}
	{\rTerm{\Gamma_p}{\astPrintInt{e}}{\astInt}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{e}{\astInt}
	}
	{\rTerm{\Gamma_p}{\astPrintChar{e}}{\astInt}}
\and
\inferrule
	{
		\rTerm{\Gamma_p}{\overline{e}}{\overline{U}} \\
		\rTerm{\Gamma_p}{f}{T}
	}
	{\rTerm{\Gamma_p}{\astBlock{\overline{e}}{f}}{T}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Validité d'un type} $\rType{T}$
\begin{mathpar}
\inferrule
	{
		\sBind{t}{\sClass{\overline{t}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c
	}
	{\rType{t}}
\and
\inferrule
	{}
	{\rType{\astNothing}}
\and
\inferrule
	{}
	{\rType{\astInt}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Sous-typage} $\rSub{T}{T}$
\begin{mathpar}
\inferrule
	{
		\sBind{t}{\sClass{\overline{t}}{\Gamma_f}{\Gamma_m}} \in \Gamma_c \\
		u \in \overline{t} \lor u = t
	}
	{\rSub{t}{u}}
\and
\inferrule
	{}
	{\rSub{\astNothing}{t}}
\and
\inferrule
	{}
	{\rSub{\astNothing}{\astNothing}}
\and
\inferrule
	{}
	{\rSub{\astInt}{\astInt}}
\end{mathpar}

%%%%%%%%%%%%%

\paragraph{Borne supérieure} $\rLub{T}{T}{T}$
\begin{mathpar}
\inferrule
	{
		\rSub{T}{U} \\
		\rSub{T'}{U} \\
		\forall U' \, . \, 
			\left.\begin{array}{r}
				\rSub{T}{U'} \endline
				\rSub{T'}{U'}
			\end{array}\right\}
		\Rightarrow \rSub{U}{U'}
	}
	{\rLub{T}{T'}{U}}
\end{mathpar}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection*{Notations}

\noindent Une notation définie sur $x$ l'est pour tout élément, une notation définie sur $\Gamma$ l'est pour toute portée.
$$
\begin{array}{r|ll}
\text{Notation} & \text{Interprétation} \\
\hline
&\\
\overline{x} & \text{séquence $x_0, \; \ldots \;, x_n$ pour $n \in \mathbb{N}$} \\
x,\overline{x} & \text{séquence $x, x_0, \; \ldots \;, x_n$} \\
\sBind{\overline{x}}{\overline{\sigma}} & \text{portée $\sBind{x_0}{\sigma_0}, \ldots, \sBind{x_n}{\sigma_n}$ pour $n \in \mathbb{N}$} \\
\epsilon & \text{portée ou séquence vide} \\
&\\
\rClassDef{\Gamma_c}{\overline{D}}{\Gamma_c'} & 
  \left\{
    \begin{array}{l}
      \rClassDef{\Gamma_c}{D_0}{\Gamma_c^0} \\
      \vdots \\
      \rClassDef{\Gamma_c^{n-1}}{D_n}{\Gamma_c'}
    \end{array}
  \right. \\
&\\
\rMemberDef{\Gamma_c}{\overline{D}}{\Gamma_c'} & 
  \left\{
    \begin{array}{l}
      \rMemberDef{\Gamma_c}{D_0}{\Gamma_c^0} \\
      \vdots \\
      \rMemberDef{\Gamma_c^{n-1}}{D_n}{\Gamma_c'}
    \end{array}
  \right. \\
&\\
\rClass{\overline{D}} & \forall D \in \overline{D} \, . \; \rClass{D} \\
\rMember{\Gamma_p}{\overline{d}} & \forall d \in \overline{d} \, . \; \rMember{\Gamma_p}{d} \\
\rType{\overline{T}} & \forall T \in \overline{T} \, . \; \rType{T} \\
\rSub{\overline{T}}{\overline{U}} & \forall T, U \in \overline{T} \times \overline{U} \, . \; \rSub{T}{U} \\
\rTerm{\Gamma_p}{\overline{e}}{\overline{T}} & \forall e, T \in \overline{e} \times \overline{T} \, . \; \rTerm{\Gamma_p}{e}{T} \\
&\\
\Gamma + \sBind{x}{\sigma} &
  \left\{
    \begin{array}{ll}
      \Gamma', \sBind{x}{\sigma}, \Gamma'' & \text{si } \exists \Gamma', \Gamma'', \sigma' \, . \; \Gamma = (\Gamma', \sBind{x}{\sigma'}, \Gamma'') \\
      \Gamma, \sBind{x}{\sigma} & \text{sinon} \\
    \end{array}
  \right. \\
&\\
\Gamma \uplus \sBind{x}{\sigma} &
  \Gamma, \sBind{x}{\sigma} \text{ si } \forall \Gamma', \Gamma'', \sigma' \, . \; \Gamma \neq (\Gamma', \sBind{x}{\sigma'}, \Gamma'') \\
&\\
\rfFieldEnv{\overline{d}} &
  \begin{array}{c}
    \biguplus\\
    \scriptstyle{\astField{a}{T}{e} \; \in \; \overline{d}}
  \end{array} \; \sBind{a}{\sField{T}} \\
&\\
\rfMethodEnv{\overline{d}} &
  \begin{array}{c}
    \biguplus\\
    \scriptstyle{\astMethod{a}{\overline{a}}{\overline{T}}{T}{e} \; \in \; \overline{d}}
  \end{array} \; \sBind{a}{\sMethod{\overline{T}}{T}} \\
&\\
\rfParamEnv{\overline{a}}{\overline{T}} &
  \begin{array}{c}
    +\\
    \scriptstyle{a : T \; \in \; \overline{a} : \overline{T}}
  \end{array} \; \sBind{a}{\sParam{T}}
\end{array} \\
$$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newpage
\section*{\normalsize Etat des changements}
\small
\begin{description}
\item[révision $\gamma_7$] Les éléments du symbole de paramètre dans la règle de validité d'une méthode sont dans le bon ordre.
\item[révision $\gamma_6$] La règle de sous-typage entre classes définit correctement une classe comme sous-type d'elle-même.
\item[révision $\gamma_5$] Le sucre syntaxique pour la négation ($\neg e$) est correct.
\item[révision $\gamma_4$] La définition de la borne supérieure est plus simple. Les règles de validité d'un membre sont correctes aussi lorsque le membre défini n'est pas hérité.
\item[révision $\gamma_3$] La grammaire abstraite est syntaxiquement plus proche de la grammaire concrète. Le type ``\lstinline@Nothing@'' s'appelle ``\lstinline@Null@''.
\item[révision $\gamma_2$] La liste des classes parentes du symbole d'une classe ne contient plus la classe elle-même. Le sous-typage entre ``\lstinline@Nothing@'' et ``\lstinline@Nothing@'' est correct.
\item[révision $\gamma_1$] Ajoute les règles de validité du typage de \emph{Vier}, et les notions annexes. Compactifie la notation de la grammaire abstraite et définit le sucre syntaxique.
\item[révision $\beta_4$] Ajoute ``\lstinline@Nothing@''.
\item[révision $\beta_3$] Modifie la syntaxe d'assignement des valeurs à un champ, qui permet maintenant une forme abrégée qui assigne plusieurs champs simultanément.
\item[révision $\beta_2$] Ajoute le paramètre manquant à ``\lstinline@printInt@'' et ``\lstinline@printChar@'' dans la grammaire abstraite et syntaxique.
\item[révision $\beta_1$] Première version publique.
\end{description}




\end{document}

