Changeset 1446 for Deliverables

Ignore:
Timestamp:
Oct 21, 2011, 6:21:59 PM (8 years ago)
Message:

...

File:
1 edited

Legend:

Unmodified
 r1434 ... | OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals ... \end{lstlisting} \end{lstlisting} Note that in the joint language, instructions are linear', in that they have an immediate successor. Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program. Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program. The conditional jump instruction COND is linear', since it has an immediate successor, but it also takes an arbitrary location (a label) to jump to. For the semantics, we need further parametererised types. Should this decision be taken, this will likely be straightforward but potentially time consuming. \newpage %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % Semantics specific files (files relating to language translations ommitted). Syntax specific files are presented in Table~\ref{table.syntax}. Here, the O'Caml column denotes the O'Caml source file(s) 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. 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. 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. Semantics specific files are presented in Table~\ref{table.semantics}. \begin{landscape} \begin{table} \end{table} \end{landscape} Here, the O'Caml column denotes the O'Caml source file(s) 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. 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. 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. Semantics specific files are presented in Table~\ref{table.semantics}. \begin{landscape} \begin{table} \texttt{RTL/semantics.ma} & Semantics of RTL & \texttt{RTL/RTLInterpret.ml} & 1.88\tnote{a} \\ \texttt{ERTL/semantics.ma} & Semantics of ERTL & \texttt{ERTL/ERTLInterpret.ml} & 1.22\tnote{a} \\ \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & Semantics of the joint LTL-LIN language & N/A & N/A \\ \texttt{LTL/semantics.ma} & Semantics of LTL & \texttt{LTL/LTLInterpret.ml} & 1.25\tnote{c} \\ \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & Semantics of the joint LTL-LIN language & N/A & N/A \\ \texttt{LIN/semantics.ma} & Semantics of LIN & \texttt{LIN/LINInterpret.ml} & 1.52\tnote{c} \end{tabular} \item{b} Includes \texttt{joint/joint\_LTL\_LIN\_semantics.ma}. \item{c} Includes \texttt{joint/semantics.ma}, \texttt{joint/SemanticUtils.ma} and \texttt{joint/joint\_LTL\_LIN\_semantics.ma}. \\ Total lines of Matita code for the above files: 1125. \\ Total lines of O'Caml code for the above files: 1978. \\ Ration of total lines: 0.57. \begin{tabular}{ll} Total lines of Matita code for the above files:& 1125 \\ Total lines of O'Caml code for the above files:& 1978 \\ Ration of total lines:& 0.57 \end{tabular} \end{tablenotes} \end{threeparttable}