# Changeset 1394

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

reconfiguring of tables, and recalculation of ratios

Location:
Deliverables/D4.2-4.3/reports
Files:
2 edited

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

 r1375 \usepackage[utf8x]{inputenc} \usepackage{listings} \usepackage{lscape} \usepackage{stmaryrd} \usepackage{threeparttable} \usepackage{url} \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 \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. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
• ## Deliverables/D4.2-4.3/reports/D4-3.tex

 r1391 In 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. Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure. As 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. However, 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. In particular, the semantics of both LTL and LIN are implemented in exactly the same way. The only difference between the two languages is how the next instruction to be interpreted is fetched. In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions. As 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. Furthermore, 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. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% Most functions in the intermediate language semantics fall into the IO monad. \end{enumerate} This monadic infrastructure is shared between the frontend and backend languages. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.