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