Changeset 1373 for Deliverables/D4.2-4.3/reports/D4-3.tex
- Timestamp:
- Oct 14, 2011, 3:51:09 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1366 r1373 146 146 \label{subsect.abstracting.related.languages} 147 147 148 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. 149 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. 150 Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure. 151 148 152 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 149 153 % SECTION. % … … 158 162 \label{subsect.what.we.do.not.implement} 159 163 164 There are a number of features that are not yet implemented in the semantics, and some routine axioms remaining. 165 We summarise them here: 166 \begin{itemize} 167 \item 168 Like in the 169 \end{itemize} 170 160 171 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 161 172 % SECTION. % … … 171 182 \section{Code listing} 172 183 \label{sect.code.listing} 184 185 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 186 % SECTION. % 187 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 188 \subsection{Listing of files} 189 \label{subsect.listing.files} 173 190 174 191 Semantics specific files (files relating to language translations ommitted): … … 178 195 \hline 179 196 \texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\ 197 \texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\ 180 198 \texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\ 199 \texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\ 181 200 \texttt{RTL/RTL.ma} & The syntax of RTL \\ 201 \texttt{RTL/semantics.ma} & The semantics of RTL \\ 182 202 \texttt{ERTL/ERTL.ma} & The syntax of ERTL \\ 203 \texttt{ERTL/semantics.ma} & The semantics of ERTL \\ 183 204 \texttt{LTL/LTL.ma} & The syntax of LTL \\ 205 \texttt{LTL/semantics.ma} & The semantics of LTL \\ 184 206 \texttt{LIN/LIN.ma} & The syntax of LIN \\ 207 \texttt{LIN/semantics.ma} & The semantics of LIN 185 208 \end{tabular*} 186 209 \end{center} 187 188 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%189 % SECTION. %190 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%191 \subsection{Listing of files}192 \label{subsect.listing.files}193 210 194 211 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% … … 198 215 \label{subsect.listing.important.functions.axioms} 199 216 217 We list some important functions and axioms in the backend semantics: 218 200 219 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.