Changeset 1414 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 19, 2011, 4:03:41 PM (9 years ago)
- Location:
- Deliverables/D4.2-4.3/reports
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1394 r1414 470 470 Translation specific files (files relating to language semantics have been omitted) are presented in Table~\ref{table.syntax}. 471 471 472 % dpm: shouldn't all these also include joint.ma 472 473 \begin{table} 473 474 \begin{threeparttable} … … 479 480 \texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 0.41 \\ 480 481 \texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 0.13 \\ 482 \texttt{joint/joint_LTL_LIN.ma} & The abstracted joint syntax of the LTL and LIN languages & N/A & N/A \\ 481 483 \texttt{LTL/LTL.ma} & The syntax of LTL & \texttt{LTL/LTL.mli} & 0.19\tnote{a} \\ 482 484 \texttt{LIN/LIN.ma} & The syntax of LIN & \texttt{LIN/LIN.mli} & 0.31\tnote{a} -
Deliverables/D4.2-4.3/reports/D4-3.tex
r1413 r1414 10 10 \usepackage[utf8x]{inputenc} 11 11 \usepackage{listings} 12 \usepackage{lscape} 12 13 \usepackage{stmaryrd} 14 \usepackage{threeparttable} 13 15 \usepackage{url} 14 16 … … 539 541 540 542 Semantics specific files (files relating to language translations ommitted). 541 Syntax specific files: 542 \begin{center} 543 \begin{tabular*}{\textwidth}{p{5.5cm}p{9.5cm}} 544 Title & Description \\ 543 Syntax specific files are presented in Table~\ref{table.syntax}. 544 545 % dpm: shouldn't all these also include joint.ma 546 \begin{landscape} 547 \begin{table} 548 \begin{threeparttable} 549 \begin{tabular}{llll} 550 Title & Description & O'Caml & Ratio \\ 545 551 \hline 546 \texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\ 547 \texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\ 548 \texttt{RTL/RTL.ma} & The syntax of RTL \\ 549 \texttt{ERTL/ERTL.ma} & The syntax of ERTL \\ 550 \texttt{LIN/joint\_LTL\_LIN.ma} & The syntax of the abstracted combined LTL and LIN language \\ 551 \texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL \\ 552 \texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN \\ 553 \end{tabular*} 554 \end{center} 555 556 \noindent 557 Semantics specific files: 558 \begin{center} 559 \begin{tabular*}{\textwidth}{p{5.5cm}p{9.5cm}} 560 Title & Description \\ 552 \texttt{RTLabs/syntax.ma} & The syntax of RTLabs & \texttt{RTLabs/RTLabs.mli} & 0.65 \\ 553 \texttt{joint/Joint.ma} & Abstracted syntax for backend languages & N/A & N/A \\ 554 \texttt{RTL/RTL.ma} & The syntax of RTL & \texttt{RTL/RTL.mli} & 0.41 \\ 555 \texttt{ERTL/ERTL.ma} & The syntax of ERTL & \texttt{ERTL/ERTL.mli} & 0.13 \\ 556 \texttt{LIN/joint\_LTL\_LIN.ma} & The syntax of the abstracted combined LTL and LIN language & N/A & N/A \\ 557 \texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL & \texttt{LTL/LTL.mli} & 0.19\tnote{a} \\ 558 \texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN & \texttt{LIN/LIN.mli} & 0.31\tnote{a} \\ 559 \end{tabular} 560 \begin{tablenotes} 561 \item[a] Includes \texttt{joint/Joint\_LTL\_LIN.ma}. 562 \end{tablenotes} 563 \end{threeparttable} 564 \caption{Syntax specific files in the intermediate language semantics} 565 \label{table.syntax} 566 \end{table} 567 \end{landscape} 568 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. 569 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file. 570 These are computed with \texttt{wc -l}, a standard Unix tool. 571 572 Semantics specific files are presented in Table~\ref{table.semantics}. 573 \begin{landscape} 574 \begin{table} 575 \begin{threeparttable} 576 \begin{tabular}{llll} 577 Title & Description & O'Caml & Ratio \\ 561 578 \hline 562 \texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\ 563 \texttt{joint/semantics.ma} & The semantics of the abstracted backend languages. \\ 564 \texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\ 565 \texttt{RTL/semantics.ma} & The semantics of RTL \\ 566 \texttt{ERTL/semantics.ma} & The semantics of ERTL \\ 567 \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & The semantics of the joint LTL-LIN language \\ 568 \texttt{LTL/semantics.ma} & The semantics of LTL \\ 569 \texttt{LIN/semantics.ma} & The semantics of LIN 570 \end{tabular*} 571 \end{center} 579 \texttt{RTLabs/semantics.ma} & The semantics of RTLabs & & \\ 580 \texttt{joint/semantics.ma} & The semantics of the abstracted backend languages & N/A & N/A \\ 581 \texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages & N/A & N/A \\ 582 \texttt{RTL/semantics.ma} & The semantics of RTL & & \\ 583 \texttt{ERTL/semantics.ma} & The semantics of ERTL & & \\ 584 \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & The semantics of the joint LTL-LIN language & N/A & N/A \\ 585 \texttt{LTL/semantics.ma} & The semantics of LTL & & \\ 586 \texttt{LIN/semantics.ma} & The semantics of LIN & & 587 \end{tabular} 588 % \begin{tablenotes} 589 % \end{tablenotes} 590 \end{threeparttable} 591 \caption{Semantics specific files in the intermediate language semantics} 592 \label{table.semantics} 593 \end{table} 594 \end{landscape} 572 595 573 596 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset
for help on using the changeset viewer.