Changeset 539 for Deliverables/D4.1/ITPPaper
 Timestamp:
 Feb 16, 2011, 5:10:33 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r538 r539 30 30 31 31 \lstdefinelanguage{matitaocaml} 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}, 33 33 morekeywords={[2]whd,normalize,elim,cases,destruct}, 34 34 morekeywords={[3]type,of,val,assert,let,function}, … … 224 224 225 225 From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes. 226 Matita's syntax is similar to that of O'Caml. 227 The only subtlety is the use of \texttt{?} in an argument position, which denotes an argument that should be inferred automatically, if possible. 226 228 227 229 \subsection{Development strategy} … … 469 471 A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows: 470 472 \begin{lstlisting} 471 let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d ≝473 let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d := 472 474 match d with 473 475 [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] … … 477 479 We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner: 478 480 \begin{lstlisting} 479 let rec is_in (n ) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l ≝481 let rec is_in (n: nat) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l := 480 482 match l return $\lambda$m.$\lambda$_: Vector addressing_mode_tag m. bool with 481 483 [ VEmpty $\Rightarrow$ false … … 485 487 Here $\mathtt{\vee}$ is inclusive disjunction on the \texttt{bool} datatype. 486 488 \begin{lstlisting} 487 record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝489 record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] := 488 490 { 489 491 subaddressing_modeel :> addressing_mode; … … 504 506 % Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on 505 507 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. 506 The previous machinery allows us to state in the type of a function what addressing modes that function expects. 508 The latter coercion is largely straightforward, however the former is not: 509 \begin{lstlisting} 510 coercion 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} 516 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. 517 This impels us to state and prove a number of auxilliary lemmas. 518 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. 519 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. 520 521 The machinery just described allows us to state in the type of a function what addressing modes that function expects. 507 522 For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}: 508 523 \begin{lstlisting}
Note: See TracChangeset
for help on using the changeset viewer.