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
|
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb,supertabular,geometry,fullpage}
\geometry{a4paper,twoside,landscape,left=10.5mm,right=10.5mm,top=20mm,bottom=30mm}
\usepackage{color}
\begin{document}
\input{doc_in}
\title{Sail Manual}
\author{Kathryn E Gray, Gabriel Kerneis, Peter Sewell}
\maketitle
\tableofcontents
\newpage
\section{Sail syntax}
\ottgrammartabular{
\ottl\ottinterrule
\ottannot\ottinterrule
\ottid\ottinterrule
\ottkid\ottinterrule
\ottbaseXXkind\ottinterrule
\ottkind\ottinterrule
\ottnexp\ottinterrule
\ottorder\ottinterrule
\ottbaseXXeffect\ottinterrule
\otteffect\ottinterrule
\otttyp\ottinterrule
\otttypXXarg\ottinterrule
\ottnXXconstraint\ottinterrule
\ottkindedXXid\ottinterrule
\ottquantXXitem\ottinterrule
\otttypquant\ottinterrule
\otttypschm\ottinterrule
\ottnameXXscmXXopt\ottinterrule
\otttypeXXdef\ottinterrule
\otttypeXXunion\ottinterrule
\ottindexXXrange\ottinterrule
\ottlit\ottinterrule
\ottsemiXXopt\ottinterrule
\ottpat\ottinterrule
\ottfpat\ottinterrule
\ottexp\ottinterrule
\ottlexp\ottinterrule
\ottfexp\ottinterrule
\ottfexps\ottinterrule
\ottoptXXdefault\ottinterrule
\ottpexp\ottinterrule
\otttannotXXopt\ottinterrule
\ottrecXXopt\ottinterrule
\otteffectXXopt\ottinterrule
\ottfuncl\ottinterrule
\ottfundef\ottinterrule
\ottletbind\ottinterrule
\ottvalXXspec\ottinterrule
\ottdefaultXXspec\ottinterrule
\ottscatteredXXdef\ottinterrule
\ottregXXid\ottinterrule
\ottaliasXXspec\ottinterrule
\ottdecXXspec\ottinterrule
\ottdef\ottinterrule
\ottdefs\ottinterrule}
\newpage
\section{Sail primitive types and functions}
\ottgrammartabular{
\ottbuiltXXinXXtypes\ottinterrule}
\ottgrammartabular{
\ottbuiltXXinXXtypeXXabbreviations\ottinterrule
\ottfunctions\ottinterrule
\ottfunctionsXXwithXXcoercions\ottinterrule}
\newpage
\section{Sail type system}
\subsection{Internal type syntax}
\ottgrammartabular{
\ottk\ottinterrule
\ottt\ottinterrule
\ottoptx\ottinterrule
\otttag\ottinterrule
\ottne\ottinterrule
\otttXXarg\ottinterrule
\otttXXargs\ottinterrule
\ottnec\ottinterrule
\ottSXXN\ottinterrule
\ottEXXd\ottinterrule
\ottkinf\ottinterrule
\otttid\ottinterrule
\ottEXXk\ottinterrule
\otttinf\ottinterrule
\ottEXXa\ottinterrule
\ottfieldXXtyps\ottinterrule
\ottEXXr\ottinterrule
\ottenumerateXXmap\ottinterrule
\ottEXXe\ottinterrule
\ottEXXt\ottinterrule
\ottts\ottinterrule
\ottE\ottinterrule
\ottI\ottinterrule
\ottformula\ottinterrule}
\subsection{ Type relations }
\ottdefnss
\section{Sail operational semantics \{TODO\}}
\end{document}
|
