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

Unify

Browse Source
This commit is contained in:
JanUlrich 2024-04-03 15:54:08 +02:00
parent 87f413241a
commit 21328a3d05
2 changed files with 27 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
prolog.tex
View File

@ -121,8 +121,8 @@
\newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}} \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
%\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}} %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
\newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}} \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}} \newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
\newcommand{\ntv}[1]{\tv{#1}} %\newcommand{\ntv}[1]{\tv{#1}}
\newcommand{\wcstore}{\ensuremath{\Delta}} \newcommand{\wcstore}{\ensuremath{\Delta}}
%\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}} %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}

40
unify.tex
View File

@ -146,21 +146,28 @@ The \unify{} algorithm internally uses the following data types:
The algorithm is split into multiple parts: The algorithm is split into multiple parts:
\begin{description} \begin{description}
\item[Step 1:] \item[Step 1:]
Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively. Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively,
Starting with the \rulename{circle} rule. starting with the \rulename{circle} rule.
\item[Step 2:] \item[Step 2:]
%If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$ %If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$
%resume with step 4. %resume with step 4.
The rules in figure \ref{fig:step2-rules} offer multiple possibilities to deal with constraints of the form $\type{N} \lessdot \tv{a}$. The second step is nondeterministic.
This builds a search tree over multiple possible solutions. %\unify{} has to pick the right transformation for each constraint of the form $\type{N} \lessdot \tv{a}$.
\unify{} has to try each branch and accumulate the resulting solutions into a solution set. %The rules in figure \ref{fig:step2-rules} offer three possibilities to deal with constraints $\type{N} \lessdot \tv{a}$.
For every $\type{T} \lessdot \tv{a}$ constraint \unify{} has to pick exactly one transformation from figure \ref{fig:step2-rules}.
The same principle goes for constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$ and the two transformations in figure \ref{fig:step2-rules2}.
%They have to be applied until the constraint set holds no constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$.
If atleast one transformation was applied in this step revert to step 1.
Otherwise proceed with step 3.
%This builds a search tree over multiple possible solutions.
%\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations. %$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
\item[Step 3:] \item[Step 3:]
We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 4. Apply the rules in figure \ref{fig:cleanup-rules} exhaustively and move on with step 4.
\item[Step 4:] \textit{(Generating Result)} \item[Step 4:] \textit{(Generating Result)}
Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$. Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$.
@ -263,6 +270,12 @@ To only rename the respective wildcards the reduce rule renames wildcards up to
\item[Free Variables:] \item[Free Variables:]
The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell. The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
% TODO: describe a function which determines free variables? or do an example? % TODO: describe a function which determines free variables? or do an example?
\begin{align*}
\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
\text{fv}(\ntv{a}) &= \emptyset \\
\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
\end{align*}
\item[Fresh Wildcards:] \item[Fresh Wildcards:]
$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards. $\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
@ -445,11 +458,11 @@ $
\hline \hline
\vspace*{-0.4cm}\\ \vspace*{-0.4cm}\\
\wildcardEnv \vdash C \wildcardEnv \vdash C
\end{array} \end{array}
$ $
\\\\ \quad
\rulename{Pit} \rulename{Pit}
& $ $
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\ \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\
\hline \hline
@ -530,10 +543,7 @@ $
\vspace*{-0.4cm}\\ \vspace*{-0.4cm}\\
\wildcardEnv \vdash C \wildcardEnv \vdash C
\end{array} \end{array}
$ \quad
\\\\
\rulename{Erase}
& $
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \type{T} \lessdot \type{T} } \\ \wildcardEnv \vdash C \cup \, \set{ \type{T} \lessdot \type{T} } \\
\hline \hline
@ -970,7 +980,7 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
} }
\end{center} \end{center}
\caption{Step 2 branching: Multiple rules can be applied to the same constraint} \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
\label{fig:step2-rules} \label{fig:step2-rules2}
\end{figure} \end{figure}
\begin{figure} \begin{figure}