From 903b2405b15422af0acb78154af9b548119c4d9a Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Wed, 6 Mar 2024 16:08:12 +0100 Subject: [PATCH] Add T-Elvis rule --- constraints.tex | 11 +++++++++++ tRules.tex | 2 ++ 2 files changed, 13 insertions(+) diff --git a/constraints.tex b/constraints.tex index 08f62c0..1ac1330 100644 --- a/constraints.tex +++ b/constraints.tex @@ -12,6 +12,17 @@ Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation. Here \fjtype{} generates capture constraints instead of normal subtype constraints. +Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}. +The \typeExpr{} function creates constraints for a given expression. + +$\begin{array}{c} +\typeExpr(\texttt{t}_1, \ntv{b}) = C_l \quad \quad \typeExpr(\texttt{t}_2, \ntv{c}) = C_l \quad \quad \ntv{b}, \ntv{c} \ \text{fresh} +\\ +\hline +\typeExpr(\texttt{t}_1 \texttt{?:} \texttt{t}_2, \tv{a}) = C_l \cup C_r \cup \set{\ntv{b} \lessdot \tv{a}, \ntv{c} \lessdot \tv{a}} +\end{array} +$ + The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call. Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion. diff --git a/tRules.tex b/tRules.tex index aa5bd4a..646994b 100644 --- a/tRules.tex +++ b/tRules.tex @@ -18,6 +18,8 @@ class List { } \end{verbatim} +%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program. + %The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}. %and is solely used for examples. The calculus does not include method overriding for simplicity reasons.