tutorial/fpmacros.sty · Idris-dev

git.iko.soy/Idris-dev

on d1663cc help sign in

Idris-dev/tutorial/fpmacros.sty

1086 lines 33 kB history raw

1%% ------------------------------------------- [ Functional Programming Macros ]

2%% A Package to provide support for functional programming.

3%%

4\NeedsTeXFormat{LaTeX2e}[1994/06/01]

5\ProvidesPackage{fpmacros}[2013/12/17 fpmacros]

6%% ------------------------------------------------------- [ Required Packages ]

7\RequirePackage{ifthen}

8\RequirePackage{amssymb}

9\RequirePackage{latexsym}

10\RequirePackage{eepic}

11\RequirePackage{fancyvrb}

12%% ----------------------------------------------------- [ Option Delcarations ]

13\newboolean{useverb}

14\setboolean{useverb}{true}

16\DeclareOption{noverb}{%

17 \setboolean{useverb}{false}

18}

20\ProcessOptions\relax

22%% --------------------------------------------------------- [ Inference Rules ]

23\newlength{\rulevgap}

24\setlength{\rulevgap}{0.05in}

25\newlength{\ruleheight}

26\newlength{\ruledepth}

27\newsavebox{\rulebox}

28\newlength{\GapLength}

29\newcommand{\gap}[1]{\settowidth{\GapLength}{#1} \hspace*{\GapLength}}

30\newcommand{\dotstep}[2]{\begin{tabular}[b]{@{}c@{}}

31 #1\\$\vdots$\\#2

32 \end{tabular}}

33\newlength{\fracwid}

34\newcommand{\dotfrac}[2]{\settowidth{\fracwid}{$\frac{#1}{#2}$}

35 \addtolength{\fracwid}{0.1in}

36 \begin{tabular}[b]{@{}c@{}}

37 $#1$\\

38 \parbox[c][0.02in][t]{\fracwid}{\dotfill} \\

39 $#2$\\

40 \end{tabular}}

41\newcommand{\Rule}[2]{\savebox{\rulebox}[\width][b] %

42 {$ \frac{\raisebox{0in} {\( #1 $}} %

43 {\raisebox{-0.03in}{$ #2 $}} \)} %

44 \settoheight{\ruleheight}{\usebox{\rulebox}} %

45 \addtolength{\ruleheight}{\rulevgap} %

46 \settodepth{\ruledepth}{\usebox{\rulebox}} %

47 \addtolength{\ruledepth}{\rulevgap} %

48 \raisebox{0in}[\ruleheight][\ruledepth] %

49 {\usebox{\rulebox}}}

50\newcommand{\Case}[2]{\savebox{\rulebox}[\width][b] %

51 {$ \dotfrac{\raisebox{0in} {\( #1 $}} %

52 {\raisebox{-0.03in}{$ #2 $}} \)} %

53 \settoheight{\ruleheight}{\usebox{\rulebox}} %

54 \addtolength{\ruleheight}{\rulevgap} %

55 \settodepth{\ruledepth}{\usebox{\rulebox}} %

56 \addtolength{\ruledepth}{\rulevgap} %

57 \raisebox{0in}[\ruleheight][\ruledepth] %

58 {\usebox{\rulebox}}}

59\newcommand{\Axiom}[1]{\savebox{\rulebox}[\width][b] %

60 {$\frac{}{\raisebox{-0.03in}{$#1$}}$} %

61 \settoheight{\ruleheight}{\usebox{\rulebox}} %

62 \addtolength{\ruleheight}{\rulevgap} %

63 \settodepth{\ruledepth}{\usebox{\rulebox}} %

64 \addtolength{\ruledepth}{\rulevgap} %

65 \raisebox{0in}[\ruleheight][\ruledepth] %

66 {\usebox{\rulebox}}}

67\newcommand{\RuleSide}[3]{\gap{$#2$} \hspace*{0.1in} %

68 \Rule{#1}{#3} %

69 \hspace*{0.1in}$#2$}

70\newcommand{\AxiomSide}[2]{\gap{$#1$} \hspace*{0.1in} %

71 \Axiom{#2} %

72 \hspace*{0.1in}$#1$}

73\newcommand{\RULE}[1]{\textbf{#1}}

74\newcommand{\hg}{\hspace{0.2in}}

76\newcommand{\ProofState}

77 [2]{\parbox{10cm}{\AR{\hg\AR{#1}\\\Axiom{\hg#2\hg}}}}

79%%%%%%%%%%%% TRISTUFF

81\newcommand{\btr}{

82\setlength{\unitlength}{0.0005in}

83\begin{picture}(69,180)(0,12)

84\blacken\path(57,192)(57,12)(12,102)

85 (57,192)(57,192)

86\path(57,192)(57,12)(12,102)

87 (57,192)(57,192)

88\end{picture}

89}

91\newcommand{\btl}{

92\setlength{\unitlength}{0.0005in}

93\begin{picture}(69,180)(0,12)

94\blacken\path(12,192)(12,12)(57,102)

95 (12,192)(12,192)\path(12,192)(12,12)(57,102)

96 (12,192)(12,192)

97\end{picture}

98}

100\newcommand{\wtr}{

101\setlength{\unitlength}{0.0005in}

102\begin{picture}(69,180)(0,12)

103%\blacken\path(57,192)(57,12)(12,102)

104% (57,192)(57,192)

105\path(57,192)(57,12)(12,102)

106 (57,192)(57,192)

107\end{picture}

108}

109

110\newcommand{\wtl}{

111\setlength{\unitlength}{0.0005in}

112\begin{picture}(69,180)(0,12)

113%\blacken\path(12,192)(12,12)(57,102)

114% (12,192)(12,192)

115\path(12,192)(12,12)(57,102)

116 (12,192)(12,192)

117\end{picture}

118}

119

120

121

122%%%%%%%%%%%% FONTS

123

124\newcommand{\TC}[1]{\mathsf{#1}}

125\newcommand{\DC}[1]{\mathsf{#1}}

126\newcommand{\VV}[1]{\mathit{#1}}

127\newcommand{\FN}[1]{\mathbf{#1}}

128\newcommand{\HFN}[1]{\mathtt{#1}}

129\newcommand{\RW}[1]{\underline{\textrm{#1}}}

130\newcommand{\MO}[1]{\mbox{\textsc{#1}}}

131

132\newcommand{\tTC}[1]{\texttt{#1}}

133\newcommand{\tDC}[1]{\texttt{#1}}

134\newcommand{\tFN}[1]{\texttt{#1}}

135

136\newcommand{\HF}[1]{\mathtt{#1}}

137

138\newcommand{\MV}[1]{\nhole\mathit{#1}}

139\newcommand{\Lang}[1]{\mathsf{#1}}

140\newcommand{\Name}[1]{\mathit{#1}}

141

142\newcommand{\demph}[1]{\textbf{#1}}

143\newcommand{\remph}[1]{\emph{#1}}

144

145%%%% Keywords for meta operations

146\newcommand{\IF}{\;\RW{if}\;\;}

147\newcommand{\THEN}{\RW{then}}

148\newcommand{\ELSE}{\RW{else}}

149\newcommand{\AND}{\RW{and}}

150\newcommand{\Otherwise}{\RW{otherwise}}

151\newcommand{\Do}{\RW{do}}

152\newcommand{\Return}{\RW{return}}

153

154\newcommand{\CASE}{\RW{case}}

155\newcommand{\LET}{\RW{let}}

156\newcommand{\IN}{\RW{in}}

157\newcommand{\of}{\RW{of}}

158

159\newcommand{\CLASS}{\mathtt{class}}

160\newcommand{\INSTANCE}{\mathtt{instance}}

161

162%%%%%%%%%%%% GROUPING

163

164\newcommand{\G}{

165\setlength{\unitlength}{1pt}

166\begin{picture}(4,10)(0,0)

167\path(2,10)(2,-10)

168\end{picture}

169}

170

171\newcommand{\E}{

172\setlength{\unitlength}{1pt}

173\begin{picture}(4,10)(0,0)

174\path(2,10)(2,-2)(4,-2)

175\end{picture}

176}

177

178%\newcommand{\C}{

179%\setlength{\unitlength}{1pt}

180%\begin{picture}(4,10)(0,0)

181%\path(4,8)(2,8)(2,-2)(4,-2)

182%\end{picture}

183%}

184

185\newcommand{\M}{

186\setlength{\unitlength}{1pt}

187\begin{picture}(4,10)(0,0)

188\path(2,10)(2,-2)(6,-2)

189\end{picture}

190}

191

192\newcommand{\F}{

193\setlength{\unitlength}{1pt}

194\begin{picture}(4,10)(0,0)

195\path(4,8)(2,8)(2,-6)

196\end{picture}

197}

198

199\newcommand{\K}{

200\setlength{\unitlength}{1pt}

201\begin{picture}(4,10)(0,0)

202\path(0,8)(4,8)

203\end{picture}

204}

205

206\newcommand{\J}{

207\setlength{\unitlength}{1pt}

208\begin{picture}(4,10)(0,0)

209\path(0,-2)(4,-2)

210\end{picture}

211}

212

213\newcommand{\W}{

214\setlength{\unitlength}{1pt}

215\begin{picture}(4,10)(0,0)

216\end{picture}

217}

218

219

220

221%%%%%%%%%%%% GUBBINS

222

223\newcommand{\mathskip}{\medskip}

224

225\newcommand{\fbx}[1]{\fbox{$#1$}}

226\newcommand{\stk}[1]{\begin{array}{c}#1\end{array}}

227%\newcommand{\DM}[1]{\hg\mbox{$#1$}}

228\newcommand{\DM}[1]{\mathskip\par$#1$\mathskip}

229\newcommand{\mbx}[1]{\mathskip\par\noindent$#1$\mathskip}

230\newcommand{\AR}[1]{\begin{array}[t]{@{}l}#1\end{array}}

231\newcommand{\ARt}[1]{\begin{array}[t]{@{}l@{}cl}#1\end{array}}

232\newcommand{\ARc}[1]{\begin{array}{@{}l}#1\end{array}}

233\newcommand{\ARd}[1]{\begin{array}[t]{cl}#1\end{array}}

234\newcommand{\DAR}[1]{\begin{array}{ll}\hg & #1\end{array}}

235\newcommand{\Dor}{\\ \hg\mid & }

236\newcommand{\EA}[1]{\begin{array}[t]{r@{}c@{}l}#1\end{array}}

237\newcommand{\A}{@{\:}c}

238%\newcommand{\R}{@{\:}r}

239\newcommand{\CA}{c}

240\newcommand{\LA}{l}

241\newcommand{\PAc}[2]{\begin{array}{l#1@{}r@{}l}#2\end{array}}

242\newcommand{\PA}[2]{\begin{array}[t]{l@{\:}l#1@{}r@{\:}l}#2\end{array}}

243\newcommand{\DTREE}[3]{\begin{array}[t]{l#1@{}r@{\:}l#2}#3\end{array}}

244\newcommand{\IDTREE}[2]{%

245 \begin{array}[t]{l@{\:}c@{\:}l@{\:}r@{\:}l#1}#2\end{array}}

246\newcommand{\IA}[2]

247 {\begin{array}[t]{l@{\:}r@{\:}c@{\:}l@{\:}#1@{\:}r@{\:}l}#2\end{array}}

248\newcommand{\IAc}[2]

249 {\begin{array}[c]{r@{\:}c@{\:}l@{\:}#1@{}r@{}l}#2\end{array}}

250\newcommand{\CS}[1]{\left\lfloor\begin{array}{@{}l}#1\end{array}\right.}

251\newcommand{\BY}[3]{\multicolumn{2}{l}{\;\RW{by}\; #1} \\ %

252 \multicolumn{#2}{l}{\CS{#3}} }

253\newcommand{\WITH}[3]{\multicolumn{2}{l}{\;\RW{with}\; #1} \\ %

254 \multicolumn{#2}{l}{\CS{#3}} }

255\newcommand{\WithBy}{\RW{with-by}}

256\newcommand{\Wb}[1]{\WithBy& #1}

257\newcommand{\By}[1]{\multicolumn{2}{l}{\Leftarrow #1}}

258\newcommand{\andby}{\Leftarrow}

259\newcommand{\MyWith}[1]{\multicolumn{2}{l}{|\;#1}}

260\newcommand{\Byr}[1]{\;\RW{by}\; #1}

261

262\newcommand{\Bar}{|}

263\newcommand{\Bart}{\settowidth{\GapLength}{$\Bar$}%

264 \raisebox{6pt}[0pt][0pt]{$\Bar$}%

265 \hspace*{-1\GapLength}%

266 \Bar}

267\newcommand{\With}[1]{\Bar & #1}

268\newcommand{\Witt}[1]{\Bart & #1}

269

270\newcommand{\B}{@{\:}r@{\:}c}

271\newcommand{\Ret}[1]{\multicolumn{2}{l}{\cq #1}}

272\newcommand{\MRet}[2]{\multicolumn{#1}{l}{\cq #2}}

273\newcommand{\HRet}[1]{\multicolumn{2}{l}{\hq #1}}

274\newcommand{\MHRet}[2]{\multicolumn{#1}{l}{\hq #2}}

275\newcommand{\IRet}[1]{\multicolumn{2}{l}{\iq #1}}

276\newcommand{\IMRet}[2]{\multicolumn{#1}{l}{\iq #2}}

277\newcommand{\MoRet}[1]{\multicolumn{2}{l}{\mq #1}}

278\newcommand{\MMoRet}[2]{\multicolumn{#1}{l}{\mq #2}}

279\newcommand{\Data}{\RW{data}}

280\newcommand{\Codata}{\RW{codata}}

281\newcommand{\Where}{\RW{where}}

282\newcommand{\Let}{\RW{let}}

283\newcommand{\Fact}{\RW{fact}}

284\newcommand{\Rec}[1]{#1\textbf{-Rec}}

285\newcommand{\Memo}[1]{#1\textbf{-Memo}}

286\newcommand{\Elim}[1]{#1\textbf{-Elim}}

287\newcommand{\Cases}[1]{#1\textbf{-Case}}

288\newcommand{\View}[1]{#1\textbf{-View}}

289\newcommand{\As}[2]{#1 \:\RW{as}\: #2}

290\newcommand{\nhole}{\Box}

291\newcommand{\turq}{\:\vdash_?\:}

292\newcommand{\split}{\;\lhd\;}

293\newcommand{\CType}[2]{\{#1 \split\; #2\}}

294\newcommand{\CC}[2]{(#1)\:#2}

295\newcommand{\UP}[2]{#1 | \{#2\}}

296\newcommand{\Ured}{\:\Downarrow\:}

297\newcommand{\gdd}{\prec}

298\newcommand{\HC}[1]{\left<#1\right>}

299\newcommand{\HT}[2]{\left<#1 \hab #2\right>}

300

301\newcommand{\view}{\RW{view}}

302\newcommand{\ecase}{\RW{case}}

303\newcommand{\rec}{\RW{rec}}

304

305\newcommand{\If}{\mathsf{if}}

306\newcommand{\Then}{\mathsf{then}}

307\newcommand{\Else}{\mathsf{else}}

308\newcommand{\elim}{\RW{elim}}

309

310\newcommand{\Payload}{\mathsf{type}}

311\newcommand{\Any}{\mathsf{Some}}

312

313\newcommand{\lbl}[2]{\langle #1 \Hab #2 \rangle}

314\newcommand{\call}[2]{\RW{call}\:\langle#1\rangle\:#2}

315\newcommand{\return}[1]{\RW{return}\:#1}

316

317\newcommand{\Remark}[1]{\noindent\textbf{Remark:} #1}

318

319\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}

320

321\ifthenelse{\boolean{useverb}}{%

322 \newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}

323 \newcommand{\useverb}[1]{\BUseVerbatim{#1}}

324 \newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

325 \newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

326 \newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

327 \newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}

328 \newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

329 \newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

330 \newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

331}{}

332

333\newcommand{\diagfig}[3]{\begin{figure}[h]\begin{center}\includegraphics[width=#1]{#2}\end{center}

334\caption{#3}\label{#2}\end{figure}}

335\newcommand{\diagfigtc}[3]{\begin{figure*}[t]\begin{center}\includegraphics[width=#1]{#2}\end{center}

336\caption{#3}\label{#2}\end{figure*}}

337

338\newcommand{\FIG}[3]{\begin{figure}[h]\DM{#1}\caption{#2}\label{#3}\end{figure}}

339\newcommand{\FFIG}[3]{\begin{figure}\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

340\newcommand{\FFIGB}[3]{\begin{figure}[b]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

341\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}

342\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}

343\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

344

345\ifthenelse{\boolean{useverb}}{%

346 \newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}

347}{}

348

349\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}

350\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}

351

352\newcommand{\RESFIG}[3]{

353\TFIG{|l|c|c|c|c|c|c|c|c|}{

354\hline

355 & \multicolumn{4}{c|}{\Naive{} compilation} &

356 \multicolumn{4}{|c|}{Optimised compilation} \\

357\cline{2-9}

358\raisebox{1.5ex}[0pt]{Program} & Instrs & Thunks & Cells &

359Accesses & Instructions & Thunks & Cells & Accesses \\

360%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\

361\hline

362#1

363\hline

364}{#2}{#3}}

365

366\newcommand{\NEWRESFIG}[3]{

367\TFIG{|l|l|c|c|c|c|}{

368\hline

369% & \multicolumn{4}{c|}{\Naive{} compilation} &

370% \multicolumn{4}{|c|}{Optimised compilation} \\

371%\cline{2-9}

372Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

373%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\

374\hline

375#1

376}{#2}{#3}}

377

378\newcommand{\NEWRESFIGTC}[3]{

379\TFIGTC{|l|l|c|c|c|c|}{

380\hline

381% & \multicolumn{4}{c|}{\Naive{} compilation} &

382% \multicolumn{4}{|c|}{Optimised compilation} \\

383%\cline{2-9}

384Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

385%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\

386\hline

387#1

388}{#2}{#3}}

389

390\newcommand{\RESLINE}[9]{

391& \Naive{} & #2 & #3 & #5 & #4 \\

392#1

393& Optimised & #6 & #7 & #9 & #8 \\

394}

395\newcommand{\RESCHANGE}[4]{

396& Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\

397\hline

398}

399\newcommand{\RESCHANGEa}[5]{

400#5 & Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\

401\hline

402}

403

404%%%%%%%%%%%% PUNCTUATION

405

406\newcommand{\pad}[2]{#1#2#1}

407

408\newcommand{\hab}{\pad{\,}{:}}

409\newcommand{\Hab}{\pad{\;}{:}}

410\newcommand{\HHab}{\pad{\;}{::}}

411

412%%%%%%%%%%%% TYPE

413

414\newcommand{\Type}{\mbox{\texttt{\#}}} %\star}

415

416

417%%%%%%%%%%%%% ARROWS

418

419\newcommand{\To}{\pad{\:}{\rightarrow}}

420\newcommand{\Gets}{\leftarrow}

421%\newcommand{\car}{\vartriangleright}

422

423%%%%%%%%%%%%% QUANTIFIERS

424

425\newcommand{\lam}[2]{\lambda#1\pad{\!}{:}#2}

426\newcommand{\fbind}[3]{(#1\Hab#2)\to#3}

427\newcommand{\all}[2]{\forall#1\pad{\!}{:}#2}

428\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}

429\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}

430\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}

431\newcommand{\remall}[2]{\forall\{#1\pad{\!}{:}#2\}}

432\newcommand{\allpi}[2]{\Pi#1\pad{\!}{:}#2}

433\newcommand{\ali}[2]{\forall#1|#2}

434\newcommand{\exi}[2]{\exists#1\pad{\!}{:}#2}

435\newcommand{\wit}[2]{\ang{#1,#2}}

436\newcommand{\X}{\times}

437\newcommand{\sig}[2]{\Sigma#1\pad{\!}{:}#2}

438

439\newcommand{\SC}{.\:}

440

441\newcommand{\letbind}[3]{\mathsf{let}\:#1{:}#2\:=\:#3\:\mathsf{in}}

442\newcommand{\ifthen}[3]{\mathsf{if}\:#1\:\mathsf{then}\:#2\:\mathsf{else}\:#3}

443

444%%%%%%%%%%%%% EQUALITIES

445

446\newcommand{\cq}{\pad{\:}{\mapsto}}

447\newcommand{\xq}{\pad{}{\doteq}}

448\newcommand{\pq}{\pad{\:}{=}}

449\newcommand{\dq}{\pad{\:}{:=}}

450\newcommand{\iq}{\pad{\:}{\leadsto}}

451\newcommand{\mq}{\Longrightarrow}

452\newcommand{\retq}{\Rightarrow}

453\newcommand{\hq}{\pad{\:}{=}}

454\newcommand{\defq}{\mapsto}

455

456\newcommand{\refl}{\TC{refl}}

461%%%%%%%%%%%%% CATSTUFF

462

463\newlength{\Lwibrs}

464\newlength{\Lwobrs}

465\newsavebox{\Bwibrs}

466\newsavebox{\Bwobrs}

467\newcommand{\Db}[5]{%

468 \savebox{\Bwobrs}[\width][b]{$#5$}%

469 \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right#3$}%

470 \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%

471 \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%

472 \addtolength{\Lwibrs}{-\Lwobrs}%

473 \left#1\pad{\hspace*{-0.25\Lwibrs}}{\usebox{\Bwibrs}}\right#4}

474\newcommand{\LDb}[3]{%

475 \savebox{\Bwobrs}[\width][b]{$#3$}%

476 \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right.$}%

477 \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%

478 \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%

479 \addtolength{\Lwibrs}{-\Lwobrs}%

480 \left#1\hspace*{-0.4\Lwibrs}\usebox{\Bwibrs}\right.}

481\newcommand{\RDb}[3]{%

482 \savebox{\Bwobrs}[\width][b]{$#3$}%

483 \savebox{\Bwibrs}[\width][b]{$\left.\usebox{\Bwobrs}\right#1$}%

484 \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%

485 \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%

486 \addtolength{\Lwibrs}{-\Lwobrs}%

487 \left.\usebox{\Bwibrs}\hspace*{-0.4\Lwibrs}\right#2}

488\newcommand{\Sc}{\Db{[}{[}{]}{]}}

489\newcommand{\Mo}{\Db{|}{>}{<}{|}}

490\newcommand{\MoL}{\LDb{|}{>}}

491\newcommand{\MoR}{\RDb{<}{|}}

492

493\newcommand{\car}{\mbox{$-\!\triangleright$}}

494\newcommand{\io}[1]{\iota_{#1}}

495\newcommand{\cc}{\diamond}

496

497

498%%%%%%%%%%%%% FNS

499

500\newcommand{\Wk}{\Uparrow}

501

502%%%%%%%%%%%%% Transformation

503

504\newcommand{\Transform}[3]{\textsc{Trans}\:_{\Name{#1}}

505 \interp{#2}\:\mq\:#3}

506%\:[\:#2\:\Longrightarrow\:#3\:]}

507\newcommand{\Morphism}[2]{\textsc{Morphism}\:#1\:\Longrightarrow\:#2}

508\newcommand{\MI}[1]{\begin{array}{ll} #1 \end{array}\\}

509\newcommand{\MorphItem}[2]{& #1 \:\Longrightarrow\: #2}

510

511%%%%%%%%%%%%% Stuff

512

513% Motive and methods

514

515\newcommand{\motive}{\vP}

516\newcommand{\meth}[1]{\vm_{#1}}

517

518% Tuples

519\newcommand{\tuple}[1]{\langle#1\rangle}

520\newcommand{\Tuple}[1]{\mathsf{Tuple}}

521\newcommand{\proj}{\mathsf{proj}}

522\newcommand{\app}{\mathrm{+\!+}}

523

524% Commenting out

525\newcommand{\ig}[1]{[#1]}

526\newcommand{\rem}[1]{\{\!#1\!\}}

527\newcommand{\igc}[1]{[#1]}

528\newcommand{\remc}[1]{\{\!#1\!\}}

529

530

531\newcommand{\ind}{\hspace*{0.1cm}}

532

533% Content free type

534\newcommand{\CF}{\TC{CF}}

535\newcommand{\cf}{\DC{cf}}

536

537% Error token

538\newcommand{\error}{\DC{error}}

539\newcommand{\fail}{\perp}

540

541% Constructor stripping

542\newcommand{\conarg}[2]{#1!#2}

543

544\newcommand{\Vect}{\TC{Vect}}

545\newcommand{\VectM}{\TC{Vect^-}}

546\newcommand{\Vnil}{\DC{\epsilon}}

547\newcommand{\Vcons}{\DC{::}}

548

549\newcommand{\Vsnoc}{\DC{::}}

550

551\newcommand{\VnilM}{\DC{\epsilon^-}}

552\newcommand{\VconsM}{\DC{::^-}}

553

554\newcommand{\Vnilcase}{\VV{vNilCase}}

555\newcommand{\Vconscase}{\VV{vConsCase}}

556

557\newcommand{\DSigma}{\TC{Sigma}}

558\newcommand{\Exists}{\DC{Exists}}

559

560\newcommand{\ListPair}[2]{\sig{#1}{\List\:\vA}.#2 = \FN{length}\:#1}

561\newcommand{\lpNilDef}{\lpNil{\FN{refl}\:\Z}}

562\newcommand{\lpNil}[1]{(\nil\:\vA,#1)}

563\newcommand{\lpConsDef}[3]{\lpCons{#1}{(\FN{fst\:#2})}{\FN{resp}\:(\FN{snd}\:#2)}}

564\newcommand{\lpCons}[3]{(\cons\:#1\:#2,#3)}

565\newcommand{\lp}[2]{(#1, #2)}

566

567\newcommand{\VnilTop}{\DC{vNil}^\ast}

568\newcommand{\VconsTop}{\DC{vCons}^\ast}

569

570\newcommand{\VnilBot}{\DC{\epsilon}^-}

571\newcommand{\VconsBot}{\DC{::}^-}

572

573\newcommand{\VectTop}{\TC{Vect}^\ast}

574\newcommand{\VectBot}{\TC{Vect}^-}

575

576\newcommand{\VectDrop}{\FN{vectDropIdx}}

577\newcommand{\VectRebuild}{\FN{vectRebuild}}

578

579\newcommand{\Prop}{\TC{Prop}}

580\newcommand{\Set}{\TC{Set}}

581\newcommand{\CoqType}{\TC{Type}}

582

583\newcommand{\List}{\TC{List}}

584\newcommand{\nil}{\DC{nil}}

585\newcommand{\cons}{\DC{cons}}

586

587\newcommand{\Zip}{\TC{Tsil}}

588\newcommand{\zip}{\FN{tsil}}

589\newcommand{\zipcons}{\FN{tsilcons}}

590\newcommand{\snoc}{\DC{Snoc}}

591\newcommand{\lin}{\DC{Empty}}

592

593\newcommand{\BigInt}{\TC{BigInt}}

594\newcommand{\False}{\TC{False}}

595\newcommand{\Unit}{\TC{Unit}}

596\newcommand{\UnitI}{\DC{unit}}

597

598\newcommand{\genType}{\TC{X}}

599\newcommand{\genIndicesDec}{\tb\Hab\tB}

600\newcommand{\genIndices}{\tb}

601\newcommand{\genConArgsDec}[1]{\vec{\VV{a_#1}}\Hab\vec{\VV{A_#1}}}

602\newcommand{\genConArgs}[1]{\vec{\VV{a_#1}}}

603\newcommand{\genConIndicesDec}[1]{\vec{\VV{b_#1}}\Hab\vec{\VV{B_#1}}}

604\newcommand{\genConIndices}[1]{\vec{\VV{b_#1}}}

605\newcommand{\genCon}[1]{\DC{x}_#1}

606

607\newcommand{\genTypeTop}{\TC{X^\ast}}

608\newcommand{\genTypeBot}{\TC{X^-}}

609

610\newcommand{\genTypeDrop}{\FN{XDropIdx}}

611\newcommand{\genTypeRebuild}{\FN{XRebuild}}

612

613\newcommand{\HTerm}{\texttt{Term}}

614\newcommand{\Term}{\TC{Term}}

615\newcommand{\Var}{\DC{var}}

616\newcommand{\Lam}{\DC{lam}}

617\newcommand{\App}{\DC{app}}

618\newcommand{\TermM}{\TC{Term^-}}

619\newcommand{\VarM}{\DC{var^-}}

620\newcommand{\LamM}{\DC{lam^-}}

621\newcommand{\AppM}{\DC{app^-}}

622\newcommand{\Env}{\TC{Env}}

623\newcommand{\SType}{\TC{STy}}

624\newcommand{\farrow}{\Rightarrow}

625\newcommand{\lookup}{\FN{lookup}}

626

627% \newcommand{\source}{\Lang{TT}}

628\newcommand{\source}{\textbf{DT-Res}}

629\newcommand{\target}{\Lang{ExTT}}

630\newcommand{\runtime}{\Lang{RunTT}}

631

632\newcommand{\lt}{\TC{<}}

633\newcommand{\ltO}{\DC{ltO}}

634\newcommand{\ltS}{\DC{ltS}}

635

636\newcommand{\interp}[1]{\llbracket #1 \rrbracket}

637\newcommand{\inferrable}[2]{\FN{inferrable}(#1,#2)}

638\newcommand{\mkPat}{\FN{mkPat}}

639

640\newcommand{\FinM}{\TC{Fin^-}}

641\newcommand{\fzM}{\DC{f0^-}}

642\newcommand{\fsM}{\DC{fs^-}}

643

644\newcommand{\concat}{\mathrm{++}}

645

646%\newcommand{\bottom}{\perp}

647

648% Reductions

649

650\newcommand{\reduces}{\mapsto}

651\newcommand{\translation}{\Rightarrow}

652%\newcommand{\reducesn}[1]{\reduces\hspace*{-0.15cm}_{#1}}

653%\newcommand{\reducesto}{\reduces\hspace*{-0.15cm}^{*}}

654\newcommand{\reducesn}[1]{\reduces_{#1}}

655\newcommand{\reducesto}{\reduces^{*}}

656

657% Equality

658

659\newcommand{\Refl}{\DC{refl}}

660\newcommand{\leZ}{\DC{O_{\le}}}

661\newcommand{\leS}{\DC{S_{\le}}}

662

663% Random elimination things

664

665\newcommand{\lte}{\TC{\leq}}

666\newcommand{\lten}{\DC{leN}}

667\newcommand{\lteO}{\DC{leO}}

668\newcommand{\lteS}{\DC{leS}}

669

670\newcommand{\ltelim}{\Elim{\lt}}

671\newcommand{\leelim}{\Elim{\lte}}

672

673\newcommand{\dD}{\TC{D}}

674\newcommand{\delim}{\Elim{\TC{D}}}

675\newcommand{\drec}{\Rec{\TC{D}}}

676\newcommand{\dcase}{\Cases{\TC{D}}}

677\newcommand{\dview}{\View{\TC{D}}}

678\newcommand{\dmemo}{\Memo{\TC{D}}}

679\newcommand{\natrec}{\Rec{\Nat}}

680\newcommand{\natmemo}{\Memo{\Nat}}

681\newcommand{\natmemogen}{\Nat\textbf{-MemoGen}}

682\newcommand{\natelim}{\Elim{\Nat}}

683\newcommand{\boolcase}{\Cases{\Bool}}

684\newcommand{\vectrec}{\Rec{\Vect}}

685\newcommand{\vectelim}{\Elim{\Vect}}

686\newcommand{\listrec}{\Rec{\List}}

687\newcommand{\listelim}{\Elim{\List}}

688\newcommand{\finrec}{\Rec{\Fin}}

689\newcommand{\finelim}{\Elim{\Fin}}

690\newcommand{\natcase}{\Cases{\Nat}}

691\newcommand{\vectcase}{\Cases{\Vect}}

692\newcommand{\natdoublerec}{\Nat\textbf{-double-elim}}

693\newcommand{\eqelim}{=\textbf{-elim}}

694\newcommand{\falsecase}{\Cases{\False}}

695

696% Code

697\ifthenelse{\boolean{useverb}}{%

698 \newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}

699}{}

700% Quicksort

701

702\newcommand{\QSView}{\TC{QuickSort}}

703\newcommand{\qsempty}{\DC{empty}}

704\newcommand{\partition}{\DC{partition}}

705\newcommand{\qsview}{\FN{mkQuickSort}}

706

707% More gubbins

708

709\newcommand{\converts}{\simeq}

710\newcommand{\cumul}{\preceq}

711\newcommand{\whnf}{\Downarrow}

712\newcommand{\elem}{\in}

713\newcommand{\proves}{\vdash}

714\newcommand{\biimplies}{\Longleftrightarrow}

715

716\newcommand{\lc}{\lambda_{\mathsf{AC}}}

717\newcommand{\zed}{\mathbb{Z}}

718

719% Haskell keywords

720

721\newcommand{\hdata}{\mathtt{data}}

722\newcommand{\newtype}{\mathtt{newtype}}

723%\newcommand{\htype}{\mathtt{type}}

724

725\newcommand{\HTC}[1]{\mathtt{#1}}

726\newcommand{\HDC}[1]{\mathtt{#1}}

727

728% Nobby

729

730\newcommand{\Value}{\HTC{Value}}

731\newcommand{\VGamma}{\HTC{Env}}

732\newcommand{\Ctxt}{\HTC{Ctxt}}

733\newcommand{\Defs}{\HTC{Defs}}

734\newcommand{\ECtxt}{\HTC{ECtxt}}

735\newcommand{\TCtxt}{\HTC{TCtxt}}

736\newcommand{\VG}{\HDC{Env}}

737\newcommand{\Model}{\HTC{Model}}

738\newcommand{\Const}{\HTC{Const}}

739\newcommand{\Normal}{\HTC{Normal}}

740\newcommand{\Scope}{\HTC{Scope}}

741\newcommand{\Kripke}{\HTC{Kripke}}

742\newcommand{\Weakening}{\HTC{Weakening}}

743\newcommand{\Ready}{\HTC{Ready}}

744\newcommand{\Blocked}{\HTC{Blocked}}

745\newcommand{\Spine}{\HTC{Spine}}

746

747\newcommand{\BV}{\HDC{BV}}

748\newcommand{\BCon}{\HDC{BCon}}

749\newcommand{\BTyCon}{\HDC{BTyCon}}

750\newcommand{\RCon}{\HDC{RCon}}

751\newcommand{\RTyCon}{\HDC{RTyCon}}

752\newcommand{\BElim}{\HDC{BElim}}

753\newcommand{\DV}{\HDC{V}}

754\newcommand{\DP}{\HDC{P}}

755

756\newcommand{\MR}{\HDC{R}}

757\newcommand{\MB}{\HDC{B}}

758\newcommand{\DSc}{\HDC{Sc}}

759\newcommand{\DKr}{\HDC{Kr}}

760\newcommand{\DWk}{\HDC{Wk}}

761\newcommand{\DSnoc}{\HDC{;}}

762\newcommand{\DType}{\HDC{Type}}

763\newcommand{\DName}{\HDC{Name}}

764\newcommand{\DInt}{\HDC{Int}}

765\newcommand{\DString}{\HDC{String}}

766\newcommand{\DElim}{\HDC{Elim}}

767\newcommand{\Empty}{\HDC{\emptyset}}

768

769\newcommand{\ConCode}{\HTC{ConCode}}

770\newcommand{\ElimRule}{\HTC{ElimRule}}

771

772\newcommand{\DConst}{\HDC{Const}}

773\newcommand{\DCon}{\HDC{Con}}

774\newcommand{\DTyCon}{\HDC{TyCon}}

775\newcommand{\RConst}{\HDC{RConst}}

776\newcommand{\RLam}{\HDC{RLam}}

777\newcommand{\RPi}{\HDC{RPi}}

778\newcommand{\DLam}{\HDC{Lam}}

779\newcommand{\DLet}{\HDC{Let}}

780\newcommand{\DPi}{\HDC{Pi}}

781\newcommand{\DApp}{\HDC{App}}

782

783\newcommand{\TMaybe}{\HTC{Maybe}}

784\newcommand{\DNothing}{\HDC{Nothing}}

785\newcommand{\DJust}{\HDC{Just}}

786

787

788% G-machine and heap

789

790\newcommand{\PUSH}{\mathsf{PUSH}}

791\newcommand{\PUSHNAME}{\mathsf{PUSHNAME}}

792\newcommand{\POP}{\mathsf{DISCARD}}

793\newcommand{\PUSHFUN}{\mathsf{PUSHFUN}}

794\newcommand{\APPLY}{\mathsf{MKAP}}

795\newcommand{\EVAL}{\mathsf{EVAL}}

796\newcommand{\GCON}{\mathsf{MKCON}}

797\newcommand{\GTUP}{\mathsf{MKTUP}}

798\newcommand{\GTYPE}{\mathsf{MKTYPE}}

799\newcommand{\UPDATE}{\mathsf{UPDATE}}

800\newcommand{\RET}{\mathsf{RET}}

801\newcommand{\UNWIND}{\mathsf{UNWIND}}

802\newcommand{\CASEJUMP}{\mathsf{CASEJUMP}}

803\newcommand{\LABEL}{\mathsf{LABEL}}

804\newcommand{\MOVE}{\mathsf{MOVE}}

805\newcommand{\JUMP}{\mathsf{JUMP}}

806\newcommand{\SPLIT}{\mathsf{SPLIT}}

807\newcommand{\SQUEEZE}{\mathsf{SQUEEZE}}

808\newcommand{\JFUN}{\mathsf{JFUN}}

809\newcommand{\PROJ}{\mathsf{PROJ}}

810\newcommand{\ERROR}{\mathsf{ERROR}}

811\newcommand{\SLIDE}{\mathsf{SLIDE}}

812\newcommand{\ALLOC}{\mathsf{ALLOC}}

813

814\newcommand{\PUSHBIG}{\mathsf{PUSHBIG}}

815\newcommand{\PUSHBASIC}{\mathsf{PUSHBASIC}}

816\newcommand{\PUSHINT}{\mathsf{PUSHINT}}

817\newcommand{\PUSHBOOL}{\mathsf{PUSHBOOL}}

818\newcommand{\GET}{\mathsf{GET}}

819\newcommand{\MKINT}{\mathsf{MKINT}}

820\newcommand{\MKBOOL}{\mathsf{MKBOOL}}

821\newcommand{\ADD}{\mathsf{ADD}}

822\newcommand{\SUB}{\mathsf{SUB}}

823\newcommand{\MULT}{\mathsf{MULT}}

824\newcommand{\LT}{\mathsf{LT}}

825\newcommand{\EQ}{\mathsf{EQ}}

826\newcommand{\GT}{\mathsf{GT}}

827\newcommand{\JTRUE}{\mathsf{JTRUE}}

828

829\newcommand{\APP}{\mathsf{APP}}

830\newcommand{\FUN}{\mathsf{FUN}}

831\newcommand{\CON}{\mathsf{CON}}

832\newcommand{\TYCON}{\mathsf{TYCON}}

833\newcommand{\TUP}{\mathsf{TUP}}

834\newcommand{\TYPE}{\mathsf{TYPE}}

835\newcommand{\INT}{\mathsf{INT}}

836\newcommand{\BIGINT}{\mathsf{BIGINT}}

837\newcommand{\BOOL}{\mathsf{BOOL}}

838\newcommand{\HOLE}{\mathsf{HOLE}}

839

840% G machine translation scheme

841

842\newcommand{\sinterp}[1]{\mathcal{S}\interp{#1}}

843\newcommand{\sinterpm}[1]{\mathcal{S}\AR{\interp{#1}}}

844\newcommand{\einterp}[3]{\mathcal{E}\interp{#1}\:#2\:#3}

845\newcommand{\cinterp}[3]{\mathcal{C}\interp{#1}\:#2\:#3}

846\newcommand{\binterp}[3]{\mathcal{B}\interp{#1}\:#2\:#3}

847\newcommand{\rinterp}[3]{\mathcal{R}\interp{#1}\:#2\:#3}

848\newcommand{\iinterp}[3]{\mathcal{I}\interp{#1}\:#2\:#3}

849\newcommand{\len}[1]{\MO{length}(#1)}

850

851\newcommand{\casecomp}[2]{\mathcal{I}(#1,\left\{\ARc{#2}\right\})}

852\newcommand{\casecompA}[3]{\mathcal{I}(#1,\left\{\ARc{#2}\right\}[#3])}

853\newcommand{\ischeme}{\mathcal{I}}

854

855% tail call markup

856

857\newcommand{\tailcall}{\mathsf{tail}}

858

859% Trees

860

861\newcommand{\Tree}{\TC{Tree}}

862\newcommand{\Leaf}{\DC{Leaf}}

863\newcommand{\Node}{\DC{Node}}

864\newcommand{\treecase}{\Cases{\Tree}}

865

866% Languages

867

868\newcommand{\Coq}{\textsc{Coq}}

869\newcommand{\Lego}{\textsc{Lego}}

870\newcommand{\Oleg}{\textsc{Oleg}}

871\newcommand{\Alf}{\textsc{Alf}}

872\newcommand{\Epigram}{\textsc{Epigram}}

873\newcommand{\SystemF}{System $\mathcal{F}$}

874\newcommand{\Iswim}{\textsc{Iswim}}

875\newcommand{\Cynthia}{\textit{C$^Y$\hspace*{-0.1cm}NTHIA}}

876

877% Accessibility

878

879\newcommand{\Acc}{\TC{Acc}}

880\newcommand{\acc}{\DC{acc}}

881\newcommand{\qsAcc}{\TC{qsAcc}}

882\newcommand{\qsNil}{\DC{qsNil}}

883\newcommand{\qsCons}{\DC{qsCons}}

884\newcommand{\allQsAcc}{\FN{allQsAcc}}

885

886% Lazy shortcuts

887

888\newcommand{\naive}{na\"{\i}ve}

889\newcommand{\Naive}{Na\"{\i}ve}

890

891% Conor's bits

892

893\newcommand{\remem}[1]{\left|#1\right|}

894\newcommand{\idsb}{\MO{id}}

895\newcommand{\ang}[1]{\langle#1\rangle}

896

897\newcommand{\vePm}[1]{\vP #1 \vm_{\Vnil} #1 \vm_{\Vcons}}%

898\newcommand{\vcrhs}{\vm_{\Vcons}\:\vk\:\va\:\vv\:%

899 (\vectelim\:\vA\:\vk\:\vv\:\vePm{\:})}%

900

901\newcommand{\igV}[2]{#1^{\ig{#2}}}

902\newcommand{\remV}[2]{#1^{\rem{#2}}}

903

904% More gubbins

905

906\newcommand{\Between}{\TC{between}}

907\newcommand{\bZ}{\DC{bO}}

908\newcommand{\bZZS}{\DC{bOOs}}

909\newcommand{\bZSS}{\DC{b0ss}}

910\newcommand{\bSSS}{\DC{bsss}}

911\newcommand{\betelim}{\Elim{\Between}}

912\newcommand{\betrhs}[1]{\motive#1\meth{\bZ}#1\meth{\bZZS}#1\meth{\bZSS}#1\meth{\bSSS}}

913

914

915\newcommand{\valenv}{\TC{ValEnv}}

916\newcommand{\vempty}{\DC{empty}}

917\newcommand{\vextend}{\DC{extend}}

918

919\newcommand{\EpiVal}{\TC{Epigram}}

920\newcommand{\unsafeCoerce}{\HF{unsafeCoerce\mbox{\texttt{\#}}}}

921

922\newcommand{\qq}{\mbox{\texttt{"}}}

923\newcommand{\impossible}{\RW{Impossible}}

924

925\newcommand{\Real}{\mathbb{R}}

926

927\newcommand{\DoubleRec}{\TC{DoubleElim}}

928\newcommand{\DoubleOn}{\DC{Double_{\Z\vn}}}

929\newcommand{\DoubleSO}{\DC{Double_{\suc\Z}}}

930\newcommand{\DoubleSS}{\DC{Double_{\suc\suc}}}

931

932\newcommand{\doublerec}{\textbf{double-elim}}

933

934\newcommand{\set}{\TC{DList}}

935\newcommand{\setuser}{\TC{DListTop}}

936\newcommand{\setempty}{\emptyset}

937\newcommand{\setinsert}{\DC{insert}}

938

939

940%%%% Type systems

941

942\newcommand{\stlc}{\lambda\hspace*{-0.15cm}\to}

943\newcommand{\plc}{\lambda2}

944\newcommand{\dlc}{\lambda{}P}

945

946\newcommand{\EC}{\mathcal{E}}

947

948%%%% reductions

949

950\newcommand{\betared}{\iq\hspace*{-0.15cm}_{\beta}}

951\newcommand{\deltared}{\iq\hspace*{-0.15cm}_{\delta}}

952\newcommand{\gammared}{\iq\hspace*{-0.15cm}_{\gamma}}

953\newcommand{\etared}{\iq\hspace*{-0.15cm}_{\eta}}

954\newcommand{\iotared}{\iq\hspace*{-0.15cm}_{\iota}}

955\newcommand{\rhored}{\iq\hspace*{-0.15cm}_{\rho}}

956

957%%%% ExTT rules

958

959\newcommand{\exconverts}{\stackrel{\mathsf{Ex}}{\converts}}

960\newcommand{\excumul}{\stackrel{\mathsf{Ex}}{\cumul}}

961\newcommand{\exequiv}{\stackrel{\mathsf{Ex}}{\equiv}}

962\newcommand{\exreduces}{\stackrel{\mathsf{Ex}}\reduces}

963\newcommand{\exreducesto}{\stackrel{\mathsf{Ex}}{\reducesto}}

964\newcommand{\exreducesn}[1]{\exreduces_{#1}}

965

966\newcommand{\ttequiv}{\stackrel{\mathsf{TT}}{\equiv}}

967\newcommand{\ttreduces}{\stackrel{\mathsf{TT}}\reduces}

968\newcommand{\ttreducesn}[1]{\ttreduces_{#1}}

969

970%%% Type synthesis

971

972\newcommand{\hastype}{\Longrightarrow}

973\newcommand{\whnfs}{\twoheadrightarrow}

974\newcommand{\conv}{\converts}

975

976\newcommand{\exhastype}{\stackrel{\mathsf{Ex}}{\hastype}}

977\newcommand{\exwhnfs}{\stackrel{\mathsf{Ex}}{\whnfs}}

978\newcommand{\exconv}{\stackrel{\mathsf{Ex}}{\conv}}

979\newcommand{\exproves}{\stackrel{\mathsf{Ex}}{\proves}}

980

981\newcommand{\tthastype}{\stackrel{\mathsf{TT}}{\hastype}}

982\newcommand{\ttwhnfs}{\stackrel{\mathsf{TT}}{\whnfs}}

983\newcommand{\ttconv}{\stackrel{\mathsf{TT}}{\conv}}

984\newcommand{\ttproves}{\stackrel{\mathsf{TT}}{\proves}}

985

986%%% Lightning

987

988\newcommand{\light}[1]{\lightning^{#1}}

989\newcommand{\LHab}[1]{\pad{\;}{:^{#1}}}

990\newcommand{\llam}[3]{\lambda#1\pad{\!}{:}^{#2}#3}

991\newcommand{\lall}[3]{\forall#1\pad{\!}{:}^{#2}#3}

992\newcommand{\lapp}[3]{#1(#2)^{#3}}

993\newcommand{\larg}[2]{(#1)^{#2}}

994

995\newcommand{\RName}[1]{\hspace*{0.1in}\mathsf{#1}}

996

997%%% LOcal macros

998

999\newcommand{\ResState}{\TC{ResourceState}}

1000\newcommand{\Locked}{\DC{Locked}}

1001\newcommand{\ResHandle}{\TC{ResourceHandle}}

1002\newcommand{\Res}{\DC{Resource}}

1003\newcommand{\CLang}{\TC{CLang}}

1004\newcommand{\CFLang}{\TC{CFLang}}

1005\newcommand{\CFType}{\TC{CFType}}

1006\newcommand{\CLType}{\TC{CType}}

1007\newcommand{\RHandle}{\DC{RHandle}}

1008\newcommand{\RType}{\DC{RType}}

1009\newcommand{\RUnit}{\DC{RUnit}}

1010\newcommand{\LOCK}{\DC{LOCK}}

1011\newcommand{\UNLOCK}{\DC{UNLOCK}}

1012\newcommand{\ACTION}{\DC{ACTION}}

1013\newcommand{\FORK}{\DC{FORK}}

1014

1015\newcommand{\FSLang}{\TC{FSLang}}

1016\newcommand{\OPEN}{\DC{OPEN}}

1017\newcommand{\CLOSE}{\DC{CLOSE}}

1018\newcommand{\READ}{\DC{READ}}

1019\newcommand{\WRITE}{\DC{WRITE}}

1020\newcommand{\PRINT}{\DC{PRINT}}

1021\newcommand{\BIND}{\DC{BIND}}

1022

1023\newcommand{\FSType}{\TC{FSType}}

1024\newcommand{\FHandle}{\DC{FHandle}}

1025\newcommand{\FString}{\DC{FString}}

1026\newcommand{\FUnit}{\DC{FUnit}}

1027\newcommand{\ElemIs}{\TC{ElemIs}}

1028\newcommand{\elemHd}{\TC{atHead}}

1029\newcommand{\elemTl}{\TC{inTail}}

1030

1031\newcommand{\emptyEnv}{\DC{empty}}

1032\newcommand{\extendEnv}{\DC{extend}}

1033

1034\newcommand{\usera}{\FN{Alice}}

1035\newcommand{\userb}{\FN{Bob}}

1036\newcommand{\userc}{\FN{Charlie}}

1037

1038\newcommand{\FAcc}{\TC{FAcc}}

1039\newcommand{\UserA}{\DC{UserAcc}}

1040\newcommand{\GroupA}{\DC{GroupAcc}}

1041\newcommand{\GlobalA}{\DC{GlobalAcc}}

1042

1043\newcommand{\Perm}{\TC{Perm}}

1044\newcommand{\Username}{\TC{Username}}

1045\newcommand{\GroupData}{\TC{GroupData}}

1046\newcommand{\File}{\TC{File}}

1047\newcommand{\FS}{\DC{file}}

1048\newcommand{\Filepath}{\TC{Filepath}}

1049

1050\newcommand{\Read}{\DC{Read}}

1051\newcommand{\Write}{\DC{Write}}

1052\newcommand{\Execute}{\DC{Execute}}

1053

1054\newcommand{\Purpose}{\TC{Mode}}

1055\newcommand{\Reading}{\DC{Reading}}

1056\newcommand{\Writing}{\DC{Writing}}

1057

1058\newcommand{\FileState}{\TC{FileState}}

1059\newcommand{\FileHandle}{\TC{FileHandle}}

1060\newcommand{\OpenH}{\DC{OpenH}}

1061\newcommand{\ClosedH}{\DC{ClosedH}}

1062\newcommand{\Handle}{\TC{Handle}}

1063\newcommand{\Open}{\DC{Open}}

1064\newcommand{\Closed}{\DC{Closed}}

1065

1066\newcommand{\UserIO}{\TC{UserIO}}

1067\newcommand{\uio}{\DC{uio}}

1068

1069\newcommand{\CFS}{\TC{C_{fs}}}

1070\newcommand{\RFS}{\FN{R_{fs}}}

1071

1072\newcommand{\String}{\TC{String}}

1073

1074% inline idris code

1075

1076\newcommand{\Tcon}[1]{\texttt{#1}}

1077\newcommand{\Dcon}[1]{\texttt{#1}}

1078\newcommand{\Fname}[1]{\texttt{#1}}

1079\newcommand{\Vv}[1]{\texttt{#1}}

1080\newcommand{\TyTy}{\texttt{\#}}

1081

1082\newcommand{\direct}[1]{\texttt{\%#1}}

1083

1084\newcommand{\Feature}[1]{\textbf{Remark:}}

1085

1086\endinput