Changeset 1398 for Deliverables/D4.2-4.3

Timestamp:

Oct 17, 2011, 8:20:05 PM (9 years ago)

Author:

mulligan

Message:

more work on parameters

File:

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

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

@@ -97 +97 @@
 \vspace*{7cm}
 \paragraph{Abstract}
+We describe the encoding in the Calculus of Constructions of the semantics of the CerCo compiler's backend intermediate languages.
+The CerCo backend consists of five distinct languages: RTL, RTLntl, ERTL, LTL and LIN.
+We describe a process of heavy abstraction of the intermediate languages and their semantics.
+We hope that this process will ease the burden of Deliverable D4.4, the proof of correctness for the compiler.
 
 \newpage
@@ -183 +187 @@
 }.
 \end{lstlisting}
+We summarise what these types mean:
+\begin{center}
+\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
+Type & Explanation \\
+\hline
+\texttt{acc\_a\_reg} & The type of the accumulator A register.  In some languages this is implemented as the hardware accumulator, whereas in others this is a pseudoregister.\\
+\texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\
+\texttt{dpl\_reg} & \\
+\texttt{dph\_reg} & \\
+\texttt{pair\_reg} & \\
+\texttt{generic\_reg} & \\
+\texttt{call\_args} & \\
+\texttt{call\_dest} & \\
+\texttt{extend\_statements} &
+\end{tabular*}
+\end{center}
 
 As mentioned in the report for Deliverable D4.2, the record \texttt{params\_\_} is enough to be able to specify the instructions of the joint languages:
@@ -192 +212 @@
 \end{lstlisting}
 
-We extend \texttt{params\_\_} with a type corresponding 
+We extend \texttt{params\_\_} with a type corresponding to labels, \texttt{succ}, obtaining a new record type of parameters called \texttt{params\_}:
 \begin{lstlisting}
 record params_: Type[1] ≝
@@ -200 +220 @@
 }.
 \end{lstlisting}
-
+The type \texttt{succ} corresponds to labels, in the case of control flow graph based languages, or is instantiated to the unit type for the linearised language, LIN.
+Using \texttt{param\_} we can define statements of the joint language:
 \begin{lstlisting}
 inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
@@ -207 +228 @@
   | RETURN: joint_statement p globals.
 \end{lstlisting}
-
+Note that in the joint language, instructions are `linear', in that they have an immediate successor.
+Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program.
+
+For the semantics, we need further parametererised types.
+In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}:
 \begin{lstlisting}
 record params0: Type[1] ≝
@@ -215 +240 @@
  }.
 \end{lstlisting}
-
+We further extend \texttt{params0} with a type for local variables in internal function calls:
 \begin{lstlisting}
 record params1 : Type[1] ≝