-
Notifications
You must be signed in to change notification settings - Fork 0
/
prolog.tex
106 lines (87 loc) · 3.82 KB
/
prolog.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
\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=b,
}
\lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
\lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
\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{\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\rulename[1]{\textup{\textrm{(#1)}}}
%%% 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{\gamma}}% {\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{\type}[1]{\texttt{#1}}
\newcommand{\gType}[1]{\texttt{#1}}
\newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
\newcommand{\methodAssumption}{\ensuremath{\mathtt{\lambda}}}
\newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
\newcommand{\expandLB}{\textit{expandLB}}
\def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
\def\exp#1#2{#1(\,#2\,)\xspace}
\newcommand{\ldo}{, \ldots , }
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "TIforGFJ"
%%% End: