Changeset 1399 for Deliverables/D4.2-4.3/reports/D4-3.tex

Timestamp:

Oct 18, 2011, 11:38:37 AM (9 years ago)

Author:

mulligan

Message:

more work on parameters

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (4 diffs)

Deliverables/D4.2-4.3/reports/D4-3.tex

@@ -20 +20 @@
 
 \lstdefinelanguage{matita-ocaml}
-  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
-   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
+  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,let,in,rec,match,return,with,Type,try},
+   morekeywords={[2]whd,normalize,elim,cases,destruct},
    morekeywords={[3]type,of},
    mathescape=true,
@@ -247 +247 @@
  }.
 \end{lstlisting}
-
+Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements).
+Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}.
+Note that \texttt{lookup} may fail, and returns an \texttt{option} type:
 \begin{lstlisting}
 record params (globals: list ident): Type[1] ≝
@@ -256 +258 @@
  }.
 \end{lstlisting}
-
-\begin{lstlisting}
-definition graph_params_: params__ $\rightarrow$ params_ :=
-  $\lambda$pars__. mk_params_ pars__ label.
-\end{lstlisting}
-
+We now have what we need to define internal functions for the joint language.
+The first two `universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics.
+The rest of the fields affect both compilation and semantics.
+In particular, we have parameterised result types, function parameter types and the type of local variables.
+Note also that we have lifted the hypothesised \texttt{lookup} function from \texttt{params} into a dependent sigma type, which combines a label (the entry and exit points of the control flow graph or list) combined with a proof that the label is in the graph structure:
 \begin{lstlisting}
 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
@@ -278 +279 @@
   joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
 }.
+\end{lstlisting}
+Naturally, a question arises as to why we have chosen to split up the parameterisation into so many intermediate records, each slightly extending earlier ones.
+The reason is because some intermediate languages share a host of parameters, and only differ on some others.
+For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific:
+\begin{lstlisting}
+...
+definition ertl_params__: params__ :=
+ mk_params__ register register register register (move_registers × move_registers)
+  register nat unit ertl_statement_extension.
+...
+definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0.
+definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
+...
+definition ertl_statement := joint_statement ertl_params_.
+
+definition ertl_internal_function :=
+  $\lambda$globals.joint_internal_function … (ertl_params globals).
+\end{lstlisting}
+Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages:
+\begin{lstlisting}
+definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register).
 \end{lstlisting}