-
Notifications
You must be signed in to change notification settings - Fork 4
/
heaplang.sty
89 lines (75 loc) · 3.05 KB
/
heaplang.sty
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
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{heaplang}
\RequirePackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CONCRETE LANGUAGE SYNTAX AND SEMANTICS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\textlang}[1]{\textsf{#1}}
\newcommand{\langkw}[1]{\textlang{\color{blue} #1}}
\newcommand{\lvar}[1]{\textit{#1}} % Yes, this makes language-level variables look like logic-level variables. but we still distinguish locally bound variables from global definitions.
\newcommand{\lvarA}{\lvar{\var}}
\newcommand{\lvarB}{\lvar{\varB}}
\newcommand{\lvarC}{\lvar{\varC}}
\newcommand{\loc}{\ell}
\newcommand{\mdef}{\eqdef}
\newcommand{\ldef}{:=}
\def\LetNoIn#1=#2{\langkw{let} \spac #1 \mathrel{\ldef} #2 \spac}
\def\In{\langkw{in}\spac}
\def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{\ldef} #2 \spac \langkw{in} \spac}
\def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac}
\def\Else{\spac\langkw{else} \spac}
\def\Ref(#1){\langkw{ref}\spac (#1)}
\def\Rec#1 #2={\langkw{rec}\spac #1\ {#2} \mathrel{\ldef}}
\def\Skip{\langkw{skip}}
\def\SkipN{\langkw{skipN}}
\def\Assert{\langkw{assert}}
\newcommand\Inj[1]{\langkw{inj}_{#1}\spac}
\def\Inl{\langkw{inl}}
\def\Inr{\langkw{inr}}
\def\Fst{\langkw{fst}}
\def\Snd{\langkw{snd}}
\newcommand\Proj[1]{\pi_{#1}\spac}
\def\True{\langkw{true}}
\def\False{\langkw{false}}
\def\Match#1with#2=>#3|#4=>#5end{\langkw{match} \spac #1 \spac \langkw{with}\spac#2\Ra#3\mid#4\Ra#5\spac\langkw{end}}
\def\MatchML#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
\multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
&\Ra#3\\|&\Ra#5\\%
\multicolumn{3}{l}{\langkw{end}#6}%
\end{array}}}
\def\MatchMLT#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}{rll}%
\multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
&\Ra#3\\|&\Ra#5\\%
\multicolumn{3}{l}{\langkw{end}#6}%
\end{array}}}
\def\MatchMLL#1with#2=>#3|#4=>#5|#6=>#7end#8{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
\multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
&\Ra#3\\|&\Ra#5\\|&\Ra#7\\%
\multicolumn{3}{l}{\langkw{end}#8}%
\end{array}}}
\def\MatchS#1with#2=>#3end{
\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}}
\newcommand\CAS{\langkw{CAS}}
\newcommand\CmpX{\langkw{CmpX}}
\newcommand*\Fork[1]{\langkw{fork}\spac\set{#1}}
\newcommand\deref{\mathop{!}}
\let\gets\leftarrow
\newcommand{\fold}{\langkw{fold}\spac}
\newcommand{\unfold}{\langkw{unfold}\spac}
\newcommand{\Op}[1]{\mathrel{#1}}
\newcommand{\binop}{\circledcirc}
\newcommand{\Plus}{\Op{+}}
\newcommand{\Minus}{\Op{-}}
\newcommand{\Mult}{\Op{*}}
\newcommand{\Eq}{\Op{=}}
\newcommand{\Lt}{\Op{<}}
\newcommand{\TT}{()}
\newcommand{\FAA}{\langkw{FAA}}
\newcommand{\free}{\langkw{free}\spac}
\newcommand{\heaplang}{HeapLang\xspace}
\newcommand{\assert}[1]{\langkw{assert}\ #1}
\newcommand{\tryacquire}{\mathsf{try\_acquire}}
\newcommand{\go}{\mathit{go}}
\newcommand{\none}{\Inj 1 {\TT}}
\newcommand{\some}[1]{\Inj 2 {#1}}
\newcommand{\parop}{\vert\vert}