-
Notifications
You must be signed in to change notification settings - Fork 0
/
macros.tex
201 lines (161 loc) · 7.84 KB
/
macros.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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
% !TEX root = ./type-inference-paper.tex
% reverse Vdash
%
% provenances
%
\newcommand{\Prov}{{\normalfont\textsf{Provenance}}}
\newcommand{\Provp}{\ensuremath{p}}
% errors with id
\newcommand{\ECMarkedId}[3]{\ensuremath{\textcolor{red}{\bm{\llparenthesis}}\textcolor{red}{#1}\textcolor{red}{\bm{\rrparenthesis}^{#3}_{#2}}}}
\newcommand{\ECMarkedFreeId}[2]{\ensuremath{\ECMarkedId{#1}{\MRFree}{#2}}}
\newcommand{\ECMarkedInconTypeId}[2]{\ensuremath{\ECMarkedId{#1}{\mathsmaller{\inconsistentRel}}{#2}}}
\newcommand{\ECMarkedInconBrId}[2]{\ensuremath{\ECMarkedId{#1}{\MRInconBr}{#2}}}
\newcommand{\ECFreeId}[2]{\ensuremath{\ECMarkedFreeId{#1}{#2}}}
\newcommand{\ECInconTypeId}[2]{\ensuremath{\ECMarkedInconTypeId{#1}{#2}}}
\newcommand{\ECInconBrId}[4]{\ensuremath{\ECMarkedInconBrId{\ECIf{#1}{#2}{#3}}{#4}}}
\newcommand{\ECApNonMatchedId}[3]{\ensuremath{\ECAp{\ECInconTypeId{#1}{#2}}{#3}}}
\newcommand{\ECApSynNonMatchedArrowId}[3]{\ensuremath{\ECAp{\ECMarkedId{#1}{\MRSynNonMatchedArrow}{\MRSyn,~#2}}{#3}}}
\newcommand{\ECLamAnaNonMatchedArrowId}[4]{\ECMarkedId{\ECLam{#1}{#2}{#3}}{\MRAnaNonMatchedArrow}{\MRAna,~#4}}
\newcommand{\ECInconMatchedId}[3]{\ensuremath{\ECMarkedId{#1}{#2}{#3}}}
\newcommand{\ECInconMatchedArrowId}[2]{\ensuremath{\ECInconMatchedId{#1}{\notMatchedArrowRel}{#2}}}
\newcommand{\ECInconMatchedPairId}[2]{\ensuremath{\ECInconMatchedId{#1}{\notMatchedProdRel}{#2}}}
\newcommand{\ECPairAnaNonMatchedProdId}[3]{\ECMarkedId{\ECPair{#1}{#2}}{\MRAnaNonMatchedProd}{\MRAna,~#3}}
\newcommand{\ECProjLSynNonMatchedProdId}[2]{\ECMarkedId{#1}{\MRSynNonMatchedProd}{\MRSyn,~#2}}
\newcommand{\ECProjRSynNonMatchedProdId}[2]{\ECMarkedId{#1}{\MRSynNonMatchedProd}{\MRSyn,~#2}}
% Violet hotdogs; highlight color helps distinguish them
\newcommand{\llparenthesiscolor}{\textcolor{violet}{\llparenthesis}}
\newcommand{\rrparenthesiscolor}{\textcolor{violet}{\rrparenthesis}}
% HTyp and HExp
\newcommand{\hcomplete}[1]{#1~\mathsf{complete}}
% HTyp
\newcommand{\htau}{\dot{\tau}}
\newcommand{\tarrnp}[2]{#1 \rightarrow #2}
\newcommand{\trul}[2]{\inparens{#1 \Rightarrow #2}}
\newcommand{\trulnp}[2]{#1 \Rightarrow #2}
\newcommand{\tnum}{\mathtt{num}}
\newcommand{\tbool}{\mathtt{bool}}
\newcommand{\tehole}{\mathtt{?}}
\newcommand{\tsum}[2]{\inparens{{#1} + {#2}}}
\newcommand{\tprod}[2]{\inparens{{#1} \times {#2}}}
\newcommand{\tunit}{\mathtt{1}}
\newcommand{\tvoid}{\mathtt{0}}
\newcommand{\tcompat}[2]{#1 \sim #2}
\newcommand{\tincompat}[2]{#1 \nsim #2}
% HExp
\newcommand{\hexp}{\dot{e}}
\newcommand{\hlam}[3]{\inparens{\lambda #1:#2.#3}}
\newcommand{\hap}[2]{#1(#2)}
\newcommand{\hapP}[2]{(#1)~(#2)} % Extra paren around function term
\newcommand{\hnum}[1]{\underline{#1}}
\newcommand{\hadd}[2]{\inparens{#1 + #2}}
\newcommand{\hpair}[2]{\inparens{#1 , #2}}
\newcommand{\htriv}{()}
\newcommand{\hehole}[1]{\llparenthesiscolor\rrparenthesiscolor}
\newcommand{\hhole}[2]{\llparenthesiscolor #1 \rrparenthesiscolor}
\newcommand{\hindet}[1]{\lceil#1\rceil}
\newcommand{\hinj}[2]{\mathtt{inj}_{#1}({#2})}
\newcommand{\hinl}[2]{\mathtt{inl}_{#1}({#2})}
\newcommand{\hinr}[2]{\mathtt{inr}_{#1}({#2})}
\newcommand{\hinlp}[1]{\mathtt{inl}(#1)}
\newcommand{\hinrp}[1]{\mathtt{inr}(#1)}
\newcommand{\hmatch}[2]{\mathtt{match}(#1) \{#2\}}
\newcommand{\hcase}[5]{\mathtt{case}({#1},{#2}.{#3},{#4}.{#5})}
\newcommand{\hrules}[2]{#1 \mid #2}
\newcommand{\hrulesP}[2]{\inparens{#1 \mid #2}}
\newcommand{\hrul}[2]{#1 \Rightarrow #2}
\newcommand{\hrulP}[2]{\inparens{#1 \Rightarrow #2}}
\newcommand{\hGamma}{\dot{\Gamma}}
\newcommand{\domof}[1]{\text{dom}(#1)}
\newcommand{\hsyn}[3]{#1 \vdash #2 \Rightarrow #3}
\newcommand{\hana}[3]{#1 \vdash #2 \Leftarrow #3}
\newcommand{\hexptyp}[4]{#1 \mathbin{;} #2 \vdash #3 : #4}
\newcommand{\hpattyp}[4]{#1 : #2 \dashV #3 \mathbin{;} #4}
\newcommand{\hsubstyp}[2]{#1 : #2}
\newcommand{\hpatmatch}[3]{#1 \vartriangleright #2 \dashV #3}
\newcommand{\hnotmatch}[2]{#1 \mathbin{\bot} #2}
\newcommand{\hmaymatch}[2]{#1 \mathbin{?} #2}
\newcommand{\htrans}[2]{#1 \mapsto #2}
\newcommand{\isVal}[1]{#1 ~\mathtt{val}}
\newcommand{\isErr}[1]{#1 ~\mathtt{err}}
\newcommand{\isIndet}[1]{#1 ~\mathtt{indet}}
\newcommand{\isFinal}[1]{#1 ~\mathtt{final}}
% ZTyp and ZExp
\newcommand{\zlsel}[1]{{\bowtie}{#1}}
\newcommand{\zrsel}[1]{{#1}{\bowtie}}
\newcommand{\zwsel}[1]{
\setlength{\fboxsep}{0pt}
\colorbox{green!10!white!100}{
\ensuremath{{{\textcolor{Green}{{\hspace{-2px}\triangleright}}}}{#1}{\textcolor{Green}{\triangleleft{\vphantom{\tehole}}}}}}
}
\newcommand{\removeSel}[1]{#1^{\diamond}}
% ZTyp
\newcommand{\ztau}{\hat{\tau}}
% ZExp
\newcommand{\zexp}{\hat{e}}
% Direction
\newcommand{\dParent}{\mathtt{parent}}
\newcommand{\dChildn}[1]{\mathtt{child}~\mathtt{{#1}}}
\newcommand{\dChildnm}[1]{\mathtt{child}~{#1}}
% Action
\newcommand{\aMove}[1]{\mathtt{move}~#1}
\newcommand{\zrightmost}[1]{\mathsf{rightmost}(#1)}
\newcommand{\zleftmost}[1]{\mathsf{leftmost}(#1)}
\newcommand{\aSelect}[1]{\mathtt{sel}~#1}
\newcommand{\aDel}{\mathtt{del}}
\newcommand{\aReplace}[1]{\mathtt{replace}~#1}
\newcommand{\aConstruct}[1]{\mathtt{construct}~#1}
\newcommand{\aConstructx}[1]{#1}
\newcommand{\aFinish}{\mathtt{finish}}
\newcommand{\performAna}[5]{#1 \vdash #2 \xlongrightarrow{#4} #5 \Leftarrow #3}
\newcommand{\performAnaI}[5]{#1 \vdash #2 \xlongrightarrow{#4}\hspace{-3px}{}^{*}~ #5 \Leftarrow #3}
\newcommand{\performSyn}[6]{#1 \vdash #2 \Rightarrow #3 \xlongrightarrow{#4} #5 \Rightarrow #6}
\newcommand{\performSynI}[6]{#1 \vdash #2 \Rightarrow #3 \xlongrightarrow{#4}\hspace{-3px}{}^{*}~ #5 \Rightarrow #6}
\newcommand{\performTyp}[3]{#1 \xlongrightarrow{#2} #3}
\newcommand{\performTypI}[3]{#1 \xlongrightarrow{#2}\hspace{-3px}{}^{*}~#3}
\newcommand{\performMove}[3]{#1 \xlongrightarrow{#2} #3}
\newcommand{\performDel}[2]{#1 \xlongrightarrow{\aDel} #2}
% Form
\newcommand{\farr}{\mathtt{arrow}}
\newcommand{\fnum}{\mathtt{num}}
\newcommand{\fsum}{\mathtt{sum}}
\newcommand{\fasc}{\mathtt{asc}}
\newcommand{\fvar}[1]{\mathtt{var}~#1}
\newcommand{\flam}[1]{\mathtt{lam}~#1}
\newcommand{\fap}{\mathtt{ap}}
% \newcommand{\farg}{\mathtt{arg}}
\newcommand{\fnumlit}[1]{\mathtt{lit}~#1}
\newcommand{\fplus}{\mathtt{plus}}
\newcommand{\fhole}{\mathtt{hole}}
\newcommand{\fnehole}{\mathtt{nehole}}
\newcommand{\finj}[1]{\mathtt{inj}~#1}
\newcommand{\fcase}[2]{\mathtt{case}~#1~#2}
% Talk about formal rules in example
\newcommand{\refrule}[1]{\textrm{Rule~(#1)}}
\newcommand{\herase}[1]{\left|#1\right|_\textsf{erase}}
\newcommand{\arrmatch}[2]{#1 \blacktriangleright_{\rightarrow} #2}
\newcommand{\TABperformAna}[5]{#1 \vdash & #2 & \xlongrightarrow{#4} & #5 & \Leftarrow #3}
\newcommand{\TABperformSyn}[6]{#1 \vdash & #2 \Rightarrow #3 & \xlongrightarrow{#4} & #5 \Rightarrow #6}
\newcommand{\TABperformTyp}[3]{& #1 & \xlongrightarrow{#2} & #3}
\newcommand{\TABperformMove}[3]{#1 & \xlongrightarrow{#2} & #3}
\newcommand{\TABperformDel}[2]{#1 \xlongrightarrow{\aDel} #2}
\newcommand{\sumhasmatched}[2]{#1 \mathrel{\textcolor{black}{\blacktriangleright_{+}}} #2}
\newcommand{\subminsyn}[1]{\mathsf{submin}_{\Rightarrow}(#1)}
\newcommand{\subminana}[1]{\mathsf{submin}_{\Leftarrow}(#1)}
\newcommand{\inparens}[1]{{\color{gray}(}#1{\color{gray})}}
%% rule names for appendix
\newcommand{\rname}[1]{\textsc{#1}}
\newcommand{\gap}{\vspace{7pt}}
%% constraints
\newcommand{\consexptyp}[4]{#1 \vdash #2 {\Rightarrow} #3 {~ \vert ~} #4}
\newcommand{\ana}[4]{#1 \vdash #2 {\Leftarrow} #3 {~ \vert ~} #4}
\newcommand{\consexptypnc}[3]{#1 \vdash #2 {\Rightarrow} #3}
\newcommand{\ananc}[3]{#1 \vdash #2 {\Leftarrow} #3}
\newcommand{\econs}{\{\}}
\newcommand{\addcons}[1]{{~ \vert ~} #1}
\newcommand{\typearrow}{\blacktriangleright_{\rightarrow}}
\newcommand{\tarr}[2]{#1 \rightarrow #2}
\newcommand{\lamfunc}[2]{( \lambda #1.#2 )}
\newcommand{\ehole}{\llparenthesiscolor\rrparenthesiscolor}
\newcommand{\notehole}[1]{\llparenthesiscolor #1 \rrparenthesiscolor}
\newcommand{\underlinenum}[1]{\underline{#1}}
\newcommand{\conless}[2]{#1 \sqsubseteq #2}