Changeset 1391


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

more added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1373 r1391  
    153153% SECTION.                                                                    %
    154154%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    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
     158Monads are a categorical notion that have recently gained an amount of traction in functional programming circles.
     159In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner.
     160Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.
     161
     162In the semantics of both front and backend intermediate languages, we make use of monads.
     163In particular, we make use of two forms of monad:
     164\begin{enumerate}
    167165\item
    168 Like in the
    169 \end{itemize}
     166An `error monad', which signals that a computation either has completed successfully, or returns with an error message.
     167The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation.
     168This monad is used extensively in the semantics to signal a state which cannot be recovered from.
     169For 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
     193An `IO' monad, signalling the emission or reading of data to some external location or memory address.
     194Here, 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).
     195Most functions in the intermediate language semantics fall into the IO monad.
     196\end{enumerate}
    170197
    171198%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     
    174201\section{Future work}
    175202\label{sect.future.work}
     203
     204A few small axioms remain to be closed.
     205These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language.
     206Closing these axioms should not be a problem.
     207No further work remains, aside from `tidying up' the code.
    176208
    177209\newpage
Note: See TracChangeset for help on using the changeset viewer.