From 8ca0e8a7b541a43fa12aa82f397b9547f7757305 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <stan@hb.dhhbw-stuttgart.de>
Date: Wed, 24 Apr 2024 17:45:14 +0200
Subject: [PATCH] List/head Beispiel

---
 vortrag.tex | 54 ++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 49 insertions(+), 5 deletions(-)

diff --git a/vortrag.tex b/vortrag.tex
index 64a5d28..24a9988 100644
--- a/vortrag.tex
+++ b/vortrag.tex
@@ -19,11 +19,11 @@
 $\begin{array}{l}
     \begin{array}{@{}c}
         \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-        \Delta \vdash  \expr{v}, \ol{v} : \ol{T}
+        \Delta \vdash  \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
+        \Delta \vdash \expr{v}.\generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
     \end{array}
 \end{array}$
 \end{center}
@@ -45,17 +45,61 @@ $\begin{array}{l}
 \end{array}$
 \end{center}
 
+\textbf{Beispiele:}\\
 \begin{verbatim}
 X head(List<X> l) { ... }
 \end{verbatim}
+\begin{itemize}
+\item 
+$\textit{mtype}(\texttt{head}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \type{X}$
+\end{itemize}
 
 \begin{verbatim}
 <X> List<X> emptyList() { ... }
 \end{verbatim}
-
-$\textit{mtype}(\texttt{head}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \type{X}$
-
+\begin{itemize}
+\item 
 $\textit{mtype}(\texttt{emptyList}) = \generics{\type{X}}\ [] \to \exptype{List}{\type{X}}$
+\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Java Method Call}
+\rulename{T-Call} \\[1em]
+\begin{center}
+$\begin{array}{l}
+    \begin{array}{@{}c}
+        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
+        \Delta \vdash  \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta \vdash \expr{v}.\generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
+    \end{array}
+\end{array}$
+\end{center}
+\textbf{Beispiel:}\\
+$\begin{array}{l}
+    \begin{array}{@{}c}
+        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
+        \texttt{new List<String>}() : [\type{String}/\type{X}]\exptype{List}{\type{X}}
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \generics{\type{String}}\texttt{head}(\texttt{new List<String>}()) : [\type{String}/\type{X}]\type{X}
+    \end{array}
+\end{array}$
+
+$\begin{array}{l}
+    \begin{array}{@{}c}
+        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
+        \texttt{new List<String>}() : \exptype{List}{\type{String}}
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \generics{\type{String}}\texttt{head}(\texttt{new List<String>}()) : \type{String}
+    \end{array}
+\end{array}$
 \end{frame}
 
 \begin{frame}[fragile]