Changeset 376 for Deliverables

Timestamp:

Dec 6, 2010, 10:19:36 AM (11 years ago)

Author:

mulligan

Message:

Work on describing sparse bitvector tries.

File:

• Deliverables/D4.1/Report/report.tex (modified) (2 diffs)

Deliverables/D4.1/Report/report.tex

@@ -185 +185 @@
 Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
 We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
-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.
-The use must manually 
 
 \subsection{Auxilliary data structures and libraries}
@@ -199 +197 @@
 \subsection{The emulator state}
 \label{subsect.emulator.state}
+
+We represent all processor memory in the Matita emulator as a sparse (bitvector)trie:
+
+\begin{quote}
+\begin{lstlisting}
+ninductive BitVectorTrie (A: Type[0]): Nat $\rightarrow$ Type[0] ≝
+  Leaf: A $\rightarrow$ BitVectorTrie A Z
+| Node: ∀n: Nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
+| Stub: ∀n: Nat. BitVectorTrie A n.
+\end{lstlisting}
+\end{quote}
+
+Nodes are addressed by a bitvector index, representing a path through the tree.
+At any point in the tree, a \texttt{Stub} may be inserted, representing a `hole' in the tree.
+All 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.
+
+We probe a trie with the \texttt{lookup} function.
+This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal.
 
 \begin{quote}