Adjust grammar and proofs in Rewriting chapter

.chktexrc

@@ -1,5 +1,5 @@
 # Exclude these environments from syntax checking
 VerbEnvir { pgfpicture tikzpicture mzn nzn grammar proof }
-MathCmd { hypo infer1 infer2 infer3 }
+MathCmd { \hypo }
 
 WipeArg { \mzninline:{} \nzninline:{} \Sem:{} \texttt:{} }

chapters/4_rewriting.tex

@@ -68,15 +68,17 @@ and where expressions have \mzninline{par} type.
 
 \begin{figure}
   \begin{grammar}
-    <model> ::= <fun-decl>*
+    <model> ::= <pred-decl>*<fun-decl>*
 
-    <fun-decl> ::= "function" <type-inst>":" <ident>"(" <param> ["," <param>]* ")" [ "=" <exp> ]";"
+    <pred-decl> ::= "predicate" <ident>"(" <param> ["," <param>]* ");"
+
+    <fun-decl> ::= "function" <type-inst>":" <ident>"(" <param> ["," <param>]* ")" "=" <exp>";"
 
     <literal> ::= <constant> | <ident>
 
     <exp> ::= <literal>
-      \alt <ident>"(" <literal> ["," <literal>]* ")"
+      \alt <ident>"(" <exp> ["," <exp>]* ")"
-      \alt "let" "{" <item>* "}" "in" <exp>
+      \alt "let" "{" <item>* "}" "in" <ident>
       \alt "if" <exp> "then" <exp> "else" <exp> "endif"
       \alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
       \alt "(" <exp> ["," <exp>]* ")"
@@ -164,7 +166,7 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
   constraint for each element of the array.
 
   \begin{mzn}
-    predicate all_different(array[int] of var int: x) =
+    function var bool: all_different(array[int] of var int: x) =
       forall([
         int_neq(element(x, i),element(x, j))
         | i in range(1, length(x)),
@@ -172,14 +174,15 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
           where int_lt(i,j)
       ]);
 
-    predicate main(int: n) = let {
+    function var bool: main(int: n) = let {
+      var bool: root_ctx;
       array[range(1, n)] of var int: pigeon;
       constraint forall([
         set_in(element(pigeon, i), range(1, int_minus(n,1)))
         | i in range(1, n)
       ])
       constraint all_different(pigeon);
-    } in true;
+    } in root_ctx;
   \end{mzn}
 
   For a concrete instance of the model, we can then create a simple \nanozinc\
@@ -308,24 +311,20 @@ suitable alpha renaming.
 \begin{figure*}
 \centering
 \begin{prooftree}
-  \hypo{\ptinline{F(\(p_1, \ldots, p_k\)) = E;} \in \Prog \text{~where the~} p_i \text{~are fresh}}
+  \hypo{\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
-  \infer[no rule]1{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \Rightarrow \tuple{v_i,
+  \infer[no rule]1{\Sem{E}{\Prog, \Env_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}} \Rightarrow \tuple{v, \Env'}}
-      \Env_i'}, \ \Env_0=\Env, \Env_i=\Env_i'\cup\{p_i\mapsto v_i\sep[]\}, \forall 1 \leq i \leq k}
+  \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'_{[a_i \mapsto p_i, \forall{} 1 \leq{} i \leq{} k]}}}
-   \infer[no rule]1{\Sem{E}{\Prog, \Env_k} \Rightarrow \tuple{v, \Env'}}
-  \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_{0}} \Rightarrow \tuple{v, \Env'}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\ptinline{F} \in \text{Builtins}}
-  \hypo{\Sem{\(a_i\)}{\Prog, \Env} \Rightarrow \tuple{v_i, \Env}, \forall{} 1 \leq{} i \leq{} k}
+  \infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{ \mathit{eval}(\ptinline{F}(a_1,\ldots, a_k)), \Env}}
-  \infer2[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow \tuple{ \mathit{eval}(\ptinline{F}(v_1,\ldots, v_k)), \Env}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
-  \hypo{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \Rightarrow \tuple{v_i, \Env_i}, \forall 1 \leq i \leq k}
+  \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow
-  \infer2[(CallPrimitive)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow
+    \tuple{\texttt{constraint~} \text{F}(v_1, \ldots, v_k), \Env_k}}
-    \tuple{ x, \{ x \mapsto \ptinline{F}(v_1,\ldots, v_k) \sep [] \} \cup \Env_k}}
 \end{prooftree}
 \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
   of \microzinc\ calls to \nanozinc.}
@@ -343,45 +342,44 @@ directly, such as arithmetic and Boolean operations on fixed values. The rule
 simply returns the result of evaluating the built-in function on the evaluated
 parameter values.
 
-The (CallPrimitive) rule applies to non-built-in functions that are defined
+The (CallPredicate) rule applies to calls to solver predicates. These are
-without a function body. These are considered primitives, and as such simply
+considered primitives, and as such simply need to be transferred into the
-need to be transferred into the \nanozinc\ program. The rule evaluates all
+\nanozinc\ program. The rule evaluates all actual parameters, and creates a new
-actual parameters, and creates a new variable \(x\) to store the result, which is
+variable \(x\) to store the result, which is simply the function applied to the
-simply the function applied to the evaluated parameters.
+evaluated parameters.
 
 \begin{figure*}
 \centering
 \begin{prooftree}
   \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env} \Rightarrow (\Ctx, \Env')}
-  \hypo{\Sem{\(E\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
+  \hypo{\Sem{\(E\)}{\Prog, \Env'} \Rightarrow \tuple{x, \{ t : x \}\cup{}\Env''}}
-  \hypo{x \text{~fresh}}
+  \infer2[(LetC)]{\Sem{let \{ \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \Rightarrow
-  \infer3[(LetC)]{\Sem{let \{ \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \Rightarrow
+    \tuple{x, \{ t : x_{\texttt{~└──~}} \Ctx \} \cup \Env''}}
-    \tuple{x, \{ x \mapsto v \sep \Ctx \} \cup \Env''}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{}
   \infer1[(Item0)]{\Sem{\(\epsilon\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \Env}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
-  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env\ \cup\ \{x \mapsto\ \texttt{mkvar()} \sep\ []\}} \Rightarrow \tuple{\Ctx, \Env'}}
+  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env\ \cup\ \{t : x\}} \Rightarrow \tuple{\Ctx, \Env'}}
   \infer1[(ItemT)]{\Sem{\(t:x, \mathbf{I}\)}{\Prog, \Env} \Rightarrow \tuple{\Ctx, \Env'}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
-  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x \mapsto\ v \sep\ [] \}} \Rightarrow \tuple{\Ctx, \Env''}}
+  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env'_{[x \mapsto v]}} \Rightarrow \tuple{\Ctx, \Env''}}
   \infer2[(ItemTE)]{\Sem{\(t:x = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow \tuple{\Ctx, \Env''}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
-  \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{1}, \ldots, v_{n}\right), \Env'}}
+  \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{\langle{}1\rangle}, \ldots, v_{\langle{}k\rangle}\right), \Env'}}
-  \infer[no rule]1{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x_{1} \mapsto\ v_{1} \sep\ [] \} \cup\ \ldots\ \cup\ \{x_{n} \mapsto\ v_{n} \sep\ [] \}} \Rightarrow \tuple{\Ctx, \Env''}}
+  \infer[no rule]1{\Sem{\(\mathbf{I}\)}{\Prog, \Env'_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}} \Rightarrow\ \tuple{\Ctx, \Env''}}
-  \infer1[(ItemTD)]{\Sem{\(\left(t_{1}: x_{1}, \ldots, t_{n}: x_{n}\right) = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow
+  \infer1[(ItemTD)]{\Sem{\(\left(t_{1}: x_{1}, \ldots, t_{k}: x_{k}\right) = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow\
     \tuple{\Ctx, \Env''}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
   \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env'} \Rightarrow \tuple{\Ctx, \Env''}}
@@ -405,56 +403,53 @@ is the base case for a list of let items.
 
 \begin{figure*}
 \centering
+% \begin{prooftree}
+%   \hypo{x \in \langle \text{ident} \rangle}
+%   \hypo{v \in \langle \text{literal} \rangle}
+%   \infer2[(IdC)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}}
+% \end{prooftree} \\
+% \bigskip
 \begin{prooftree}
-  \hypo{x \in \syntax{<ident>}}
+  \hypo{x \in \langle \text{ident} \rangle}
-  \hypo{v \in \syntax{<literal>}}
-  \infer2[(IdC)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}}
-\end{prooftree} \\
-\medskip
-\begin{prooftree}
-  \hypo{x \in \syntax{<ident>}}
   \hypo{v}
   \hypo{\phi \text{~otherwise}}
-  \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ \phi\ \} \cup\ \Env} \Rightarrow \tuple{x, \{x \mapsto v \sep \phi \} \cup \Env}}
+  \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{t: x^{\texttt{~└──~}} \phi\ \} \cup\ \Env} \Rightarrow \tuple{x, \{t: x^{\texttt{~└──~}} \phi \cup \phi}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{c \text{~constant}}
   \infer1[(Const)]{\Sem{c}{\Prog, \Env} \Rightarrow \tuple{c, \Env}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k}
-  \infer1[(Tuple)]{\Sem{\(\left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}} \Rightarrow \tuple{x, \{x \mapsto \left(v_{1}, \ldots, v_{n}\right) \sep [] \} \cup \Env^{k}}}
+  \infer1[(Tuple)]{\Sem{\(\left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}} \Rightarrow \tuple{x, \Env^{k}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \_}}
   \infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow \Sem{\(E_t\)}{\Prog, \Env}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{false}, \_}}
   \infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow \Sem{\(E_e\)}{\Prog, \Env}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{ \ptinline{true}, \_}}
   \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple {v, \Env'}}
   \infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[v], \Env'}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}}
   \infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[], \Env}}
 \end{prooftree} \\
-\medskip
+\bigskip
 \begin{prooftree}
   \hypo{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \Rightarrow \tuple{S, \_}}
-  \infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env\ \cup\ \{ x\mapsto\
+  \infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env_{[x \mapsto v]}} \Rightarrow \tuple{A_v, \Env_{[x \mapsto v]} \cup \Env_v}, \forall{} v \in S }
-      v \sep\ []\}}}
-  \infer[no rule]1{\hspace{8em} \Rightarrow \tuple{A_v, \Env \cup \{x \mapsto v \sep []\} \cup \Env_v}, \forall
-    v \in S }
   \infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow
     \tuple{\mbox{concat} [ A_v ~|~ v \in S ], \Env \cup \bigcup_{v \in S} \Env_v}}
 \end{prooftree}