/
macros.tex
222 lines (189 loc) · 8.47 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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
% !TEX root = hazelnut-dynamics-LIVE2017.tex
% Violet hotdogs; highlight color helps distinguish them
\newcommand{\llparenthesiscolor}{\textcolor{violet}{\llparenthesis}}
\newcommand{\rrparenthesiscolor}{\textcolor{violet}{\rrparenthesis}}
% \newcommand{\llparenthesiscolor}{\textcolor{red}{\lfloor}}
% \newcommand{\rrparenthesiscolor}{\textcolor{red}{\rfloor}}
% HTyp and HExp
\newcommand{\hcomplete}[1]{#1~\mathsf{complete}}
% HTyp
\newcommand{\htau}{\tau}
\newcommand{\tarr}[2]{#1 \rightarrow #2}
\newcommand{\tprod}[2]{#1 \times #2}
\newcommand{\tnum}{\texttt{num}}
\newcommand{\tb}{\texttt{b}}
\newcommand{\tehole}{\llparenthesiscolor\rrparenthesiscolor}
\newcommand{\tsum}[2]{{#1} + {#2}}
\newcommand{\tconsistent}[2]{#1 \sim #2}
\newcommand{\tinconsistent}[2]{#1 \nsim #2}
% HExp
\newcommand{\hexp}{\dot{e}}
\newcommand{\hlam}[2]{\lambda #1.#2}
\newcommand{\halam}[3]{\lambda #1{:}#2.#3}
\newcommand{\hap}[2]{#1(#2)}
\newcommand{\hapP}[2]{(#1)~(#2)} % Extra paren around function term
\newcommand{\hpair}[2]{(#1, #2)}
\newcommand{\hprj}[2]{\mathsf{prj}_{#1}(#2)}
\newcommand{\lblL}{\mathsf{L}}
\newcommand{\lblR}{\mathsf{R}}
\newcommand{\hnum}[1]{\underline{#1}}
\newcommand{\hadd}[2]{#1 + #2}
\newcommand{\hehole}[1]{\Circle^{#1}}
\newcommand{\heholechk}[1]{\CIRCLE^{#1}}
% \newcommand{\hhole}[1]{\setlength{\fboxsep}{0pt}\fcolorbox{red}{white}{\vphantom{)}$#1$}}
\newcommand{\hhole}[2]{\llparenthesiscolor#1\rrparenthesiscolor^{#2}}
% \newcommand{\hhole}[1]{
% \setlength{\fboxsep}{0pt}
% \colorbox{violet!10!white!100}{\ensuremath{\llparenthesiscolor#1\rrparenthesiscolor}}}
\newcommand{\hindet}[1]{\lceil#1\rceil}
\newcommand{\hinj}[2]{\texttt{inj}_{#1}({#2})}
\newcommand{\hcase}[5]{\texttt{case}({#1},{#2}.{#3},{#4}.{#5})}
\newcommand{\hGamma}{\Gamma}
\newcommand{\domof}[1]{\text{dom}(#1)}
\newcommand{\hsyn}[3]{#1 \vdash #2 \Rightarrow #3}
\newcommand{\hana}[3]{#1 \vdash #2 \Leftarrow #3}
% ZTyp and ZExp
\newcommand{\zlsel}[1]{{\bowtie}{#1}}
\newcommand{\zrsel}[1]{{#1}{\bowtie}}
%\newcommand{\zwsel}[1]{\adjustbox{cframe=blue}{\ensuremath{{\textcolor{blue}{\triangleright}}{#1}{\textcolor{blue}{\triangleleft}}}}}
\newcommand{\zwsel}[1]{
\setlength{\fboxsep}{0pt}
\colorbox{green!10!white!100}{
\ensuremath{{{\textcolor{Green}{{\hspace{-2px}\triangleright}}}}{#1}{\textcolor{Green}{\triangleleft{\vphantom{\tehole}}}}}}
}
%\newcommand{\zwsel}[1]{{\triangleright}{#1}{\triangleleft}}
\newcommand{\removeSel}[1]{#1^{\diamond}}
% ZTyp
\newcommand{\ztau}{\hat{\tau}}
% ZExp
\newcommand{\zexp}{\hat{e}}
% Direction
\newcommand{\dParent}{\mathtt{parent}}
\newcommand{\dChild}{\mathtt{firstChild}}
\newcommand{\dNext}{\mathtt{nextSib}}
\newcommand{\dPrev}{\mathtt{prevSib}}
% 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{\prodmatch}[2]{#1 \blacktriangleright_{\times} #2}
\newcommand{\summatch}[2]{#1 \blacktriangleright_{+} #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}
%%%% DYNAMICS %%%%
\newcommand{\mvar}[0]{u}
\newcommand{\subst}[0]{\sigma}
\newcommand{\dexp}[0]{\ddot{e}}
\newcommand{\dval}[0]{\ddot{v}}
\newcommand{\dcast}[2]{\langle #1 \rangle ~ #2}
\newcommand{\dlam}[3]{\lambda #1:#2.#3}
\newcommand{\dap}[2]{#1(#2)}
\newcommand{\dapP}[2]{(#1)(#2)} % Extra paren around function term
\newcommand{\dnum}[1]{\underline{#1}}
\newcommand{\dadd}[2]{#1 + #2}
\newcommand{\dehole}[2]{\llparenthesiscolor\rrparenthesiscolor^{#1}_{#2}}
\newcommand{\dhole}[3]{\llparenthesiscolor#1\rrparenthesiscolor^{#2}_{#3}}
\newcommand{\dindet}[1]{\lceil#1\rceil}
\newcommand{\dinj}[2]{\texttt{inj}_{#1}({#2})}
\newcommand{\dcase}[5]{\texttt{case}({#1},{#2}.{#3},{#4}.{#5})}
\newcommand{\expandAna}[6]{#1 \vdash #2 \Leftarrow #3 \leadsto #4 : #5 \dashv #6}
\newcommand{\expandSyn}[5]{#1 \vdash #2 \Rightarrow #3 \leadsto #4 \dashv #5}
\newcommand{\hasType}[4]{#1; #2 \vdash #3 : #4}
\newcommand{\isValue}[1]{#1~\mathsf{val}}
\newcommand{\isIndet}[1]{#1~\mathsf{indet}}
\newcommand{\isFinal}[1]{#1~\mathsf{final}}
\newcommand{\isErr}[2]{#2~\mathsf{err}_{#1}}
\newcommand{\stepsTo}[2]{#1 \mapsto_{\Delta} #2}
\newcommand{\stepsToD}[3]{#1 \mapsto_{#3} #2}
\newcommand{\Dunion}[2]{#1 \cup #2}
\newcommand{\idof}[1]{\mathsf{id}(#1)}
\newcommand{\Dbinding}[3]{#1 :: [#2]#3}
\definecolor{dRed}{rgb}{0.65, 0.0, 0.0}
\definecolor{dDkRed}{rgb}{0.35, 0.0, 0.0}
\definecolor{dLighterGreen}{rgb}{0.70, 0.95, 0.70}
\definecolor{dGreen}{rgb}{0.0, 0.65, 0.0}
\definecolor{dDkGreen}{rgb}{0.0, 0.35, 0.0}
\definecolor{dBlue}{rgb}{0.0, 0.0, 0.65}
\definecolor{dLightBlue}{rgb}{0.4, 0.4, 0.9}
\definecolor{dLighterBlue}{rgb}{0.8, 0.8, 1.0}
\definecolor{dDkBlue}{rgb}{0.0, 0.0, 0.45}
\definecolor{dLightPurple}{rgb}{0.9, 0.5, 0.9}
\definecolor{dLighterPurple}{rgb}{1.0, 0.7, 1.0}
\definecolor{dPurple}{rgb}{0.65, 0.0, 0.65}
\definecolor{dDigPurple}{rgb}{0.5, 0.0, 0.5}
% \definecolor{DDIGPURPLE}{rgb}{0.5, 0.0, 0.5} % laughable
\definecolor{dFaint}{rgb}{0.7, 0.7, 0.7}
\definecolor{dVeryFaint}{rgb}{0.9, 0.9, 0.9}
\definecolor{dGray}{rgb}{0.5, 0.5, 0.5}
\definecolor{dDark}{rgb}{0.2, 0.2, 0.2}
\definecolor{dAlmostBlack}{rgb}{0.1, 0.1, 0.1}
\definecolor{lred}{rgb}{1.0, 0.8, 0.8}
\definecolor{white}{rgb}{1.0, 1.0, 1.0}
\newcommand{\OmitThis}[1]{}
\newcommand{\metavar}[0]{u}
%Matt's hole macro
%\newcommand{\mhole}[1]{%
%{\color{dPurple}(\!|}%
%{#1}%
%{\color{dPurple}|\!)}%
%}
%\newcommand{\mhole}[1]{\colorbox{dPurple}{\colorbox{white}{\ensuremath{#1}}}}
\newcommand{\mhole}[1]{\hehole}
\newcommand{\indet}[1]{\lfloor{#1}\rfloor}
\newcommand{\desc}[1]{\textrm{#1}}
%% \newcommand{\testaction}[1]{\colorbox{dLighterGreen}{\ensuremath{#1}}}
%% \newcommand{\editaction}[1]{\colorbox{dLighterPurple}{\ensuremath{#1}}}
%% \newcommand{\editreaction}[1]{\colorbox{dLightPurple}{\ensuremath{#1}}}
%% \newcommand{\indetaction}[1]{\colorbox{dFaint}{\ensuremath{#1}}}
%% \newcommand{\detaction}[1]{\colorbox{dLightPurple}{\ensuremath{#1}}}
%% \newcommand{\stepaction}[1]{\colorbox{dLighterBlue}{#1}}
\newcommand{\testaction}[1]{\ensuremath{#1}}
\newcommand{\editaction}[1]{\ensuremath{#1}}
\newcommand{\editreaction}[1]{\ensuremath{#1}}
\newcommand{\indetaction}[1]{\ensuremath{#1}}
\newcommand{\detaction}[1]{\ensuremath{#1}}
\newcommand{\stepaction}[1]{{#1}}
\newcommand{\ScenerioOne}{Scenario 1\xspace}
\newcommand{\ScenerioOneA}{Scenario 1(a)\xspace}
\newcommand{\ScenerioOneB}{Scenario 1(b)\xspace}
\newcommand{\ScenerioTwo}{Scenario 2\xspace}
\newcommand{\Pass}{\colorbox{dLighterBlue}{P}}
\newcommand{\Fail}{\colorbox{lred}{F}}
\newcommand{\Indet}{\colorbox{dFaint}{I}}