# Changeset 1420 for Deliverables/D4.2-4.3/reports/D4-2.tex

Ignore:
Timestamp:
Oct 19, 2011, 5:50:10 PM (8 years ago)
Message:

more changes

File:
1 edited

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

 r1418 Title & Description & O'Caml & Ratio \\ \hline \texttt{RTLabs/RTLabsToRTL.ma} & The translation from RTLabs to RTL & \texttt{RTLabs/RTLabsToRTL.ml} & 1.61 \\ \texttt{RTLabs/RTLabsToRTL.ma} & 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} & 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} & 2.43\tnote{c} \\ \texttt{LIN/LINToASM.ma} & The translation from LIN to assembly language & \texttt{LIN/LINToASM.ml} & 0.41\tnote{c} \texttt{RTL/RTLToERTL.ma} & Translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml} & 1.38\tnote{a}\tnote{b}\tnote{c} \\ \texttt{RTL/RTLtailcall.ma} & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml} & 2.01 \\ \texttt{ERTL/ERTLToLTL.ma} & Translation from ERTL to LTL & \texttt{ERTL/ERTLToLTL.ml} & 1.39\tnote{a}\tnote{b}\tnote{c}\tnote{d} \\ \texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.23\tnote{b} \\ \texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 1.46\tnote{b} \\ \texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10 \tnote{a}\tnote{b}\tnote{c}\tnote{e}\tnote{f} \\ \texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 4.06\tnote{a}\tnote{b}\tnote{c}\tnote{f} \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}. \item[a] Includes \texttt{joint/TranslateUtils.ma}. \item[b] Includes \texttt{joint/Joint.ma}. \item[c] Includes \texttt{joint/TranslateUtil.ma}. \item[d] Includes \texttt{ERTL/ERTLToLTLI.ml}. \item[e] Includes \texttt{LTL/LTLToLINI.ml}. \item[f] Includes \texttt{joint/joint\_LTL\_LIN.ma}. \end{tablenotes} \end{threeparttable} 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. 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. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.