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

Add ntv to syntax

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-13 21:05:29 +01:00
parent 8b44a5bf5a
commit 34530270c6
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
unify.tex
View File

@ -73,8 +73,8 @@ and a list of constraints $C' = \set{ \type{T} \lessdotCC \type{T}}$.
The input constraints must be of the following format:
\begin{tabular}{lcll}
$c $ &$::=$ & $\type{T} \lessdot \type{U}$ & Constraint \\
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \wtv{a} \mid \ntype{N}$ & Type variable or Wildcard Variable or Type \\
$c $ &$::=$ & $\type{T} \lessdot \type{T}, \type{T} \lessdotCC \type{T}$ & Constraint \\
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\ntv{a} \mid \wtv{a} \mid \ntype{N}$ & Type variable or Wildcard Variable or Type \\
$\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}} $ & Class Type \\
\end{tabular}\\[0.5em]
@ -110,7 +110,8 @@ The \unify{} algorithm internally uses the following data types:
\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 \\
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \wtv{a} \mid \gtype{G}$ & Type variable or Type \\
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
$\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
$\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
$\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
$\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\