aboutsummaryrefslogtreecommitdiffstats
path: root/papers/cfrontend_new/dynsem3.etex
diff options
context:
space:
mode:
Diffstat (limited to 'papers/cfrontend_new/dynsem3.etex')
-rw-r--r--papers/cfrontend_new/dynsem3.etex48
1 files changed, 0 insertions, 48 deletions
diff --git a/papers/cfrontend_new/dynsem3.etex b/papers/cfrontend_new/dynsem3.etex
deleted file mode 100644
index bddcef64..00000000
--- a/papers/cfrontend_new/dynsem3.etex
+++ /dev/null
@@ -1,48 +0,0 @@
-\begin{figure}
-Compatibility between values, outcomes and return types:
-
-$$\begin{array}{rclr}
-"Out_normal", "Tvoid" & \# & "Vundef"& \\
-"Out_normal", "Tvoid" & \# & "Vundef"& \\
-"Out_return", \, "Tvoid" & \# & "Vundef" & \\
-"Out_return" \some v, \, \tau & \# & v & \mbox{when}\,\tau~\not="Tvoid"
-\end{array}$$
-
-\numberrules
-
-Function calls:
-\begin{pannel}
-
-\irule
- G, E |- {a_{fun}}^{\tau}, M \evalexpr v_{fun}, \tr_1, M_1 &
- G, E |- a_{args}, M_1 \evalexpr v_{args}, \tr_2, M_2 \\
- G[v_{fun}] = \some{f} &
- "type_of_fundef" (f) = \tau \\
- G |- f(v_{args}), M_2 \evalfunc v_{res}, \tr_3, M_3
- --------------------------------------------------
- G, E |- {({a_{fun}}^{\tau} (a_{args}))}^{\tau'}, M \evalexpr v_{res}, \cat {\cat {\tr_1} \tr_2} \tr_3, M_3
-\end \label{rule:25}
-\end{pannel}
-
-Function invocations:
-\begin{pannel}
-
-\irule
- "alloc" ({\it \emptyset_E}, M, "params" (f) + "vars" (f),E) = (M_1, b) \\
- "bind_params" (E, M_1, "params" (f), v_{args}) = M_2 \\
- G, E |- "body" (f), M_2 \evalstmt \out, \tr, M_3 \\
- \out, \, "fn_return" (f) \, "#" \, v_{res}
- --------------------------------------------------
- G, E |- f(v_{args}), M \evalstmt v_{res}, \tr, "free" (M_3, b)
-\end \label{rule:26}
-
-\irule
- v_{args}, v_{res} \cong^{\sigma} e_{args}, e_{res}
- --------------------------------------------------
- G, E |- <\id \, \sigma>(v_{args}), M \evalstmt v_{res}, [\id \,e_{args}\, e_{res}], M
-\end \label{rule:27}
-
-\end{pannel}
-\caption{Dynamic semantics of function call}
-\label{fig:dynsem3}
-\end{figure}