Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Update the rewrite rules with correct projection rules

Browse Source
This commit is contained in:
Jip J. Dekker 2021-04-07 15:50:06 +10:00
parent e5e8b9d7ec
commit 548a482b6e
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 27 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
chapters/4_rewriting.tex
View File

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