# Changeset 1391 for Deliverables

Ignore:
Timestamp:
Oct 17, 2011, 1:09:44 PM (9 years ago)
Message:

 r1373 % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{Use of dependent types} \label{subsect.use.of.dependent.types} %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{What we do not implement} \label{subsect.what.we.do.not.implement} There are a number of features that are not yet implemented in the semantics, and some routine axioms remaining. We summarise them here: \begin{itemize} \subsection{Use of monads} \label{subsect.use.of.monads} Monads are a categorical notion that have recently gained an amount of traction in functional programming circles. In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner. Here, effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state. In the semantics of both front and backend intermediate languages, we make use of monads. In particular, we make use of two forms of monad: \begin{enumerate} \item Like in the \end{itemize} An error monad', which signals that a computation either has completed successfully, or returns with an error message. The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation. This monad is used extensively in the semantics to signal a state which cannot be recovered from. For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states: \begin{lstlisting} ... | Returnstate v dst fs m $\Rightarrow$ match fs with [ nil ⇒ Error $\ldots$ (msg FinalState) (* Already in final state *) | cons f fs' $\Rightarrow$ ! locals $\leftarrow$ match dst with [ None $\Rightarrow$ match v with [ None $\Rightarrow$ OK $\ldots$ (locals f) | _ $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch) ] | Some d $\Rightarrow$ match v with [ None $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch) | Some v' $\Rightarrow$ reg_store d v' (locals f) ] ]; ret $\ldots$ $\langle$E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m$\rangle$ ] ... \end{lstlisting} \item An IO' monad, signalling the emission or reading of data to some external location or memory address. 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). Most functions in the intermediate language semantics fall into the IO monad. \end{enumerate} %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \section{Future work} \label{sect.future.work} A few small axioms remain to be closed. These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language. Closing these axioms should not be a problem. No further work remains, aside from `tidying up' the code. \newpage