Changeset 510


Ignore:
Timestamp:
Feb 14, 2011, 4:17:42 PM (8 years ago)
Author:
mulligan
Message:

more added, talking about dependent types now

File:
1 edited

Legend:

Unmodified
Added
Removed

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

    r509 r510  
    1414
    1515\lstdefinelanguage{matita-ocaml}
    16   {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
    17    morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
    18    morekeywords={[3]type,of},
     16  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on},
     17   morekeywords={[2]whd,normalize,elim,cases,destruct},
     18   morekeywords={[3]type,ofm},
    1919   mathescape=true,
    2020  }
    … …  
    216216% SECTION                                                                      %
    217217%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    218 \subsection{The CerCo project}
    219 \label{subsect.cerco.project}
    220 
    221 The CerCo project (`Certified Complexity') is a current European FeT-Open project incorporating three sites---the Universities of Bologna, Edinburgh and Paris Diderot 7---throughout the European Union.
    222 The ultimate aim of the project is to produce a certified compiler for a large subset of the C programming language targetting a microprocessor used in embedded systems.
    223 In this respect, the CerCo project bears a deal of similarity with CompCert, another European funded project.
    224 However, we see a number of important differences between the aims of the two projects.
    225 \begin{enumerate}
    226 \item
    227 The CerCo project aims to allow reasoning on aspects of the intensional properties of C programs.
    228 That is,
    229 \item
    230 The CompCert project compiled a subset of C down to the assembly level.
    231 A semantics for assembly language was provided.
    232 \end{enumerate}
    233 
    234 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    235 % SECTION                                                                      %
    236 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    237218\subsection{Overview of paper}
    238219\label{subsect.overview.paper}
    … …  
    294275\subsection{Putting dependent types to work}
    295276\label{subsect.putting.dependent.types.to.work}
     277
     278We typeset O'Caml source with blue, and Matita source with red.
    296279
    297280A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
    … …  
    330313\end{lstlisting}
    331314\end{quote}
    332 For our purposes, the types \texttt{union2} and \texttt{union3} were also necessary.
    333 
    334 This polymorphic variant machinery worked well: it allowed us to pattern match
    335 
    336 We provide an inductive data type representing all possible addressing modes of 8051 assembly.
    337 This is the type that functions will pattern match against.
    338 
    339 \begin{quote}
    340 \begin{lstlisting}
    341 ninductive addressing_mode: Type[0] ≝
     315For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
     316
     317This polymorphic variant machinery worked well: it introduced a certain level of type safety (for instance, the type of our \texttt{MOV} instruction above guarantees it cannot be invoked with arguments in the \texttt{carry} and \texttt{data16} addressing modes, respectively), and also allowed us to pattern match against instructions, when necessary.
     318However, this polymorphic variant machinery is \emph{not} present in Matita.
     319We needed some way to produce the same effect, which Matita supported.
     320For this task, we used dependent types.
     321
     322We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against:
     323\begin{quote}
     324\begin{lstlisting}
     325inductive addressing_mode: Type[0] ≝
    342326  DIRECT: Byte $\rightarrow$ addressing_mode
    343327| INDIRECT: Bit $\rightarrow$ addressing_mode
    … …  
    345329\end{lstlisting}
    346330\end{quote}
    347 However, we also wish to express in the type of our functions the \emph{impossibility} of pattern matching against certain constructors.
    348 In order to do this, we introduce an inductive type of addressing mode `tags'.
    349 The constructors of \texttt{addressing\_mode\_tag} are in one-one correspondence with the constructors of \texttt{addressing\_mode}:
    350 \begin{quote}
    351 \begin{lstlisting}
    352 ninductive addressing_mode_tag : Type[0] ≝
     331We also wished to express in the type of functions the \emph{impossibility} of pattern matching against certain constructors.
     332In order to do this, we introduced an inductive type of addressing mode `tags'.
     333The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}:
     334\begin{quote}
     335\begin{lstlisting}
     336inductive addressing_mode_tag : Type[0] ≝
    353337  direct: addressing_mode_tag
    354338| indirect: addressing_mode_tag
    … …  
    356340\end{lstlisting}
    357341\end{quote}
    358 We then provide a function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag}, as follows:
    359 \begin{quote}
    360 \begin{lstlisting}
    361 nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
     342A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows:
     343\begin{quote}
     344\begin{lstlisting}
     345let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d ≝
    362346  match d with
    363347   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
    … …  
    369353\begin{quote}
    370354\begin{lstlisting}
    371 nlet rec is_in (n: Nat) (l: Vector addressing_mode_tag n) (A:addressing_mode) on l ≝
    372  match l return $\lambda$m.$\lambda$_ :Vector addressing_mode_tag m.Bool with
     355let rec is_in (n) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l ≝
     356 match l return $\lambda$m.$\lambda$_: Vector addressing_mode_tag m. bool with
    373357  [ VEmpty $\Rightarrow$ false
    374358  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
    … …  
    379363\begin{quote}
    380364\begin{lstlisting}
    381 nrecord subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
     365record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
    382366{
    383367  subaddressing_modeel :> addressing_mode;
    … …  
    389373\begin{quote}
    390374\begin{lstlisting}
    391 ninductive preinstruction (A: Type[0]): Type[0] ≝
     375inductive preinstruction (A: Type[0]): Type[0] ≝
    392376   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
    393377 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
    … …  
    403387\begin{quote}
    404388\begin{lstlisting}
    405 ndefinition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
     389definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
    406390  $\lambda$s, v, a.
    407391   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
Note: See TracChangeset for help on using the changeset viewer.