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

Add rewriting rule for array access

Browse Source
This commit is contained in:
Jip J. Dekker 2021-04-08 14:20:46 +10:00
parent 9d2b6fd070
commit 2f5fbbacd9
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 25 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
chapters/4_rewriting.tex
View File

@ -82,6 +82,7 @@ and where expressions have \mzninline{par} type.
\alt "let" "{" <item>* "}" "in" <literal>
\alt "if" <exp> "then" <exp> "else" <exp> "endif"
\alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
\lat <ident>"[" <literal> "]"
<item> ::= <param> [ "=" <exp> ]";"
\alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")";
@ -303,19 +304,19 @@ 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{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env}} \Rightarrow \tuple{v, \Env'}
\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}
\hypo{\ptinline{F} \in \text{Builtins}}
\infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{ \mathit{eval}(\ptinline{F}(a_1,\ldots, a_k)), \Env}}
\infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{\ensuremath{\mathit{eval}(\ptinline{F}(a_1,\ldots, a_k))}, \Env}}
\end{prooftree} \\
\bigskip
\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}~\ptinline{F}(a_1, \ldots, a_k), \Env_k}}
\infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow{}
\tuple{\ensuremath{\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.}
@ -348,12 +349,12 @@ considered primitives, and as such simply need to be transferred into the
\bigskip
\begin{prooftree}
\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'}}
\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} \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'}}
\infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
@ -365,7 +366,7 @@ considered primitives, and as such simply need to be transferred into the
\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{\( \texttt{tuple(}t_{1}, \ldots, t_{k}\texttt{):}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow \tuple{x, \Env'}}
\infer1[(ItemTupC)]{\Sem{\( \texttt{tuple(}t_{1}, \ldots, t_{k}\texttt{):}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
@ -408,40 +409,47 @@ notation.
\hypo{x \in \langle \text{ident} \rangle}
\hypo{v}
\hypo{\phi \text{~otherwise}}
\infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{t: x^{\texttt{~└──~}} \phi\ \} \cup\ \Env} \Rightarrow \tuple{x, \{t: x^{\texttt{~└──~}} \phi \cup \phi}}
\infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{t: x^{\texttt{~└──~}} \phi\ \} \cup\ \Env} \Rightarrow{} \tuple{x, \{t: x^{\texttt{~└──~}} \phi{} \cup{} \Env}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(x\)}{\Prog, \Env} \Rightarrow \tuple{[x_{1}, \ldots, x_{n}], \Env'}}
\hypo{\Sem{\(i\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
\hypo{v \in [1 \ldots{} n]}
\infer3[(Access)]{\Sem{\(x\texttt{[}i\texttt{]}\)}{\Prog, \Env} \Rightarrow{} \tuple{x_{v}, \Env''}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{c \text{~constant}}
\infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env}}
\infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow{} \tuple{c, \Env}}
\end{prooftree} \\
\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}}
\infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_t\)}{\Prog, \Env}}
\end{prooftree} \\
\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}}
\infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_e\)}{\Prog, \Env}}
\end{prooftree} \\
\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'}}
\infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[v], \Env'}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}}
\infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[], \Env}}
\infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[], \Env}}
\end{prooftree} \\
\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_{[x \mapsto v]}} \Rightarrow \tuple{A_v, \Env_{[x \mapsto v]} \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}}
\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 }
\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}
\caption{\label{fig:4-rewrite-to-nzn-other} Rewriting rules for partial evaluation
of other \microzinc\ expressions to \nanozinc.}