diff --git a/prolog.tex b/prolog.tex new file mode 100755 index 0000000..efe0afe --- /dev/null +++ b/prolog.tex @@ -0,0 +1,226 @@ +\usepackage{xspace} +\usepackage{color,ulem} +\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{\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} + +\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: