Changeset 510
- Timestamp:
- Feb 14, 2011, 4:17:42 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r509 r510 14 14 15 15 \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}, 19 19 mathescape=true, 20 20 } … … 216 216 % SECTION % 217 217 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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 \item227 The CerCo project aims to allow reasoning on aspects of the intensional properties of C programs.228 That is,229 \item230 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%237 218 \subsection{Overview of paper} 238 219 \label{subsect.overview.paper} … … 294 275 \subsection{Putting dependent types to work} 295 276 \label{subsect.putting.dependent.types.to.work} 277 278 We typeset O'Caml source with blue, and Matita source with red. 296 279 297 280 A peculiarity of the MCS-51 is the non-orthogonality of its instruction set. … … 330 313 \end{lstlisting} 331 314 \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] ≝ 315 For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed. 316 317 This 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. 318 However, this polymorphic variant machinery is \emph{not} present in Matita. 319 We needed some way to produce the same effect, which Matita supported. 320 For this task, we used dependent types. 321 322 We 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} 325 inductive addressing_mode: Type[0] ≝ 342 326 DIRECT: Byte $\rightarrow$ addressing_mode 343 327 | INDIRECT: Bit $\rightarrow$ addressing_mode … … 345 329 \end{lstlisting} 346 330 \end{quote} 347 However, we also wish to express in the type of ourfunctions 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] ≝331 We also wished to express in the type of functions the \emph{impossibility} of pattern matching against certain constructors. 332 In order to do this, we introduced an inductive type of addressing mode `tags'. 333 The 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} 336 inductive addressing_mode_tag : Type[0] ≝ 353 337 direct: addressing_mode_tag 354 338 | indirect: addressing_mode_tag … … 356 340 \end{lstlisting} 357 341 \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 ≝342 A 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} 345 let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d ≝ 362 346 match d with 363 347 [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ] … … 369 353 \begin{quote} 370 354 \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 with355 let 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 373 357 [ VEmpty $\Rightarrow$ false 374 358 | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$ … … 379 363 \begin{quote} 380 364 \begin{lstlisting} 381 nrecord subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝365 record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝ 382 366 { 383 367 subaddressing_modeel :> addressing_mode; … … 389 373 \begin{quote} 390 374 \begin{lstlisting} 391 ninductive preinstruction (A: Type[0]): Type[0] ≝375 inductive preinstruction (A: Type[0]): Type[0] ≝ 392 376 ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A 393 377 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A … … 403 387 \begin{quote} 404 388 \begin{lstlisting} 405 ndefinition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝389 definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝ 406 390 $\lambda$s, v, a. 407 391 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.