Add A-Normal Form transform
This commit is contained in:
Andreas Stadelmeier
parent
e7b6786f08
commit
e9f86ffda3
@ -64,12 +64,10 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
|
||||
\type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
|
||||
\type{N} &::= \exptype{C}{\il{T}} && \text{class type (with type variables)} \\
|
||||
% Constraints
|
||||
\simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\
|
||||
\orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\
|
||||
\constraint &::= \simpleCons \mid \orCons && \text{constraint}\\
|
||||
\constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
|
||||
\consSet &::= \set{\constraints} && \text{constraint set}\\
|
||||
% Method assumptions:
|
||||
\methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \exptype{}{\ol{Y}
|
||||
\methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
|
||||
\triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T} &&
|
||||
\text{method
|
||||
type assumption}\\
|
||||
@ -79,7 +77,7 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
|
||||
& \text{method type environment} \\
|
||||
\typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption})
|
||||
\end{align*}
|
||||
\caption{Syntax of constraints and type assumptions.}
|
||||
\caption{Syntax of constraints and type assumptions}
|
||||
\label{fig:syntax-constraints}
|
||||
\end{figure}
|
||||
|
||||
@ -141,6 +139,23 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
|
||||
% <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
|
||||
% \end{verbatim}
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{e} \ \text{fresh} \\
|
||||
& \consSet_R = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e})\\
|
||||
& \constraint =
|
||||
\set{
|
||||
\tv{e} \lessdotCC \tv{x}
|
||||
}\\
|
||||
{\mathbf{in}} & {
|
||||
\consSet_R \cup \set{\constraint}} \cup \typeExpr(\mtypeEnvironment \cup \set{\expr{x} : \tv{x}})
|
||||
\end{array}
|
||||
\end{array}
|
||||
\end{displaymath}
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
|
||||
@ -168,6 +183,24 @@ The set of method assumptions returned by the \textit{mtypes} function is used t
|
||||
|
||||
There are two kinds of method calls.
|
||||
The ones to already typed methods and calls to untyped methods.
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{}' & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
|
||||
& \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
|
||||
\ol{S} \lessdot \ol{T}, \type{T} \lessdot \tv{a},
|
||||
\ol{Y} \lessdot \ol{N} }\\
|
||||
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
|
||||
& \mathbf{where}\ \begin{array}[t]{l}
|
||||
\expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
|
||||
\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment}
|
||||
\end{array}
|
||||
|
||||
\end{array}
|
||||
\end{array}
|
||||
\end{displaymath}
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
|
||||
@ -521,19 +521,34 @@ The \unify{} algorithm only sees the constraints with no information about the p
|
||||
The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
|
||||
|
||||
\subsection{ANF transformation}
|
||||
The input is transformed to A-normal form.
|
||||
%TODO: describe ANF syntax (which is different then the one from the wiki: https://en.wikipedia.org/wiki/A-normal_form)
|
||||
The input is a \letfj{} program without \texttt{let} statements, which is then transformed to A-normal form \cite{aNormalForm}
|
||||
before getting processed by \fjtype{}.
|
||||
|
||||
$
|
||||
\begin{array}{lrcl}
|
||||
\begin{array}{lrcl|l}
|
||||
\hline
|
||||
\text{Terms} & t & ::= & v \\
|
||||
& & \ \ | & \texttt{let}\ x = v \ \texttt{in}\ x.f\\
|
||||
& & \ \ | & \texttt{let}\ x_1 = v \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{v} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})\\
|
||||
& & \ \ | & t \elvis{} t\\
|
||||
\text{Var} & v & ::= & \expr{x} \\
|
||||
& & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
|
||||
\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
|
||||
& & & \textbf{\letfj{}} & \textbf{A-Normal form} \\
|
||||
\text{Terms} & t & ::=
|
||||
& \expr{x}
|
||||
& \expr{x}
|
||||
\\
|
||||
& & \ \ |
|
||||
& \texttt{new} \ \type{C}(\overline{t})
|
||||
& \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x})
|
||||
\\
|
||||
& & \ \ |
|
||||
& t.f
|
||||
& \texttt{let}\ x = t \ \texttt{in}\ x.f
|
||||
\\
|
||||
& & \ \ |
|
||||
& t.\texttt{m}(\overline{t})
|
||||
& \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{v} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})
|
||||
\\
|
||||
& & \ \ |
|
||||
& t \elvis{} t
|
||||
& t \elvis{} t\\
|
||||
%
|
||||
\hline
|
||||
\end{array}
|
||||
$
|
||||
|
||||
10
martin.bib
10
martin.bib
@ -456,3 +456,13 @@ keywords = {Compilation, Java, generic classes, language design, language semant
|
||||
year={1996}
|
||||
}
|
||||
|
||||
@article{aNormalForm,
|
||||
title={Reasoning about programs in continuation-passing style.},
|
||||
author={Sabry, Amr and Felleisen, Matthias},
|
||||
journal={ACM SIGPLAN Lisp Pointers},
|
||||
number={1},
|
||||
pages={288--298},
|
||||
year={1992},
|
||||
publisher={ACM New York, NY, USA}
|
||||
}
|
||||
|
||||
|
||||
111
tRules.tex
111
tRules.tex
@ -196,72 +196,98 @@ $\begin{array}{l}
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Field}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad
|
||||
\Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
|
||||
\Delta | \Gamma \vdash \expr{v} : \type{T} \quad \quad
|
||||
\Delta \vdash \type{T} <: \wcNtype{}{N} \quad \quad
|
||||
\textit{fields}(\type{N}) = \ol{U\ f} \\
|
||||
\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
|
||||
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
|
||||
\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
|
||||
\Delta | \Gamma \vdash \expr{v}.\texttt{f}_i : \type{U}_i
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
% $\begin{array}{l}
|
||||
% \typerule{T-Field}\\
|
||||
% \begin{array}{@{}c}
|
||||
% \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad
|
||||
% \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
|
||||
% \textit{fields}(\type{N}) = \ol{U\ f} \\
|
||||
% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
|
||||
% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
|
||||
% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
|
||||
% \\
|
||||
% \hline
|
||||
% \vspace*{-0.3cm}\\
|
||||
% \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
|
||||
% \end{array}
|
||||
% \end{array}$
|
||||
% \\[1em]
|
||||
% $\begin{array}{l}
|
||||
% \typerule{T-New}\\
|
||||
% \begin{array}{@{}c}
|
||||
% \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} \ \ok \quad \quad
|
||||
% \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
|
||||
% \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
|
||||
% \Delta \vdash \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
|
||||
% \Delta, \overline{\Delta} \vdash \overline{\type{N}} <: \overline{\type{U}} \quad \quad
|
||||
% \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
|
||||
% \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
|
||||
% \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok
|
||||
% \\
|
||||
% \hline
|
||||
% \vspace*{-0.3cm}\\
|
||||
% \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
|
||||
% \end{array}
|
||||
% \end{array}$
|
||||
% \\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-New}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} \ \ok \quad \quad
|
||||
\text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
|
||||
\Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
|
||||
\Delta \vdash \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
|
||||
\Delta, \overline{\Delta} \vdash \overline{\type{N}} <: \overline{\type{U}} \quad \quad
|
||||
\Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
|
||||
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
|
||||
\Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok
|
||||
\Delta \vdash \overline{\type{S}} <: \overline{\type{U}} \\
|
||||
\Delta | \Gamma \vdash \overline{\expr{v} : \type{S}} \quad \quad
|
||||
\text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
|
||||
\triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{v}) : \exptype{C}{\ol{T}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[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'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
|
||||
\\
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
|
||||
\Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
|
||||
\\
|
||||
\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
|
||||
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
|
||||
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
\hfill
|
||||
% $\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'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
|
||||
% \\
|
||||
% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
|
||||
% \Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \quad \quad
|
||||
% \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
|
||||
% \\
|
||||
% \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
|
||||
% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
|
||||
% \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
|
||||
% \\
|
||||
% \hline
|
||||
% \vspace*{-0.3cm}\\
|
||||
% \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
|
||||
% \end{array}
|
||||
% \end{array}$
|
||||
% \\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Call}\\
|
||||
\begin{array}{@{}c}
|
||||
\generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
|
||||
\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
|
||||
\\
|
||||
\Delta \vdash \ol{S} \ \ok \quad \quad
|
||||
\Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \quad \quad
|
||||
\Delta | \Gamma \vdash \expr{v}, \ol{v} : \ol{T} \quad \quad
|
||||
\Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
|
||||
\Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
@ -278,7 +304,7 @@ $\begin{array}{l}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{let} \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2 : \type{T}
|
||||
\Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2 : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
@ -368,4 +394,5 @@ $\begin{array}{l}
|
||||
\text{fields}(\exptype{C}{\ol{T}}) = \ol{U\ g}, [\ol{T}/\ol{X}]\ol{S\ f}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\caption{Field access}
|
||||
\end{figure}
|
||||
Loading…
Reference in New Issue
Block a user