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

Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-05 14:54:46 +01:00
commit df119b1995
1 changed files with 43 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
unify.tex
View File

@ -128,27 +128,27 @@ $
\rulename{Upper} \rulename{Upper}
& $ & $
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{T} } \\ \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{G} } \\
\hline \hline
\vspace*{-0.4cm}\\ \vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{T} } \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{G} }
\end{array} \end{array}
\quad \quad \quad \quad
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{T} } \\ \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\
\hline \hline
\vspace*{-0.4cm}\\ \vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{T} } \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G} }
\end{array} \end{array}
$ $
\\\\ \\\\
\rulename{Lower} \rulename{Lower}
& $ & $
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{T} \lessdot \type{A} } \\ \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{A} } \\
\hline \hline
\vspace*{-0.4cm}\\ \vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{T} \lessdot \type{L} } \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{L} }
\end{array} \end{array}
$ $
\\\\ \\\\
@ -607,6 +607,21 @@ This builds a search tree over multiple possible solutions.
\begin{center} \begin{center}
\fbox{ \fbox{
\begin{tabular}[t]{l@{~}l} \begin{tabular}[t]{l@{~}l}
\rulename{Same}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \type{G} \lessdot \tv{a}\\
\hline
\wildcardEnv \vdash
C \cup \set{
\tv{a} \doteq \type{G}
}
\end{array} \quad \begin{array}[c]{l}
\text{fv}(\type{G}) \in \Delta_{in}
\end{array}
$
\\\\
\rulename{\generalizeRule} \rulename{\generalizeRule}
& $ & $
\begin{array}[c]{l} \begin{array}[c]{l}
@ -665,28 +680,28 @@ This builds a search tree over multiple possible solutions.
\end{array} \end{array}
$ $
\\\\ \\\\
\rulename{Settle} % \rulename{Settle}
& $ % & $
\begin{array}[c]{l} % \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N}, % \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\tv{a} \lessdot^* \tv{b}} % \tv{a} \lessdot^* \tv{b}}
\\ % \\
\hline % \hline
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} } % \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} }
\end{array} % \end{array}
$ % $
\\\\ % \\\\
\rulename{Raise} % \rulename{Raise}
& $ % & $
\begin{array}[c]{l} % \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N}, % \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\tv{a} \lessdot \tv{b}} % \tv{a} \lessdot \tv{b}}
\\ % \\
\hline % \hline
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} } % \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
\end{array} % \end{array}
$ % $
\\\\ % \\\\
\end{tabular}} \end{tabular}}
\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}