%************************************************
\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> ::= <type-inst> ":" <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" <type-inst> ":" <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
  <type-inst> ::= <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" [ <type-inst> "," ... ] "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{\textbackslash{}d+}\right)\)
  \alt \(regexp\left(\texttt{0x\textbackslash{}x+}\right)\)
  \alt \(regexp\left(\texttt{0o\textbackslash{}O+}\right)\)

  % Float literals
  <float-literal> ::= \(regexp\left(\verb=\d+\.\d+=\right)\)
  \alt \(regexp\left(\verb=\d+\.\d+[Ee][-+]?\d+=\right)\)
  \alt \(regexp\left(\verb=\d+[Ee][-+]?\d+=\right)\)
  \alt \(regexp\left(\verb=0[xX](\x*\.\x+|\x+\.)([pP][+-]?\d+)=\right)\)
  \alt \(regexp\left(\verb=(0[xX]\x+[pP][+-]?\d+)=\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}