From 548a482b6e76ea16b8465a71f86729bfac7422ea Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 7 Apr 2021 15:50:06 +1000 Subject: [PATCH] Update the rewrite rules with correct projection rules --- chapters/4_rewriting.tex | 57 +++++++++++++++++++--------------------- 1 file changed, 27 insertions(+), 30 deletions(-) diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index eaac2a4..87696d0 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -304,8 +304,8 @@ suitable alpha renaming. \centering \begin{prooftree} \hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}} - \infer[no rule]1{\Sem{E}{\Prog, \Env_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}} \Rightarrow \tuple{v, \Env'}} - \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{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env}} \Rightarrow \tuple{v, \Env'} + \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}} \end{prooftree} \\ \bigskip \begin{prooftree} @@ -316,7 +316,7 @@ suitable alpha renaming. \begin{prooftree} \hypo{\texttt{predicate}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog} \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow - \tuple{\texttt{constraint~} \text{F}(v_1, \ldots, v_k), \Env_k}} + \tuple{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env_k}} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc\ calls to \nanozinc.} @@ -324,10 +324,10 @@ suitable alpha renaming. The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls. The first rule (Call) evaluates a function call expression in the context of a \microzinc\ -program \(\Prog\) and \nanozinc\ program \(\Env\). The rule first evaluates all -actual parameter expressions \(a_i\), creating new contexts where the evaluation -results are bound to the formal parameters \(p_i\). It then evaluates the -function body \(\ptinline{E}\) on this context, and returns the result. +program \(\Prog\) and \nanozinc\ program \(\Env\). The rule creates a new +contexts where the evaluation results are bound to the formal parameters +\(p_i\). It then evaluates the function body \(\ptinline{E}\) on this context, +and returns the result. The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated directly, such as arithmetic and Boolean operations on fixed values. The rule @@ -343,40 +343,42 @@ evaluated parameters. \begin{figure*} \centering \begin{prooftree} - \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env} \Rightarrow (\Ctx, \Env')} - \hypo{\Sem{\(E\)}{\Prog, \Env'} \Rightarrow \tuple{x, \{ t : x \}\cup{}\Env''}} - \infer2[(LetC)]{\Sem{let \{ \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \Rightarrow - \tuple{x, \{ t : x_{\texttt{~└──~}} \Ctx \} \cup \Env''}} + \hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \emptyset} \Rightarrow \tuple{x, \Env'}} + \infer1[(Let)]{\Sem{let \{ \(\mathbf{I}\) \} in \(\mathbf{X}\)}{\Prog, \Env} \Rightarrow\ \tuple{x, \Env'}} \end{prooftree} \\ \bigskip \begin{prooftree} - \hypo{} - \infer1[(Item0)]{\Sem{\(\epsilon\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \Env}} + \hypo{\Sem{\(\mathbf{X}\)}{\Prog, \{ t : x \} \cup{} \Env} \Rightarrow \tuple{x, \{ t : x \} \cup{} \Env'}} + \infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t : x \}\cup{}\Env, \Ctx} \Rightarrow \tuple{x, \{ t : x_{\texttt{~└──~}} \Ctx \} \cup \Env'}} \end{prooftree} \\ \bigskip \begin{prooftree} - \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'}} + \hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env\ \cup\ \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}} + \infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow \tuple{x, \Env'}} \end{prooftree} \\ \bigskip \begin{prooftree} \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \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''}} + \hypo{\Sem{\(\mathbf{I}_{[x \mapsto v]} \mid{} \mathbf{X}_{[x \mapsto v]}\)}{\Prog, \Env', \Ctx} \Rightarrow\ \tuple{x, \Env''}} + \infer2[(ItemTE)]{\Sem{\(t\texttt{:}~x = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}} +\end{prooftree} \\ +\bigskip +\begin{prooftree} + \hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k} + \infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env^{k}, \Ctx} \Rightarrow\ \tuple{x, \Env'}} + \infer1[(ItemTupC)]{\Sem{\( \left(t_{1}, \ldots, t_{k}\right)\texttt{:}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow \tuple{x, \Env'}} \end{prooftree} \\ \bigskip \begin{prooftree} \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'_{[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_{k}: x_{k}\right) = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow\ - \tuple{\Ctx, \Env''}} + \infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow\ \tuple{x, \Env''}} + \infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}} \end{prooftree} \\ \bigskip \begin{prooftree} - \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}} - \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env'} \Rightarrow \tuple{\Ctx, \Env''}} - \infer2[(ItemC)]{\Sem{\(\mbox{constraint~} C, \mathbf{I}\)}{\Prog, \Env} \Rightarrow - \tuple{\{v\}\cup\Ctx, \Env''}} + \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env'}} + \hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env', \{c\}\cup\Ctx} \Rightarrow \tuple{x, \Env''}} + \infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-let} Rewriting rules for partial evaluation of \microzinc\ let expressions to \nanozinc.} @@ -410,12 +412,7 @@ is the base case for a list of let items. \bigskip \begin{prooftree} \hypo{c \text{~constant}} - \infer1[(Const)]{\Sem{c}{\Prog, \Env} \Rightarrow \tuple{c, \Env}} -\end{prooftree} \\ -\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, \Env^{k}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}}} + \infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env}} \end{prooftree} \\ \bigskip \begin{prooftree}