Changeset 1414 for Deliverables/D4.2-4.3

Timestamp:

Oct 19, 2011, 4:03:41 PM (8 years ago)

Author:

mulligan

Message:

more added

Location:

Deliverables/D4.2-4.3/reports

Files:

• D4-2.tex (modified) (2 diffs)
• D4-3.tex (modified) (2 diffs)

Deliverables/D4.2-4.3/reports/D4-2.tex

@@ -470 +470 @@
 Translation specific files (files relating to language semantics have been omitted) are presented in Table~\ref{table.syntax}.
 
+% dpm: shouldn't all these also include joint.ma
 \begin{table}
 \begin{threeparttable}
@@ -479 +480 @@
 \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{joint/joint_LTL_LIN.ma} & The abstracted joint syntax of the LTL and LIN languages & N/A & N/A \\
 \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}

Deliverables/D4.2-4.3/reports/D4-3.tex

@@ -10 +10 @@
 \usepackage[utf8x]{inputenc}
 \usepackage{listings}
+\usepackage{lscape}
 \usepackage{stmaryrd}
+\usepackage{threeparttable}
 \usepackage{url}
 
@@ -539 +541 @@
 
 Semantics specific files (files relating to language translations ommitted).
-Syntax specific files:
-\begin{center}
-\begin{tabular*}{\textwidth}{p{5.5cm}p{9.5cm}}
-Title & Description \\
+Syntax specific files are presented in Table~\ref{table.syntax}.
+
+% dpm: shouldn't all these also include joint.ma
+\begin{landscape}
+\begin{table}
+\begin{threeparttable}
+\begin{tabular}{llll}
+Title & Description & O'Caml & Ratio \\
 \hline
-\texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
-\texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
-\texttt{RTL/RTL.ma} & The syntax of RTL \\
-\texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
-\texttt{LIN/joint\_LTL\_LIN.ma} & The syntax of the abstracted combined LTL and LIN language \\
-\texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL \\
-\texttt{LIN/LIN.ma} & The specialisation of the above file to the syntax of LIN \\
-\end{tabular*}
-\end{center}
-
-\noindent
-Semantics specific files:
-\begin{center}
-\begin{tabular*}{\textwidth}{p{5.5cm}p{9.5cm}}
-Title & Description \\
+\texttt{RTLabs/syntax.ma} & The syntax of RTLabs & \texttt{RTLabs/RTLabs.mli} & 0.65 \\
+\texttt{joint/Joint.ma} & Abstracted syntax for backend languages & N/A & N/A \\
+\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{LIN/joint\_LTL\_LIN.ma} & The syntax of the abstracted combined LTL and LIN language & N/A & N/A \\
+\texttt{LTL/LTL.ma} & The specialisation of the above file to the syntax of LTL & \texttt{LTL/LTL.mli} & 0.19\tnote{a} \\
+\texttt{LIN/LIN.ma} & The specialisation of the above file to 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 specific files in the intermediate language semantics}
+\label{table.syntax}
+\end{table}
+\end{landscape}
+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.
+
+Semantics specific files are presented in Table~\ref{table.semantics}.
+\begin{landscape}
+\begin{table}
+\begin{threeparttable}
+\begin{tabular}{llll}
+Title & Description & O'Caml & Ratio \\
 \hline
-\texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\
-\texttt{joint/semantics.ma} & The semantics of the abstracted backend languages. \\
-\texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\
-\texttt{RTL/semantics.ma} & The semantics of RTL \\
-\texttt{ERTL/semantics.ma} & The semantics of ERTL \\
-\texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & The semantics of the joint LTL-LIN language \\
-\texttt{LTL/semantics.ma} & The semantics of LTL \\
-\texttt{LIN/semantics.ma} & The semantics of LIN
-\end{tabular*}
-\end{center}
+\texttt{RTLabs/semantics.ma} & The semantics of RTLabs & & \\
+\texttt{joint/semantics.ma} & The semantics of the abstracted backend languages & N/A & N/A  \\
+\texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages & N/A & N/A \\
+\texttt{RTL/semantics.ma} & The semantics of RTL & & \\
+\texttt{ERTL/semantics.ma} & The semantics of ERTL & & \\
+\texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & The semantics of the joint LTL-LIN language & N/A & N/A \\
+\texttt{LTL/semantics.ma} & The semantics of LTL & & \\
+\texttt{LIN/semantics.ma} & The semantics of LIN & &
+\end{tabular}
+% \begin{tablenotes}
+% \end{tablenotes}
+\end{threeparttable}
+\caption{Semantics specific files in the intermediate language semantics}
+\label{table.semantics}
+\end{table}
+\end{landscape}
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%