Changeset 1439 for Deliverables/D4.2-4.3

Timestamp:

Oct 21, 2011, 5:47:33 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

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

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

@@ -488 +488 @@
 \end{itemize}
 
-\newpage
-
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
 % SECTION.                                                                    %
@@ -503 +501 @@
 
 Translation specific files (files relating to language semantics have been omitted) are presented in Table~\ref{table.syntax}.
+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(s).
+These are computed with \texttt{wc -l}, a standard Unix tool.
+
+Individual file's ratios are an over approximation, due to the fact that it's hard to relate an individual O'Caml file to the abstracted Matita code that has been spread across multiple files.
+The ratio between total Matita code lines and total O'Caml code lines is more reflective of the compressed and abstracted state of the Matita translation.
+
+Translations and utilities are presented in Table~\ref{table.translation.utilities}.
+
+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 backend codebase consists of 6770 lines of O'Caml code (including comments).
+The Matita codebase consists of 6447 lines of Matita code (including comments).
+This is a ratio of 0.95.
+
 \begin{landscape}
 \begin{table}
@@ -511 +533 @@
 \texttt{joint/Joint.ma} & Abstracted syntax for backend languages & N/A & N/A \\
 \texttt{RTLabs/syntax.ma} & The syntax of RTLabs & \texttt{RTLabs/RTLabs.mli} & 0.65 \\
-\texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 1.85\tnote{b} \\
-\texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 1.04\tnote{b} \\
-\texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL & \texttt{LTL/LTL.mli} & 1.86\tnote{a} \\
+\texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 1.85\tnote{a} \\
+\texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 1.04\tnote{a} \\
 \texttt{LIN/joint\_LTL\_LIN.ma} & The syntax of the abstracted combined LTL and LIN language & N/A & N/A \\
-\texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN & \texttt{LIN/LIN.mli} & 2.27\tnote{a} \\
+\texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL & \texttt{LTL/LTL.mli} & 1.86\tnote{b} \\
+\texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN & \texttt{LIN/LIN.mli} & 2.27\tnote{b} \\
 \end{tabular}
 \begin{tablenotes}
-  \item[a] Includes \texttt{joint/Joint\_LTL\_LIN.ma} and \texttt{joint/Joint.ma}.
-  \item[b] Includes \texttt{joint/Joint.ma}.\\
-  Total lines of Matita code for the above files: 347. \\
-  Total lines of O'Caml code for the above files: 616. \\
-  Ration of total lines: 0.56.
+  \item[a] Includes \texttt{joint/Joint.ma}.
+  \item[b] Includes \texttt{joint/Joint\_LTL\_LIN.ma} and \texttt{joint/Joint.ma}.\\
+  \begin{tabular}{ll}
+  Total lines of Matita code for the above files:& 347 \\
+  Total lines of O'Caml code for the above files:& 616 \\
+  Ration of total lines:& 0.56
+  \end{tabular}
 \end{tablenotes}
 \end{threeparttable}
@@ -529 +553 @@
 \end{table}
 \end{landscape}
-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(s).
-These are computed with \texttt{wc -l}, a standard Unix tool.
-
-Individual file's ratios are an over approximation, due to the fact that it's hard to relate an individual O'Caml file to the abstracted Matita code that has been spread across multiple files.
-The ratio between total Matita code lines and total O'Caml code lines is more reflective of the compressed and abstracted state of the Matita translation.
-
-Translations and utilities are presented in Table~\ref{table.translation.utilities}.
 \begin{landscape}
 \begin{table}
@@ -550 +566 @@
 \texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.23\tnote{c} \\
 \texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 1.46\tnote{c} \\
-\texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10 \tnote{d} \\
+\texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10\tnote{d} \\
 \texttt{LIN/joint\_LTL\_LIN.ma} & Generic code for LTL and LIN languages & N/A & N/A \\
 \texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 4.06\tnote{e}
@@ -556 +572 @@
 \begin{tablenotes}
   \item[a] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma} and \texttt{joint/TranslateUtil.ma}.
-  \item[b] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and \texttt{ERTL/ERTLToLTLI.ml}.
+  \item[b] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{ERTL/ERTLToLTLI.ml}.
   \item[c] Includes \texttt{joint/Joint.ma}.
   \item[d] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}.
-  \item[e] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and \texttt{joint/joint\_LTL\_LIN.ma}.\\
-  Total lines of Matita code for the above files: 3032. \\
-  Total lines of O'Caml code for the above files: 3332. \\
-  Ration of total lines: 0.91.
+  \item[e] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{joint/joint\_LTL\_LIN.ma}.\\
+  \begin{tabular}{ll}
+  Total lines of Matita code for the above files:& 3032. \\
+  Total lines of O'Caml code for the above files:& 3332. \\
+  Ration of total lines:& 0.91.
+  \end{tabular}
 \end{tablenotes}
 \end{threeparttable}
@@ -569 +587 @@
 \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 backend codebase consists of 6770 lines of O'Caml code (including comments).
-The Matita codebase consists of 6447 lines of Matita code (including comments).
-This is a ratio of 0.95.
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%