Add Prolog
This commit is contained in:
JanUlrich
parent
2702bf6cab
commit
4efda6cae2
226
prolog.tex
Executable file
226
prolog.tex
Executable file
@ -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:
|
||||||
Loading…
Reference in New Issue
Block a user