May 16, 2011, 6:07:52 PM (8 years ago)

added boxing of matita code to distinguish from o'caml

1 edited


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

    r812 r813  
    304304Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq.
    305 Matita's internal language is similar to O'Caml's.
    306 The symbols `\texttt{?}' or `\texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively.
     305Matita's internal language is similar to O'Caml's; we frame Matita code to distinguish the two.
     306In Matita, `\texttt{?}' or `\texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively.
    308308A full account of the formalisation can be found in~\cite{cerco-report:2011}.
    363363In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
    364 \begin{lstlisting}
    365365inductive Vector (A: Type[0]): nat $\rightarrow$ Type[0] ≝
    366366  VEmpty: Vector A O
    369369We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
    370370We may use Matita's type system to provide precise typings for functions that are polymorphic in the size without code duplication:
    371 \begin{lstlisting}
    372372let rec split (A: Type[0]) (m,n: nat) on m:
    373373   Vector A (m + n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ...
    388388We picked a modified form of trie of fixed height $h$.
    389389Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$:
    390 \begin{lstlisting}
    391391inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
    392392  Leaf: A $\rightarrow$ BitVectorTrie A 0
    439439The internal state of the Matita emulator is represented as a record:
    440 \begin{lstlisting}
    441441record Status: Type[0] :=
    464464An updated program counter, along with its concrete cost in processor cycles, is also returned.
    465465These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations.
    466 \begin{lstlisting}
    467467definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$
    468468  instruction $\times$ Word $\times$ nat
    470470Instruction are assembled to bit encodings by \texttt{assembly1}:
    471 \begin{lstlisting}
    472472definition assembly1: instruction $\rightarrow$ list Byte
    475475Pseudoinstructions and labels are eliminated in favour of instructions from the MCS-51 instruction set.
    476476A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced.
    477 \begin{lstlisting}
    478478definition assembly: assembly_program $\rightarrow$
    479479  option (list Byte $\times$ (BitVectorTrie String 16))
    481481A single fetch-decode-execute cycle is performed by \texttt{execute\_1}:
    482 \begin{lstlisting}
    483483definition execute_1: Status $\rightarrow$ Status
    485485The \texttt{execute} functions performs a fixed number of cycles by iterating
    487 \begin{lstlisting}
    488488let rec execute (n: nat) (s: Status): Status := ...
    541541We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against:
    542 \begin{lstlisting}
    543543inductive addressing_mode: Type[0] :=
    544544  DIRECT: Byte $\rightarrow$ addressing_mode
    549549In order to do this, we introduced an inductive type of addressing mode `tags'.
    550550The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}:
    551 \begin{lstlisting}
    552552inductive addressing_mode_tag : Type[0] :=
    553553  direct: addressing_mode_tag
    557557The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}:
    558 \begin{lstlisting}
    559559let rec is_a
    560560  (d: addressing_mode_tag)
    571571A \texttt{subaddressing\_mode} is an \emph{ad hoc} non-empty $\Sigma$-type of \texttt{addressing\_mode}s constrained to be in a set of tags:
    572 \begin{lstlisting}
    573573record subaddressing_mode
    574574  (n: nat)
    582582An implicit coercion is provided to promote vectors of tags (denoted with $\llbracket - \rrbracket$) to the corresponding \texttt{subaddressing\_mode} so that we can use a syntax close to that of O'Caml to specify \texttt{preinstruction}s:
    583 \begin{lstlisting}
    584584inductive preinstruction (A: Type[0]): Type[0] ≝
    585585  ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$
    606606This allows us to skip impossible cases.
    607607For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
    608 \begin{lstlisting}
    609609definition set_arg_16:
    610610  Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a.
Note: See TracChangeset for help on using the changeset viewer.