Changeset 1391

Oct 17, 2011, 1:09:44 PM (8 years ago)

more added

1 edited


  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1373 r1391  
    153153% SECTION.                                                                    %
    155 \subsection{Use of dependent types}
    156 \label{subsect.use.of.dependent.types}
    158 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    159 % SECTION.                                                                    %
    160 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    161 \subsection{What we do not implement}
    162 \label{}
    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}
     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.
     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:
    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:
     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  ]
     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.
    174201\section{Future work}
     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.
Note: See TracChangeset for help on using the changeset viewer.