From 25c23ae3789b527a3a0bbb70f762d23db6408a6e Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Mon, 8 Mar 2021 11:42:49 +1100
Subject: [PATCH] Add MiniZinc syntax specification in the appendix

---
 chapters/4_rewriting.tex         |  41 +++--
 chapters/A1_minizinc_grammar.tex | 274 +++++++++++++++++++++++++++++++
 dekker_thesis.tex                |  10 +-
 3 files changed, 300 insertions(+), 25 deletions(-)
 create mode 100644 chapters/A1_minizinc_grammar.tex

diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex
index 766d51a..de3c789 100644
--- a/chapters/4_rewriting.tex
+++ b/chapters/4_rewriting.tex
@@ -180,20 +180,19 @@ This section introduces the two sub-languages of \minizinc\ at the core of the
 new abstract machine model we have developed.
 
 MicroZinc (\microzinc) is a simplified subset of \minizinc\ that only contains
-function declarations and a restricted expression language. \minizinc\ models
-can be translated into \microzinc. NanoZinc (\nanozinc) is similar to
-\flatzinc\ in that it contains only simple variable declarations and flat
-constraints. However, while all function calls in \flatzinc\ need to be
+function declarations and a restricted expression language. Models written in
+different \cmls\ can be translated into \microzinc. NanoZinc (\nanozinc) is
+similar to \flatzinc\ in that it contains only simple variable declarations and
+flat constraints. However, while all function calls in \flatzinc\ need to be
 solver-level primitives, \nanozinc\ calls can refer to functions implemented in
 \microzinc.
 
-The core of the syntax of \microzinc\ is defined in
-\cref{fig:4-uzn-syntax}. We have omitted the definitions of
-\syntax{<type-inst>} and \syntax{<ident>}, which you can assume to be the same
-as in the definition of \minizinc. While we omit the typing rules here for
-space reasons, we will assume that in well-typed \microzinc\ programs, the
-conditions \syntax{<exp>} in if-then-else and where expressions have \pari\
-type.
+The core of the syntax of \microzinc\ is defined in \cref{fig:4-uzn-syntax}. We
+have omitted the definitions of \syntax{<type-inst>} and \syntax{<ident>}, which
+you can assume to be the same as in the definition of \minizinc. While we omit
+the typing rules here for space reasons, we will assume that in well-typed
+\microzinc\ programs, the conditions \syntax{<exp>} in if-then-else and where
+expressions have \pari\ type.
 
 \begin{figure}
   \begin{grammar}
@@ -219,11 +218,11 @@ type.
 
 \newcommand{\sep}{\rhd}
 
-A \nanozinc\ program, defined in \cref{fig:4-nzn-syntax}, is simply a list
-of calls, where the result of each call is bound to either an identifier or the
+A \nanozinc\ program, defined in \cref{fig:4-nzn-syntax}, is simply a list of
+calls, where the result of each call is bound to either an identifier or the
 constant true. The \syntax{$\sep$ <ident>*} will be used to track dependent
-constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for
-now you can assume it is empty).
+constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for now
+you can assume it is empty).
 
 \begin{figure}
   \begin{grammar}
@@ -270,9 +269,9 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
 
   \begin{mzn}
     predicate all_different(array[int] of var int: x) =
-    forall (i,j in 1..length(x) where i<j) (
-      x[i] != x[j]
-    );
+      forall (i,j in 1..length(x) where i<j) (
+        x[i] != x[j]
+      );
 
     int: n;
     array[1..n] of var 1..n-1: pigeon;
@@ -304,9 +303,9 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
     } in true;
   \end{mzn}
 
-For a concrete instance of the model, we can then create a simple \nanozinc
-program that calls \mzninline{main}, for example for $n=10$: \mzninline{true
-@$\mapsto$@ main(10) @$\sep$@ []}.
+  For a concrete instance of the model, we can then create a simple \nanozinc
+  program that calls \mzninline{main}, for example for $n=10$: \mzninline{true
+    @$\mapsto$@ main(10) @$\sep$@ []}.
 \end{example}
 
 \subsection{Partial Evaluation of NanoZinc}
diff --git a/chapters/A1_minizinc_grammar.tex b/chapters/A1_minizinc_grammar.tex
new file mode 100644
index 0000000..fc7efe6
--- /dev/null
+++ b/chapters/A1_minizinc_grammar.tex
@@ -0,0 +1,274 @@
+%************************************************
+\chapter{The Syntax of \glsentrytext{minizinc}}\label{ch:minizinc-grammar}
+%************************************************
+%
+\minizinc\ \autocite{nethercote-2007-minizinc} is a solver-independent
+constraint modelling language that is used as the example high-level constraint
+modelling language throughout this thesis. This chapter offers a formal
+specification of the grammar of the current version \minizinc\ language,
+corresponding with \minizinc\ version 2.5.3.
+
+For the convinience of the reader the grammar has been split into several parts.
+\Cref{sec:mzn-grammar-items} shows the syntax for the top-level structure of a
+model. \Cref{sec:mzn-grammar-typeinst} shows the syntax of type expressions,
+used for variable declarations and return types of variables.
+\Cref{sec:mzn-grammar-expressions} shows the syntax of expressions used all
+other parts of the model. Finally, \Cref{sec:mzn-grammar-expressions} contains
+the rules for identifiers and annotations.
+
+\section{Items}
+\label{sec:mzn-grammar-items}
+
+\begin{grammar}
+  % A MiniZinc model
+  <model> ::= [ <item> ";" ... ]
+
+  % Items
+  <item> ::= <include-item>
+    \alt <var-decl-item>
+    \alt <enum-item>
+    \alt <assign-item>
+    \alt <constraint-item>
+    \alt <solve-item>
+    \alt <output-item>
+    \alt <predicate-item>
+    \alt <test-item>
+    \alt <function-item>
+    \alt <annotation-item>
+
+  <ti-expr-and-id> ::= <ti-expr> ":" <ident>
+
+  % Include items
+  <include-item> ::= "include" <string-literal>
+
+  % Variable declaration items
+  <var-decl-item> ::= <ti-expr-and-id> <annotations> [ "=" <expr> ]
+
+  % Enum items
+  <enum-item>  ::= "enum" <ident> <annotations> [ "=" <enum-cases-list> ]
+
+  <enum-cases-list> ::= <enum-cases>
+  \alt <enum-cases-list> "++" <enum-cases>
+
+  <enum-cases> ::= "{" <ident> "," ... "}"
+  \alt <ident> "(" <ident> ")"
+
+  % Assign items
+  <assign-item> ::= <ident> "=" <expr>
+
+  % Constraint items
+  <constraint-item> ::= "constraint" <string-annotation> <expr>
+
+  % Solve item
+  <solve-item> ::= "solve" <annotations> "satisfy"
+  \alt "solve" <annotations> "minimize" <expr>
+  \alt "solve" <annotations> "maximize" <expr>
+
+  % Output items
+  <output-item> ::= "output" <expr>
+
+  % Annotation items
+  <annotation-item> ::= "annotation" <ident> <params>
+
+  % Predicate, test and function items
+  <predicate-item> ::= "predicate" <operation-item-tail>
+
+  <test-item> ::= "test" <operation-item-tail>
+
+  <function-item> ::= "function" <ti-expr> ":" <operation-item-tail>
+
+  <operation-item-tail> ::= <ident> <params> <annotations> [ "=" <expr> ]
+
+  <params> ::= [ ( <ti-expr-and-id> "," ... ) ]
+
+\end{grammar}
+
+\section{Type Instance Expressions}
+\label{sec:mzn-grammar-typeinst}
+
+\begin{grammar}
+  % Type-inst expressions
+  <ti-expr> ::= <base-ti-expr>
+  \alt <array-ti-expr>
+
+  <base-ti-expr> ::= <var-par> <opt-ti> <set-ti> <base-ti-expr-tail>
+
+  <var-par> ::= "var" \alt "par" \alt <empty>
+
+  <opt-ti> ::= "opt" \alt <empty>
+
+  <set-ti> ::= "set" "of" \alt <empty>
+
+  <base-type> ::= "bool"
+  \alt "int"
+  \alt "float"
+  \alt "string"
+
+  <base-ti-expr-tail> ::= <ident>
+  \alt <base-type>
+  \alt <ti-variable-expr-tail>
+  \alt "ann"
+  \alt \{ <expr> "," ... \}
+  \alt <num-expr> ".." <num-expr>
+
+  % % Type-inst variables
+  <ti-variable-expr-tail> ::= \(regexp\left(\texttt{\$[A-Za-z][A-Za-z0-9\_]*}\right)\)
+
+  % Array type-inst expressions
+  <array-ti-expr> ::= "array" [ <ti-expr> "," ... ] "of" <base-ti-expr>
+  \alt "list" "of" <base-ti-expr>
+\end{grammar}
+
+\section{Expressions}
+\label{sec:mzn-grammar-expressions}
+
+\begin{grammar}
+  % Expressions
+  <expr> ::= <expr-atom> <expr-binop-tail>
+
+  <expr-atom> ::= <expr-atom-head> <expr-atom-tail> <annotations>
+
+  <expr-binop-tail> ::= [ <bin-op> <expr> ]
+
+  <expr-atom-head> ::= <builtin-un-op> <expr-atom>
+  \alt "(" <expr> ")"
+  \alt <ident-or-quoted-op>
+  \alt "_"
+  \alt <bool-literal>
+  \alt <int-literal>
+  \alt <float-literal>
+  \alt <string-literal>
+  \alt <set-literal>
+  \alt <set-comp>
+  \alt <array-literal>
+  \alt <array-literal-2d>
+  \alt <array-comp>
+  \alt <ann-literal>
+  \alt <if-then-else-expr>
+  \alt <let-expr>
+  \alt <call-expr>
+  \alt <gen-call-expr>
+
+  <expr-atom-tail> ::= <empty>
+  \alt <array-access-tail> <expr-atom-tail>
+
+  % Numeric expressions
+  <num-expr> ::= <num-expr-atom> <num-expr-binop-tail>
+
+  <num-expr-atom> ::= <num-expr-atom-head> <expr-atom-tail> <annotations>
+
+  <num-expr-binop-tail> ::= [ <num-bin-op> <num-expr> ]
+
+  <num-expr-atom-head> ::= <builtin-num-un-op> <num-expr-atom>
+  \alt "(" <num-expr> ")"
+  \alt <ident-or-quoted-op>
+  \alt <int-literal>
+  \alt <float-literal>
+  \alt <if-then-else-expr>
+  \alt <let-expr>
+  \alt <call-expr>
+  \alt <gen-call-expr>
+
+  % Built-in operators
+  <builtin-op> ::= <builtin-bin-op> \alt <builtin-un-op>
+
+  <bin-op> ::= <builtin-bin-op> \alt ‘<ident>‘
+
+  <builtin-bin-op> ::= "<->" \alt "->" \alt "<-" \alt "\\/" \alt "xor" \alt "/\\" \alt "<" \alt ">" \alt "<=" \alt ">=" \alt "==" \alt "=" \alt "!="
+  \alt "in" \alt "subset" \alt "superset" \alt "union" \alt "diff" \alt "symdiff"
+  \alt ".." \alt "intersect" \alt "++" \alt <builtin-num-bin-op>
+
+  <builtin-un-op> ::= "not" \alt <builtin-num-un-op>
+
+  % Built-in numeric operators
+  <num-bin-op> ::= <builtin-num-bin-op> \alt ‘<ident>‘
+
+  <builtin-num-bin-op> ::= "+" \alt "-" \alt "*" \alt "/" \alt "div" \alt "mod" \alt "^"
+
+  <builtin-num-un-op> ::= "+" \alt "-"
+
+  % Boolean literals
+  <bool-literal> ::= "false" \alt "true"
+
+  % Integer literals
+  <int-literal> ::= \(regexp\left(\texttt{[0-9]+}\right)\)
+  \alt \(regexp\left(\texttt{0x[0-9A-Fa-f]+}\right)\)
+  \alt \(regexp\left(\texttt{0o[0-7]+}\right)\)
+
+  % Float literals
+  <float-literal> ::= \(regexp\left(\verb=[0-9]+\.[0-9]+=\right)\)
+  \alt \(regexp\left(\verb=[0-9]+\.[0-9]+[Ee][-+]?[0-9]+=\right)\)
+  \alt \(regexp\left(\verb=[0-9]+[Ee][-+]?[0-9]+=\right)\)
+  \alt \(regexp\left(\verb=0[xX]([0-9a-fA-F]*"."[0-9a-fA-F]+|[0-9a-fA-F]+".")([pP][+-]?[0-9]+)=\right)\)
+  \alt \(regexp\left(\verb=(0[xX][0-9a-fA-F]+[pP][+-]?[0-9]+)=\right)\)
+
+  % String literals
+  <string-contents> ::= \(regexp\left(\verb=([^"\n\] | \[^\n(])*=\right)\)
+
+  <string-literal> ::= \" <string-contents> \"
+  \alt \" <string-contents> "\\(" <string-interpolate-tail>
+
+  <string-interpolate-tail> ::= <expr> ")" <string-contents> \"
+  \alt <expr> ")"<string-contents> "\\(" <string-interpolate-tail>
+
+  % Set literals
+  <set-literal> ::= "{" [ <expr> "," ... ] "}"
+
+  % Set comprehensions
+  <set-comp> ::= "{" <expr> "\alt" <comp-tail> "}"
+
+  <comp-tail> ::= <generator> [ "where" <expr> ] "," ...
+
+  <generator> ::= <ident> "," ... "in" <expr>
+
+  % Array literals
+  <array-literal> ::= "[" [ <expr> "," ... ] "]"
+
+  % 2D Array literals
+  <array-literal-2d> ::= "[\alt" [ (<expr> "," ...) "\alt" ... ] "\alt]"
+
+  % Array comprehensions
+  <array-comp> ::= "[" <expr> "\alt" <comp-tail> "]"
+
+  % Array access
+  <array-access-tail> ::= "[" <expr> "," ... "]"
+
+  % Annotation literals
+  <ann-literal> ::= <ident> [ "(" <expr> "," ... ")" ]
+
+  % If-then-else expressions
+  <if-then-else-expr> ::= "if" <expr> "then" <expr> [ "elseif" <expr> "then" <expr> ]* "else" <expr> "endif"
+
+  % Call expressions
+  <call-expr> ::= <ident-or-quoted-op> [ "(" <expr> "," ... ")" ]
+
+  % Let expressions
+  <let-expr> ::= "let" "{" <let-item> ";" ... "}" "in" <expr>
+
+  <let-item> ::= <var-decl-item>
+  \alt <constraint-item>
+
+  % Generator call expressions
+  <gen-call-expr> ::= <ident-or-quoted-op> "(" <comp-tail> ")" "(" <expr> ")"
+\end{grammar}
+
+\section{Identifiers and Annotations}
+\label{sec:mzn-grammar-misc}
+
+\begin{grammar}
+  % % Miscellaneous
+  % Identifiers
+  <ident> ::= \(regexp\left(\texttt{[A-Za-z][A-Za-z0-9\_]*}\right)\)
+     \alt \(regexp\left(\verb|'[^'\xa\xd\x0]*'|\right)\)
+
+  % Identifiers and quoted operators
+  <ident-or-quoted-op> ::= <ident>
+  \alt ’<builtin-op>’
+
+  % Annotations
+  <annotations> ::= [ "::" <annotation> ]*
+
+  <annotation> ::= <expr-atom-head> <expr-atom-tail>
+
+  <string-annotation> ::= "::" <string-literal>
+\end{grammar}
diff --git a/dekker_thesis.tex b/dekker_thesis.tex
index fa8ecc0..19a699a 100644
--- a/dekker_thesis.tex
+++ b/dekker_thesis.tex
@@ -33,9 +33,9 @@ Some ideas and figures included in this thesis have previously appeared in the
 following publication:
 
 \begin{refsection}[ownpubs]
-    \small
-    \nocite{*} % is local to to the enclosing refsection
-    \printbibliography[heading=none]
+  \small
+  \nocite{*} % is local to to the enclosing refsection
+  \printbibliography[heading=none]
 \end{refsection}
 
 \mainmatter{}
@@ -46,8 +46,10 @@ following publication:
 \include{chapters/5_half_reif}
 \include{chapters/6_incremental}
 
-\backmatter{}
+\appendix{}
+\include{chapters/A1_minizinc_grammar}
 
+\backmatter{}
 \printbibliography{}
 % \tableofcontents{}
 % \addcontentsline{toc}{chapter}{Contents}