Changeset 1394 for Deliverables/D4.2-4.3/reports/D4-2.tex

Timestamp:

Oct 17, 2011, 4:50:44 PM (9 years ago)

Author:

mulligan

Message:

reconfiguring of tables, and recalculation of ratios

File:

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

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

@@ -10 +10 @@
 \usepackage[utf8x]{inputenc}
 \usepackage{listings}
+\usepackage{lscape}
 \usepackage{stmaryrd}
+\usepackage{threeparttable}
 \usepackage{url}
 
@@ -466 +468 @@
 \label{subsect.listing.files}
 
-Translation specific files (files relating to language semantics have been omitted).
-Syntax:
-\begin{center}
-\begin{tabular*}{\textwidth}{p{3.5cm}p{5.5cm}p{3.5cm}p{1cm}}
+Translation specific files (files relating to language semantics have been omitted) are presented in Table~\ref{table.syntax}.
+
+\begin{table}
+\begin{threeparttable}
+\begin{tabular}{llll}%{\textwidth}{p{3.5cm}p{5.5cm}p{3.5cm}p{1cm}}
 Title & Description & O'Caml & Ratio \\
 \hline
@@ -476 +479 @@
 \texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 0.41 \\
 \texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 0.13 \\
-\texttt{LTL/LTL.ma} & The syntax of LTL & \texttt{LTL/LTL.mli} & 0.13 \\
-\texttt{LIN/LIN.ma} & The syntax of LIN & \texttt{LIN/LIN.mli} & 0.36
-\end{tabular*}
-\end{center}
+\texttt{LTL/LTL.ma} & The syntax of LTL & \texttt{LTL/LTL.mli} & 0.19\tnote{a} \\
+\texttt{LIN/LIN.ma} & The syntax of LIN & \texttt{LIN/LIN.mli} & 0.31\tnote{a}
+\end{tabular}
+\begin{tablenotes}
+  \item[a] Includes \texttt{joint/Joint\_LTL\_LIN.ma}.
+\end{tablenotes}
+\end{threeparttable}
+\caption{Syntax files}
+\label{table.syntax}
+\end{table}
 Here, the O'Caml column denotes the O'Caml source file in the prototype compiler's implementation that corresponds to the Matita script in question.
 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file.
 These are computed with \texttt{wc -l}, a standard Unix tool.
-
-\noindent
-Translations and utilities:
-\begin{center}
-\begin{tabular*}{\textwidth}{p{4.5cm}p{4.5cm}p{4.5cm}p{1cm}}
+Translations and utilities are presented in Table~\ref{table.translation.utilities}.
+\begin{landscape}
+\begin{table}
+\begin{threeparttable}
+\begin{tabular}{llll}
 Title & Description & O'Caml & Ratio \\
 \hline
 \texttt{RTLabs/RTLabsToRTL.ma} & The translation from RTLabs to RTL & \texttt{RTLabs/RTLabsToRTL.ml} & 1.61 \\
 \texttt{joint/TranslateUtils.ma} & Generic translation utilities & N/A & N/A \\
+\texttt{joint/Joint\_LTL\_LIN.ma} & Generic code for LTL and LIN languages & N/A & N/A \\
 \texttt{RTL/RTLToERTL.ma} & The translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml} & 0.88 \\
 \texttt{RTL/RTLtailcall.ma} & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml} & 2.08 \\
-\texttt{ERTL/ERTLToLTL.ma} & The translation from ERTL to LTL & \texttt{ERTL/ERTLToRTL.ml} & 3.46 \\
-\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\footnote{The majority of this file is axiomatised.} \\
+\texttt{ERTL/ERTLToLTL.ma} & The translation from ERTL to LTL & \texttt{ERTL/ERTLToRTL.ml} & 1.1\tnote{a} \\
+\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\tnote{b} \\
 \texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 0.92 \\
-\texttt{LTL/LTLToLIN.ma} & The translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 0.75 \\
-\texttt{LIN/LINToASM.ma} & The translation from LIN to assembly language & \texttt{LIN/LINToASM.ml} 2.45 &
-\end{tabular*}
-\end{center}
+\texttt{LTL/LTLToLIN.ma} & The translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 2.43\tnote{c} \\
+\texttt{LIN/LINToASM.ma} & The translation from LIN to assembly language & \texttt{LIN/LINToASM.ml} & 0.41\tnote{c}
+\end{tabular}
+\begin{tablenotes}
+  \item[a] This figure includes the line count of \texttt{ERTLToLTLI.ml} and \texttt{ERTLToLTL.ml}.
+  \item[b] The majority of this file is axiomatised.
+  \item[c] This figure includes the line count of \texttt{joint/Joint\_LTL\_LIN.ma}.
+\end{tablenotes}
+\end{threeparttable}
+\caption{Translation files.}
+\label{table.translation.utilities}
+\end{table}
+\end{landscape}
 Given that Matita code is much more verbose than O'Caml code, with explicit typing and inline proofs, we have achieved respectable line count ratios in the translation.
+Some of these ratio, however, need explanation.
+In particular, the RTLabs to RTL translation stands out.
+Note that RTLabs is not subject to our abstraction process, and the language's syntax is fully explicated.
+Further, the RTLabs to RTL translation is quite involved, including instruction selection.
+
+Other, longer translations include the file \texttt{ERTLtoLTL.ma}.
+This is actually the concatenation of the files \texttt{ERTLtoLTLI.ml} and \texttt{ERTLtoLTL.ml} in the O'Caml source, hence its length.
+
+Further, many translations are actually significantly shorter than their O'Caml counterparts due to axiomatisation, and the lack of structure and functor declarations in Matita.
+
+We note that the O'Caml codebase consists of 26989 lines of O'Caml code (including comments).
+The Matita codebase consists of 41959 lines of Matita code (including comments).
+This is a ratio of 1.55 --- not bad considering the Matita code also includes implementations of data structures that are present in the O'Caml standard library, and some proofs.
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%