Changeset 1373 for Deliverables/D4.2-4.3/reports/D4-3.tex

Timestamp:

Oct 14, 2011, 3:51:09 PM (9 years ago)

Author:

mulligan

Message:

changes to file based on claudio's suggestions

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (5 diffs)

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

@@ -146 +146 @@
 \label{subsect.abstracting.related.languages}
 
+As mentioned in the report for Deliverable D4.2, a systematic process of abstraction, over the O'Caml code, has taken place in the Matita encoding.
+In particular, we have merged many of the syntaxes of the intermediate languages (i.e. RTL, ERTL, LTL and LIN) into a single `joint' syntax, which is parameterised by various types.
+Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure.
+
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
 % SECTION.                                                                    %
@@ -158 +162 @@
 \label{subsect.what.we.do.not.implement}
 
+There are a number of features that are not yet implemented in the semantics, and some routine axioms remaining.
+We summarise them here:
+\begin{itemize}
+\item
+Like in the 
+\end{itemize}
+
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
 % SECTION.                                                                    %
@@ -171 +182 @@
 \section{Code listing}
 \label{sect.code.listing}
+
+%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
+% SECTION.                                                                    %
+%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
+\subsection{Listing of files}
+\label{subsect.listing.files}
 
 Semantics specific files (files relating to language translations ommitted):
@@ -178 +195 @@
 \hline
 \texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
+\texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\
 \texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
+\texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\
 \texttt{RTL/RTL.ma} & The syntax of RTL \\
+\texttt{RTL/semantics.ma} & The semantics of RTL \\
 \texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
+\texttt{ERTL/semantics.ma} & The semantics of ERTL \\
 \texttt{LTL/LTL.ma} & The syntax of LTL \\
+\texttt{LTL/semantics.ma} & The semantics of LTL \\
 \texttt{LIN/LIN.ma} & The syntax of LIN \\
+\texttt{LIN/semantics.ma} & The semantics of LIN
 \end{tabular*}
 \end{center}
-
-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
-% SECTION.                                                                    %
-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
-\subsection{Listing of files}
-\label{subsect.listing.files}
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
@@ -198 +215 @@
 \label{subsect.listing.important.functions.axioms}
 
+We list some important functions and axioms in the backend semantics:
+
 \end{document}