Ignore:
Timestamp:
Oct 17, 2011, 4:50:44 PM (9 years ago)
Author:
mulligan
Message:

reconfiguring of tables, and recalculation of ratios

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1375 r1394  
    1010\usepackage[utf8x]{inputenc}
    1111\usepackage{listings}
     12\usepackage{lscape}
    1213\usepackage{stmaryrd}
     14\usepackage{threeparttable}
    1315\usepackage{url}
    1416
     
    466468\label{subsect.listing.files}
    467469
    468 Translation specific files (files relating to language semantics have been omitted).
    469 Syntax:
    470 \begin{center}
    471 \begin{tabular*}{\textwidth}{p{3.5cm}p{5.5cm}p{3.5cm}p{1cm}}
     470Translation specific files (files relating to language semantics have been omitted) are presented in Table~\ref{table.syntax}.
     471
     472\begin{table}
     473\begin{threeparttable}
     474\begin{tabular}{llll}%{\textwidth}{p{3.5cm}p{5.5cm}p{3.5cm}p{1cm}}
    472475Title & Description & O'Caml & Ratio \\
    473476\hline
     
    476479\texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 0.41 \\
    477480\texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 0.13 \\
    478 \texttt{LTL/LTL.ma} & The syntax of LTL & \texttt{LTL/LTL.mli} & 0.13 \\
    479 \texttt{LIN/LIN.ma} & The syntax of LIN & \texttt{LIN/LIN.mli} & 0.36
    480 \end{tabular*}
    481 \end{center}
     481\texttt{LTL/LTL.ma} & The syntax of LTL & \texttt{LTL/LTL.mli} & 0.19\tnote{a} \\
     482\texttt{LIN/LIN.ma} & The syntax of LIN & \texttt{LIN/LIN.mli} & 0.31\tnote{a}
     483\end{tabular}
     484\begin{tablenotes}
     485  \item[a] Includes \texttt{joint/Joint\_LTL\_LIN.ma}.
     486\end{tablenotes}
     487\end{threeparttable}
     488\caption{Syntax files}
     489\label{table.syntax}
     490\end{table}
    482491Here, the O'Caml column denotes the O'Caml source file in the prototype compiler's implementation that corresponds to the Matita script in question.
    483492The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file.
    484493These are computed with \texttt{wc -l}, a standard Unix tool.
    485 
    486 \noindent
    487 Translations and utilities:
    488 \begin{center}
    489 \begin{tabular*}{\textwidth}{p{4.5cm}p{4.5cm}p{4.5cm}p{1cm}}
     494Translations and utilities are presented in Table~\ref{table.translation.utilities}.
     495\begin{landscape}
     496\begin{table}
     497\begin{threeparttable}
     498\begin{tabular}{llll}
    490499Title & Description & O'Caml & Ratio \\
    491500\hline
    492501\texttt{RTLabs/RTLabsToRTL.ma} & The translation from RTLabs to RTL & \texttt{RTLabs/RTLabsToRTL.ml} & 1.61 \\
    493502\texttt{joint/TranslateUtils.ma} & Generic translation utilities & N/A & N/A \\
     503\texttt{joint/Joint\_LTL\_LIN.ma} & Generic code for LTL and LIN languages & N/A & N/A \\
    494504\texttt{RTL/RTLToERTL.ma} & The translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml} & 0.88 \\
    495505\texttt{RTL/RTLtailcall.ma} & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml} & 2.08 \\
    496 \texttt{ERTL/ERTLToLTL.ma} & The translation from ERTL to LTL & \texttt{ERTL/ERTLToRTL.ml} & 3.46 \\
    497 \texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\footnote{The majority of this file is axiomatised.} \\
     506\texttt{ERTL/ERTLToLTL.ma} & The translation from ERTL to LTL & \texttt{ERTL/ERTLToRTL.ml} & 1.1\tnote{a} \\
     507\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\tnote{b} \\
    498508\texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 0.92 \\
    499 \texttt{LTL/LTLToLIN.ma} & The translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 0.75 \\
    500 \texttt{LIN/LINToASM.ma} & The translation from LIN to assembly language & \texttt{LIN/LINToASM.ml} 2.45 &
    501 \end{tabular*}
    502 \end{center}
     509\texttt{LTL/LTLToLIN.ma} & The translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 2.43\tnote{c} \\
     510\texttt{LIN/LINToASM.ma} & The translation from LIN to assembly language & \texttt{LIN/LINToASM.ml} & 0.41\tnote{c}
     511\end{tabular}
     512\begin{tablenotes}
     513  \item[a] This figure includes the line count of \texttt{ERTLToLTLI.ml} and \texttt{ERTLToLTL.ml}.
     514  \item[b] The majority of this file is axiomatised.
     515  \item[c] This figure includes the line count of \texttt{joint/Joint\_LTL\_LIN.ma}.
     516\end{tablenotes}
     517\end{threeparttable}
     518\caption{Translation files.}
     519\label{table.translation.utilities}
     520\end{table}
     521\end{landscape}
    503522Given 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.
     523Some of these ratio, however, need explanation.
     524In particular, the RTLabs to RTL translation stands out.
     525Note that RTLabs is not subject to our abstraction process, and the language's syntax is fully explicated.
     526Further, the RTLabs to RTL translation is quite involved, including instruction selection.
     527
     528Other, longer translations include the file \texttt{ERTLtoLTL.ma}.
     529This is actually the concatenation of the files \texttt{ERTLtoLTLI.ml} and \texttt{ERTLtoLTL.ml} in the O'Caml source, hence its length.
     530
     531Further, many translations are actually significantly shorter than their O'Caml counterparts due to axiomatisation, and the lack of structure and functor declarations in Matita.
     532
     533We note that the O'Caml codebase consists of 26989 lines of O'Caml code (including comments).
     534The Matita codebase consists of 41959 lines of Matita code (including comments).
     535This 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.
    504536
    505537%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.