-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathnamespaces.tex
210 lines (189 loc) · 8 KB
/
namespaces.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
\namespace{nstar:rules}{
\newcommand*\CodeTypeSequent[7]{\ensuremath{{#1};{#2};{#3};{#4};{#5}\vdash^\text{\tiny T}_\text{code}{#6:#7}}}
\newcommand*\DataTypeSequent[3]{\ensuremath{{#1}\vdash^\text{\tiny T}_\text{data}{#2:#3}}}
\newcommand*\KindSequent[3]{\ensuremath{{#1}\vdash^\text{\tiny K}{#2\ifx&\else:#3\fi}}}
\newcommand*\ISequent[9]{\ensuremath{{#1};{#2};{#3};{#4};{#5}\vdash^\text{\tiny I}{#6}\dashv{#7};{#8};{#9}}}
}{}
\namespace{nstar:grammar}{
%% TYPES
\def\Tformat#1{\color{OliveGreen}\relax\ifmmode\bm{#1}\else\textbf{#1}\fi}
%
\newcommand*\Tunsigned[1]{\ensuremath{\text{\Tformat{u#1}}}}
\newcommand*\Tsigned[1]{\ensuremath{\text{\Tformat{s#1}}}}
\VARIADIC{Tstruct}{\ensuremath}{(}{,\,}{)}{}
\VARIADIC{Tunion}{\ensuremath}{\langle}{,\,}{\rangle}{}
\newcommand*\Tbang{\ensuremath{\text{\Tformat !}}}
\newcommand*\Tptr[1]{\ensuremath{{\Tformat{{}^\ast}}#1}}
\newcommand*\Tchar{\ensuremath{\text{\Tformat{char}}}}
\newcommand*\Tcontext[3]{\ensuremath{\{ #1 \mid #2 \to #3 \}}}
\newcommand*\Tforall[2]{\ensuremath{{\Tformat \forall}(#1){\Tformat .}\,{#2}}}
\newcommand*\Tstack[2]{\ensuremath{#1\,{\Tformat \dblcolon}\,#2}}
\VARIADIC{Tsstack}{\ensuremath}{}{\,{\Tformat \dblcolon}\,}{}{}
\newcommand*\Tkind[1]{\ensuremath{\text{\Tformat{T#1}}}}
\def\Ts{\T{s}}
\def\Ta{\T{a}}
\def\Tc{\T{c}}
\let\T\Tkind
%% EXPRESSIONS
\newcommand*\Echar[1]{\ensuremath{\text{'#1'}}}
\newcommand*\EInt[2][]{\ensuremath{#1#2}}
\newcommand*\Eregister[1]{\ensuremath{\text{\bfseries \%r#1}}}
\newcommand*\Ebyteoff[2]{\ensuremath{#1(#2)}}
\newcommand*\Ebaseoff[2]{\ensuremath{#1 [#2]}}
\VARIADIC{Earray}{\ensuremath}{[}{,\,}{]}{}
\newcommand*\Estring[1]{\ensuremath{\text{"#1"}}}
\VARIADIC{Estruct}{\ensuremath}{(}{,\,}{)}{}
\let\r\Eregister
%% INSTRUCTIONS
\definecolor{kw}{HTML}{5B269A}
\def\Iformat{\ttfamily\color{kw}}
%
\newcommand*\definstr[2][0]{%
\ifnum#1=0%
\expandafter\newcommand\csname I#2\endcsname{\ensuremath{\text{\Iformat #2}}}
\else%
\expandafter\VARIADIC{I#2}{\ensuremath}{\text{\Iformat #2}\ }{,\,}{}{}
\fi%
}
%
\definstr{nop}
\definstr[1]{jmp}
\definstr[1]{call}
\definstr{ret}
\definstr{halt}
\definstr[2]{sld}
\definstr[2]{sst}
\definstr[1]{salloc}
\definstr{sfree}
\definstr[1]{sref}
\definstr[2]{ld}
\definstr[2]{st}
\definstr[2]{mv}
\definstr[3]{cjZ}
\definstr[3]{cjz}
\definstr[3]{cjnz}
\definstr[4]{cjC}
\definstr[4]{cje}
\definstr[4]{cjne}
\definstr[4]{cjl}
\definstr[4]{cjle}
\definstr[4]{cjg}
\definstr[4]{cjge}
\definstr[3]{and}
\definstr[3]{or}
\definstr[3]{xor}
\definstr[2]{not}
\definstr[3]{shiftl}
\definstr[3]{shiftr}
\definstr[3]{shiftX}
\definstr[4]{cmvZ}
\definstr[5]{cmvC}
\definstr[4]{cmvz}
\definstr[4]{cmvnz}
\definstr[5]{cmve}
\definstr[5]{cmvne}
\definstr[5]{cmvl}
\definstr[5]{cmvle}
\definstr[5]{cmvg}
\definstr[5]{cmvge}
\definstr[3]{div}
\definstr[3]{add}
\definstr[3]{sub}
\definstr[3]{mul}
% Add more instructions here, not below
\let\definstr\undefined
}{}
\namespace{nsam}{
\definecolor{kw2}{HTML}{A90D91}
\def\Ifmt{\ttfamily\bfseries\color{kw2}}
\newcommand*\definstr[2][0]{%
\ifnum#1=0%
\expandafter\newcommand\csname In#2\endcsname{\ensuremath{\text{\Ifmt #2}}}
\else%
\expandafter\VARIADIC{In#2}{}{\text{\Ifmt #2}\ }{\ }{}{}
\fi%
}
\definstr[1]{jmp}
\definstr[1]{salloc}
\definstr[1]{sfree}
\definstr{halt}
\definstr[2]{mv}
\definstr[3]{sld}
\definstr[2]{sst}
\definstr[4]{ld}
\definstr[3]{st}
\definstr[3]{sref}
\definstr[4]{cjmp}
\definstr[6]{cmv}
\definstr[4]{log2}
\definstr[4]{arith2}
\definstr[2]{not}
%% ENVS
\def\Efmt{\color{MidnightBlue}}
\newcommand*\Enstack[3]{\ensuremath{{#1}^{#2}\,{\Efmt \dblcolon}\,#3}}
\newcommand*\Enaddrof[1]{\ensuremath{{\Efmt {}^\&}#1}}
\newcommand*\Enindex[2]{\ensuremath{{#1}\left[{#2}\right]}}
\newcommand*\Enderef[1]{\ensuremath{{\Efmt {}^\ast}#1}}
\newcommand*\Enset[2]{\ensuremath{{#1}\coloneqq{#2}}}
\def\HC{H^\text{\tiny C}}
\def\HD{H^\text{\tiny D}}
%% Notations
\newcommand*\Enstate[3]{\ensuremath{\left({#1},{#2},{#3}\right)}}
\newcommand*\Enconfig[4]{\ensuremath{\left\langle{#1},\Enstate{#2}{#3}{#4}\right\rangle}}
}{}
\namespace{zilch:rules}{
\newcommand*\TypeSequent[5]{\ensuremath{{#1}\vdash{#2}:^{#3}{#4}\mid{#5}}}
\newcommand*\scale[2]{\ensuremath{{#1}{#2}}}
\newcommand*\add[2]{\ensuremath{{#1}+{#2}}}
}{}
\namespace{zilch:grammar}{
\definecolor{kw3}{HTML}{2CAB26}
\def\Ifmt{\color{kw3}}
\newcommand*\subst[3]{{#1}[{#2}/{#3}]}
\newcommand*\Etype[1]{\ensuremath{\operatorname{\mathsf{\Ifmt type}}{#1}}}
\newcommand*\Ellift[1]{\ensuremath{\uparrow {#1}}}
\newcommand*\Elsuc[1]{\ensuremath{\operatorname{\mathsf{\Ifmt lsuc}}{#1}}}
\newcommand*\Elmax[2]{\ensuremath{{#1}\mathrel{\mathsf{\Ifmt \sqcup}}{#2}}}
\newcommand*\Elevel{\ensuremath{\mathsf{\Ifmt level}}}
\newcommand*\Etotal{\ensuremath{\langle\rangle}}
\newcommand*\Efun[3]{\ensuremath{{#1}\mathrel{\mathsf{\Ifmt \rightarrow}}{#2}\ {#3}}}
\newcommand*\Epi[5]{\Efun{({#2}\ {#1} : {#3})}{#4}{#5}}
\newcommand*\Elam[4]{\ensuremath{\mathsf{\Ifmt \lambda}({#2}\ {#1} : {#3})\mathrel{\mathsf{\Ifmt \Rightarrow}}{#4}}}
\newcommand*\Eeffect{\ensuremath{\mathsf{\Ifmt effect}}}
\newcommand*\Eeffectrow[2]{\ensuremath{\mathsf{\Ifmt \langle}{#1}\mathrel{\mathsf{\Ifmt \mid}}{#2}\mathsf{\Ifmt \rangle}}}
\newcommand*\Eapp[2]{\ensuremath{{#1}({#2})}}
\newcommand*\Eaddunit{\ensuremath{\mathsf{\Ifmt \langle\rangle}}}
\newcommand*\Etop{\ensuremath{\mathsf{\Ifmt \top}}}
\newcommand*\Emultunit{\ensuremath{\mathsf{\Ifmt ()}}}
\newcommand*\Eone{\ensuremath{\mathsf{\mathbf{\Ifmt 1}}}}
\newcommand*\Emultunitelim[4]{\ensuremath{\mathsf{\Ifmt let}\ {#2}\ \Emultunit\ \mathsf{\Ifmt as}\ {#1}\mathrel{\mathsf{\Ifmt \coloneqq}}{#3}\mathrel{\mathsf{\Ifmt ;}}{#4}}}
\newcommand*\Edo[1]{\ensuremath{\mathsf{\Ifmt do}\ {#1}}}
\newcommand*\Eunderscore{\ensuremath{\mathsf{\Ifmt \underline{\hspace{2mm}}}}}
\newcommand*\Etensor[4]{\ensuremath{({#2}\ {#1} : {#3})\mathrel{\mathsf{\Ifmt \otimes}}{#4}}}
\newcommand*\Eand[3]{\ensuremath{({#1} : {#2})\mathrel{\mathsf{\Ifmt \&}}{#3}}}
\newcommand*\Emultpair[2]{\ensuremath{\mathsf{\Ifmt (}{#1}\mathrel{\mathsf{\Ifmt ,}}{#2}\mathsf{\Ifmt )}}}
\newcommand*\Eaddpair[2]{\ensuremath{\mathsf{\Ifmt \langle}{#1}\mathrel{\mathsf{\Ifmt ,}}{#2}\mathsf{\Ifmt \rangle}}}
\newcommand*\Eaccess[2]{\ensuremath{{#1}\mathsf{\Ifmt \dblcolon}{#2}}}
\newcommand*\Emultpairelim[6]{\ensuremath{\mathsf{\Ifmt let}\ {#4}\ \Emultpair{#1}{#2}\ \mathsf{\Ifmt as}\ {#3}\mathrel{\mathsf{\Ifmt \coloneqq}}{#5}\mathrel{\mathsf{\Ifmt ;}}{#6}}}
\newcommand*\Ebool{\ensuremath{\mathsf{\Ifmt bool}}}
\newcommand*\Etrue{\ensuremath{\mathsf{\Ifmt true}}}
\newcommand*\Efalse{\ensuremath{\mathsf{\Ifmt false}}}
\newcommand*\Eifthenelse[3]{\ensuremath{\mathsf{\Ifmt if}\ {#1}\ \mathsf{\Ifmt then}\ {#2}\ \mathsf{\Ifmt else}\ {#3}}}
\newcommand*\Eunsigned[1]{\ensuremath{\mathsf{\Ifmt u{#1}}}}
\newcommand*\Esigned[1]{\ensuremath{\mathsf{\Ifmt s{#1}}}}
\newcommand*\Echar{\ensuremath{\mathsf{\Ifmt char}}}
\newcommand*\Eref[2]{\ensuremath{\operatorname{\mathsf{\Ifmt ref}}{#1}\;\mathsf{\Ifmt @}\;{#2}}}
\newcommand*\Eletin[5]{\ensuremath{\mathsf{\Ifmt let}\ {#2}\ {#1}\ \mathsf{\Ifmt :}\ {#3}\mathrel{\mathsf{\Ifmt \coloneqq}}{#4}\mathrel{\mathsf{\Ifmt ;}}{#5}}}
\newcommand*\Erecin[5]{\ensuremath{\mathsf{\Ifmt rec}\ {#2}\ {#1}\ \mathsf{\Ifmt :}\ {#3}\mathrel{\mathsf{\Ifmt \coloneqq}}{#4}\mathrel{\mathsf{\Ifmt ;}}{#5}}}
\newcommand*\Ediv{\ensuremath{\mathsf{\Ifmt div}}}
\newcommand*\Eterminates[1]{\ensuremath{\mathsf{terminates?}({#1})}}
\newcommand*\Efix[2]{\ensuremath{\mathsf{\Ifmt fix}({#1})\mathrel{\mathsf{\Ifmt \Rightarrow}}{#2}}}
\newcommand*\Ewithhnd[6]{\ensuremath{\mathsf{\Ifmt with}\ {#1}\ \mathsf{\Ifmt let}\ {#2}\ {#3}{#4}\mathrel{\mathsf{\Ifmt \coloneqq}}{#5}\mathrel{\mathsf{\Ifmt ;}}{#6}}}
\newcommand*\Ewith[2]{\ensuremath{\mathsf{\Ifmt with}\ {#1}\mathrel{\mathsf{\Ifmt ;}}{#2}}}
\newcommand*\Eresume{\ensuremath{\mathsf{\Ifmt resume}}}
\newcommand*\Ederef[1]{\ensuremath{\mathsf{\Ifmt !}{#1}}}
\newcommand*\Emkref[1]{\ensuremath{\mathsf{\Ifmt \&}{#1}}}
\newcommand*\Eregion{\ensuremath{\mathsf{\Ifmt region}}}
\newcommand*\surface[1]{\ensuremath{{\color{Fuchsia}\mathsf{#1}}}}
\newcommand*\core[1]{\ensuremath{{\color{WildStrawberry}\mathsf{#1}}}}
}{}