Changeset 1391
 Timestamp:
 Oct 17, 2011, 1:09:44 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.24.3/reports/D43.tex
r1373 r1391 153 153 % SECTION. % 154 154 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 155 \subsection{Use of dependent types} 156 \label{subsect.use.of.dependent.types} 157 158 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 159 % SECTION. % 160 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 161 \subsection{What we do not implement} 162 \label{subsect.what.we.do.not.implement} 163 164 There are a number of features that are not yet implemented in the semantics, and some routine axioms remaining. 165 We summarise them here: 166 \begin{itemize} 155 \subsection{Use of monads} 156 \label{subsect.use.of.monads} 157 158 Monads are a categorical notion that have recently gained an amount of traction in functional programming circles. 159 In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner. 160 Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state. 161 162 In the semantics of both front and backend intermediate languages, we make use of monads. 163 In particular, we make use of two forms of monad: 164 \begin{enumerate} 167 165 \item 168 Like in the 169 \end{itemize} 166 An `error monad', which signals that a computation either has completed successfully, or returns with an error message. 167 The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation. 168 This monad is used extensively in the semantics to signal a state which cannot be recovered from. 169 For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states: 170 \begin{lstlisting} 171 ... 172  Returnstate v dst fs m $\Rightarrow$ 173 match fs with 174 [ nil ⇒ Error $\ldots$ (msg FinalState) (* Already in final state *) 175  cons f fs' $\Rightarrow$ 176 ! locals $\leftarrow$ match dst with 177 [ None $\Rightarrow$ 178 match v with 179 [ None $\Rightarrow$ OK $\ldots$ (locals f) 180  _ $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch) 181 ] 182  Some d $\Rightarrow$ 183 match v with 184 [ None $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch) 185  Some v' $\Rightarrow$ reg_store d v' (locals f) 186 ] 187 ]; 188 ret $\ldots$ $\langle$E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m$\rangle$ 189 ] 190 ... 191 \end{lstlisting} 192 \item 193 An `IO' monad, signalling the emission or reading of data to some external location or memory address. 194 Here, the monads sequencing operation ensures that emissions and reads are maintained in the correct order (i.e. it maintains a `trace', or ordered sequence of IO events). 195 Most functions in the intermediate language semantics fall into the IO monad. 196 \end{enumerate} 170 197 171 198 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% … … 174 201 \section{Future work} 175 202 \label{sect.future.work} 203 204 A few small axioms remain to be closed. 205 These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language. 206 Closing these axioms should not be a problem. 207 No further work remains, aside from `tidying up' the code. 176 208 177 209 \newpage
Note: See TracChangeset
for help on using the changeset viewer.