reference.tex

\documentclass[12pt,a4paper]{book}
\usepackage[scaled]{berasans}
\usepackage[scaled]{berasans}
\usepackage[scaled]{beraserif}

\usepackage{todonotes}

\usepackage{hyperref}
\usepackage{amssymb}
\usepackage{amsmath}

\usepackage{supertabular}


\usepackage{xcolor}
\usepackage{lem}

\usepackage[cache=false]{minted}
\newminted{sml}{}
\newmintinline{sml}{}
\usemintedstyle{bw}

\newcommand{\gramsep}{|}

\title{CakeML Reference Manual}
\author{Scott Owens\\
University of Kent\\
\url{https://cakeml.org}
}
\usepackage[T1]{fontenc}

\begin{document}\sloppy
\maketitle
\frenchspacing

\frontmatter

\chapter{Preface}

This manual is intended to describe the CakeML language, compiler, and associated proof technologies. We hope that it will be useful for anyone who wants to understand  CakeML, either with an aim to collaborate with main CakeML team,\footnote{Project ideas are listed at \url{https://cakeml.org/projects.html}.}
or to work with CakeML independently.

We have attempted to make this reference manual self-contained. However, our aim is not to explain the basics of functional programming, programming language semantics, or interactive theorem proving, and so we expect of the reader at least some familiarity with a functional programming language, and with basic discrete mathematics: logic, inductively defined relations, etc.

\mainmatter
\tableofcontents


\part{The CakeML Language}
\label{part:lang}

\chapter{An informal description of CakeML}

CakeML is a functional language in the ML family. Its syntax and semantics
resembles Standard ML, and the concepts will also be largely familiar
to OCaml and Haskell programmers. This chapter describes the CakeML language.
Although it uses example programs to illustrate its various features, its focus
is on what the language is, and not on how to effectively use it. However,
these pragmatics should be clear to programmers with experience in other
functional languages.

CakeML's syntax has a two-level structure with declarations and expressions. A
program is a sequence of top-level declarations that define variables,
functions, types, and modules. Computations are performed by expressions that form the bodies of functions and initialise variables.

Expression are built up from constants, variables, function applications, and
special forms for conditionals, pattern matching, exception handling, anonymous
functions, and local definitions. Each expression has a type, and computes a
value of that type, unless it infinite loops or raises an exception.

CakeML supports the following types of values:
\begin{itemize}
  \item atomic values -- booleans, integers, words, strings, and characters (\S\ref{sect:val} and \S\ref{ch:stdlib});
  \item functions (\S\ref{sect:func});
  \item immutable containers -- lists, tuples, user-defined algebraic data types (also called variant types) (\S\ref{sect:compound}), and vectors (\S\ref{sect:vector}); and
  \item mutable containers -- references (\S\ref{sect:ref}) and arrays (\S\ref{sect:array}).
\end{itemize}

\section{Comments and white space}
All comments and white space act as delimiters, but are otherwise ignored. Comments are surrounded by \smlinline{(* *)}. They nest properly, so that the following idiom works.\begin{smlcode}
(*
  commented out code
  (* comment inside of commented out code *)
  commented out code
*)
\end{smlcode}
The first \smlinline{*)} does not end the entire comment, but only the
corresponding \smlinline{(*}.


\section{Atomic values}
\label{sect:val}

\paragraph{Booleans} The boolean constants are written as \smlinline{true} and
\smlinline{false}. The type of booleans is \smlinline{bool}. The conjunction and
disjunction logical operators are written as infix \smlinline{andalso} and
\smlinline{orelse}. They evaluate the left argument first, and only evaluate the
right one if necessary (short-circuit evaluation). The \smlinline{not} function
negates a boolean value.

\paragraph{Integers} Integers constants are written in decimal notation. The
\texttt{\textasciitilde} character acts as the minus sign for writing negative
numbers. So negative one is \smlinline{~1} instead of \texttt{-1}. The type of integers is
\smlinline{int}.

CakeML provides the following infix arithmetic operators on integers: \smlinline{+}, \smlinline{-}, \smlinline{*}, \smlinline{div}, \smlinline{mod}. Integers are represented internally as arbitrary precision numbers (\emph{bignums}) so they can never overflow, and there is no maximum or minimum representable integer. The \smlinline{div} and \smlinline{mod} operations will raise the \smlinline{Div} exception if given a divisor of 0. \smlinline{div} returns the least integer less than the real quotient, so \smlinline{~10 div 3} returns \smlinline{~4}, and not \smlinline{~3}. \smlinline{mod} is consistent with this, so that \smlinline{~10 mod 3} returns \smlinline{2}, not \smlinline{1}.

Integers are compared with the infix operators \smlinline{=}, \smlinline{<>}, \smlinline{<}, \smlinline{>}, \smlinline{<=}, \smlinline{>=}, each of which returns a \smlinline{bool}.

\paragraph{Words} CakeML supports both 64-bit and 8-bit words. All word
constants are 64-bit, but 8-bit words can be created using functions in the
standard library's Word8 module~(\S\ref{sect:word8}). Word constants in decimal
notation are prefixed with \smlinline{0w} (for example, \smlinline{0w256}).
Words constants in hexadecimal notation are prefixed with \smlinline{0wx} (for
example, \smlinline{0wx3fA}). 64-bit words have the type \smlinline{word}, whereas
the type of 8-bit words is \smlinline{Word8.word} from the standard library.
See \S\ref{sect:word64} and \S\ref{sect:word8} for the operations on words.

\paragraph{Strings} String constants are enclosed in double quotation marks (\texttt{"}). The type of strings is \smlinline{string}.

The escape character is \verb|\|, and it supports the following:
\begin{itemize}
\item
\verb|\n| : a newline character
\item
\verb|\"| : a double quotation (\texttt{"}) character
\item
\verb|\\| : a single backslash (\verb|\|) character, and
\item
\verb|\t| : a tab character.
\end{itemize}

The \smlinline{^} infix operator concatenates strings. See \S\ref{sect:string} for
other operations on strings.

\paragraph{Characters} A character constant is just a string constant of length
1, with a \texttt{\#} prefix, for example \smlinline{#"c"} for the character `c'.
This means that characters use the same escape sequences as strings. The type
of characters is \smlinline{char}. See \S\ref{sect:char} for the operations on characters.

\section{Variables and other names}
\label{sect:variables}

\paragraph{Variable syntax} There are two kinds of variable names: alphanumeric and symbolic. An alphanumeric variable must start
with a lower case letter and be a sequence of letters, digits and the \texttt{\_} and \texttt{'} characters. A symbolic variable is a sequence of the following characters: \verb)! % & $ # + - / : < = > ? @ \ ~ ^ | ` *).

Names of modules (\S\ref{sect:modules}) and constructors (from algebraic data types~\S\ref{sect:compound} and exceptions~\S\ref{sect:exceptions}) are alphanumeric and
start with an upper case letter. Additionally, the names \smlinline{true},
\smlinline{false}, \smlinline{ref}, and \smlinline{nil} are
constructors, rather than variables.

Names of types are alphanumeric and start
with a lower case letter.
%
Type variables must be alphanumeric and start with \texttt{'}.

No name can be any of the following reserved words:
\begin{verbatim}
and  andalso  case  datatype  else  end  exception
fn  handle  if  in  let  op  of  orelse  raise
ref  sig  struct  structure  then  type  val
:>  =>  :  |
\end{verbatim} \todo{Make this list and CakeML's lexer agree.}

\paragraph{Declaration of variables} A \smlinline{val} declaration introduces a new variable name with a given value.
We will follow tradition and refer to these as variables, although their values
cannot be changed once initialised.
\begin{smlcode}
val x = 1 + 2
val my_string = "Happy"
\end{smlcode}
Variable declarations may optionally be followed by a semi-colon (\smlinline{;}).

\section{Conditionals}

Conditionals are expressions that compute a value. They use \smlinline{if},
\smlinline{then}, and \smlinline{else}. For example,
\begin{smlcode}
if x < 0 then 0 - x else x
\end{smlcode}
This tests if \smlinline{x} is less than \smlinline{0}, and if so, evaluates to \smlinline{0-x}, and if not evaluates to \smlinline{x}.
The \smlinline{else} and associated sub-expression cannot by omitted. The test expression (following \smlinline{if}) must be of \smlinline{bool} type, and the result expressions must both have the same types.

\section{Functions}
\label{sect:func}

\paragraph{Declaration of functions}
A function is declared with \smlinline{fun}, followed by the
function's name, its parameters, \smlinline{=}, and finally its body expression, as follows:
\begin{smlcode}
fun abs x =
  if x < 0 then 0 - x else x
\end{smlcode}
A function returns whatever its body expression evaluates
to, in this example the absolute value of its argument. Functions are called by placing
their argument expression(s) immediately after the function's name:
\begin{smlcode}
val x = abs ~100
val y = abs (if x mod 2 = 0 then x - 2 else x - 5)
\end{smlcode}

Functions can be recursive, and can have multiple arguments/parameters which are all placed in
order after the function name without any punctuation, for both calls and declarations.
\begin{smlcode}
fun gcd a b =
  if b = 0 then
    a
  else
    gcd b (a - b * (a div b));
\end{smlcode}

Mutually recursive functions are separated by \smlinline{and} instead of \smlinline{fun}:
\begin{smlcode}
fun even x =
  if x = 0 then true
  else odd (x - 1)
and odd x =
  if x = 0 then false
  else even (x - 1)
\end{smlcode}

Function call expressions evaluate their argument in right-to-left order,
before calling the function.

Function declarations may optionally be followed by a semi-colon (\smlinline{;}).

\paragraph{Anonymous and partially applied functions}

Functions are first-class values. This means that a function can be returned
from another functions, or passed as an argument to another function, and that
a variable can have a function as its value. In fact, the function name in a
\smlinline{fun} declaration is just a normal variable that has a function value.

The \smlinline{->} type operator gives the type of a variable or expression
that has a function value. In the above examples, \smlinline{abs},
\smlinline{gcd}, \smlinline{even}, \smlinline{odd} have types \smlinline{int ->
int}, \smlinline{int -> int -> int}, \smlinline{int -> bool}, and
\smlinline{int -> bool} respectively.

An anonymous function can be created directly inside of an expression with \smlinline{fn} as follows:
\begin{smlcode}
val f =
  if should_inc then (fn a => fn b => a + b + 1)
  else (fn a => fn b => a + b)
val x = f 1 2
\end{smlcode}
Here \smlinline{f} is a function with type \smlinline{int -> int -> int}.

The type of a function with more than one argument has multiple
arrows \smlinline{->}, and in the above, we used \smlinline{fn} twice to build a
two argument anonymous function. In CakeML, functions are curried, meaning that
they all take exactly one argument, and multiple argument functions are
simulated by passing in the arguments one after the other. This means that we do not have to
apply a function to all of it's arguments at once.\footnote{The compiler optimises multiple argument functions so that the arguments are not actually passed in one at a time when the program is run.} Using the same \smlinline{f}:
\begin{smlcode}
val g = f 8
val x = g 1
val y = g 2
\end{smlcode}
Here \smlinline{g} is a one argument function with type {int -> int}, and thus
\smlinline{x} and \smlinline{y} are integers.

\paragraph{Lexical scope}
A function value can be created inside of another function and returned from
it. If the returned function refers to variables from the function that created
it, then it will continue to do so after it is returned. In the following \smlinline{x} is equal to \smlinline{5} both times that \smlinline{do_add} is called.
\begin{smlcode}
fun mk_add x =
  if should_inc then (fn y => x + y + 1)
  else (fn y => x + y)
val do_add = mk_add 5
val x = do_add 10
val y = do_add 11
\end{smlcode}

\section{Compound values and pattern matching}
\label{sect:compound}

\paragraph{Tuples} A tuple expression is surrounded by parentheses and its constituent expressions are separated by commas. For example, \smlinline{("1", 3+5, true)} is a three element tuple. The empty tuple \smlinline{()} is the (only) member of the type \smlinline{unit}. The type of a tuple is formed from the types of its members, separated by \texttt{*}, so our first tuple example has type \smlinline{string * int * bool}.

\paragraph{Lists} A list of values is surrounded by square brackets and separated by commas. Each element of the list must have the same type. For example, the expression \smlinline{[1, 2+3, 0, 4]} is a list of integers containing four elements. Its type is \smlinline{int list}. The empty list is written \smlinline{[]}, and has a polymorphic type \smlinline{'a list}, indicating that it can be used as an empty list of any type of contents. The cons operator (constructing a list with one more element) is written as \smlinline{::}, so the above list could also have been written as \smlinline{1::2+3::0::4::[]}.

The \smlinline{@} infix operator appends two lists. See \S\ref{sect:list} for more list-related functions.

\paragraph{Algebraic data types}

A new data type is declared with \smlinline{datatype}, giving the
type a name, and listing the constructors that form elements of the new type,
separated by \smlinline{|}. For example, the following introduces a new type \smlinline{colour} and three new values of type \smlinline{colour}: \smlinline{Red}, \smlinline{Green}, and \smlinline{Blue}.
The type name must begin with a lower case letter, and the constructors with upper case letters.
\begin{smlcode}
datatype colour = Red | Green | Blue
\end{smlcode}

The constructors can contain values of given types specified with
\smlinline{of}. Those values can be of the same type as the datatype
itself; that is, the types constructed by \smlinline{datatype} can be recursive.
We can model a binary search tree with a terminal leaf, and interior nodes that
contain left and right child trees, and integer keys and values.
\begin{smlcode}
datatype search_tree =
  Leaf
| Node of search_tree * int * int * search_tree
\end{smlcode}
We can create a \smlinline{search_tree} by applying the constructor to four
arguments of the given types using a tuple-like syntax. Here are some example
\smlinline{search_tree}s.
\begin{smlcode}
val empty_tree = Leaf
val two_node = Node (Leaf, 1, 0, Node (Leaf, 2, 100, Leaf))
\end{smlcode}
Although the syntax looks like the constructor applied to a tuple expression,
it is not as flexible as that, and we cannot apply \smlinline{Node} to an
actual tuple value, as in the following \textbf{non-example}.
\begin{smlcode}
val tup = (Leaf, 2, 100, Leaf)
val error = Node tup
\end{smlcode}

We can generalise the tree datatype to contain values of any type by
introducing a type parameter, which is written \emph{before} the type name:
\begin{smlcode}
datatype 'a search_tree =
  Leaf
| Node of 'a search_tree * int * 'a * 'a search_tree
\end{smlcode}
The \smlinline{Leaf} example now has type \smlinline{'a search_tree}, and our
\smlinline{Node} example has type \smlinline{int search_tree}. We can create a
\smlinline{char search_tree} or \smlinline{string list search_tree} as follows.\footnote{Type application is left associative, so \smlinline{string list search_tree} is the same as \smlinline{(string list) search_tree}.}
\begin{smlcode}
val char_tree =
  Node (Leaf, 1, #"0", Node (Leaf, 2, #"A", Leaf))
val sl_tree =
  Node (Leaf, 1, ["44", "name"], Node (Leaf, 2, [""], Leaf))
\end{smlcode}


Types with multiple parameters put them in parentheses and separate them with commas:
\begin{smlcode}
datatype ('k, 'a) search_tree =
  Leaf
| Node of ('k, 'a) search_tree * 'k * 'a * ('k, 'a) search_tree
\end{smlcode}

Similar to functions, data types can be mutually recursive with subsequent types being separated by
\smlinline{and}.
\begin{smlcode}
datatype ('k, 'a) nary_tree =
  Node of 'k * 'a * ('k, 'a) tree_list
and ('k, 'a) tree_list =
  Empty
| Cons of ('k, 'a) nary_tree * ('k, 'a) tree_list
\end{smlcode}

Algebraic data types can also be composed. For example, the above
\smlinline{nary_tree} type could be defined using the built-in list type.
\begin{smlcode}
datatype ('k, 'a) nary_tree =
  Node of 'k * 'a * ('k, 'a) nary_tree list
\end{smlcode}

No \smlinline{datatype} declaration may use the special constructor names
\smlinline{true}, \smlinline{false}, \smlinline{ref}, \smlinline{::}, and
\smlinline{nil}. \todo{Add this check to the type system.}


\paragraph{Pattern matching}
Compound values are de-structured with pattern matching \smlinline{case}
expressions. A pattern has the same shape as the value that it matches. Patterns are separated by \smlinline{|}, and each pattern is accompanied by a \smlinline{=>} and expression. The \smlinline{case} expression finds the first pattern that matches the value given to it, and evaluates that pattern's expression. The patterns must all match values of the same type, and the expression must all have the same type as each other.
\begin{smlcode}
fun is_red c =
  case c of
    Red => true
  | Green => false
  | Blue => false
\end{smlcode}

Variables inside of patterns match anything, and are bound to the corresponding piece of the value being matched. Underscore \smlinline{_} matches anything, but binds nothing. Patterns can also be nested.
\begin{smlcode}
fun is_red c =
  case c of
    Red => true
  | _ => false

fun first p =
  case p of
    (x, _) => x

fun first_red p =
  case p of
    (Red, _) => true
  | _ => false
\end{smlcode}

Numbers, booleans, lists, tuples, and constructors from algebraic data types and exceptions can all appear in
patterns. As a final example, the following function searches for a given
element in an \smlinline{nary_tree}, using patterns for data type constructors and lists.
\begin{smlcode}
fun nary_mem k tree =
  case tree of
    Node (k1, v, []) => k1 = k
  | Node (k1, v, tree1::trees) =>
    nary_mem k tree1 orelse nary_mem k (Node (k1, v, trees))
\end{smlcode}

\paragraph{Other places patterns can appear} Besides \smlinline{case}
expressions and \smlinline{handle} expressions (\S\ref{sect:exceptions}),
patterns can also be used in variable declarations (\smlinline{val}), and as
an anonymous function expression's (\smlinline{fn}) parameter.
\begin{smlcode}
val (x, y, z) = if something then (1, 2, 3) else (4, 5, 6)
val _ = print "message"
val f = fn (Node (k, v, ts) => v)
\end{smlcode}

\paragraph{Unmatched patterns}
If no pattern in a \smlinline{case} expression matches the value, then a \smlinline{Bind} exception is raised. Similarly, if the pattern given in a \smlinline{val} declaration or \smlinline{fn} expression does not match the initialisation value, or function argument, a \smlinline{Bind} exception is raised.

\section{Type annotations}

Types are inferred in CakeML, so programs do not need to specify the types of
variable declarations or functions. However, we can optionally annotate any
pattern or expression with its type using a colon \smlinline{:}. That type is then enforced by the compiler.
\begin{smlcode}
val (x : int) = 1
fun f (x : bool) = if x then 0 else 1
\end{smlcode}

\section{References}
\label{sect:ref}

A reference is a mutable structure that contains exactly one value. The type of a reference containing a value of type $\tau$ is written $\tau$ \smlinline{ref}.
References have the following operations, where \smlinline{:=} is written infix.
\begin{itemize}
\item
\smlinline{ref : 'a -> 'a ref}\\ Create a new reference with an initial value.
\item
\smlinline{! : 'a ref -> 'a}\\ Get the value from a reference.
\item
\smlinline{:= : 'a ref -> 'a -> unit}\\ Replace the value in the reference with a new one.
\end{itemize}

For example, the following code initialises a reference to \smlinline{0}, then
increments it to contain \smlinline{1}. Finally, the value of \smlinline{x} is
also \smlinline{1}.
\begin{smlcode}
val r = ref 0
val _ = r := !r + 1
val x = !r
\end{smlcode}

\section{Infix operators}
\label{sect:infix}

CakeML supports the set of infix operators listed in Figure~\ref{precedences}.
Except for \smlinline{=}, \smlinline{<>}, \smlinline{o}, and
\smlinline{before}, these all operate on primitive values, and they are
described in the listed sections.

\begin{figure}
\centering
\begin{tabular}{ll}
  \smlinline{*} \smlinline{div} \smlinline{mod} \smlinline{/} & (\S\ref{sect:val}, \smlinline{/} unimplemented)\\
  \smlinline{+} \smlinline{-} \smlinline{^} & (\S\ref{sect:val})\\
  \smlinline{@} \smlinline{::} & (\S\ref{sect:compound})\\
  \smlinline{<} \smlinline{>} \smlinline{<=} \smlinline{>=} \smlinline{<>} \smlinline{=} & (\S\ref{sect:val}, \S\ref{sect:infix} for \smlinline{=})\\
  \smlinline{o} \smlinline{:=} & (\S\ref{sect:ref}, \smlinline{o} unimplemented)\\
  \smlinline{before} & (unimplemented)\\
  \smlinline{orelse} \smlinline{andalso} & (\S\ref{sect:val})
 \end{tabular}
\caption{Infix operators from tightest (at the top) to loosest binding}
\label{precedences}
\end{figure}

\paragraph{Equality}

The infix equality operator \smlinline{=} checks whether two values are equal, returning a boolean. The values must be of the same type. For atomic data (booleans, integers, bytes, and strings), they are equal exactly when they are the same value. For immutable data (tuples, lists, vectors, and algebraic data types), they are equal if they are made up of equal elements, recursively. For mutable data (references, arrays, and byte arrays), they are equal if they are the same structure. Their elements are not inspected.
If the equality function encounters a function value while traversing its arguments, it returns \smlinline{true}.

The \smlinline{<>} operator is the negation of \smlinline{=}.

\paragraph{The \smlinline{before} and \smlinline{o} operators}

The \smlinline{before} operator sequences two expressions, and returns the
value of the first one. The second is evaluate for its side effect. The type of
\smlinline{before} is \smlinline{'a -> unit -> 'a}. The following function
increments a reference, and returns the pre-increment value.
\begin{smlcode}
fun inc r =
  !r before r := !r + 1
\end{smlcode}

The \smlinline{o} operator composes two functions, first applying the one on
the right, then the one on the left. Its type is \smlinline{('a -> 'b) -> ('c ->
'a) -> 'c -> 'b}. In the following example, \smlinline{a} is bound to the
string \smlinline{"2"}.
\begin{smlcode}
fun add1 x = x + 1
val a = (Int.toString o add1) 1
\end{smlcode}

\todo{Implement o and before in the basis. I suspect this will require making
before a keyword, due to evaluation order issues.}

\paragraph{Suppressing infix status}
Infix status is suppressed with the \smlinline{op} prefix.
For example, we can use \smlinline{op+} to get a prefix
addition function, and then partially apply it to an argument.
\begin{smlcode}
val add1 = op+ 1
\end{smlcode}

The \smlinline{op} prefix also works in patterns, which lets us define our own
versions of these operators, shadowing their global definitions.
\begin{smlcode}
val op< = String.<
val x = "1" < "2"
\end{smlcode}

Since \smlinline{andalso} and \smlinline{orelse} are reserved words
(\S\ref{sect:variables}), \smlinline{op} cannot be used on them.

\section{Sequencing}

Expressions are sequenced by enclosing them in parentheses \smlinline{(}
\smlinline{)}, and separating them with semi-colons \smlinline{;}. The sequence
is evaluated left-to-right. The value of the last expression is returned; the
previous expressions are evaluated only for their side-effects.
The following function increments a reference and returns the post-increment value.
\begin{smlcode}
fun inc r =
  (r := !r + 1; !r)
\end{smlcode}

\section{Exceptions}
\label{sect:exceptions}

\paragraph{Exception declarations}
%Python hangs on \mintinline{sml}{exception}
The \mintinline{ocaml}{exception} declaration creates a new kind of exception. It must
start with a capital letter, and can have arguments similar to the constructor
of an algebraic data type.
\begin{smlcode}
exception Error
exception Type_error of int * string
\end{smlcode}

\paragraph{Raising exceptions}
A \smlinline{raise} expression raises its argument as an exception. For example,
\begin{smlcode}
if x < 0 then raise Error
else x
\end{smlcode}

\begin{smlcode}
if t1 = t2 then t1
else raise (Type_error (loc, "type mismatch"))
\end{smlcode}

A \smlinline{raise} expression can have any type, and so can be used anywhere
an expression is expected, as in \smlinline{4 + (raise Error)}.

\paragraph{Handling exceptions} If an exception is not handled, it will
terminate the execution of the program.  A \smlinline{handle} expression allows
us to handle exceptions raised in the preceding expression. It is followed by a
pattern match with the same syntax as in \smlinline{case}
(\S\ref{sect:compound}). Each pattern must match either an exception or be
\smlinline{_} to handle all exceptions. If no pattern matches the raised
exception, it is not handled and instead raised out of the \smlinline{handle}
expression.

The first declaration below sets \smlinline{m} to \smlinline{0}, whereas the second prints
the error message from a \smlinline{Type_error} exception, and a generic
message for any other exception.
\begin{smlcode}
val m =
  1 div 0 handle Div => 0
val x =
  type_check p
  handle
    Type_error (i, s) => print (Int.toString i ^ " " ^ s)
  | _ => print "unknown exception"
\end{smlcode}
\todo{Update print function call}

\section{Local bindings}

A \smlinline{let} expression lets us declare variables in a local scope.
\begin{smlcode}
let
  val x = 1
  fun f y = x + y
in
  f 10 + x
end
\end{smlcode}
The declarations occur between the \smlinline{let} and \smlinline{in}.
The expression between \smlinline{in} and \smlinline{end} becomes the value
for the whole \smlinline{let} expression.

\section{Modules}
\label{sect:modules}
\todo{Write this section}

\section{Differences from Standard ML}

\subsection{Unsupported features}
Here we only list missing features of the language, and not the basis library.

The CakeML module system is heavily restricted compared to SML's. Structures cannot be nested, and functors are not supported. Structures cannot be given alternate names, or opened. Signatures cannot be named, and must appear directly on the structure that they seal. Only opaque sealing is supported (\smlinline{:>}, but not \smlinline{:}). Signatures cannot contain \smlinline{include}, \smlinline{sharing}, \smlinline{structure}, \smlinline{eqtype} or datatype replication specifications.

In contrast, CakeML's core language is more fully featured, with only the following omissions. The \smlinline{local}, \smlinline{abstype}, and datatype replication declarations are not supported. Neither are records, type annotations that contain type variables, and \smlinline{while} loops. Furthermore, \smlinline{let} expressions are restricted to \smlinline{val} and \smlinline{fun} declarations; they cannot contain type or exception declarations. The pattern language does not support the \smlinline{as} form.

CakeML has a fixed set of infix operators, and does not support user defined parsing precedences (\smlinline{infix}, \smlinline{infixr}, and \smlinline{nonfix}). See Figure~\ref{precedences} for the supported infix operators.

Floating point numbers are not supported, nor are integer constants written in hexadecimal notation (\smlinline{0x}). Lastly, only the most basic escape sequences are supported in strings (just \texttt{\textbackslash n}, \texttt{\textbackslash t}, \texttt{\textbackslash "}, and \texttt{\textbackslash\textbackslash}).

Syntactic sugar for \smlinline{fun} declarations with pattern parameters is not provided, instead parameters are variables, and must be matched against with \smlinline{case} expressions, if desired.

\subsection{Syntactic and semantic differences}

All names must follow the OCaml convention where structure and constructor names start with a capital letter, and type and variable names must either start with a lower case letter, or be symbolic names.

CakeML does not support the limited overloading found in the SML Basis Library.

CakeML does not support the equality types that SML uses to ensure that the \smlinline{=} operation never encounters a function value. Instead, the \smlinline{=} returns \smlinline{true} if it does.

The types of bindings in \smlinline{let} expressions cannot be generalised. This restriction does not affect top level, or structure top level declarations.

The built-in CakeML functions prefer the curried style over SML's preferred tupled style. For example, we write \smlinline{Vector.sub v 12} to get the 12$^\textrm{th}$ element of vector v, rather than \smlinline{Vector.sub (v,12)}. The infix operators are also curried when used with \smlinline{op}.

CakeML guarantees right to left evaluation order for function calls.

\section{Differences from OCaml}

Because CakeML has a significantly different syntax, we focus here on the major features and semantic differences rather than attempt to catalogue every piece of OCaml syntax that lacks a CakeML analogue. Briefly, CakeML does not have floating point numbers, records, objects, polymorphic variants, labels, nested/local modules, or functors.

Strings are immutable; however, the Word8Array structure provides byte arrays.

CakeML guarantees right to left evaluation order for function calls.

The \texttt{=} operator does not traverse mutable data (arrays and references), instead it compares the pointers, SML style.

\chapter{Standard library}
\label{ch:stdlib}

%CakeML supports data of boolean, integer, character, and string types. It also supports compound data of tuple, list, option, vector, reference, array, and byte array types. Additionally, users can define new algebraic data types: these are described in  \S\ref{expressions} on pattern matching, and in \S\ref{declarations} on type definitions.


\section{Array}
\label{sect:array}

Arrays have a fixed length and support constant-time indexing. Each element of an array must have the same type. The operations on arrays are collected in the \texttt{Array} module. If the elements of an array are of some type $\tau$ then the vector's type is $\tau$\ \texttt{Array.array}.

The following are the supported operations on arrays. If an index is out of bounds (or negative), the \texttt{Subscript} exception is raised.
\begin{itemize}
\item \texttt{Array.array : int -> 'a -> 'a array} Create a new array of given length and default value.
\item \texttt{Array.length : 'a array -> int} Get the array's length.
\item \texttt{Array.sub : 'a array -> int -> 'a} Get the i$^\textrm{th}$ element.
\item \texttt{Array.update : 'a array -> int -> 'a -> unit} Set the i$^\textrm{th}$ element.
\end{itemize}

\section{Char}
\label{sect:char}

\section{Int}

\section{List}
\label{sect:list}

\section{Option} An optional value is either \texttt{NONE}, indicating that no value is present, or \texttt{SOME}\ $v$ for a value $v$. They type of an optional value that might contain a value of type $\tau$ is $\tau$\ \texttt{option}. There are no operations for de-structuring options.

\section{String}
\label{sect:string}

\section{Vector}
\label{sect:vector}

Vectors are immutable array-like structures. They have a fixed length and support constant-time indexing. Each element of a vector must have the same type. The operations on vectors are collected in the \texttt{Vector} module. If the elements of a vector are of some type $\tau$ then the vector's type is $\tau$\ \texttt{Vector.vector}.

The following are the supported operations on vectors. If an index is out of bounds (or negative), the \texttt{Subscript} exception is raised.
\begin{itemize}
\item \texttt{Vector.fromList : 'a list -> 'a vector} Convert a list to a vector containing the same elements (in order).
\item \texttt{Vector.length : 'a vector -> int} Get the vector's length.
\item \texttt{Vector.sub : 'a vector -> int -> 'a} Get the i$^\textrm{th}$ element.
\end{itemize}

\section{Word64}
\label{sect:word64}

\section{Word8}
\label{sect:word8}

\section{Word8Array}
Byte arrays have a fixed length and support constant-time indexing. Each element of an array must be a byte (\texttt{Word8.word} type). The operations on byte arrays are collected in the \texttt{Word8Array} module. The type of a byte array is \texttt{Word8Array.array}.

The following are the supported operations on byte arrays. If an index is out of bounds (or negative), the \texttt{Subscript} exception is raised.
\begin{itemize}
\item \texttt{Word8Array.array : int -> Word8.word -> Word8Array.array} Create a new array of given length and default value.
\item \texttt{Word8Array.length : Word8Array.array -> int} Get the array's length.
\item \texttt{Word8Array.sub : Word8Array.array -> int -> Word8.word} Get the i$^\textrm{th}$ element.
\item \texttt{Word8Array.update : Word8Array.array -> int -> Word8.word -> unit} Set the i$^\textrm{th}$ element.
\end{itemize}



\chapter{Formal syntax and semantics}

\section{Lexical and context free syntax}

\[
\begin{array}{lcll}
\alpha&=& \mbox{\texttt{'}[\texttt{a}-\texttt{z}\texttt{A}-\texttt{Z}\texttt{'}\texttt{\_}]}^*&\mbox{type variable}\\
i &=& \verb|~|^?\mbox{[\texttt{0}-\texttt{9}]}^+&\mbox{integer constant}\\
\end{array}
\]


\todo{Lexical syntax for str, tn, v, fqv, C, fqC, S}

\[
\begin{array}{lcll}
t & ::= & &\mbox{types}\\
&&\alpha & \mbox{type variable}\\
& \gramsep& t\ \texttt{*}\ t & \mbox{tuple}\\
 &\gramsep &t\ \texttt{->}\ t&\mbox{function}\\
 &\gramsep& \mathit{tn}&\mbox{type name}\\
 &\gramsep&t\ \mathit{tn}&\mbox{type application}\\
 &\gramsep& \texttt{(}t\texttt{,}t(\texttt{,}t)^*\texttt{)}\ \mathit{tn}&\mbox{type application}\\
 &\gramsep&\texttt{(}t\texttt{)}
 \end{array}
 \]

 \[
\begin{array}{lcll}
l & ::= &&\mbox{literal constants}\\
&& \texttt{true}\\
&\gramsep& \texttt{false}\\
&\gramsep& \texttt{(}\texttt{)}&\mbox{unit}\\
&\gramsep& \texttt{[}\texttt{]}&\mbox{empty list}\\
&\gramsep& \texttt{nil}&\mbox{empty list}\\
&\gramsep& i &\mbox{integer}\\
&\gramsep& \textit{str} &\mbox{string}\\
 \end{array}
\]

\[
\begin{array}{lcll}
p & ::= & &\mbox{patterns}\\
&&\texttt{\_}&\mbox{wildcard}\\
&\gramsep& v &\mbox{variable}\\
&\gramsep& l &\mbox{constant}\\
&\gramsep& \mathit{fqC} & \mbox{constant constructor}\\
&\gramsep& \mathit{fqC}\ p & \mbox{constructor application}\\
&\gramsep& \texttt{(}p\texttt{,}p(\texttt{,}p)^*\texttt{)}&\mbox{tuple}\\
&\gramsep& p \texttt{::} p&\mbox{list (first and rest)}\\
&\gramsep& \texttt{[}p(\texttt{,}p)^*\texttt{]}&\mbox{list (fixed length)}\\
 &\gramsep& \texttt{ref}\ p&\mbox{reference}\\
 &\gramsep& \texttt{(}p\texttt{)}
 \end{array}
\]

\[
\begin{array}{lcll}

e & ::= & &\mbox{expressions}\\
&&l &\mbox{constant}\\
&|& \mathit{fqv}&\mbox{variable}\\
&|&\mathit{fqC}&\mbox{constant constructor}\\
&|&\mathit{fqC}\ e&\mbox{constructor application}\\
&|&\texttt{(}e\texttt{,}e(\texttt{,}e)^*\texttt{)}&\mbox{tuple}\\
&|&\texttt{[}e(\texttt{,}e)^*\texttt{]}&\mbox{list}\\
&|&\texttt{raise}\ e & \mbox{exception raising}\\
&|& e\ \texttt{handle}\ p\ \texttt{=>}\ e\ (\texttt{|}p\ \texttt{=>}\ e)^*&\mbox{exception handling}\\
&|& \texttt{fn}\ v\ \texttt{=>}\ e&\mbox{function}\\
&|& e\ e&\mbox{function application}\\
&|& e\ \mathit{op}\ e&\mbox{binary operator}\\
&|& \texttt{(}(e\texttt{;})^*e\texttt{)}&\mbox{sequencing}\\
&|& \texttt{if}\ e\ \texttt{then}\ e\ \texttt{else}\ e&\mbox{conditional}\\
&|& \texttt{case}\ e\ \texttt{of}\ p\ \texttt{=>}\ e\ (\texttt{|}p\ \texttt{=>}\ e)^*&\mbox{pattern matching}\\
&|& \texttt{let}\ (\mathit{ld}|\texttt{;})^*\ \texttt{in}\ (e\texttt{;})^*e\ \texttt{end}&\mbox{let}\\
&|&\texttt{(}e\texttt{)}\\\\

\mathit{ld} &::=& &\mbox{local definition}\\
&& \texttt{val}\ x\ \texttt{=}\ e&\mbox{value}\\
 &|&\texttt{fun}\ v\ v^+\ \texttt{=}\ e\ (\texttt{and}\ v\ v^+\ \texttt{=}\ e)^*&\mbox{function}\\\\

\mathit{op} &::=& &\mbox{infix operators}\\
&&\texttt{*}\gramsep \texttt{div}\gramsep \texttt{mod}&\mbox{multipicative}\\
&|& \texttt{+}\gramsep \texttt{-}&\mbox{additive} \\
&|&\texttt{@}\gramsep{::} & \mbox{list}\\
&|&\texttt{=} \gramsep \texttt{<}\gramsep \texttt{<=}\gramsep \texttt{>}\gramsep \texttt{>=} \gramsep\texttt{<>}&\mbox{comparison}\\
&|&\texttt{o}\gramsep \texttt{:=}\\
&|&\texttt{before}&\mbox{sequencing}\\
&|&\texttt{andalso} \gramsep \texttt{orelse}&\mbox{logical}
\end{array}
\]


\[
\begin{array}{lcll}
d &::=& &\mbox{declarations}\\
&&\texttt{val}\ p\ \texttt{=}\ e&\mbox{value}\\
&|& \texttt{fun}\ v\ v^+\ \texttt{=}\ e\ (\texttt{and}\ v\ v^+\ \texttt{=}\ e)^*&\mbox{function}\\
&|&  \texttt{datatype}\ \mathit{tyd}\ (\texttt{and}\ \mathit{tyd})^*&\mbox{type}\\
&|& \texttt{exception}\ c&\mbox{exception}\\\\

c & ::= &&\mbox{constructors}\\
&& C&\mbox{constant}\\
& \gramsep &C\ \texttt{of}\ t&\mbox{with arguments}\\\\

\mathit{ptn} &::=& &\mbox{type names w/parameters}\\
&& \texttt{(}\alpha(\texttt{,}\alpha)^*\texttt{)}\ \mathit{tn}\\
&\gramsep& \alpha\ \mathit{tn}\\
&\gramsep& \mathit{tn}\\\\

\mathit{tyd} & ::= & \mathit{ptn}\ \texttt{=}\ c(\texttt{|}c)^* & \mbox{define a single type}
\end{array}
\]

\[
\begin{array}{lcll}
m &::=& \texttt{structure}\ S\ s^?\ \texttt{=}\ \texttt{struct}\ (d|\texttt{;})^*\ \texttt{end}&\mbox{modules}\\\\

s &::=& \texttt{:>}\ \texttt{sig}\ (\mathit{sp}|\texttt{;})^*\ \texttt{end}&\mbox{signatures}\\\\

\mathit{sp}&::=&  &\mbox{specifications}\\
&&\texttt{val}\ v\ \texttt{:}\ t& \mbox{value}\\
&\gramsep& \texttt{type}\ \textit{tyn}&\mbox{opaque type}\\
&|&  \texttt{datatype}\ \mathit{tyd}\ (\texttt{and}\ \mathit{tyd})^*&\mbox{type}\\
&|& \texttt{exception}\ c&\mbox{exception}
\end{array}
\]

\[
\begin{array}{lcll}
\mathit{top} &::=& &\mbox{top-level declaration}\\
&& m &\mbox{module}\\
&& d &\mbox{declaration}\\
\end{array}
\]



\section{Abstract syntax}
%
%The abstract syntax of CakeML is defined in Lem in \texttt{semantics/ast.lem}\footnote{\url{https://github.com/CakeML/cakeml/blob/master/semantics/ast.lem}}. This file is included here.
%
%{\setlength{\parindent}{0pt}
%\todo{Figure out why Lem is omitting leading comments. Possibly change the typesetting}
%\include{lem-generated/Ast-inc}
%
%\LEMTypeLit
%
%\LEMTypeOpn
%
%\LEMTypeOpb
%
%\LEMTypeModN
%
%%\LEMTypeId
%
%\LEMTypeVarN
%
%\LEMTypeConN
%
%\LEMTypeTypeN
%
%\LEMTypeTvarN
%
%%\LEMValspecMkId
%
%%\LEMmkId
%
%%\LEMValspecIdToN
%
%%\LEMidToN
%
%\LEMTypeOp
%
%\LEMTypeLop
%
%\LEMTypeTctor
%
%\LEMTypeT
%
%\LEMTint
%
%\LEMTstring
%
%%\LEMTunit
%
%%\LEMTbool
%
%\LEMTref
%
%\LEMTwordEight
%
%\LEMTwordEightarray
%
%\LEMTfn
%
%\LEMTexn
%
%\LEMTypePat
%
%\LEMTypeExp
%
%\LEMTypeTypeDef
%
%\LEMTypeDec
%
%\LEMTypeDecs
%
%\LEMTypeSpec
%
%\LEMTypeSpecs
%
%\LEMTypeTop
%
%\LEMTypeProg
%
%\LEMValspecPatBindings
%
%\LEMconstZero
%}

\section{Type system}

\section{Operational semantics}

\chapter{Theorems}


\part{The CakeML compiler and verification tools}

\chapter{Installing and using the compiler}

\chapter{Extracting pure CakeML programs from HOL4}

\chapter{Verifying effectful CakeML programs with characteristic formulae}

\end{document}