Changeset 376 for Deliverables
 Timestamp:
 Dec 6, 2010, 10:19:36 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Report/report.tex
r375 r376 185 185 Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files. 186 186 We 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 manually189 187 190 188 \subsection{Auxilliary data structures and libraries} … … 199 197 \subsection{The emulator state} 200 198 \label{subsect.emulator.state} 199 200 We represent all processor memory in the Matita emulator as a sparse (bitvector)trie: 201 202 \begin{quote} 203 \begin{lstlisting} 204 ninductive 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 211 Nodes are addressed by a bitvector index, representing a path through the tree. 212 At any point in the tree, a \texttt{Stub} may be inserted, representing a `hole' in the tree. 213 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. 214 215 We probe a trie with the \texttt{lookup} function. 216 This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal. 201 217 202 218 \begin{quote}
Note: See TracChangeset
for help on using the changeset viewer.