# Changeset 1407 for Deliverables/D4.2-4.3

Ignore:
Timestamp:
Oct 19, 2011, 11:17:21 AM (8 years ago)
Message:

almost finished

File:
1 edited

### Legend:

Unmodified
 r1406 \end{lstlisting} The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register: \begin{lstlisting} record more_sem_params (p:params_): Type[1] := }. \end{lstlisting} \begin{lstlisting} record sem_params: Type[1] := { spp :> params_; more_sem_pars :> more_sem_params spp }. \end{lstlisting} For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively. Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language. Here \texttt{framesT} is the type of stack frames. We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}: \begin{lstlisting} record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] := { more_sparams1 :> more_sem_params p; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals); fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address); result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p)); init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1)); pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1))); fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val); set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1)); exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1))) fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals); ... save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1)); pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1))); ... set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1)); exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1))) }. \end{lstlisting} Here, \texttt{fetch\_statement} fetches the next statement to be executed, \texttt{save\_frame} and \texttt{pop\_frame} manipulate stack frames, \texttt{set\_result} saves the result of the function computation, and \texttt{exec\_extended} is a function that executes the extended statements, peculiar to each individual intermediate language. We bundle \texttt{params} and \texttt{sem\_params} together into a single record. This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language: \begin{lstlisting} record sem_params2 (globals: list ident): Type[1] := }. \end{lstlisting} \noindent The \texttt{state} record holds the current state of the interpreter: \begin{lstlisting} ... \end{lstlisting} We examine the type of this function We examine the type of this function. Note that it returns a monadic action, \texttt{IO}, denoting that it may have an IO \emph{side effect}, where the program reads or writes to some external device or memory address. Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}. Further, the function returns a new state, updated by the single step of execution of the program. Finally, a \emph{trace} is also returned, which records the trace of cost labels that the program passes through, in order to calculate the cost model for the CerCo compiler. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% Here, effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state. A monad can be characterised by the following: \begin{itemize} \item A data type, $M$. For instance, the \texttt{option} type in O'Caml or Matita. \item A way to inject' or lift' pure values into this data type (usually called \texttt{return}). We call this function \texttt{return} and say that it must have type $\alpha \rightarrow M \alpha$, where $M$ is the name of the monad. In our example, the lifting' function for the \texttt{option} monad can be implemented as: \begin{lstlisting} let return x = Some x \end{lstlisting} \item A way to sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}. Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$. We can see that bind unpacks' a monadic value, applies a function after unpacking, and repacks' the new value in the monad. In our example, the sequencing function for the \texttt{option} monad can be implemented as: \begin{lstlisting} let bind o f = match o with None -> None Some s -> f s \end{lstlisting} \item A series of algebraic laws that relate \texttt{return} and \texttt{bind}, ensuring that the sequencing operation does the right thing' by retaining the order of effects. These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler. \end{itemize} 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 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} XXX \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). This monadic infrastructure is shared between the frontend and backend languages. In particular, an IO' monad, signalling the emission or reading of data to some external location or memory address, is heavily used in the semantics of the intermediate languages. Here, the monad's sequencing operation ensures that emissions and reads are maintained in the correct order. Most functions in the intermediate language semantics fall into the IO monad. \end{enumerate} This monadic infrastructure is shared between the frontend and backend languages. In particular, we have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type: \begin{lstlisting} definition eval_statement: ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) := ... \end{lstlisting} If we in the body of \texttt{eval\_statement}, we may also see how the monad sequences effects. For instance, in the case for the \texttt{LOAD} statement, we have the following: \begin{lstlisting} definition eval_statement: ∀globals: list ident. ∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) := $\lambda$globals, p, ge, st. ... match s with | LOAD dst addrl addrh ⇒ ! vaddrh $\leftarrow$ dph_retrieve … st addrh; ! vaddrl $\leftarrow$ dpl_retrieve … st addrl; ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉; ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); ! st $\leftarrow$ acca_store p … dst v st; ! st $\leftarrow$ next … l st ; ret ? $\langle$E0, st$\rangle$ \end{lstlisting} Here, we employ a certain degree of syntactic sugaring. The syntax \begin{lstlisting} ... ! vaddrh $\leftarrow$ dph_retrieve … st addrh; ! vaddrl $\leftarrow$ dpl_retrieve … st addrl; ... \end{lstlisting} is sugaring for the \texttt{IO} monad's binding operation. We can expand this sugaring to the following much more verbose code: \begin{lstlisting} ... bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl) ($\lambda$vaddrl. ...)) \end{lstlisting} Note also that the function \texttt{ret} is implementing the lifting', or return function of the \texttt{IO} monad. We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about. In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic. The function \texttt{opt\_to\_res} is also --- this is a utility' function that lifts an option type into the \texttt{IO} monad. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%