diff options
Diffstat (limited to 'papers/cfrontend_new/dynsem3.etex')
-rw-r--r-- | papers/cfrontend_new/dynsem3.etex | 48 |
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} |