Changeset 1414

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

Location:
Deliverables/D4.2-4.3/reports
Files:
2 edited

Legend:

Unmodified
 r1413 \usepackage[utf8x]{inputenc} \usepackage{listings} \usepackage{lscape} \usepackage{stmaryrd} \usepackage{threeparttable} \usepackage{url} 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} %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%