Index: /Deliverables/D4.1/ITPPaper/itp2011.tex
===================================================================
 /Deliverables/D4.1/ITPPaper/itp2011.tex (revision 553)
+++ /Deliverables/D4.1/ITPPaper/itp2011.tex (revision 554)
@@ 231,5 +231,5 @@
From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}} to distinguish the two syntaxes.
Matita's syntax is largely straightforward to those familiar with Coq or O'Caml.
The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically, if possible.
+The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically.
\subsection{Development strategy}
@@ 250,5 +250,5 @@
% SECTION %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Representation of integers}
+\subsection{Representation of bytes, words, etc.}
\label{subsect.representation.integers}
@@ 258,10 +258,8 @@
\begin{lstlisting}
type 'a vect = bit list
type word = [`Sixteen] vect
+type nibble = [`Sixteen] vect
type byte = [`Eight] vect
$\color{blue}{\mathtt{let}}$ from_nibble =
 function
 [b1;b2;b3;b4] > b1,b2,b3,b4
  _ > assert false
+$\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w
+$\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b
\end{lstlisting}
\end{minipage}
@@ 273,5 +271,6 @@
type word = [`Sixteen] vect
type byte = [`Eight] vect
val from_nibble: nibble > bit*bit*bit*bit
+val split_word: word > byte * word
+val split_byte: byte > nibble * nibble
\end{lstlisting}
\end{minipage}
@@ 280,10 +279,9 @@
\end{figure}
Integers are represented using bitvectors, i.e. fixed length vectors of booleans.
In our O'Caml emulator, we `faked' bitvectors using phantom types and polymorphic variants, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
From within the bitvector module (left column) bitvectors are just lists of bits.
However, the module's interface (right column) hides this implementation completely.

In Matita, we are able to use the full power of dependent types to define `real' bitvectors:
+The formalization of MCS51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits). To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
+In our O'Caml emulator, we `faked' bitvectors using phantom types implemented with polymorphic variants\cite{phantom_types_ocaml}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
+From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes. However, the module's interface (right column) enforces the size invariants in the rest of the code.
+
+In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
\begin{lstlisting}
inductive Vector (A: Type[0]): nat → Type[0] ≝
@@ 292,5 +290,6 @@
\end{lstlisting}
We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
We may use Matita's type system to provide even stronger guarantees, here on a function that splits a vector into two pieces at any index, providing that the index is smaller than the length of the \texttt{Vector} to be split:
+We may use Matita's type system to provide precise typing for functions that are
+polymorphic in the size without having to duplicate the code as we did in O'Caml:
\begin{lstlisting}
let rec split (A: Type[0]) (m,n: nat) on m: