Changeset 1439


Ignore:
Timestamp:
Oct 21, 2011, 5:47:33 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1438 r1439  
    488488\end{itemize}
    489489
    490 \newpage
    491 
    492490%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    493491% SECTION.                                                                    %
     
    503501
    504502Translation specific files (files relating to language semantics have been omitted) are presented in Table~\ref{table.syntax}.
     503Here, the O'Caml column denotes the O'Caml source file in the prototype compiler's implementation that corresponds to the Matita script in question.
     504The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file(s).
     505These are computed with \texttt{wc -l}, a standard Unix tool.
     506
     507Individual 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.
     508The 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.
     509
     510Translations and utilities are presented in Table~\ref{table.translation.utilities}.
     511
     512Given 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.
     513Some of these ratio, however, need explanation.
     514In particular, the RTLabs to RTL translation stands out.
     515Note that RTLabs is not subject to our abstraction process, and the language's syntax is fully explicated.
     516Further, the RTLabs to RTL translation is quite involved, including instruction selection.
     517
     518Other, longer translations include the file \texttt{ERTLtoLTL.ma}.
     519This is actually the concatenation of the files \texttt{ERTLtoLTLI.ml} and \texttt{ERTLtoLTL.ml} in the O'Caml source, hence its length.
     520
     521Further, many translations are actually significantly shorter than their O'Caml counterparts due to axiomatisation, and the lack of structure and functor declarations in Matita.
     522
     523We note that the O'Caml backend codebase consists of 6770 lines of O'Caml code (including comments).
     524The Matita codebase consists of 6447 lines of Matita code (including comments).
     525This is a ratio of 0.95.
     526
    505527\begin{landscape}
    506528\begin{table}
     
    511533\texttt{joint/Joint.ma} & Abstracted syntax for backend languages & N/A & N/A \\
    512534\texttt{RTLabs/syntax.ma} & The syntax of RTLabs & \texttt{RTLabs/RTLabs.mli} & 0.65 \\
    513 \texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 1.85\tnote{b} \\
    514 \texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 1.04\tnote{b} \\
    515 \texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL & \texttt{LTL/LTL.mli} & 1.86\tnote{a} \\
     535\texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 1.85\tnote{a} \\
     536\texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 1.04\tnote{a} \\
    516537\texttt{LIN/joint\_LTL\_LIN.ma} & The syntax of the abstracted combined LTL and LIN language & N/A & N/A \\
    517 \texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN & \texttt{LIN/LIN.mli} & 2.27\tnote{a} \\
     538\texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL & \texttt{LTL/LTL.mli} & 1.86\tnote{b} \\
     539\texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN & \texttt{LIN/LIN.mli} & 2.27\tnote{b} \\
    518540\end{tabular}
    519541\begin{tablenotes}
    520   \item[a] Includes \texttt{joint/Joint\_LTL\_LIN.ma} and \texttt{joint/Joint.ma}.
    521   \item[b] Includes \texttt{joint/Joint.ma}.\\
    522   Total lines of Matita code for the above files: 347. \\
    523   Total lines of O'Caml code for the above files: 616. \\
    524   Ration of total lines: 0.56.
     542  \item[a] Includes \texttt{joint/Joint.ma}.
     543  \item[b] Includes \texttt{joint/Joint\_LTL\_LIN.ma} and \texttt{joint/Joint.ma}.\\
     544  \begin{tabular}{ll}
     545  Total lines of Matita code for the above files:& 347 \\
     546  Total lines of O'Caml code for the above files:& 616 \\
     547  Ration of total lines:& 0.56
     548  \end{tabular}
    525549\end{tablenotes}
    526550\end{threeparttable}
     
    529553\end{table}
    530554\end{landscape}
    531 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.
    532 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file(s).
    533 These are computed with \texttt{wc -l}, a standard Unix tool.
    534 
    535 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.
    536 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.
    537 
    538 Translations and utilities are presented in Table~\ref{table.translation.utilities}.
    539555\begin{landscape}
    540556\begin{table}
     
    550566\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.23\tnote{c} \\
    551567\texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 1.46\tnote{c} \\
    552 \texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10 \tnote{d} \\
     568\texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10\tnote{d} \\
    553569\texttt{LIN/joint\_LTL\_LIN.ma} & Generic code for LTL and LIN languages & N/A & N/A \\
    554570\texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 4.06\tnote{e}
     
    556572\begin{tablenotes}
    557573  \item[a] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma} and \texttt{joint/TranslateUtil.ma}.
    558   \item[b] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and \texttt{ERTL/ERTLToLTLI.ml}.
     574  \item[b] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{ERTL/ERTLToLTLI.ml}.
    559575  \item[c] Includes \texttt{joint/Joint.ma}.
    560576  \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}.
    561   \item[e] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and \texttt{joint/joint\_LTL\_LIN.ma}.\\
    562   Total lines of Matita code for the above files: 3032. \\
    563   Total lines of O'Caml code for the above files: 3332. \\
    564   Ration of total lines: 0.91.
     577  \item[e] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{joint/joint\_LTL\_LIN.ma}.\\
     578  \begin{tabular}{ll}
     579  Total lines of Matita code for the above files:& 3032. \\
     580  Total lines of O'Caml code for the above files:& 3332. \\
     581  Ration of total lines:& 0.91.
     582  \end{tabular}
    565583\end{tablenotes}
    566584\end{threeparttable}
     
    569587\end{table}
    570588\end{landscape}
    571 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.
    572 Some of these ratio, however, need explanation.
    573 In particular, the RTLabs to RTL translation stands out.
    574 Note that RTLabs is not subject to our abstraction process, and the language's syntax is fully explicated.
    575 Further, the RTLabs to RTL translation is quite involved, including instruction selection.
    576 
    577 Other, longer translations include the file \texttt{ERTLtoLTL.ma}.
    578 This is actually the concatenation of the files \texttt{ERTLtoLTLI.ml} and \texttt{ERTLtoLTL.ml} in the O'Caml source, hence its length.
    579 
    580 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.
    581 
    582 We note that the O'Caml backend codebase consists of 6770 lines of O'Caml code (including comments).
    583 The Matita codebase consists of 6447 lines of Matita code (including comments).
    584 This is a ratio of 0.95.
    585589
    586590%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.