Changeset 532


Ignore:
Timestamp:
Feb 16, 2011, 3:38:43 PM (6 years ago)
Author:
mulligan
Message:

after much faffing, top of minipages now align correctly

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r529 r532  
    3232  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on},
    3333   morekeywords={[2]whd,normalize,elim,cases,destruct},
    34    morekeywords={[3]type,of,val},
     34   morekeywords={[3]type,of,val,assert,let,function},
    3535   mathescape=true,
    3636  }
     
    247247\label{subsect.representation.integers}
    248248
    249 Integers are represented using bitvectors, i.e. fixed length vectors of booleans.
    250 In our O'Caml emulator, we `faked' bitvectors using phantom types and polymorphic variants, like so:
    251 \begin{lstlisting}
    252 type bit = bool
     249\begin{figure}[t]
     250\begin{minipage}[t]{0.5\textwidth}
     251\vspace{0pt}
     252\begin{lstlisting}
    253253type 'a vect = bit list
    254254type word = [`Sixteen] vect
    255255type byte = [`Eight] vect
    256 \end{lstlisting}
    257 Using this technique, we can provide precise typings for utility and arithmetic functions giving us some stronger guarantees of type safety.
    258 For instance, functions that split \texttt{word}s into their constituent \texttt{byte}s:
    259 \begin{lstlisting}
    260 val from_word: word -> byte * byte
    261 \end{lstlisting}
     256let from_nibble =
     257 function
     258    [b1; b2; b3; b4] -> b1,b2,b3,b4
     259  | _ -> assert false
     260\end{lstlisting}
     261\end{minipage}
     262\quad
     263\begin{minipage}[t]{0.5\textwidth}
     264\vspace{0pt}
     265\begin{lstlisting}
     266type 'a vect
     267type word = [`Sixteen] vect
     268type byte = [`Eight] vect
     269val from_nibble: nibble -> bit*bit*bit*bit
     270\end{lstlisting}
     271\end{minipage}
     272\caption{Sample of O'Caml implementation and interface for bitvectors module}
     273\label{fig.ocaml.implementation.bitvectors}
     274\end{figure}
     275
     276Integers are represented using bitvectors, i.e. fixed length vectors of booleans.
     277In our O'Caml emulator, we `faked' bitvectors using phantom types and polymorphic variants, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
     278From within the bitvector module (left column) bitvectors are just lists of bits.
     279However, the module's interface (right column) hides this implementation completely.
     280
    262281In Matita, we are able to use the full power of dependent types to define `real' bitvectors:
    263282\begin{lstlisting}
     
    360379Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation.
    361380The most important functions in the Matita emulator are highlighted below.
    362 \begin{lstlisting}
    363 definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat := ...
    364 \end{lstlisting}
    365 The next instruction, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
     381
     382The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
    366383An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
    367384These costs are taken from a Siemen's data sheet for the MCS-51, and will likely vary across manufacturers and particular derivatives of the processor.
    368385\begin{lstlisting}
    369 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ...
     386definition fetch:
     387  BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ...
    370388\end{lstlisting}
    371389A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}:
     
    377395A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is also produced.
    378396\begin{lstlisting}
    379 definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ...
     397definition assembly:
     398  assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ...
    380399\end{lstlisting}
    381400A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}:
    382401\begin{lstlisting}
    383 definition execute_1: Status Status := ...
     402definition execute_1: Status $\rightarrow$ Status := ...
    384403\end{lstlisting}
    385404Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}:
     
    387406let rec execute (n: nat) (s: Status) on n: Status := ...
    388407\end{lstlisting}
     408This differs slightly from the design of the O'Caml emulator, which executed a program indefinitely, and also accepted a callback function as an argument, which could `witness' the execution as it happened, and providing a print-out of the processor state, and other debugging information.
     409Due to Matita's requirement that all functions be strongly normalizing, \texttt{execute} cannot execute a program indefinitely, and must execute a fixed number of steps.
    389410
    390411%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.