Changeset 1394


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

reconfiguring of tables, and recalculation of ratios

Location:
Deliverables/D4.2-4.3/reports
Files:
2 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%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1391 r1394  
    149149In particular, we have merged many of the syntaxes of the intermediate languages (i.e. RTL, ERTL, LTL and LIN) into a single `joint' syntax, which is parameterised by various types.
    150150Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure.
     151
     152As mentioned in the report for Deliverable D4.2, there are a number of advantages that this process of abstraction brings, from code reuse to allowing us to get a clearer view of the intermediate languages and their structure.
     153However, the semantics of the intermediate languages allow us to concretely demonstrate this improvement in clarity, by noting that the semantics of the LTL and the semantics of the LIN languages are identical.
     154In particular, the semantics of both LTL and LIN are implemented in exactly the same way.
     155The only difference between the two languages is how the next instruction to be interpreted is fetched.
     156In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions.
     157
     158As a result, we see that the semantics of LIN and LTL are both instances of a single, more general language that is parametric in how the next instruction is fetched.
     159Furthermore, any prospective proof that the semantics of LTL and LIN are identical is not almost trivial, saving a deal of work in Deliverable D4.4.
    151160
    152161%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     
    195204Most functions in the intermediate language semantics fall into the IO monad.
    196205\end{enumerate}
     206This monadic infrastructure is shared between the frontend and backend languages.
    197207
    198208%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.