Changeset 1439 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 21, 2011, 5:47:33 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1438 r1439 488 488 \end{itemize} 489 489 490 \newpage491 492 490 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 493 491 % SECTION. % … … 503 501 504 502 Translation specific files (files relating to language semantics have been omitted) are presented in Table~\ref{table.syntax}. 503 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. 504 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file(s). 505 These are computed with \texttt{wc -l}, a standard Unix tool. 506 507 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. 508 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. 509 510 Translations and utilities are presented in Table~\ref{table.translation.utilities}. 511 512 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. 513 Some of these ratio, however, need explanation. 514 In particular, the RTLabs to RTL translation stands out. 515 Note that RTLabs is not subject to our abstraction process, and the language's syntax is fully explicated. 516 Further, the RTLabs to RTL translation is quite involved, including instruction selection. 517 518 Other, longer translations include the file \texttt{ERTLtoLTL.ma}. 519 This is actually the concatenation of the files \texttt{ERTLtoLTLI.ml} and \texttt{ERTLtoLTL.ml} in the O'Caml source, hence its length. 520 521 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. 522 523 We note that the O'Caml backend codebase consists of 6770 lines of O'Caml code (including comments). 524 The Matita codebase consists of 6447 lines of Matita code (including comments). 525 This is a ratio of 0.95. 526 505 527 \begin{landscape} 506 528 \begin{table} … … 511 533 \texttt{joint/Joint.ma} & Abstracted syntax for backend languages & N/A & N/A \\ 512 534 \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} \\ 516 537 \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} \\ 518 540 \end{tabular} 519 541 \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} 525 549 \end{tablenotes} 526 550 \end{threeparttable} … … 529 553 \end{table} 530 554 \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}.539 555 \begin{landscape} 540 556 \begin{table} … … 550 566 \texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.23\tnote{c} \\ 551 567 \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 568 \texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10\tnote{d} \\ 553 569 \texttt{LIN/joint\_LTL\_LIN.ma} & Generic code for LTL and LIN languages & N/A & N/A \\ 554 570 \texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 4.06\tnote{e} … … 556 572 \begin{tablenotes} 557 573 \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}. 559 575 \item[c] Includes \texttt{joint/Joint.ma}. 560 576 \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} 565 583 \end{tablenotes} 566 584 \end{threeparttable} … … 569 587 \end{table} 570 588 \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.585 589 586 590 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset
for help on using the changeset viewer.