Index: /Deliverables/D4.1/ITP-Paper/itp-2011.tex
===================================================================
--- /Deliverables/D4.1/ITP-Paper/itp-2011.tex (revision 538)
+++ /Deliverables/D4.1/ITP-Paper/itp-2011.tex (revision 539)
@@ -30,5 +30,5 @@
\lstdefinelanguage{matita-ocaml}
- {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on},
+ {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
morekeywords={[2]whd,normalize,elim,cases,destruct},
morekeywords={[3]type,of,val,assert,let,function},
@@ -224,4 +224,6 @@
From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.
+Matita's syntax is similar to that of O'Caml.
+The only subtlety is the use of \texttt{?} in an argument position, which denotes an argument that should be inferred automatically, if possible.
\subsection{Development strategy}
@@ -469,5 +471,5 @@
A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows:
\begin{lstlisting}
-let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d ≝
+let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d :=
match d with
[ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
@@ -477,5 +479,5 @@
We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
\begin{lstlisting}
-let rec is_in (n) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l ≝
+let rec is_in (n: nat) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l :=
match l return $\lambda$m.$\lambda$_: Vector addressing_mode_tag m. bool with
[ VEmpty $\Rightarrow$ false
@@ -485,5 +487,5 @@
Here $\mathtt{\vee}$ is inclusive disjunction on the \texttt{bool} datatype.
\begin{lstlisting}
-record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
+record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] :=
{
subaddressing_modeel :> addressing_mode;
@@ -504,5 +506,18 @@
% Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on
The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
-The previous machinery allows us to state in the type of a function what addressing modes that function expects.
+The latter coercion is largely straightforward, however the former is not:
+\begin{lstlisting}
+coercion mk_subaddressing_mode:
+ $\forall$n. $\forall$l: Vector addressing_mode_tag (S n).
+ $\forall$a: addressing_mode.
+ $\forall$p: bool_to_Prop (is_in ? l a). subaddressing_mode n l :=
+ mk_subaddressing_mode on a: addressing_mode to subaddressing_mode ? ?.
+\end{lstlisting}
+Using this coercion opens a proof obligation wherein we must prove that the \texttt{addressing\_mode\_tag} in correspondence with the \texttt{addressing\_mode} is a member of the \texttt{Vector} of permissible \texttt{addressing\_mode\_tag}s.
+This impels us to state and prove a number of auxilliary lemmas.
+For instance, we prove that if an \texttt{addressing\_mode\_tag} is a member of a \texttt{Vector}, and we possess a supervector, then the same \texttt{addressing\_mode\_tag} is a member of this supervector.
+Without combining Matita's automation and lemmas such as these our approach becomes infeasible: type checking the main \texttt{execute1} function opens up over 200 proof obligations.
+
+The machinery just described allows us to state in the type of a function what addressing modes that function expects.
For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
\begin{lstlisting}