%************************************************
\chapter{The Syntax of \glsentrytext{minizinc}}\label{ch:minizinc-grammar}
%************************************************

\noindent{}\minizinc\ \autocite{nethercote-2007-minizinc} is a solver-independent \gls{cml} that is used as the leading \gls{cml} throughout this thesis.
This chapter offers a formal specification of the grammar of the current version \minizinc{} language, corresponding with \minizinc{} version 2.5.5.

For the convenience 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 \minizinc{} model.
\Cref{sec:mzn-grammar-typeinst} shows the syntax of type expressions, used for declarations and return types of functions.
\Cref{sec:mzn-grammar-expressions} shows the syntax of \minizinc{}'s expressions.
Finally, \Cref{sec:mzn-grammar-misc} contains the rules for identifiers and \glspl{annotation}.

\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}