Changeset 1364 for Deliverables/D4.2-4.3

Timestamp:

Oct 13, 2011, 11:11:03 AM (9 years ago)

Author:

mulligan

Message:

finished the report on d4.2. starting d4.3 report

File:

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

Deliverables/D4.2-4.3/reports/D4-2.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,in,rec,match,return,with,Type,try},
+   morekeywords={[2]whd,normalize,elim,cases,destruct},
    morekeywords={[3]type,of},
    mathescape=true,
@@ -289 +289 @@
   $\lambda$dest_lbl: label.
   $\lambda$def: rtl_internal_function globals.
-  $\lambda$prf: |destrs| = |srcrs|. (* assert in caml code *)
+  $\lambda$prf: |destrs| = |srcrs|. (* assert here *)
     ...
 \end{lstlisting}
@@ -424 +424 @@
 % SECTION.                                                                    %
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
-\subsection{Listing of important functions}
-\label{subsect.listing.important.functions}
+\subsection{Listing of important functions and axioms}
+\label{subsect.listing.important.functions.and.axioms}
+
+We list some important functions in the backend compilation:
+
+\paragraph{From RTL/RTLabsToRTL.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{translate\_stmt} & Translation of an RTLabs statement to an RTL statement \\
+\texttt{translate\_internal} & Translation of an RTLabs internal function to an RTL internal function \\
+\texttt{rtlabs\_to\_rtl} & Translation of an RTLabs program to an RTL program
+\end{tabular*}
+\end{center}
+
+\paragraph{From joint/TranslateUtils.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{fresh\_regs} & Generic fresh pseudoregister generation, for any intermediate language \\
+\texttt{adds\_graph} & Generic means of adding a statement to a graph, for any intermediate language
+\end{tabular*}
+\end{center}
+
+\paragraph{From RTL/RTLTailcall.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{simplify\_statement} & Remove a single tailcall \\
+\texttt{simplify\_graph} & Remove all tailcalls in the function graph \\
+\texttt{tailcall\_simplify} & Simplify an RTL program by removing tailcalls
+\end{tabular*}
+\end{center}
+
+\paragraph{From RTL/RTLToERTL.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{translate\_stmt} & Translation of an RTL statement to an ERTL statement \\
+\texttt{translate\_funct\_internal} & Translation of an RTL internal function to an ERTL internal function \\
+\texttt{translate} & Translation of an RTL program to an ERTL program
+\end{tabular*}
+\end{center}
+
+\paragraph{From ERTL/liveness.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{analyse} & Dead code analysis
+\end{tabular*}
+\end{center}
+
+\paragraph{From ERTL/Interference.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{build} & The (axiomatised) graph colouring for register and stack slot allocation
+\end{tabular*}
+\end{center}
+
+\paragraph{From ERTL/ERTLToLTL.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{translate\_statement} & Translation of an ERTL statement into multiple LTL statements \\
+\texttt{translate\_internal} & Translation of an ERTL internal function into an LTL internal function \\
+\texttt{ertl\_to\_ltl} & Translation of an ERTL program into an LTL program
+\end{tabular*}
+\end{center}
+
+\paragraph{From LTL/LTLToLIN.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{visit} & Visits, in order, every node in the statement graph for linearisation \\
+\texttt{translate\_stmt} & Translation of an LTL statement to a LIN statement \\
+\texttt{branch\_compress} & Place holder (currently identity) function for branch compression \\
+\texttt{translate\_internal} & Translation of an LTL internal function into a LIN internal function \\
+\texttt{ltl\_to\_lin} & Translation of an LTL program to a LIN program
+\end{tabular*}
+\end{center}
+
+\paragraph{From LIN/LINToASM.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{translate\_statements} & Translation of a LIN statement to mutliple assembly instructions \\
+\texttt{translate\_fun\_def} & Translation of a LIN internal function definition into assembly \\
+\texttt{translate} & Translation of a LIN program into assembly
+\end{tabular*}
+\end{center}
 
 \end{document}