Changeset 539


Ignore:
Timestamp:
Feb 16, 2011, 5:10:33 PM (6 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

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

    r538 r539  
    3030
    3131\lstdefinelanguage{matita-ocaml}
    32   {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on},
     32  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
    3333   morekeywords={[2]whd,normalize,elim,cases,destruct},
    3434   morekeywords={[3]type,of,val,assert,let,function},
     
    224224
    225225From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.
     226Matita's syntax is similar to that of O'Caml.
     227The only subtlety is the use of \texttt{?} in an argument position, which denotes an argument that should be inferred automatically, if possible.
    226228
    227229\subsection{Development strategy}
     
    469471A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows:
    470472\begin{lstlisting}
    471 let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d
     473let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d :=
    472474  match d with
    473475   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     
    477479We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
    478480\begin{lstlisting}
    479 let rec is_in (n) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l ≝
     481let rec is_in (n: nat) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l :=
    480482 match l return $\lambda$m.$\lambda$_: Vector addressing_mode_tag m. bool with
    481483  [ VEmpty $\Rightarrow$ false
     
    485487Here $\mathtt{\vee}$ is inclusive disjunction on the \texttt{bool} datatype.
    486488\begin{lstlisting}
    487 record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
     489record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] :=
    488490{
    489491  subaddressing_modeel :> addressing_mode;
     
    504506% Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on
    505507The 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.
    506 The previous machinery allows us to state in the type of a function what addressing modes that function expects.
     508The latter coercion is largely straightforward, however the former is not:
     509\begin{lstlisting}
     510coercion mk_subaddressing_mode:
     511  $\forall$n.  $\forall$l: Vector addressing_mode_tag (S n).
     512  $\forall$a: addressing_mode.
     513  $\forall$p: bool_to_Prop (is_in ? l a). subaddressing_mode n l :=
     514    mk_subaddressing_mode on a: addressing_mode to subaddressing_mode ? ?.
     515\end{lstlisting}
     516Using 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.
     517This impels us to state and prove a number of auxilliary lemmas.
     518For 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.
     519Without 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.
     520
     521The machinery just described allows us to state in the type of a function what addressing modes that function expects.
    507522For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
    508523\begin{lstlisting}
Note: See TracChangeset for help on using the changeset viewer.