Add Syntax for Constraints

This commit is contained in:
JanUlrich 2024-05-14 15:15:02 +02:00
parent 81f44caac1
commit bdfacdf3dd

View File

@ -148,23 +148,6 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
%NO equals constraints during the constraint generation step!
\begin{figure}[tp]
\begin{align*}
% Type
\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}{\ol{T}} && \text{class type (with type variables)} \\
% Constraints
\constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
\consSet &::= \set{\constraints} && \text{constraint set}\\
% Method assumptions:
\methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
\triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T} &&
\text{method
type assumption}\\
\localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
assumption}\\
\mtypeEnvironment & ::= \overline{\methodAssumption} &
& \text{method type environment}
\end{align*}
\begin{tabular}{lcll}
$C $ &$::=$ &$\overline{c}$ & Constraint set \\
$c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
@ -175,7 +158,7 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
$\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
$\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
\end{tabular}
\caption{Syntax of constraints and type assumptions}
\caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
\label{fig:syntax-constraints}
\end{figure}