Changeset 376 for Deliverables


Ignore:
Timestamp:
Dec 6, 2010, 10:19:36 AM (9 years ago)
Author:
mulligan
Message:

Work on describing sparse bitvector tries.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r375 r376  
    185185Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
    186186We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
    187 Instead, the Matita emulator is initialised with a call to \texttt{load}, which takes as input a list of bytes representing the compiled IHX file.
    188 The use must manually
    189187
    190188\subsection{Auxilliary data structures and libraries}
     
    199197\subsection{The emulator state}
    200198\label{subsect.emulator.state}
     199
     200We represent all processor memory in the Matita emulator as a sparse (bitvector)trie:
     201
     202\begin{quote}
     203\begin{lstlisting}
     204ninductive BitVectorTrie (A: Type[0]): Nat $\rightarrow$ Type[0] ≝
     205  Leaf: A $\rightarrow$ BitVectorTrie A Z
     206| Node: ∀n: Nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
     207| Stub: ∀n: Nat. BitVectorTrie A n.
     208\end{lstlisting}
     209\end{quote}
     210
     211Nodes are addressed by a bitvector index, representing a path through the tree.
     212At any point in the tree, a \texttt{Stub} may be inserted, representing a `hole' in the tree.
     213All functions operating on tries use dependent types to enforce the invariant that the height of the tree and the length of the bitvector representing a path through the tree are the same.
     214
     215We probe a trie with the \texttt{lookup} function.
     216This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal.
    201217
    202218\begin{quote}
Note: See TracChangeset for help on using the changeset viewer.