Ecoop2024_TIforWildFJ/prolog.tex
2024-07-24 00:38:29 +02:00

234 lines
7.6 KiB
TeX
Executable File

\usepackage{xspace}
\usepackage{color,ulem}
\usepackage{mathpartir}
\usepackage{listings}
\lstset{language=Java,
showspaces=false,
showtabs=false,
%breaklines=true,
showstringspaces=false,
%breakatwhitespace=true,
basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize
escapeinside={(*@}{@*)},
captionpos=t,float,abovecaptionskip=-\medskipamount
}
\lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
\lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
\lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}}
\lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}}
\lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}}
\lstdefinestyle{constraints}{
basicstyle=\normalfont,
backgroundcolor=\color{red!20}
}
\newtheorem{recap}[note]{Recap}
\newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
\newcommand{\tifj}{\texttt{TamedFJ}}
\newcommand{\wcSep}{\vdash}
\newcommand\mv[1]{{\tt #1}}
\newcommand{\ol}[1]{\overline{\tt #1}}
\newcommand{\exptype}[2]{\mathtt{#1 \texttt{<} #2 \texttt{>} }}
\newcommand\ddfrac[2]{\frac{\displaystyle #1}{\displaystyle #2}}
\newcommand{\sarray}[2]{\begin{array}[t]{#1} #2 \end{array}}
%\newcommand{\olsub}{\textrm{$\, \leq^\ast \,$}\ }
\newcommand{\olsub}{\textrm{$<:$}\ }
\newcommand{\sub}\olsub%{\mbox{$<$}}
\newcommand{\ok}{\texttt{ok}}
\newcommand{\set}[1]{\{ #1 \} }
\definecolor{red}{rgb}{1,0,0}
\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\commentarystar}[1]{\red{\({}^*\)}\marginpar[\tiny
\red{\({}^*\)#1}]{\tiny \red{\({}^*\)#1}}}
\newcommand{\commentary}[1]{\marginpar[\tiny
\red{#1}]{\tiny \red{#1}}}
\newcommand{\commentarymark}[1]{\color{red} #1\ensuremath{^*}\color{black}}
\newcommand{\commentarymargintext}[2]{\color{red} #1$^*$
\color{black}\marginpar[\tiny \red{\({}^*\)#2}]{\tiny \red{\({}^*\)#2}}}
\newcommand{\commentaryintext}[2]{\color{red} #1\textrm{$^*${\tiny #2}}\color{black}}
\newcommand{\commentarymath}[2]{\color{red} #1^*\color{black}\)\marginpar[\tiny \red{\({}^*\)#2}]{\tiny \red{\({}^*\)#2}}\(}
\newcommand{\replaced}[2]{\erased{#1}\inserted{#2}}
\newcommand{\erased}[1]{\commentary{\sout{#1}}}
\newcommand{\inserted}[1]{\color{red}#1\color{black}\xspace}
\newcommand\Erase[1]{|#1|}
\newcommand\Angle[1]{\langle#1\rangle}
\newcommand\TFGJ{FGJ-GT\xspace}
\newcommand\FGJGT{FGJ-GT\xspace}
\newcommand\FGJType{\textbf{FGJType} }
\newcommand\TVX{\mv X}
\newcommand\TVY{\mv Y}
\newcommand\TVZ{\mv Z}
\newcommand\TVW{\mv W}
\newcommand\CL[1]{\textit{Cl}$_{#1}$}
\newcommand\subconstr{\lessdot}
\newcommand\eqconstr{\doteq}
\newcommand\subeq{\mathbin{\texttt{<:}}}
\newcommand\extends{\ensuremath{\triangleleft}}
\newcommand{\QMextends}[1]{\textrm{\normalshape\ttfamily ?\,extends}\linebreak[0]\,#1}
\newcommand{\QMsuper}[1]{\textrm{\normalshape\ttfamily ?\linebreak[0]\,su\-per}\linebreak[0]\,#1}
\newcommand\rulename[1]{\textup{\textsc{(#1)}}}
\newcommand{\generalizeRule}{General}
%%% FJ-IT Type rules
\newcommand{\environmentvdash}{\Pi;\Delta;\Gamma \vdash}
\newcommand{\fjtypeinference}{\textbf{FJTypeInference}}
%%% Commands for FGJTYPE algorithm
\newcommand{\tv}[1]{\mathit{ #1 }}
%\newcommand{\fjtypeInsert}{\textbf{FJTypeInsert}}
\newcommand{\unifyGenerics}{\ensuremath{\Delta}}% {\ensuremath{\overline{\type{G}\triangleleft \type{H}}}}
\newcommand{\fjtype}{\textbf{FJType}}
\newcommand{\unify}{\textbf{Unify}}
\newcommand{\typeMethod}{\textbf{TYPEMethod}}
\newcommand{\typeExpr}{\textbf{TYPEExpr}}
\newcommand{\constraint}{\ensuremath{\mathit{c}}}%{\ensuremath{\mathtt{C}}}
\newcommand{\consSet}{C}%{\ensuremath{\overline{\mathtt{C}}}}
\newcommand{\orCons}{\textit{oc}}%{\ensuremath{\textbf{C}_{||}}}
\newcommand{\simpleCons}{\textit{sc}}
\newcommand{\overridesFunc}{\textit{overrides}}
\newcommand{\typeAssumptionsSymbol}{\ensuremath{\Theta}}
\newcommand{\typeAssumptions}{\ensuremath{(\mv{\Pi} ; \overline{\localVarAssumption})}}%{\ensuremath{(\overline{\methodAssumption} ; \overline{\fieldAssumption}; \overline{\localVarAssumption})}}
\newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
\newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
\newcommand{\gtype}[1]{\type{#1}}
\newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\anyType}[1]{\mathit{#1}}
\newcommand{\gType}[1]{\texttt{#1}}
\newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
\newcommand{\methodAssumption}{\ensuremath{\mathtt{\lambda}}}
\newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
\newcommand{\expandLB}{\textit{expandLB}}
\newcommand{\letfj}{\textbf{LetFJ}}
\newcommand{\tph}{\text{tph}}
\newcommand{\expr}[1]{\texttt{#1}}
\def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
\def\exp#1#2{#1(\,#2\,)\xspace}
\newcommand{\ldo}{, \ldots , }
% WILDCARD specific:
\newcommand{\xtype}[2]{\ensuremath{\exists #1 . \type{#2}}}
\newcommand{\xtypevar}[1]{\ensuremath{\exists \emptyset . \type{#1}}}
\newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
%\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
\newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
\newcommand{\cctv}[1]{\ensuremath{\tv{#1}_!}}
\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
%\newcommand{\ntv}[1]{\tv{#1}}
\newcommand{\wcstore}{\ensuremath{\Delta}}
%\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}
\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\wildcardEnv}{\ensuremath{\mathbb{W}}}
\newcommand{\wildcard}[3]{\ensuremath{\mathtt{#1 : [#3 .. #2]}}}
\newcommand{\cwildcard}[3]{\ensuremath{\mathtt{\overleftarrow{#1}^{#2}_{#3}}}}
\newcommand{\generics}[1]{\ensuremath{\mathtt{\texttt{<} {#1} \texttt{>} }}}
\newcommand{\lessdotCC}{\ensuremath{\lessdot^{\texttt{c}}}}
\newcommand{\ccDecaptureRule}{\rulename{CC-Decapture}}
\newcommand{\ccInvalidate}{\rulename{CC-Invalidate}}
\newcommand{\ruleWCEquals}[0]{\rulename{WC-Equals}}
\newcommand{\ruleReduceWC}[0]{\rulename{Reduce}}
\newcommand{\ruleReduce}[0]{\rulename{Reduce}}
\newcommand{\ruleSubstWC}[0]{\rulename{Subst-WC}}
\newcommand{\subclass}{\mathtt{\sqsubset}\mkern-5mu :}
\newcommand{\TamedFJ}{\textbf{TamedFJ}}
\newcommand{\TYPE}{\textbf{TYPE}}
\newcommand{\vdashI}[0]{\ \ . \kern-0.8em \vdash }
\newcommand{\wildcardTV}[1]{\type{#1}_?}
\newcommand{\replaceWC}[2]{\ensuremath{[#1/#2]_?}}
\newcommand{\replaceAdapt}[2]{\ensuremath{[#1/#2]_\uparrow}}
\newcommand{\wcEnv}[3]{#1 : [#2\ ..\ #3]}
\newcommand{\fresh}[1]{\textit{fresh}(#1)}
\newcommand{\typerule}[1]{\small\textsc{#1}}
\newcommand{\letstmt}[2]{\texttt{let}\ #1 \ \texttt{in} \ #2}
\newcommand{\elvis}[0]{\ensuremath{\ {?}{:}\ }}
\newcommand{\wildFJ}[0]{\textbf{WildFJ}}
%\newcommand{\wfresh}[0]{\textit{wfresh}}
%COLORS:
\definecolor{change}{RGB}{201,201,255}
\definecolor{subst}{RGB}{241,203,255}
\definecolor{addition}{RGB}{225,247,213}
\definecolor{highlight}{RGB}{255,189,189}
\definecolor{frame}{HTML}{634b7d}
%\definecolor{gray}{RGB}{120, 120, 120}
%\definecolor{frame}{RGB}{241, 246, 249}
\tcbset{colback=white,colframe=frame,fonttitle=\bfseries,coltitle=white}
\newcommand{\deduction}[2]{
\begin{array}[c]{l}
#1 \\
\hline
\vspace*{-0.4cm}\\
#2
\end{array}
}
\newcommand{\nextdeduction}[1]
{
\begin{array}{@{}l@{}r@{}}
\begin{array}[c]{l}
\hline
\vspace*{-0.4cm}\\
#1
\end{array} % \rulename{#3}
\end{array}
}
\newcommand{\subst}[2]{
\left[ #1 / #2 \right]
}
\newenvironment{constraintset}
{
\begin{tcolorbox}
}
{
\end{tcolorbox}
}
\newcommand{\wcNtype}[2]{\exists #1 .\ntype{#2}}
\newcommand{\wctype}[3]{\exists #1 .\exptype{#2}{#3}}
\newcommand{\wtype}[1]{\mathit{#1}}
\newcommand{\ntype}[1]{\mathtt{#1}}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "TIforGFJ"
%%% End: