From 48ba118e8d28f2ffc9ea549b9d0063370edb63d7 Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Sat, 27 Aug 2022 19:42:47 +0200
Subject: [PATCH] Petites modifications

---
 DiaposSoutenance.tex | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/DiaposSoutenance.tex b/DiaposSoutenance.tex
index ef854b3..d286fe2 100644
--- a/DiaposSoutenance.tex
+++ b/DiaposSoutenance.tex
@@ -245,6 +245,7 @@
 				\end{center}
 				\pause
 				\[\fj{new Paire((D)new B().get(), new C(new A())).snd.apply()}\]
+				\pdfpcnote{Distinction ouvert/ferme}
 			\end{frame}
 		\subsection{Ses structures}
 			\begin{frame}
@@ -267,8 +268,10 @@
 				\begin{itemize}[<+->]
 					\item $\fj{new C(e1,e2,...,en).field} \rightarrow \fj{ek}$ (\textsc{R-Field})
 					\item $\fj{new C(e1,e2,...,en).meth(f1,f2,...,fn)} \rightarrow e_{\fj{C.meth}}\bracket{\fj{new C(e1,e2,...,en)}\middle/ \fj{this},\fj{f1}\middle/\fj{x1},\fj{f2}\middle/\fj{x2},...,\fj{fn}\middle/\fj{xn}}$ (\textsc{R-Invk})
-					\item $\fj{(C) expr} \rightarrow \fj{expr}$ (\textsc{R-Cast})
+					\item $\fj{(C) new D(...)} \rightarrow \fj{new D(...)}$ si $\fj{D}\subclass\fj{C}$ (\textsc{R-Cast})
+					\item $e \rightarrow^* f \implies h\bracket{e} \rightarrow^* h\bracket{f}$
 				\end{itemize}
+				
 			\end{frame}
 			
 		\subsection{Son typage}
@@ -339,7 +342,7 @@
 					Contextualisation : $C\bracket{P}$
 					\vspace{2ex}\pause
 					
-					Préordre : $P \prec Q \iff \forall C\quad C\bracket{P} \implies C\bracket{Q}$
+					Préordre : $P \prec Q \iff \forall C\quad C\bracket{P}\rightarrow^* v \implies C\bracket{Q}\rightarrow^* v$
 					\vspace{2ex}\pause
 					
 					Équivalence : $P \equiv Q \iff P \prec Q \land Q \prec P$
@@ -357,7 +360,7 @@
 					\begin{fjlisting}[width=.49\textwidth]
 						\textbf{class} XXX \textbf{extends} XXX \{\}\\
 						\vdots\\
-						\fjmain{expression}
+						\fjmain{expr}
 					\end{fjlisting}
 					\vfill\null
 					\columnbreak
@@ -468,6 +471,7 @@
 					{\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]}
 					{\fj{C} \subclass_\mathcal{A} \fj{D}}
 				\]
+				\pause
 				\vspace{2ex}
 				\[
 					\infer
@@ -683,7 +687,17 @@
 		
 		\subsection{Redéfinition des préordres}
 			\begin{frame}
-				\[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\]
+				\[\boxed{\mathcal{A} \prec_\mathfrak{T} \mathcal{A'}}\qquad \forall (\mathcal{B},e) \left|\begin{array}{l}
+					\mathcal{B} \OKin \mathfrak{T}\\
+					\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}\\
+					\mathcal{A}\oplus\mathcal{B} \Downarrow v
+				\end{array}\right. \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\]
+			
+				\[\boxed{\mathcal{A} \pprec_\mathfrak{T} \mathcal{A'}}\quad \forall \hbar,\alpha,(\mathcal{B},e) \left|\begin{array}{l}
+					\mathcal{B} \OKin \mathfrak{T}\\
+					\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}\\
+					\mathcal{A}\oplus\mathcal{B} \rightarrow^*\hbar\bracket{\alpha}
+				\end{array}\right. \implies \exists\beta\quad \mathcal{A'}\oplus\mathcal{B}\rightarrow^* \hbar\bracket{\beta}\]
 			\end{frame}
 		\subsection{Propriétés}
 			\begin{frame}