1%
2% Copyright 2016, NICTA
3%
4% This software may be distributed and modified according to the terms of
5% the GNU General Public License version 2. Note that NO WARRANTY is provided.
6% See "LICENSE_GPLv2.txt" for details.
7%
8% @TAG(NICTA_GPL)
9%
10
11%\newlength{\tpheight}\setlength{\tpheight}{0.9\textheight}
12%\newlength{\txtheight}\setlength{\txtheight}{0.9\tpheight}
13%\newlength{\tpwidth}\setlength{\tpwidth}{0.9\textwidth}
14%\newlength{\txtwidth}\setlength{\txtwidth}{0.9\tpwidth}
15%\newlength{\drop}                     
16%\setlength{\parindent}{0cm}
17%\setlength{\parskip}{9pt plus 1pt minus 1pt}
18\newcommand{\alt}{\;\mid\;}
19
20\newcommand{\boxlabel}[1]{\begin{center}
21\framebox{#1}
22\end{center}}
23
24\setlength{\fboxsep}{1pt}
25
26\newsavebox{\@brx}
27\newcommand{\llangle}[1][]{\savebox{\@brx}{\(\m@th{#1\langle}\)}%
28    \mathopen{\copy\@brx\mkern2mu\kern-0.9\wd\@brx\usebox{\@brx}}}
29\newcommand{\rrangle}[1][]{\savebox{\@brx}{\(\m@th{#1\rangle}\)}%
30    \mathclose{\copy\@brx\mkern2mu\kern-0.9\wd\@brx\usebox{\@brx}}}
31
32\newenvironment{inductive}[1]{\boxlabel{$#1$} \vspace{-0.8em} \start@gather\st@rredtrue}{\endgather}
33\newenvironment{inductive0}{\vspace{-0.8em} \start@gather\st@rredtrue}{\endgather}
34% Side by Side layout
35\newenvironment{sidebyside}{
36\begin{tabular}{p{0.48\textwidth}p{0.5\textwidth}}
37  }{
38\end{tabular}
39}
40\newenvironment{fundef}[2]{\begin{center}\boxlabel{$#1 : #2$} \begin{displaymath}\begin{array}{lclr}}{  \end{array}\end{displaymath}\end{center}}
41\newcommand{\taken}[1]{\text{\sout{\ensuremath{#1}}}}
42\newcommand{\PrimType}[1]{\texttt{#1}}
43\newcommand{\Observed}[1]{#1!}
44\newcommand{\Unit}{\texttt{()}}
45\newcommand{\AbsN}[1]{\texttt{#1}}
46\newcommand{\AbsTy}[3]{\AbsN{#1}\ #2\ #3}
47\newcommand{\FunTy}[2]{#1 \rightarrow #2}
48\newcommand{\PrdTy}[2]{#1 \times #2}
49\newcommand{\PolyTy}[2]{\forall (#1).\ #2}
50\newcommand{\VariantTy}[1]{\langle #1 \rangle}
51\newcommand{\RecordTy}[2]{\{ #1 \}\ #2}
52\newcommand{\ConsN}[1]{\mathsf{#1}}
53\newcommand{\FunN}[1]{#1}
54\newcommand{\VarN}[1]{#1}
55\newcommand{\Cons}[2]{\ConsN{#1}\ #2}
56\newcommand{\FieldN}[1]{\text{#1}}
57\newcommand{\FieldTy}[2]{\FieldN{#1}\ :: #2}
58\newcommand{\FieldEq}[2]{\FieldN{#1}\ = #2}
59\newcommand{\Discardable}{\mathsf{D}}
60\newcommand{\Shareable}{\mathsf{S}}
61\newcommand{\Escapable}{\mathsf{E}}
62\newcommand{\Linear}{\mathsf{DS}}
63\newcommand{\TyApp}[2]{\FunN{#1}[#2]}
64\newcommand{\GenPrimOp}[2]{#1(#2)}
65\newcommand{\LET}{\mathbf{let}}
66\newcommand{\IN}{\mathbf{in}}
67\newcommand{\CAST}{\mathbf{cast}}
68\newcommand{\SPLIT}{\mathbf{split}}
69\newcommand{\IF}{\mathbf{if}}
70\newcommand{\PROMOTE}{\mathbf{promote}}
71\newcommand{\THEN}{\mathbf{then}}
72\newcommand{\ELSE}{\mathbf{else}}
73\newcommand{\OF}{\mathbf{of}}
74\newcommand{\CASE}{\mathbf{case}}
75\newcommand{\ESAC}{\mathbf{esac}}
76\newcommand{\TAKE}{\mathbf{take}}
77\newcommand{\PUT}{\mathbf{put}}
78\newcommand{\VAR}{\mathbf{var}}
79\newcommand{\Let}[3]{\LET\ \VarN{#1} = #2\ \IN\ #3}
80\newcommand{\LetBang}[4]{\LET!(\VarN{#1})\ \VarN{#2} = #3\ \IN\ #4}
81\newcommand{\Cast}[2]{\CAST\ #1\ #2}
82\newcommand{\Split}[3]{\SPLIT\ #1\ \IN\ \VarN{#2}.\ #3}
83%\newcommand{\Split}[3]{\FIXME{Split now absent.}}
84\newcommand{\Promote}[2]{\PROMOTE\ \VariantTy{#1}\ #2}
85\newcommand{\If}[3]{\IF\ #1\ \THEN\ #2\ \ELSE\ #3}
86\newcommand{\Esac}[1]{\ESAC\ #1}
87\newcommand{\Case}[5]{\CASE\ #1\ \OF\ #2 \rightarrow #3\ \ELSE\ #4 \rightarrow #5}
88\newcommand{\Take}[5]{\TAKE\ \VarN{#1}\ \{ \FieldEq{#2}{#3} \} = #4\ \IN\ #5}
89\newcommand{\Put}[3]{\PUT\ #1.\FieldN{#2} \coloneqq #3}
90\newcommand{\FunDef}[4]{\langle #1 :: #2, #1\ \VarN{#3} = #4\rangle}
91\newcommand{\AbsFunDef}[2]{\langle #1 :: #2, \blacksquare\rangle}
92\newcommand{\StructInit}[1]{\{ #1 \}}
93\newcommand{\Tup}[2]{(#1,#2)}
94%\newcommand{\Tup}[2]{\FIXME{Tuples now absent.}}
95\newcommand{\App}[2]{#1\ #2}
96\newcommand{\Member}[2]{#1.\FieldN{#2}}
97\newcommand{\ModeN}[1]{\texttt{#1}}
98\newcommand{\ReadOnly}{\ModeN{r}}
99\newcommand{\Writable}{\ModeN{w}}
100\newcommand{\Unboxed}{\ModeN{u}}
101\newcommand{\perhaps}[1]{#1^?}
102\newcommand{\many}[1]{\overline{#1}}
103\newcommand{\OfKind}[2]{#1 ::_{\mathrm{K}} #2}
104\newcommand{\ofKind}[2]{#1 :_{\mathrm{K}} #2}
105\newcommand{\ofType}[2]{#1 : #2}
106\newcommand{\ofTypeS}[2]{#1 :\!*\ #2}
107\newcommand{\Kinding}[3]{#1 \vdash \ofKind{#2}{#3} }
108\newcommand{\BangF}[1]{\textbf{bang}(#1)}
109\newcommand{\LitType}[1]{\textbf{litType}(#1)}
110%\newcommand{\FunType}[1]{\textbf{funType}(#1)}
111\newcommand{\FunType}[1]{\FIXME{funType now absent}}
112%\newcommand{\FunTypes}{\textbf{funType}}
113\newcommand{\FunTypes}[1]{\FIXME{funType now absent}}
114%\newcommand{\FunTyEnv}[2]{\textbf{funType}(#1) = #2}
115\newcommand{\FunTyEnv}[2]{\textbf{funDef}(#1) = \langle#2,\_\rangle}
116\newcommand{\AbsFunTyEnv}[2]{\textbf{funDef}(#1) = \langle#2,\blacksquare\rangle}
117%\newcommand{\FunTyEnv}[1]{\FIXME{funType now absent}}
118\newcommand{\Typing}[4]{#1; #2 \vdash \ofType{#3}{#4}}
119\newcommand{\TypingS}[4]{#1; #2 \vdash \ofTypeS{#3}{#4}}
120\newcommand{\Subst}[3]{#1[#3 / #2]}
121\newcommand{\Weakening}[3]{#1 \vdash #2 \stackrel{\text{weak}}{\leadsto} #3}
122\newcommand{\Contraction}[4]{#1 \vdash #2 \leadsto #3 \boxplus #4}
123\newcommand{\PrimOpType}[1]{\textbf{primopType}(#1)}
124\newcommand{\ValSem}[3]{#1 \vdash #2 \Downarrow_v #3}
125\newcommand{\FunVal}[2]{ \llangle \lambda #1.\ #2 \rrangle }
126\newcommand{\AbsFunVal}[2]{ \llangle \textbf{abs.} #1\ |\ #2 \rrangle }
127\newcommand{\FunDefn}[1]{\textbf{funDef}(#1)}
128\newcommand{\FunDefns}{\textbf{funDef}}
129\newcommand{\EnvBind}[2]{#1 \mapsto #2}
130\newcommand{\rulename}[1]{\textsc{\small#1}}
131\newcommand{\semantics}[1]{\llbracket #1 \rrbracket}
132\newcommand{\AValSem}[2]{\semantics{#1}_v\ #2}
133\newcommand{\AUpdSem}[1]{\semantics{#1}_u}
134\newcommand{\AbsValSem}[3]{\AValSem{#1}{#2} = #3}
135\newcommand{\AbsUpdSem}[5]{\AUpdSem{#1}\ (#2,#3) = (#4,#5)}
136\newcommand{\RecordVal}[1]{\StructInit{#1}}
137\newcommand{\UpdSem}[5]{#1 \vdash #2\ |\ #3 \Downarrow_u #4\ |\ #5}
138\newcommand{\UpdSemA}[5]{#1 \vdash #2\ |\ #3 \Downarrow_u\!\!*\ #4\ |\ #5}
139\newcommand{\HiBlue}[1]{\text{\colorbox{light-gray}{$\textcolor{blue}{#1}$}}}
140\newcommand{\HiPurple}[1]{\textcolor{purple}{#1}}
141\newcommand{\VTRN}[6]{#1\ |\ #2 : #3 :\ #4\ [#5 \ast #6]}
142\newcommand{\VTR}[6]{\HiBlue{#1\ |\ #2 :}\ \HiPurple{#3 :}\ #4\ \HiBlue{[#5 \ast #6]}}
143\newcommand{\VTRA}[6]{\HiBlue{#1\ |\ #2 :\!\!*}\ \HiPurple{#3 :\!\!*}\ #4\ \HiBlue{[#5 \ast  #6]}}
144\newcommand{\VTRAbs}[6]{\HiBlue{#1\ |\ #2 :_A}\ \HiPurple{#3 :_A}\ #4\ \HiBlue{[#5 \ast #6]}}
145\newcommand{\dash}{\mbox{-}}
146\newcommand{\set}{\ensuremath{\mathit{set}}\xspace}
147\newcommand{\bool}{\ensuremath{\mathit{bool}}\xspace}
148\newcommand{\monad}{\ensuremath{\mathit{monad}}\xspace}
149
150\newcommand{\srel}{\ensuremath{\mathit{\mathcal{R}}}\xspace}
151\newcommand{\valrel}{\ensuremath{\mathit{val\dash{}rel}}\xspace}
152\newcommand{\typerel}{\ensuremath{\mathit{type\dash{}rel}}\xspace}
153\newcommand{\heaprelptr}{\ensuremath{\mathit{heap\dash{}rel\dash{}ptr}}\xspace}
154\newcommand{\heaprel}{\ensuremath{\mathit{heap\dash{}rel}}\xspace}
155\newcommand{\heap}{\ensuremath{\mathit{heap}}\xspace}
156\newcommand{\isvalid}{\ensuremath{\mathit{is\dash{}valid}}\xspace}
157
158\newcommand{\TYPE}{\ensuremath{\mathit{TYPE}}\xspace}
159
160\newcommand{\corres}{\ensuremath{\mathbf{corres}}\xspace}
161\newcommand{\correspond}{\ensuremath{\mathbf{correspondence}}\xspace}
162\newcommand{\corresargs}[2]{\ensuremath{\corres \ R\ #1 \ #2 \ U \ \Gamma \ \mu \ \sigma}\xspace}
163\newcommand{\corresargsE}[4]{\ensuremath{\corres \ R\ #1 \ #2 \ #3 \ #4 \ \mu \ \sigma}\xspace}
164
165\newcommand{\scorres}{\ensuremath{\mathbf{scorres}}\xspace}
166\newcommand{\monoexpr}{\ensuremath{\mathcal{M}_e}\xspace}
167\newcommand{\monoval}{\ensuremath{\mathcal{M}_v}\xspace}
168\newcommand{\rename}{\ensuremath{r}\xspace}
169
170\newcommand{\some}{\ensuremath{\mathit{Some}}\xspace}
171\newcommand{\none}{\ensuremath{\mathit{None}}\xspace}
172\newcommand{\failed}{\ensuremath{\mathit{failed}}\xspace}
173\newcommand{\results}{\ensuremath{\mathit{results}}\xspace}
174
175\newcommand{\mreturn}{\ensuremath{\mathbf{return}}\xspace}
176\newcommand{\mgets}{\ensuremath{\mathbf{gets}}\xspace}
177