Changeset 620 for Deliverables/D1.1/Presentations
 Timestamp:
 Mar 2, 2011, 3:56:18 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.1/Presentations/WP4dominicpresentation.tex
r618 r620 4 4 \logo{\includegraphics[height=1.0cm]{fetopen.png}} 5 5 6 \usepackage{amsfonts} 7 \usepackage{amsmath} 8 \usepackage{amssymb} 6 9 \usepackage[english]{babel} 7 \usepackage{inputenc} 10 \usepackage{color} 11 \usepackage[utf8x]{inputenc} 12 \usepackage{listings} 13 \usepackage{stmaryrd} 14 % \usepackage{microtype} 8 15 9 16 \author{Dominic P. Mulligan and Claudio Sacerdoti Coen} … … 13 20 \setlength{\parskip}{1em} 14 21 22 \lstdefinelanguage{matitaocaml} 23 {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to}, 24 morekeywords={[2]whd,normalize,elim,cases,destruct}, 25 morekeywords={[3]type,of,val,assert,let,function}, 26 mathescape=true, 27 } 28 \lstset{language=matitaocaml,basicstyle=\small\tt,columns=flexible,breaklines=false, 29 keywordstyle=\color{red}\bfseries, 30 keywordstyle=[2]\color{blue}, 31 keywordstyle=[3]\color{blue}\bfseries, 32 commentstyle=\color{green}, 33 stringstyle=\color{blue}, 34 showspaces=false,showstringspaces=false} 35 15 36 \begin{document} 16 37 … … 105 126 \end{frame} 106 127 107 \begin{frame} 128 \begin{frame}[fragile] 108 129 \frametitle{Polymorphic variants and phantom types} 109 \begin{itemize}110 \item111 130 The instruction set is highly nonorthogonal. 112 \item 113 We needed a way of 114 \end{itemize} 115 \end{frame} 116 117 \begin{frame} 118 \frametitle{Use of dependent types} 131 We used polymorphic variants and phantom types to capture this nonorthogonality in the type system. 132 For instance: 133 134 \begin{small} 135 \begin{lstlisting} 136 type direct = [ `DIRECT of byte ] 137 type indirect = [ `INDIRECT of bit ] 138 ... 139 type 'addr preinstruction = 140 [ `ADD of acc * [ reg  direct  indirect  data ] 141 ... 142  `MOV of 143 (acc * [ reg  direct  indirect  data ], 144 [ reg  indirect ] * [ acc  direct  data ], 145 direct * [ acc  reg  direct  indirect  data ], ...) 146 ... 147 \end{lstlisting} 148 \end{small} 149 \end{frame} 150 151 \begin{frame}[fragile] 152 \frametitle{Use of dependent types I} 153 This approach worked well in O'Caml, but Matita does not have polymorphic variants, so we need a substitute. 154 We use dependent types. 155 156 Introduce a type for addressing modes: 157 \begin{small} 158 \begin{lstlisting} 159 inductive addressing_mode: Type[0] := 160 DIRECT: Byte $\rightarrow$ addressing_mode 161 ... 162 \end{lstlisting} 163 \end{small} 164 And another type \texttt{addressing\_mode\_tag} of `tags' whose constructors are in correspondence with those of \texttt{addressing\_mode}. 165 \end{frame} 166 167 \begin{frame}[fragile] 168 \frametitle{Use of dependent types II} 169 We use vectors of \texttt{addressing\_mode\_tag}s in our type signatures for instructions. 170 For instance: 171 \begin{small} 172 \begin{lstlisting} 173 inductive preinstruction (A: Type[0]): Type[0] := 174 ADD: $\llbracket$ acc_a $\rrbracket$ 175 $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ 176 $\rightarrow$ preinstruction A 177 ... 178 \end{lstlisting} 179 \end{small} 180 We need: an \emph{ad hoc} $\Sigma$ type and two coercions. 181 One coercion automatically opens up a proof obligation when it is used, which requires some lemmas. 182 183 These lemmas and automation close all proof obligations generated (over 300 in typechecking the main interpreter function). 184 \end{frame} 185 186 \begin{frame} 187 \frametitle{Overlapping memory spaces and addressing modes} 188 MCS51 memory spaces overlap, and can be addressed using different modes and sized pointers. 189 The status record models memory merely as disjoint spaces, using a `tries with holes' datastructure. 190 191 All complications to do with overlapping are handled 119 192 \end{frame} 120 193
Note: See TracChangeset
for help on using the changeset viewer.