stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add T-Call rule without receiver

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-11 23:29:34 +01:00
parent 3017cfc796
commit cbd0a48ca6
1 changed files with 22 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
tRules.tex
View File

@ -10,8 +10,8 @@ where existential types are implicitly \textit{opened} and \textit{closed}.
%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}. %The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
%and is solely used for examples. %and is solely used for examples.
The calculus does not include method overloading or method overriding for simplicity reasons. The calculus does not include method overriding for simplicity reasons.
Type inference for both are described in \cite{TIforFGJ} and can be added to this algorithm accordingly. Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
Our algorithm is designed for extensibility with the final goal of full support for Java. Our algorithm is designed for extensibility with the final goal of full support for Java.
\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}. \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}. Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
@ -239,6 +239,26 @@ $\begin{array}{l}
\end{array} \end{array}
\end{array}$ \end{array}$
\\[1em] \\[1em]
$\begin{array}{l}
\typerule{T-Call}\\
\begin{array}{@{}c}
\Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok
\\
\Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
\Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \texttt{m}(\ol{e}) : \type{T}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Elvis}\\ \typerule{T-Elvis}\\
\begin{array}{@{}c} \begin{array}{@{}c}