Changeset 1447
 Timestamp:
 Oct 21, 2011, 6:30:02 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.24.3/reports/D42.tex
r1445 r1447 528 528 \begin{table} 529 529 \begin{threeparttable} 530 \begin{tabular}{l rllrl}531 Title & Lines & Description & O'Caml & Size& Ratio \\532 \hline 533 \texttt{joint/Joint.ma} & 173 & Abstracted syntax for backend languages& N/A & N/A & N/A \\534 \texttt{RTLabs/syntax.ma} & 73 & The syntax of RTLabs& \texttt{RTLabs/RTLabs.mli} & 113 & 0.65 \\535 \texttt{RTL/RTL.ma} & 222\tnote{a} & The syntax of RTL & \texttt{RTL/RTL.mli} & 120\tnote{a}& 1.85\tnote{a} \\536 \texttt{ERTL/ERTL.ma} & 198\tnote{a} & The syntax of ERTL& \texttt{ERTL/ERTL.mli} & 191 & 1.04\tnote{a} \\537 \texttt{LIN/joint\_LTL\_LIN.ma} & 10 & The syntax of the abstracted combined LTL and LIN language& N/A & N/A & N/A \\538 \texttt{LTL/LTL.ma} & 193\tnote{b} & The specialisation of the above file to the syntax of LTL& \texttt{LTL/LTL.mli} & 104 & 1.86\tnote{b} \\539 \texttt{LIN/LIN.ma} & 200\tnote{b} & The specialisation of the above file to the syntax of LIN& \texttt{LIN/LIN.mli} & 88 & 2.27\tnote{b} \\530 \begin{tabular}{llrlrl} 531 Description & Matita & Lines & O'Caml & Lines & Ratio \\ 532 \hline 533 Abstracted syntax for backend languages & \texttt{joint/Joint.ma} & 173 & N/A & N/A & N/A \\ 534 The syntax of RTLabs & \texttt{RTLabs/syntax.ma} & 73 & \texttt{RTLabs/RTLabs.mli} & 113 & 0.65 \\ 535 The syntax of RTL & \texttt{RTL/RTL.ma} & 49 & \texttt{RTL/RTL.mli} & 120 & 1.85\tnote{a} \\ 536 The syntax of ERTL & \texttt{ERTL/ERTL.ma} & 25 & \texttt{ERTL/ERTL.mli} & 191 & 1.04\tnote{a} \\ 537 The syntax of the abstracted combined LTL and LIN language & \texttt{LIN/joint\_LTL\_LIN.ma} & 10 & N/A & N/A & N/A \\ 538 The specialisation of the above file to the syntax of LTL & \texttt{LTL/LTL.ma} & 10 & \texttt{LTL/LTL.mli} & 104 & 1.86\tnote{b} \\ 539 The specialisation of the above file to the syntax of LIN & \texttt{LIN/LIN.ma} & 17 & \texttt{LIN/LIN.mli} & 88 & 2.27\tnote{b} \\ 540 540 \end{tabular} 541 541 \begin{tablenotes} 542 \item[a] Includes\texttt{joint/Joint.ma}.543 \item[b] Includes\texttt{joint/Joint\_LTL\_LIN.ma} and \texttt{joint/Joint.ma}.\\542 \item[a] After inlining of \texttt{joint/Joint.ma}. 543 \item[b] After inlining of \texttt{joint/Joint\_LTL\_LIN.ma} and \texttt{joint/Joint.ma}.\\ 544 544 \begin{tabular}{ll} 545 545 Total lines of Matita code for the above files:& 347 \\ … … 556 556 \begin{table} 557 557 \begin{threeparttable} 558 \begin{tabular}{l rlll}559 Title & Description & Lines & O'Caml& Ratio \\560 \hline 561 \texttt{joint/TranslateUtils.ma} & 59 & Generic translation utilities& N/A & N/A \\562 \texttt{RTLabs/RTLabsToRTL.ma} & 1251 & Translation from RTLabs to RTL & \texttt{RTLabs/RTLabsToRTL.ml}& 1.61 \\563 \texttt{RTL/RTLToERTL.ma} & 417 & Translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml}& 1.01\tnote{a} \\564 \texttt{RTL/RTLTailcall.ma} & 52 & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml}& 2.02 \\565 \texttt{ERTL/ERTLToLTL.ma} & 464 & Translation from ERTL to LTL & \texttt{ERTL/ERTLToLTL.ml}& 1.22\tnote{b} \\566 \texttt{ERTL/Interference.ma} & 26 & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\tnote{c} \\567 \texttt{ERTL/liveness.ma} & 298 & Liveness analysis & \texttt{ERTL/liveness.ml}& 0.92 \\568 \texttt{LTL/LTLToLIN.ma} & 92 & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml}& 0.53\tnote{c} \\569 \texttt{LIN/joint\_LTL\_LIN.ma} & 10 & Generic code for LTL and LIN languages& N/A & N/A \\570 \texttt{LIN/LINToASM.ma} & 335 & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml}& 2.85\tnote{d}558 \begin{tabular}{llrlrl} 559 Description & Matita & Lines & O'Caml & Lines & Ratio \\ 560 \hline 561 Generic translation utilities & \texttt{joint/TranslateUtils.ma} & 59 & N/A & N/A & N/A \\ 562 Translation from RTLabs to RTL & \texttt{RTLabs/RTLabsToRTL.ma} & 1251 & \texttt{RTLabs/RTLabsToRTL.ml} & 778 & 1.61 \\ 563 Translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ma} & 417 & \texttt{RTL/RTLToERTL.ml} & 472 & 1.01\tnote{a} \\ 564 Elimination of tailcalls & \texttt{RTL/RTLTailcall.ma} & 52 & \texttt{RTL/RTLtailcall.ml} & 25 & 2.02 \\ 565 Translation from ERTL to LTL & \texttt{ERTL/ERTLToLTL.ma} & 464 & \texttt{ERTL/ERTLToLTL.ml} & 429 & 1.22\tnote{b} \\ 566 Axiomatised graph colouring component & \texttt{ERTL/Interference.ma} & 26 & \texttt{common/interference.ml} & 861 & 0.03\tnote{a} \\ 567 Liveness analysis & \texttt{ERTL/liveness.ma} & 298 & \texttt{ERTL/liveness.ml} & 323 & 0.92 \\ 568 Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ma} & 92 & \texttt{LTL/LTLToLIN.ml} & 131 & 0.53\tnote{c} \\ 569 Generic code for LTL and LIN languages & \texttt{LIN/joint\_LTL\_LIN.ma} & 10 & N/A & N/A & N/A \\ 570 Translation from LIN to assembly & \texttt{LIN/LINToASM.ma} & 335 & \texttt{LIN/LINToASM.ml} & 142 & 2.85\tnote{d} 571 571 \end{tabular} 572 572 \begin{tablenotes} 573 \item[a] Includes\texttt{joint/TranslateUtils.ma}.574 \item[b] Includes\texttt{joint/TranslateUtils.ma} and \texttt{ERTL/ERTLToLTLI.ml}.575 \item[c] Includes\texttt{joint/TranslateUtils.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}.576 \item[d] Includes\texttt{joint/TranslateUtils.ma}, and \texttt{joint/joint\_LTL\_LIN.ma}.\\573 \item[a] After inlining of \texttt{joint/TranslateUtils.ma}. 574 \item[b] After inlining of \texttt{joint/TranslateUtils.ma} and \texttt{ERTL/ERTLToLTLI.ml}. 575 \item[c] After inlining of \texttt{joint/TranslateUtils.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}. 576 \item[d] After inlining of \texttt{joint/TranslateUtils.ma}, and \texttt{joint/joint\_LTL\_LIN.ma}.\\ 577 577 \begin{tabular}{ll} 578 578 Total lines of Matita code for the above files:& 3032. \\
Note: See TracChangeset
for help on using the changeset viewer.